@[simp]

theorem AP.init_initState {pw : ℕ} {p : PointZ} : (initState pw p).init = initState pw p

theorem AP.DState.of_taken_eq_empty {s : State} [hs : sys.WF s] (h : s.taken = ∅) : DState s

theorem AP.State.hist_eq_aPos_of {s : State} [hs : sys.WF s] (h₁ : s.taken = ∅) : s.hist = [s.aPos]

theorem AP.State.aPos₀_eq_aPos_of {s : State} [hs : sys.WF s] (h₁ : s.taken = ∅) : s.aPos₀ = s.aPos

@[simp]

theorem AP.State.wfCnd_setHist {s : State} {hist : List PointZ} : WFCnd (s.setHist hist) ↔ WFCnd s

@[simp]

theorem AP.State.pw_init {s : State} : s.init.pw = s.pw

theorem AP.State.taken_eq_empty_of_dState_and_pw_eq_zero {s : State} [hs : DState s] (h : s.pw = 0) : s.taken = ∅

theorem AP.State.pw_ne_zero_of_dState_and_taken_ne_empty {s : State} [hs : DState s] (h : s.taken ≠ ∅) : s.pw ≠ 0