Documentation

Projects.AP.HistBlind.D

noncomputable def AP.State.dwn (s : State) :

Equations

s.dwn = Nat.find! fun (n : ℕ) => ∃ (d : AP.DStrat), d.WF ∧ ∀ (a : AP.AStrat), a.WF → (AP.sys.simulate { a := a, d := d }.f s n).2 ≠ 0

Instances For

theorem AP.State.dwn_eq_zero_of_aHws {s : State} [hs : sys.WF s] (h : s.aHws) :

s.dwn = 0

@[simp]

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

(s.setHist hist).dwn = s.dwn

theorem AP.State.aHws_of_dwn_eq_zero {s : State} [hs : sys.WF s] (h : s.dwn = 0) :

theorem AP.State.dwn_eq_zero_iff_aHws {s : State} [hs : sys.WF s] :

s.dwn = 0 ↔ s.aHws

theorem AP.State.dHws_iff_dwn_ne_zero {s : State} [hs : sys.WF s] :

s.dHws ↔ s.dwn ≠ 0

theorem AP.State.dwn_pos_of_dHws {s : State} [hs : sys.WF s] (h : s.dHws) :

0 < s.dwn

theorem AP.AState.dwn_lt_of_tr {sa sd : State} {p : PointZ} [hsa : AState sa] (h₁ : sa.dHws) (h₂ : sys.tr sa p = some sd) :

sd.dwn < sa.dwn

theorem AP.DState.exi_tr_dHws_and_dwn_lt {sd : State} [hsd : DState sd] (h₁ : sd.dHws) :

∃ (p : PointZ) (sa : State), sys.tr sd p = some sa ∧ sa.dHws ∧ sa.dwn < sd.dwn

theorem AP.DState.exi_tr_dwn_lt {sd : State} [hsd : DState sd] (h₁ : sd.dHws) :

∃ (p : PointZ) (sa : State), sys.tr sd p = some sa ∧ sa.dwn < sd.dwn

noncomputable def AP.dHistBlind :

Equations

AP.dHistBlind = AP.DStrat.mk fun (s : AP.State) => do let sd ← choose? fun (sd : AP.State) => AP.sys.WF sd ∧ sd.setHist s.hist = s choose? fun (p : PointZ) => ∃ (sa : AP.State), AP.sys.tr sd p = some sa ∧ sa.dHws ∧ sa.dwn < sd.dwn

Instances For

instance AP.instWFDHistBlind :

theorem AP.histBlind_dHistBlind :

dHistBlind.HistBlind

@[simp]

instance AP.instHistBlindDHistBlind :

dHistBlind.HistBlind

theorem AP.dHws_and_dwn_lt_of_dHistBlind_tr {sd sa : State} [hsd : DState sd] (h₁ : sys.tr sd (dHistBlind.f sd) = some sa) (h₂ : sd.dHws) :

sa.dHws ∧ sa.dwn < sd.dwn

theorem AP.State.dHws_histBlind_of_dHws {s : State} [hs : sys.WF s] (h : s.dHws) :

∃ (d : DStrat), d.HistBlind ∧ ∀ (a : AStrat), a.WF → s.dWins { a := a, d := d }

theorem AP.State.dHws_iff_dHws_histBlind {s : State} [hs : sys.WF s] :

s.dHws ↔ ∃ (d : DStrat), d.HistBlind ∧ ∀ (a : AStrat), a.WF → s.dWins { a := a, d := d }