noncomputable def AP.aHistBlind : AStrat

Equations

• AP.aHistBlind = AP.AStrat.mk fun (s : AP.State) => do let s' ← choose? fun (s' : AP.State) => AP.sys.WF s' ∧ s'.setHist s.hist = s let a ← choose? fun (a : AP.AStrat) => a.WF ∧ ∀ (d : AP.DStrat), d.WF → s'.aWins { a := a, d := d } pure (a.f s')

instance AP.instWFAHistBlind : aHistBlind.WF

theorem AP.histBlind_aHistBlind : aHistBlind.HistBlind

@[simp]

instance AP.instHistBlindAHistBlind : aHistBlind.HistBlind

def AP.State.setHistAt' (s : State) (hist₁ hist₂ : List PointZ) : State

Equations

• s.setHistAt' hist₁ hist₂ = s.setHist (List.take (s.hist.length - hist₁.length) s.hist ++ hist₂)

def AP.State.setHistAt (s : State) (hist₁ hist₂ : List PointZ) : State

Equations

• s.setHistAt hist₁ hist₂ = if ¬(hist₁ <:+ s.hist ∧ AP.sys.WF (s.setHistAt' hist₁ hist₂)) then s else s.setHistAt' hist₁ hist₂

@[simp]

theorem AP.State.validTr_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} : sys.validTr (s.setHistAt' hist₁ hist₂) p ↔ sys.validTr s p

@[simp]

theorem AP.State.hasTr_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} : sys.hasTr (s.setHistAt' hist₁ hist₂) = sys.hasTr s

@[simp]

theorem AP.State.validTr_setHistAt {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} : sys.validTr (s.setHistAt hist₁ hist₂) p ↔ sys.validTr s p

@[simp]

theorem AP.State.hasTr_setHistAt {s : State} {hist₁ hist₂ : List PointZ} : sys.hasTr (s.setHistAt hist₁ hist₂) = sys.hasTr s

@[simp]

instance AP.instAStateSetHistAt'OfWFStatePointZSys {s : State} {hist₁ hist₂ : List PointZ} [hs : AState s] [hs' : sys.WF (s.setHistAt' hist₁ hist₂)] : AState (s.setHistAt' hist₁ hist₂)

@[simp]

instance AP.instDStateSetHistAt'OfWFStatePointZSys {s : State} {hist₁ hist₂ : List PointZ} [hs : DState s] [hs' : sys.WF (s.setHistAt' hist₁ hist₂)] : DState (s.setHistAt' hist₁ hist₂)

@[simp]

instance AP.instWFStatePointZSysSetHistAt {s : State} {hist₁ hist₂ : List PointZ} [hs : sys.WF s] : sys.WF (s.setHistAt hist₁ hist₂)

@[simp]

instance AP.instAStateSetHistAt {s : State} {hist₁ hist₂ : List PointZ} [hs : AState s] : AState (s.setHistAt hist₁ hist₂)

@[simp]

instance AP.instDStateSetHistAt {s : State} {hist₁ hist₂ : List PointZ} [hs : DState s] : DState (s.setHistAt hist₁ hist₂)

@[simp]

theorem AP.State.setHistAt'_self {s : State} {hist : List PointZ} : s.setHistAt' s.hist hist = s.setHist hist

@[simp]

theorem AP.State.setHistAt_self {s : State} {hist : List PointZ} [hs' : sys.WF (s.setHist hist)] : s.setHistAt s.hist hist = s.setHist hist

theorem AP.State.wf_setHist_take_append_of_reachable {s₀ s : State} {hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h : sys.Reachable s₀ s) : sys.WF (s.setHist (List.take (s.hist.length - s₀.hist.length) s.hist ++ hist))

theorem AP.State.wf_setHistAt'_of_reachable {s₀ s : State} {hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h : sys.Reachable s₀ s) : sys.WF (s.setHistAt' s₀.hist hist)

theorem AP.State.wf_setHistAt_of_reachable {s₀ s : State} {hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h : sys.Reachable s₀ s) : sys.WF (s.setHistAt s₀.hist hist)

theorem AP.State.setHistAt_cancel_of_reachable {s₀ s : State} {hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h : sys.Reachable s₀ s) : (s.setHistAt s₀.hist hist).setHistAt hist s₀.hist = s

theorem AP.State.setHistAt_eq_of_reachable' {s₀ s : State} {hist₀ hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h₀ : hist₀ = s₀.hist) (h : sys.Reachable s₀ s) : s.setHistAt hist₀ hist = s.setHistAt' hist₀ hist

theorem AP.State.setHistAt_eq_of_reachable {s₀ s : State} {hist : List PointZ} [hs₀ : sys.WF s₀] [hs₀' : sys.WF (s₀.setHist hist)] (h : sys.Reachable s₀ s) : s.setHistAt s₀.hist hist = s.setHistAt' s₀.hist hist

def AP.AStrat.setHistAt (a : AStrat) (hist₁ hist₂ : List PointZ) : AStrat

Equations

• a.setHistAt hist₁ hist₂ = { f := fun (s : AP.State) => a.f (s.setHistAt hist₁ hist₂) }

def AP.DStrat.setHistAt (d : DStrat) (hist₁ hist₂ : List PointZ) : DStrat

Equations

• d.setHistAt hist₁ hist₂ = { f := fun (s : AP.State) => d.f (s.setHistAt hist₁ hist₂) }

instance AP.instWFSetHistAt {a : AStrat} {hist₁ hist₂ : List PointZ} [ha : a.WF] : (a.setHistAt hist₁ hist₂).WF

instance AP.instWFSetHistAt_1 {d : DStrat} {hist₁ hist₂ : List PointZ} [hd : d.WF] : (d.setHistAt hist₁ hist₂).WF

theorem AP.eq_iff_eq_left_of {α : Type u_1} {x y z : α} (h : x = y) : x = z ↔ y = z

theorem AP.eq_iff_eq_right_of {α : Type u_1} {x y z : α} (h : x = y) : z = x ↔ z = y

@[simp]

theorem AP.State.pw_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt' hist₁ hist₂).pw = s.pw

@[simp]

theorem AP.State.aTurn_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt' hist₁ hist₂).aTurn = s.aTurn

@[simp]

theorem AP.State.aPos_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt' hist₁ hist₂).aPos = s.aPos

@[simp]

theorem AP.State.taken_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt' hist₁ hist₂).taken = s.taken

@[simp]

theorem AP.State.pw_setHistAt {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt hist₁ hist₂).pw = s.pw

@[simp]

theorem AP.State.aTurn_setHistAt {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt hist₁ hist₂).aTurn = s.aTurn

@[simp]

theorem AP.State.aPos_setHistAt {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt hist₁ hist₂).aPos = s.aPos

@[simp]

theorem AP.State.taken_setHistAt {s : State} {hist₁ hist₂ : List PointZ} : (s.setHistAt hist₁ hist₂).taken = s.taken

@[simp]

theorem AP.State.aMove_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} : (s.setHistAt' hist₁ hist₂).aMove p = Option.map (fun (x : State) => x.setHistAt' hist₁ hist₂) (s.aMove p)

@[simp]

theorem AP.State.dMove_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} : (s.setHistAt' hist₁ hist₂).dMove p = Option.map (fun (x : State) => x.setHistAt' hist₁ hist₂) (s.dMove p)

theorem AP.State.move_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} (h : hist₁.length ≤ s.hist.length) : (s.setHistAt' hist₁ hist₂).move p = Option.map (fun (x : State) => x.setHistAt' hist₁ hist₂) (s.move p)

