theorem AP.AState.aNbhdsIcoPrev_eq_of_tr {s s₁ s₂ : State} {p : PointZ} [hs : sys.WF s] [hs₁ : AState s₁] (h : sys.tr s₁ p = some s₂) (h₁ : sys.Reachable s s₁) : s.aNbhdsIcoPrev s₂ = s.aNbhdsIcoPrev s₁ ∪ if s = s₁ then ∅ else Set'.ofList (Point.nbhd s₁.prev.aPos ↑s.pw)

theorem AP.State.aNbhdsIcoPrev_eq_of_tr {s s₁ s₂ : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s₁ p = some s₂) (h₁ : sys.Reachable s s₁) : s.aNbhdsIcoPrev s₂ = s.aNbhdsIcoPrev s₁ ∪ if s = s₁ then ∅ else Set'.ofList (Point.nbhd s₁.prev.aPos ↑s.pw)

@[simp]

theorem AP.State.aNbhdsIcoPrev_self {s : State} : s.aNbhdsIcoPrev s = ∅

@[simp]

instance AP.init_reachable {s : State} [hs : sys.WF s] : sys.Reachable s.init s

theorem AP.State.wf_iff {s : State} : sys.WF s ↔ ∃ (ps : List PointZ), sys.trs s.init ps = (s, [])

theorem AP.init_eq_of_tr {s s₁ : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s₁) : s₁.init = s.init

theorem AP.init_eq_of_trs {s s₁ : State} {ps ps' : List PointZ} [hs : sys.WF s] (h : sys.trs s ps = (s₁, ps')) : s₁.init = s.init

theorem AP.init_eq_of_reachable {s s₁ : State} [hs : sys.WF s] (h : sys.Reachable s s₁) : s₁.init = s.init

@[simp]

theorem AP.State.odd_length_hist {s : State} [hs : sys.WF s] : Odd s.hist.length ↔ s.aTurn = false

@[simp]

theorem AP.State.even_length_hist {s : State} [hs : sys.WF s] : Even s.hist.length ↔ s.aTurn = true

@[simp]

theorem AP.State.odd_length_hist_sub_one {s : State} [hs : sys.WF s] : Odd (s.hist.length - 1) ↔ s.aTurn = true

@[simp]

theorem AP.State.even_length_hist_sub_one {s : State} [hs : sys.WF s] : Even (s.hist.length - 1) ↔ s.aTurn = false

@[simp]

theorem AP.taken_init {s : State} : s.init.taken = ∅

@[simp]

theorem AP.aPos_init {s : State} : s.init.aPos = s.aPos₀

@[simp]

theorem AP.hist_init {s : State} : s.init.hist = [s.aPos₀]

@[simp]

theorem AP.init_init {s : State} : s.init.init = s.init

@[simp]

theorem AP.Strat.a_ofFn {f : State → Option PointZ} : (ofFn f).a = AStrat.mk f

@[simp]

theorem AP.Strat.d_ofFn {f : State → Option PointZ} : (ofFn f).d = DStrat.mk f

@[simp]

instance AP.Strat.wf_ofFn {f : State → Option PointZ} : (ofFn f).WF

@[simp]

theorem AP.Strat.f_ofFn {f : State → Option PointZ} : (ofFn f).f = mkStratFn f

theorem AP.State.eq_of_reachable_and_hist_eq {s s₁ s₂ : State} (h₁ : sys.Reachable s s₁) (h₂ : sys.Reachable s s₂) (h₃ : s₁.hist = s₂.hist) : s₁ = s₂

theorem AP.State.eq_of_reachable_and_length_hist_eq {s s₁ s₂ s₃ : State} (h₁ : sys.Reachable s s₁) (h₂ : sys.Reachable s s₂) (h₃ : sys.Reachable s₁ s₃) (h₄ : sys.Reachable s₂ s₃) (h₅ : s₁.hist.length = s₂.hist.length) : s₁ = s₂

theorem AP.point_eq_of_tr_eq_tr {s s' : State} {p₁ p₂ : PointZ} (h₁ : sys.tr s p₁ = some s') (h₂ : sys.tr s p₂ = some s') : p₁ = p₂

theorem AP.diff_eq_length_diffTrs {s s₁ : State} : s.diff s₁ = (s.diffTrs s₁).length

theorem AP.State.simulate_diffStrat_eq_of {s s₁ : State} {n : ℕ} [hs : sys.WF s] (h : sys.Reachable s s₁) (hn : n = s.diff s₁) : sys.simulate (s.diffStrat s₁).f s n = (s₁, 0)

@[simp]

theorem AP.State.trs_diffTrs_iff {s s₁ : State} [hs : sys.WF s] : sys.trs s (s.diffTrs s₁) = (s₁, []) ↔ sys.Reachable s s₁

theorem AP.State.diffTrs_prefix_of {s s₁ s₂ : State} (h₁ : sys.Reachable s s₁) (h₂ : sys.Reachable s₁ s₂) : s.diffTrs s₁ <+: s.diffTrs s₂

@[simp]

theorem AP.State.simulate_diffStrat_iff {s s₁ : State} {n : ℕ} [hs : sys.WF s] : sys.simulate (s.diffStrat s₁).f s n = (s₁, 0) ↔ sys.Reachable s s₁ ∧ n = s.diff s₁

theorem AP.State.mem_simStatesIcc_iff {s s₁ sx : State} [hs : sys.WF s] : sx ∈ s.simStatesIcc s₁ ↔ sys.Reachable s s₁ ∧ ∃ (ps : List PointZ), ps <+: s.diffTrs s₁ ∧ sys.trs s ps = (sx, [])

theorem AP.State.mem_simStatesIco_iff {s s₁ sx : State} [hs : sys.WF s] : sx ∈ s.simStatesIco s₁ ↔ sx ≠ s₁ ∧ sys.Reachable s s₁ ∧ ∃ (ps : List PointZ), ps <+: s.diffTrs s₁ ∧ sys.trs s ps = (sx, [])

theorem AP.State.mem_aSimStatesIcc_iff {s s₁ sx : State} [hs : sys.WF s] : sx ∈ s.aSimStatesIcc s₁ ↔ AState sx ∧ sys.Reachable s s₁ ∧ ∃ (ps : List PointZ), ps <+: s.diffTrs s₁ ∧ sys.trs s ps = (sx, [])

theorem AP.State.mem_aSimStatesIco_iff {s s₁ sx : State} [hs : sys.WF s] : sx ∈ s.aSimStatesIco s₁ ↔ sx ≠ s₁ ∧ AState sx ∧ sys.Reachable s s₁ ∧ ∃ (ps : List PointZ), ps <+: s.diffTrs s₁ ∧ sys.trs s ps = (sx, [])