@[simp]

theorem AP.State.aVisitedIcc'_nil {s : State} : s.aVisitedIcc' [] = ∅

@[simp]

theorem AP.State.aVisitedIcc_self {s : State} : s.aVisitedIcc s = Set'.singleton s.aPos

theorem AP.State.aTurn_iff_aState {s : State} [hs : sys.WF s] : s.aTurn = true ↔ AState s

@[simp]

theorem AP.State.aVisitedIcc'_singleton {s : State} {p : PointZ} : s.aVisitedIcc' [p] = if s.aTurn = true then Set'.singleton p else ∅

theorem AP.AState.aVisitedIcc'_cons {s s' : State} {p : PointZ} {ps : List PointZ} [hs : AState s] (h : sys.tr s p = some s') : s.aVisitedIcc' (p :: ps) = (s'.aVisitedIcc' ps).insert p

theorem AP.DState.aVisitedIcc'_cons {s s' : State} {p : PointZ} {ps : List PointZ} [hs : DState s] (h : sys.tr s p = some s') : s.aVisitedIcc' (p :: ps) = s'.aVisitedIcc' ps

theorem AP.AState.aVisitedIcc'_snoc {s s₁ : State} {ps : List PointZ} {p : PointZ} [hs : sys.WF s] [hs₁ : AState s₁] (h₁ : sys.trs s ps = (s₁, [])) : s.aVisitedIcc' (ps ++ [p]) = (s.aVisitedIcc' ps).insert p

theorem AP.DState.aVisitedIcc'_snoc {s s₁ : State} {ps : List PointZ} {p : PointZ} [hs : sys.WF s] [hs₁ : DState s₁] (h₁ : sys.trs s ps = (s₁, [])) : s.aVisitedIcc' (ps ++ [p]) = s.aVisitedIcc' ps

theorem AP.AState.aVisitedIcc_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.aVisitedIcc s₂ = (s.aVisitedIcc s₁).insert p

theorem AP.DState.aVisitedIcc_eq_of_tr {s s₁ s₂ : State} {p : PointZ} [hs : sys.WF s] [hs₁ : DState s₁] (h : sys.tr s₁ p = some s₂) (h₁ : sys.Reachable s s₁) : s.aVisitedIcc s₂ = s.aVisitedIcc s₁

theorem AP.State.mem_aVisitedIcc_iff_of {s : State} {f : State → PointZ} {n : ℕ} {s₁ : State} {p : PointZ} [hs : sys.WF s] (h : sys.simulate f s n = (s₁, 0)) : p ∈ s.aVisitedIcc s₁ ↔ p = s.aPos ∨ ∃ k < n, ∃ (s' : State), AState s' ∧ sys.simulate f s k = (s', 0) ∧ f s' = p

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

theorem AP.State.simulate_diff {s s₁ : State} {f : State → PointZ} {n r : ℕ} [hs : sys.WF s] (h : sys.simulate f s n = (s₁, r)) : sys.simulate f s (s.diff s₁) = (s₁, 0)

theorem AP.State.aSimPts_eq_ofPred {s : State} {st : Strat} : s.aSimPts st = {p : PointZ | ∃ (s₁ : State) (s₂ : State), s.aMoveSim st s₁ = some (p, s₂)}

theorem AP.State.mem_aSimPts_iff_aSimPairs {s : State} {st : Strat} {p : PointZ} : p ∈ s.aSimPts st ↔ ∃ (s₁ : State), (s₁, p) ∈ s.aSimPairs st

@[simp]

theorem AP.State.mem_simStates_iff {s : State} {st : Strat} {s₁ : State} : s₁ ∈ s.simStates st ↔ ReachableVia st s s₁

theorem AP.State.false_of_aState_and_dState (s : State) [hs₁ : AState s] [hs₂ : DState s] : False

theorem AP.AState.even_of_simulate {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : AState s] [hs₁ : AState s₁] (h : sys.simulate f s n = (s₁, 0)) : Even n

theorem AP.AState.odd_of_simulate {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : AState s] [hs₁ : DState s₁] (h : sys.simulate f s n = (s₁, 0)) : Odd n

theorem AP.DState.even_of_simulate {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : DState s] [hs₁ : DState s₁] (h : sys.simulate f s n = (s₁, 0)) : Even n

theorem AP.DState.odd_of_simulate {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : DState s] [hs₁ : AState s₁] (h : sys.simulate f s n = (s₁, 0)) : Odd n

@[simp]

theorem AP.State.mem_aSimStates_iff {s : State} {st : Strat} {s₁ : State} [hs : sys.WF s] : s₁ ∈ s.aSimStates st ↔ AState s₁ ∧ ∃ (n : ℕ), sys.simulate st.f s n = (s₁, 0)

theorem AP.State.mem_aSimPairs_iff_simulate_tr {s s₁ : State} {p : PointZ} {st : Strat} [hs : sys.WF s] : (s₁, p) ∈ s.aSimPairs st ↔ AState s₁ ∧ ∃ (n : ℕ), sys.simulate st.f s n = (s₁, 0) ∧ ∃ (s₂ : State), sys.tr s₁ (st.a.f s₁) = some s₂ ∧ st.a.f s₁ = p

theorem AP.State.mem_aSimPts_iff_simulate_tr {s : State} {p : PointZ} {st : Strat} [hs : sys.WF s] : p ∈ s.aSimPts st ↔ ∃ (n : ℕ) (s₁ : State), AState s₁ ∧ sys.simulate st.f s n = (s₁, 0) ∧ ∃ (s₂ : State), sys.tr s₁ (st.a.f s₁) = some s₂ ∧ st.a.f s₁ = p

theorem AP.State.mem_aSimPts_iff_simulate_ge_two {s : State} {p : PointZ} {st : Strat} [hst : st.WF] [hs : sys.WF s] : p ∈ s.aSimPts st ↔ ∃ (n : ℕ) (s₁ : State), 2 ≤ n ∧ sys.simulate st.f s n = (s₁, 0) ∧ s₁.aPos = p

theorem AP.State.aVisitedIcc_subset_of_simulate_le (st : Strat) (k n : ℕ) {s s₁ s₂ : State} [hs : sys.WF s] (hn : k ≤ n) (h₁ : sys.simulate st.f s k = (s₁, 0)) (h₂ : sys.simulate st.f s n = (s₂, 0)) : s.aVisitedIcc s₁ ⊆ s.aVisitedIcc s₂

@[simp]

instance AP.instInitialStatePointZSysInit {s : State} : sys.Initial s.init

@[simp]

theorem AP.State.one_le_hist_length {s : State} [hs : sys.WF s] : 1 ≤ s.hist.length

theorem AP.State.diff_init_succ {s : State} [hs : sys.WF s] : s.init.diff s + 1 = s.hist.length

@[simp]

theorem AP.State.diff_init {s : State} [hs : sys.WF s] : s.init.diff s = s.hist.length - 1

@[simp]

theorem AP.State.isInit_initial {s : State} [hs : sys.Initial s] : s.IsInit

theorem AP.State.isInit_of_length_hist_eq_one {s : State} [hs : sys.WF s] (h : s.hist.length = 1) : s.IsInit

theorem AP.State.length_hist_eq_one_of_isInit {s : State} (h : s.IsInit) : s.hist.length = 1

theorem AP.State.isInit_iff_length_hist_eq_one {s : State} [hs : sys.WF s] : s.IsInit ↔ s.hist.length = 1

@[simp]

theorem AP.State.length_hist_init {s : State} : s.init.hist.length = 1

@[simp]

theorem AP.State.diffTrs_init {s : State} [hs : sys.WF s] : s.init.diffTrs s = s.hist.init.reverse

@[simp]

theorem AP.AState.initState_ne {s : State} {pw : ℕ} {p₀ : PointZ} [ha : AState s] : initState pw p₀ ≠ s

@[simp]

theorem AP.AState.not_isInit {s : State} [ha : AState s] : ¬s.IsInit

theorem AP.State.wf_prev_and_tr {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : sys.WF s.prev ∧ sys.tr s.prev s.lastMove = some s

theorem AP.State.wf_prev {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : sys.WF s.prev

theorem AP.State.prev_tr_lastMove {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : sys.tr s.prev s.lastMove = some s

theorem AP.State.length_hist_prev {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : s.prev.hist.length = s.hist.length - 1

theorem AP.State.not_isInit_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : ¬s'.IsInit

theorem AP.State.eq_iff_pw_and_hist {s₁ s₂ : State} [hs₁ : sys.WF s₁] [hs₂ : sys.WF s₂] : s₁ = s₂ ↔ s₁.pw = s₂.pw ∧ s₁.hist = s₂.hist

theorem AP.State.tr_inj {s₁ s₂ s₃ : State} {p₁ p₂ : PointZ} [hs₁ : sys.WF s₁] [hs₂ : sys.WF s₂] (h₁ : sys.tr s₁ p₁ = some s₃) (h₂ : sys.tr s₂ p₂ = some s₃) : s₁ = s₂ ∧ p₁ = p₂

theorem AP.State.lastMove_eq_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s'.lastMove = p

theorem AP.State.diffTrs_prev {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : s.prev.diffTrs s = [s.lastMove]

theorem AP.State.diff_prev {s : State} [hs : sys.WF s] (h : ¬s.IsInit) : s.prev.diff s = 1

theorem AP.State.prev_eq_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s'.prev = s

theorem AP.State.aSimPairs_point_eq_of_state_eq {s s₁ : State} {p₁ p₂ : PointZ} {st : Strat} [hs : sys.WF s] (h₁ : (s₁, p₁) ∈ s.aSimPairs st) (h₂ : (s₁, p₂) ∈ s.aSimPairs st) : p₁ = p₂

@[simp]

theorem AP.State.aSimPtsNcard_empty {s : State} {st : Strat} : s.aSimPtsNcard st ∅ = some 0

@[simp]

theorem AP.State.aSimPtsNcard_eq_zero_iff {s : State} {st : Strat} {set : Set PointZ} [hs : sys.WF s] : s.aSimPtsNcard st set = some 0 ↔ ∀ (n : ℕ) (s₁ s₂ : State) [AState s₁], sys.simulate st.f s n = (s₁, 0) → sys.tr s₁ (st.a.f s₁) = some s₂ → s₂.aPos ∉ set

theorem AP.State.aSimPairs_eq_of_length_hist_eq {s s₁ s₂ : State} {p₁ p₂ : PointZ} {st : Strat} [hs : sys.WF s] (h₁ : (s₁, p₁) ∈ s.aSimPairs st) (h₂ : (s₂, p₂) ∈ s.aSimPairs st) (h₃ : s₁.hist.length = s₂.hist.length) : s₁ = s₂

theorem AP.State.finite_filter_aSimPairs_iff_image_length_hist {s : State} {st : Strat} {p : State × PointZ → Prop} [hs : sys.WF s] : ((s.aSimPairs st).filter p).Finite ↔ ((fun (x : State × PointZ) => x.1.hist.length) '' (s.aSimPairs st).filter p).Finite

theorem AP.State.infinite_filter_aSimPairs_iff_image_length_hist {s : State} {st : Strat} {p : State × PointZ → Prop} [hs : sys.WF s] : ((s.aSimPairs st).filter p).Infinite ↔ ((fun (x : State × PointZ) => x.1.hist.length) '' (s.aSimPairs st).filter p).Infinite

theorem AP.State.nonempty_filter_aSimPairs_iff_image_length_hist {s : State} {st : Strat} {p : State × PointZ → Prop} : ((s.aSimPairs st).filter p).Nonempty ↔ ((fun (x : State × PointZ) => x.1.hist.length) '' (s.aSimPairs st).filter p).Nonempty

theorem AP.State.eq_simulate_eq_and_length_hist_eq {s s₁ s₂ : State} {n₁ n₂ : ℕ} {st : Strat} (h₁ : sys.simulate st.f s n₁ = (s₁, 0)) (h₂ : sys.simulate st.f s n₂ = (s₂, 0)) (h₃ : s₁.hist.length = s₂.hist.length) : s₁ = s₂

theorem AP.State.eq_of_mem_aSimPairs' {s : State} {st : Strat} {s₁ s₂ : State} {p₁ p₂ : PointZ} [hs : sys.WF s] (h₁ : (s₁, p₁) ∈ s.aSimPairs st) (h₂ : (s₂, p₂) ∈ s.aSimPairs st) (h₃ : s₁.hist.length = s₂.hist.length) : s₁ = s₂ ∧ p₁ = p₂

theorem AP.State.eq_of_mem_aSimPairs {s : State} {st : Strat} {r₁ r₂ : State × PointZ} [hs : sys.WF s] (h₁ : r₁ ∈ s.aSimPairs st) (h₂ : r₂ ∈ s.aSimPairs st) (h₃ : r₁.1.hist.length = r₂.1.hist.length) : r₁ = r₂

theorem AP.State.ncard_filter_aSimPairs_eq_image_length_hist {s : State} {st : Strat} {p : State × PointZ → Prop} [hs : sys.WF s] : ((s.aSimPairs st).filter p).ncard = ((fun (x : State × PointZ) => x.1.hist.length) '' (s.aSimPairs st).filter p).ncard

theorem AP.AState.aSeek_exi_tr_of {s : State} {P : State → Prop} [hs : AState s] (h : ∃ (p : PointZ) (s₁ : State), sys.tr s p = some s₁ ∧ P s₁) : ∃ (s₁ : State), sys.tr s ((aSeek P).f s) = some s₁ ∧ P s₁

theorem AP.AState.ne_of_tr {s s₁ : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s₁) : p ≠ s.aPos

theorem AP.AState.aPos_ne_of_tr {s s₁ : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s₁) : s₁.aPos ≠ s.aPos

theorem AP.AState.exi_dState_of_aSimPtsNcard_eq_succ {s : State} {st : Strat} {set : Set PointZ} {n : ℕ} [hs : AState s] [hst : st.WF] (h : s.aSimPtsNcard st set = some (n + 1)) : ∃ (n : ℕ) (s₁ : State), sys.simulate st.f s (n * 2 + 1) = (s₁, 0) ∧ s₁.aPos ∈ set ∧ ∀ (k : ℕ) (s₂ : State), 2 ≤ k → sys.simulate st.f s₁ k = (s₂, 0) → s₂.aPos ∉ set

theorem AP.AState.exi_aState_of_aSimPtsNcard_eq_succ {s : State} {st : Strat} {set : Set PointZ} {n : ℕ} [hs : AState s] [hst : st.WF] (h : s.aSimPtsNcard st set = some (n + 1)) : ∃ (n : ℕ) (s₁ : State), sys.simulate st.f s (n * 2) = (s₁, 0) ∧ s₁.aPos ∈ set ∧ ∀ (k : ℕ) (s₂ : State), k ≠ 0 → sys.simulate st.f s₁ k = (s₂, 0) → s₂.aPos ∉ set

theorem AP.AState.getd_aSimPtsNcard_lt_of_odd {s : State} {st₁ st₂ : Strat} {set : Set PointZ} (n : ℕ) [hs : AState s] (hn : Odd n) (h₁ : s.aWins st₁) (h₂ : s.aWins st₂) (h₃ : (s.aSimPtsNcard st₁ set).isSome = true) (h₄ : (s.aSimPtsNcard st₂ set).isSome = true) (h₅ : ∀ (k : ℕ) (s₁ s₂ : State), sys.simulate st₁.f s k = (s₁, 0) → sys.simulate st₂.f s k = (s₂, 0) → s₁.aPos ∈ set → s₂.aPos ∈ set) (h₆ : ∀ (s₁ : State), sys.simulate st₁.f s n = (s₁, 0) → s₁.aPos ∉ set) (h₇ : ∀ (s₁ : State), sys.simulate st₂.f s n = (s₁, 0) → s₁.aPos ∈ set) : (s.aSimPtsNcard st₁ set).getd < (s.aSimPtsNcard st₂ set).getd

theorem AP.AState.getd_aSimPtsNcard_lt_of {s : State} {st₁ st₂ : Strat} {set : Set PointZ} (n : ℕ) [hs : AState s] (h₁ : s.aWins st₁) (h₂ : s.aWins st₂) (h₃ : (s.aSimPtsNcard st₁ set).isSome = true) (h₄ : (s.aSimPtsNcard st₂ set).isSome = true) (h₅ : ∀ (k : ℕ) (s₁ s₂ : State), sys.simulate st₁.f s k = (s₁, 0) → sys.simulate st₂.f s k = (s₂, 0) → s₁.aPos ∈ set → s₂.aPos ∈ set) (h₆ : ∀ (s₁ : State), sys.simulate st₁.f s n = (s₁, 0) → s₁.aPos ∉ set) (h₇ : ∀ (s₁ : State), sys.simulate st₂.f s n = (s₁, 0) → s₁.aPos ∈ set) : (s.aSimPtsNcard st₁ set).getd < (s.aSimPtsNcard st₂ set).getd

theorem AP.State.validTr_of_mem_aSimPairs {s s' : State} {p : PointZ} {st : Strat} [hs : sys.WF s] (h : (s', p) ∈ s.aSimPairs st) : sys.validTr s' p

theorem AP.steps_eq_of_simulate_full_eq {s s₁ : State} {n m : ℕ} {f : State → PointZ} [hs : sys.WF s] (h₁ : sys.simulate f s n = (s₁, 0)) (h₂ : sys.simulate f s m = (s₁, 0)) : n = m

theorem AP.State.mem_simStatesRangeAuxVia_iff {s s₁ s' : State} {st : Strat} {r : ℕ → ℕ → Prop} {n : ℕ} [hr : DecidableRel r] (h : sys.simulate st.f s n = (s₁, 0)) : s' ∈ simStatesRangeAuxVia r st s s₁ ↔ s' ∈ s.simStates st ∧ s' ∈ (s.simStates st).filter fun (s₃ : State) => s₃.hist.length ≤ s₁.hist.length ∧ r s₃.hist.length s₁.hist.length

theorem AP.State.mem_simStatesIccVia_iff_of {s s₁ s₂ : State} {st : Strat} {n : ℕ} (h : sys.simulate st.f s n = (s₁, 0)) : s₂ ∈ simStatesIccVia st s s₁ ↔ ∃ k ≤ n, sys.simulate st.f s k = (s₂, 0)

theorem AP.State.mem_simStatesIcoVia_iff_of {s s₁ s₂ : State} {st : Strat} {n : ℕ} (h : sys.simulate st.f s n = (s₁, 0)) : s₂ ∈ simStatesIcoVia st s s₁ ↔ ∃ k < n, sys.simulate st.f s k = (s₂, 0)

theorem AP.State.mem_aSimStatesIccVia_iff_of {s s₁ s₂ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, 0)) : s₂ ∈ aSimStatesIccVia st s s₁ ↔ AState s₂ ∧ ∃ k ≤ n, sys.simulate st.f s k = (s₂, 0)

theorem AP.State.mem_aSimStatesIcoVia_iff_of {s s₁ s₂ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, 0)) : s₂ ∈ aSimStatesIcoVia st s s₁ ↔ AState s₂ ∧ ∃ k < n, sys.simulate st.f s k = (s₂, 0)

theorem AP.State.mem_simStatesIccVia_iff {s s₁ s₂ : State} {st : Strat} [hs : sys.WF s] : s₁ ∈ simStatesIccVia st s s₂ ↔ ∃ (k : ℕ) (n : ℕ), k ≤ n ∧ sys.simulate st.f s k = (s₁, 0) ∧ sys.simulate st.f s n = (s₂, 0)

theorem AP.State.mem_simStatesIcoVia_iff {s s₁ s₂ : State} {st : Strat} [hs : sys.WF s] : s₁ ∈ simStatesIcoVia st s s₂ ↔ ∃ (k : ℕ) (n : ℕ), k < n ∧ sys.simulate st.f s k = (s₁, 0) ∧ sys.simulate st.f s n = (s₂, 0)

theorem AP.State.mem_aSimStatesIccVia_iff {s s₁ s₂ : State} {st : Strat} [hs : sys.WF s] : s₁ ∈ aSimStatesIccVia st s s₂ ↔ AState s₁ ∧ ∃ (k : ℕ) (n : ℕ), k ≤ n ∧ sys.simulate st.f s k = (s₁, 0) ∧ sys.simulate st.f s n = (s₂, 0)

theorem AP.State.mem_aSimStatesIcoVia_iff {s s₁ s₂ : State} {st : Strat} [hs : sys.WF s] : s₁ ∈ aSimStatesIcoVia st s s₂ ↔ AState s₁ ∧ ∃ (k : ℕ) (n : ℕ), k < n ∧ sys.simulate st.f s k = (s₁, 0) ∧ sys.simulate st.f s n = (s₂, 0)

@[simp]

theorem AP.State.simulate_full_eq_self_iff {s : State} {f : State → PointZ} {n : ℕ} : sys.simulate f s n = (s, 0) ↔ n = 0

@[simp]

theorem AP.State.mem_simStatesIccVia_self_iff {s s' : State} {st : Strat} [hs : sys.WF s] : s' ∈ simStatesIccVia st s s ↔ s' = s

theorem AP.State.exi_aPos_simulate_eq_of_aPos_simulate_ne {s s₁ : State} {f : State → PointZ} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate f s n = (s₁, 0)) (h₂ : s₁.aPos ≠ s.aPos) : ∃ k < n, ∃ (s₀ : State) (s' : State), AState s₀ ∧ DState s' ∧ sys.simulate f s k = (s₀, 0) ∧ sys.tr s₀ (f s₀) = some s' ∧ s'.aPos = s₁.aPos

theorem AP.State.mem_aVisitedIcc_of_mem_simStatesIccVia {s s' s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : s' ∈ simStatesIccVia st s s₁) : s'.aPos ∈ s.aVisitedIcc s₁

theorem AP.State.mem_aVisitedIcc_iff_mem_simStatesIccVia {s s₁ : State} {st : Strat} {n : ℕ} {p : PointZ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, 0)) : p ∈ s.aVisitedIcc s₁ ↔ ∃ s' ∈ simStatesIccVia st s s₁, s'.aPos = p

theorem AP.State.mem_simStatesIccVia_of_mem_simStatesIcoVia {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h : s' ∈ simStatesIcoVia st s s₁) : s' ∈ simStatesIccVia st s s₁

theorem AP.State.mem_aSimStatesIccVia_of_mem_aSimStatesIcoVia {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h : s' ∈ aSimStatesIcoVia st s s₁) : s' ∈ aSimStatesIccVia st s s₁

theorem AP.State.simStatesIcoVia_subset_simStatesIccVia {s s₁ : State} {st : Strat} [hs : sys.WF s] : simStatesIcoVia st s s₁ ⊆ simStatesIccVia st s s₁

theorem AP.State.aSimStatesIcoVia_subset_aSimStatesIccVia {s s₁ : State} {st : Strat} [hs : sys.WF s] : aSimStatesIcoVia st s s₁ ⊆ aSimStatesIccVia st s s₁

theorem AP.State.simStatesIcoVia_eq_erase_simStatesIccVia {s s₁ : State} {st : Strat} [hs : sys.WF s] : simStatesIcoVia st s s₁ = (simStatesIccVia st s s₁).erase s₁

theorem AP.State.aSimStatesIcoVia_eq_erase_aSimStatesIccVia {s s₁ : State} {st : Strat} [hs : sys.WF s] : aSimStatesIcoVia st s s₁ = (aSimStatesIccVia st s s₁).erase s₁

theorem AP.State.mem_simStatesIcoVia_mem_simStatesIccVia_and_ne {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h₁ : s' ∈ simStatesIccVia st s s₁) (h₂ : s' ≠ s₁) : s' ∈ simStatesIcoVia st s s₁

theorem AP.State.mem_aSimStatesIcoVia_of_mem_aSimStatesIccVia_and_ne {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h₁ : s' ∈ aSimStatesIccVia st s s₁) (h₂ : s' ≠ s₁) : s' ∈ aSimStatesIcoVia st s s₁

theorem AP.State.mem_simStatesIccVia_of_mem_aSimStatesIccVia {s s₁ s' : State} {st : Strat} (h : s' ∈ aSimStatesIccVia st s s₁) : s' ∈ simStatesIccVia st s s₁

theorem AP.State.mem_simStatesIcoVia_of_mem_aSimStatesIcoVia {s s₁ s' : State} {st : Strat} (h : s' ∈ aSimStatesIcoVia st s s₁) : s' ∈ simStatesIcoVia st s s₁

theorem AP.State.mem_aVisitedIcc_of_mem_aSimStatesIccVia {s s' s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : s' ∈ aSimStatesIccVia st s s₁) : s'.aPos ∈ s.aVisitedIcc s₁

theorem AP.State.mem_aVisitedIcc_of_mem_aSimStatesIcoVia {s s' s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : s' ∈ aSimStatesIcoVia st s s₁) : s'.aPos ∈ s.aVisitedIcc s₁

theorem AP.wf_of_mem_simStates {s s' : State} {st : Strat} [hs : sys.WF s] (h : s' ∈ s.simStates st) : sys.WF s'

theorem AP.wf_of_mem_simStatesRangeAuxVia {s s₁ s' : State} {st : Strat} {r : ℕ → ℕ → Prop} [hr : DecidableRel r] [hs : sys.WF s] (h : s' ∈ State.simStatesRangeAuxVia r st s s₁) : sys.WF s'

theorem AP.wf_of_mem_simStatesIccVia {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h : s' ∈ State.simStatesIccVia st s s₁) : sys.WF s'

theorem AP.wf_of_mem_simStatesIcoVia {s s₁ s' : State} {st : Strat} [hs : sys.WF s] (h : s' ∈ State.simStatesIcoVia st s s₁) : sys.WF s'

theorem AP.State.mem_aVisitedIcc_iff_mem_aSimStatesIccVia {s s₁ : State} {st : Strat} {n : ℕ} {p : PointZ} [hs : sys.WF s] [hs₁ : AState s₁] (h : sys.simulate st.f s n = (s₁, 0)) : p ∈ s.aVisitedIcc s₁ ↔ ∃ s' ∈ aSimStatesIccVia st s s₁, s'.aPos = p

theorem AP.State.wf_prev_of_reachable_and_ne {s s₁ : State} [hs : sys.WF s] (h₁ : sys.Reachable s s₁) (h₂ : s ≠ s₁) : sys.WF s₁.prev

theorem AP.State.reachable_prev_of_reachable_and_ne {s s₁ : State} [hs : sys.WF s] (h₁ : sys.Reachable s s₁) (h₂ : s ≠ s₁) : sys.Reachable s s₁.prev

theorem AP.State.mem_aVisitedIcc'_append {s : State} {ps₁ ps₂ : List PointZ} {p : PointZ} (h : p ∈ s.aVisitedIcc' ps₁) : p ∈ s.aVisitedIcc' (ps₁ ++ ps₂)

theorem AP.State.mem_aVisitedIcc_of_mem_aVisitedIco {s s₁ : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.Reachable s s₁) (h₂ : p ∈ s.aVisitedIco s₁) : p ∈ s.aVisitedIcc s₁

theorem AP.State.false_of_simulate_eq_simulate (s : State) (f : State → PointZ) (s₁ s₂ : State) (n m : ℕ) [hs : sys.WF s] (h₁ : sys.simulate f s n = (s₁, 0)) (h₂ : sys.simulate f s m = (s₁, 0)) (h₃ : s₁ = s₂) (h₄ : n ≠ m) : False

theorem AP.State.mem_aVisitedIco_iff_of {s : State} {f : State → PointZ} {n : ℕ} {s₁ : State} {p : PointZ} [hs : sys.WF s] (h : sys.simulate f s n = (s₁, 0)) : p ∈ s.aVisitedIco s₁ ↔ n ≠ 0 ∧ p = s.aPos ∨ ∃ (k : ℕ), k + 1 < n ∧ ∃ (s' : State), AState s' ∧ sys.simulate f s k = (s', 0) ∧ f s' = p

theorem AP.State.mem_aVisitedIco_of_mem_simStatesIcoVia {s s' s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : s' ∈ simStatesIcoVia st s s₁) : s'.aPos ∈ s.aVisitedIco s₁

theorem AP.State.mem_aVisitedIco_iff_mem_simStatesIcoVia {s s₁ : State} {st : Strat} {n : ℕ} {p : PointZ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, 0)) : p ∈ s.aVisitedIco s₁ ↔ ∃ s' ∈ simStatesIcoVia st s s₁, s'.aPos = p

@[simp]

theorem AP.State.simStatesIcoVia_self {s : State} {st : Strat} : simStatesIcoVia st s s = ∅

@[simp]

theorem AP.State.aSimStatesIcoVia_self {s : State} {st : Strat} : aSimStatesIcoVia st s s = ∅

@[simp]

theorem AP.State.aVisitedIco_self {s : State} : s.aVisitedIco s = ∅

theorem AP.State.simStatesIccVia_eq_of_tr {s s₁ : State} {st : Strat} [hs : sys.WF s] (h : sys.tr s (st.f s) = some s₁) : simStatesIccVia st s s₁ = {s, s₁}

theorem AP.State.simStatesIcoVia_eq_of_tr {s s₁ : State} {st : Strat} (h : sys.tr s (st.f s) = some s₁) : simStatesIcoVia st s s₁ = {s}

theorem AP.State.simStatesIcoVia_eq_simStatesIccVia_prev_of {s s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : n ≠ 0) : simStatesIcoVia st s s₁ = simStatesIccVia st s s₁.prev

theorem AP.State.aSimStatesIcoVia_eq_aSimStatesIccVia_prev_of {s s₁ : State} {st : Strat} {n : ℕ} [hs : sys.WF s] (h₁ : sys.simulate st.f s n = (s₁, 0)) (h₂ : n ≠ 0) : aSimStatesIcoVia st s s₁ = aSimStatesIccVia st s s₁.prev

theorem AP.State.mem_aVisitedIcoPrev_iff_exi_aSimStatesIcoVia {s s₁ : State} {st : Strat} {n : ℕ} {p : PointZ} [hs : AState s] [hs₁ : AState s₁] [hst : st.WF] (h₁ : s ≠ s₁) (h₂ : sys.simulate st.f s n = (s₁, 0)) : p ∈ s.aVisitedIcoPrev s₁ ↔ ∃ s' ∈ aSimStatesIcoVia st s s₁, s'.aPos = p

@[simp]

theorem AP.State.aVisitedIcoPrev_self {s : State} : s.aVisitedIcoPrev s = ∅

theorem AP.DState.aNbhdsIcoPrev_eq_of_tr {s s₁ s₂ : State} {p : PointZ} [hs : sys.WF s] [hs₁ : DState 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)