theorem AP.State.tr_setHistAt' {s : State} {hist₁ hist₂ : List PointZ} {p : PointZ} (h : hist₁.length ≤ s.hist.length) : sys.tr (s.setHistAt' hist₁ hist₂) p = Option.map (fun (x : State) => x.setHistAt' hist₁ hist₂) (sys.tr s p)

theorem AP.State.setHistAt'_cancel_of_reachable {s s₁ : State} {hist : List PointZ} (h : sys.Reachable s s₁) : (s₁.setHistAt' s.hist hist).setHistAt' hist s.hist = s₁

theorem AP.State.wf_setHistAt'_iff_of_reachable {s s₁ : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] (h : sys.Reachable s s₁) : sys.WF (s₁.setHistAt' s.hist hist) ↔ sys.WF s₁

theorem AP.AState.setHistAt'_iff_of_reachable {s s₁ : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] (h : sys.Reachable s s₁) : AState (s₁.setHistAt' s.hist hist) ↔ AState s₁

theorem AP.DState.setHistAt'_iff_of_reachable {s s₁ : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] (h : sys.Reachable s s₁) : DState (s₁.setHistAt' s.hist hist) ↔ DState s₁

theorem AP.State.setHist_reachable_setHistAt'_of_reachable_and_tr {s s₁ s' : State} {hist : List PointZ} {p : PointZ} (h₁ : sys.Reachable s s') (h₂ : sys.tr s' p = some s₁) : sys.Reachable (s'.setHistAt' s.hist hist) (s₁.setHistAt' s.hist hist)

theorem AP.State.setHist_reachable_setHistAt'_of_reachable {s s₁ : State} {hist : List PointZ} (h : sys.Reachable s s₁) : sys.Reachable (s.setHist hist) (s₁.setHistAt' s.hist hist)

