@[simp]

theorem AP.DStrat.tr_ne_none {s : State} {d : DStrat} [hs : DState s] [hd : d.WF] : sys.tr s (d.f s) ≠ none

@[simp]

theorem AP.State.chooseDMove_tr_ne_none {s : State} [hs : DState s] : sys.tr s s.chooseDMove ≠ none

@[simp]

theorem AP.State.dHws_of_pw_0 {s : State} [hs : sys.WF s] (h : s.pw = 0) : s.dHws

@[simp]

theorem AP.dHwsPw_0 : dHwsPw 0

@[simp]

theorem AP.DState.tr_setPw {s : State} {p : PointZ} {pw : ℕ} [hs : DState s] : sys.tr (s.setPw pw) p = Option.map (fun (x : State) => x.setPw pw) (sys.tr s p)

@[simp]

theorem AP.DState.validTr_setPw {s : State} {p : PointZ} {pw : ℕ} [hs : DState s] : sys.validTr (s.setPw pw) p = sys.validTr s p

theorem AP.State.aHws_setPw_of_le {s : State} {pw : ℕ} [hs : sys.WF s] (h₁ : s.pw ≤ pw) (h₂ : s.aHws) : (s.setPw pw).aHws

theorem AP.State.dHws_of_setPw_le {s : State} {pw : ℕ} [hs : sys.WF s] (h₁ : s.pw ≤ pw) (h₂ : (s.setPw pw).dHws) : s.dHws

theorem AP.State.dHws_setPw_of_le {s : State} {pw : ℕ} [hs : sys.WF (s.setPw pw)] (h₁ : pw ≤ s.pw) (h₂ : s.dHws) : (s.setPw pw).dHws

theorem AP.State.aHws_of_setPw_le {s : State} {pw : ℕ} [hs : sys.WF (s.setPw pw)] (h₁ : pw ≤ s.pw) (h₂ : (s.setPw pw).aHws) : s.aHws

theorem AP.aHws_initState_iff_aHws_origin {pw : ℕ} {p : PointZ} : (initState pw p).aHws ↔ (initState pw 0).aHws

theorem AP.dHws_initState_iff_dHws_origin {pw : ℕ} {p : PointZ} : (initState pw p).dHws ↔ (initState pw 0).dHws

@[simp]

theorem AP.not_aHwsPw_iff {pw : ℕ} : ¬aHwsPw pw ↔ dHwsPw pw

@[simp]

theorem AP.not_dHwsPw_iff {pw : ℕ} : ¬dHwsPw pw ↔ aHwsPw pw

theorem AP.aHwsPw_of_le {pw pw' : ℕ} (h₁ : pw ≤ pw') (h₂ : aHwsPw pw) : aHwsPw pw'

theorem AP.dHwsPw_of_le {pw pw' : ℕ} (h₁ : pw' ≤ pw) (h₂ : dHwsPw pw) : dHwsPw pw'

theorem AP.aHwsPw_iff_p {pw : ℕ} (p : PointZ) : aHwsPw pw ↔ (initState pw p).aHws

theorem AP.dHwsPw_iff_p {pw : ℕ} (p : PointZ) : dHwsPw pw ↔ (initState pw p).dHws