def AP.State.diff (s s₁ : State) : ℕ

Equations

• s.diff s₁ = s₁.hist.length - s.hist.length

def AP.State.diffTrs (s s₁ : State) : List PointZ

Equations

• s.diffTrs s₁ = (List.take (s.diff s₁) s₁.hist).reverse

def AP.State.isReachable (s₁ s₂ : State) : Bool

Equations

• s₁.isReachable s₂ = (AP.sys.trs s₁ (s₁.diffTrs s₂) == (s₂, []))

def AP.State.exiSimulate (f : State → PointZ) (s s₁ : State) : Bool

Equations

• AP.State.exiSimulate f s s₁ = decide (AP.sys.simulate f s (s.diff s₁) = (s₁, 0))

theorem AP.State.diff_eq_of_simulate' {s : State} {f : State → PointZ} {n : ℕ} {s₁ : State} {r : ℕ} (h : sys.simulate f s n = (s₁, r)) : s.diff s₁ + r = n

theorem AP.State.diff_eq_of_simulate {s : State} {f : State → PointZ} {n : ℕ} {s₁ : State} {r : ℕ} (h : sys.simulate f s n = (s₁, r)) : s.diff s₁ = n - r

theorem AP.State.diff_eq_of_simulate_full {s : State} {f : State → PointZ} {n : ℕ} {s₁ : State} (h : sys.simulate f s n = (s₁, 0)) : s.diff s₁ = n

@[simp]

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

@[simp]

theorem AP.State.diff_self {s : State} : s.diff s = 0

@[simp]

theorem AP.State.diffTrs_self {s : State} : s.diffTrs s = []

theorem AP.State.diff_eq_of_tr {s s₁ s₂ : State} {p : PointZ} (h : sys.tr s₁ p = some s₂) (h₁ : sys.Reachable s s₁) : s.diff s₂ = s.diff s₁ + 1

theorem AP.State.diffTrs_eq_of_tr {s s₁ s₂ : State} {p : PointZ} (h : sys.tr s₁ p = some s₂) (h₁ : sys.Reachable s s₁) : s.diffTrs s₂ = s.diffTrs s₁ ++ [p]

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

theorem AP.State.isReachable_of_reachable {s₁ s₂ : State} (h : sys.Reachable s₁ s₂) : s₁.isReachable s₂ = true

theorem AP.State.reachable_of_isReachable {s₁ s₂ : State} (h : s₁.isReachable s₂ = true) : sys.Reachable s₁ s₂

theorem AP.State.reachable_iff_isReachable {s₁ s₂ : State} : sys.Reachable s₁ s₂ ↔ s₁.isReachable s₂ = true

@[instance_reducible]

instance AP.instDecidableReachableStatePointZSys {s₁ s₂ : State} : Decidable (sys.Reachable s₁ s₂)

Equations

• AP.instDecidableReachableStatePointZSys = decidable_of_iff' (s₁.isReachable s₂ = true) ⋯

@[simp]

theorem AP.State.isReachable_eq {s₁ s₂ : State} : s₁.isReachable s₂ = decide (sys.Reachable s₁ s₂)

theorem AP.State.exiSimulate_of_simulate {s s₁ : State} {f : State → PointZ} {n : ℕ} (h : sys.simulate f s n = (s₁, 0)) : exiSimulate f s s₁ = true

theorem AP.State.exiSimulate_of_exi_simulate {s s₁ : State} {f : State → PointZ} (h : ∃ (n : ℕ), sys.simulate f s n = (s₁, 0)) : exiSimulate f s s₁ = true

theorem AP.State.exi_simulate_of_exiSimulate {s s₁ : State} {f : State → PointZ} (h : exiSimulate f s s₁ = true) : ∃ (n : ℕ), sys.simulate f s n = (s₁, 0)

theorem AP.State.exi_simulate_iff_exiSimulate {s s₁ : State} {f : State → PointZ} : (∃ (n : ℕ), sys.simulate f s n = (s₁, 0)) ↔ exiSimulate f s s₁ = true

@[instance_reducible]

instance AP.instDecidableExistsNatEqProdStateSimulatePointZSysMkOfNat {s s₁ : State} {f : State → PointZ} : Decidable (∃ (n : ℕ), sys.simulate f s n = (s₁, 0))

Equations

• AP.instDecidableExistsNatEqProdStateSimulatePointZSysMkOfNat = decidable_of_iff' (AP.State.exiSimulate f s s₁ = true) ⋯

@[simp]

theorem AP.State.exiSImulate_eq {s s₁ : State} {f : State → PointZ} : exiSimulate f s s₁ = decide (∃ (n : ℕ), sys.simulate f s n = (s₁, 0))

theorem AP.State.diff_eq_of_trs_full {s : State} {ps : List PointZ} {s₁ : State} (h : sys.trs s ps = (s₁, [])) : s.diff s₁ = ps.length

@[simp]

theorem AP.not_tr_eq_self {s : State} {p : PointZ} : sys.tr s p ≠ some s

@[simp]

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

theorem AP.length_hist_sub_one_add {s : State} {n : ℕ} [hs : sys.WF s] : s.hist.length - 1 + n = s.hist.length + n - 1