theorem AP.State.exi_aWins_cnd_setHist_of {s : State} {hist : List PointZ} {p : (ℕ → State) → Prop} {a : AStrat} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] [ha : a.WF] (hp : ∀ (st : Strat) [st.WF] (hist₁ : List PointZ), (p fun (x : ℕ) => (sys.simulate st.f s x).1.setHistAt s.hist hist₁) ↔ p fun (x : ℕ) => (sys.simulate st.f s x).1) (h : ∀ (d : DStrat) [d.WF], (p fun (x : ℕ) => (sys.simulate { a := a, d := d }.f s x).1) ∧ s.aWins { a := a, d := d }) : ∃ (a : AStrat), a.WF ∧ ∀ (d : DStrat), d.WF → (p fun (x : ℕ) => (sys.simulate { a := a, d := d }.f (s.setHist hist) x).1) ∧ (s.setHist hist).aWins { a := a, d := d }

theorem AP.State.aHws_setHist_of {s : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] (h : s.aHws) : (s.setHist hist).aHws

@[simp]

theorem AP.State.aHws_setHist_iff {s : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] : (s.setHist hist).aHws ↔ s.aHws

@[simp]

theorem AP.State.dHws_setHist_iff {s : State} {hist : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHist hist)] : (s.setHist hist).dHws ↔ s.dHws

@[simp]

theorem AP.State.setHistAt_setHist {s : State} {hist₁ hist₂ : List PointZ} [hs : sys.WF (s.setHist hist₂)] : (s.setHist hist₁).setHistAt hist₁ hist₂ = s.setHist hist₂

instance AP.instWFStatePointZSysSetHistHist_1 {s : State} [hs : sys.WF s] : sys.WF (s.setHist s.hist)

theorem AP.State.setHistAt_cancel_of_suffix {s : State} {hist₁ hist₂ : List PointZ} [hs : sys.WF s] [hs' : sys.WF (s.setHistAt' hist₁ hist₂)] (h : hist₁ <:+ s.hist) : (s.setHistAt hist₁ hist₂).setHistAt hist₂ hist₁ = s

theorem AP.AState.aHistBlind_tr_aHws {sa : State} [ha : AState sa] (h₁ : sa.aHws) : ∃ (sd : State), sys.tr sa (aHistBlind.f sa) = some sd ∧ sd.aHws

theorem AP.State.aHws_histBlind_of_aHws {s : State} [hs : sys.WF s] (h : s.aHws) : ∃ (a : AStrat), a.HistBlind ∧ ∀ (d : DStrat), d.WF → s.aWins { a := a, d := d }

theorem AP.State.aHws_iff_aHws_histBlind {s : State} [hs : sys.WF s] : s.aHws ↔ ∃ (a : AStrat), a.HistBlind ∧ ∀ (d : DStrat), d.WF → s.aWins { a := a, d := d }