theorem System.invariant {S T : Type u} {sys : System S T} {p : S → Prop} {a b : S} [ha : sys.WF a] (h₁ : p a) (h₂ : sys.Reachable a b) (h₃ : ∀ {x y : S} {t : T} [sys.WF x] [sys.WF y], p x → sys.tr x t = some y → p y) : p b

theorem System.invariant_wf {S T : Type u} {sys : System S T} {p : S → Prop} {a : S} (h₁ : sys.WF a) (h₂ : ∀ {a : S}, sys.Initial a → p a) (h₃ : ∀ {x y : S} {t : T} [sys.WF x] [sys.WF y], p x → sys.tr x t = some y → p y) : p a

theorem System.invariant_val {S T : Type u} {sys : System S T} {α : Type u_1} {a b : S} [ha : sys.WF a] {f : S → α} (h₁ : sys.Reachable a b) (h₂ : ∀ {x y : S} {t : T} [sys.WF x] [sys.WF y], sys.tr x t = some y → f y = f x) : f b = f a

theorem System.simulate_snd_ne_zero_of_tr_eq_none {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} (h₁ : sys.tr s (f s) = none) (h₂ : n ≠ 0) : (sys.simulate f s n).2 ≠ 0

theorem System.exi_simulate_succ_eq_of {S T : Type u} {sys : System S T} {f : S → T} {s₀ s s' : S} {n k r₀ r : ℕ} (h₁ : sys.simulate f s₀ n = (s', r₀)) (hr₀ : r₀ = 0) (h₂ : sys.simulate f s₀ k = (s, r)) (hk : k < n) : r = 0 ∧ ∃ (s' : S), sys.simulate f s₀ (k + 1) = (s', 0) ∧ sys.tr s (f s) = some s'

theorem System.simulate_add' {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n m : ℕ} : sys.simulate f s (m + n) = match sys.simulate f s n with | (s₁, n') => match sys.simulate f s₁ m with | (s₂, m') => if n' ≠ 0 then (s₁, n' + m) else (s₂, n' + m')

theorem System.simulate_snd_eq_zero_of_tr {S T : Type u} {sys : System S T} {f : S → T} [hf : sys.SimFn f] {a b c : S} {t : T} {n r : ℕ} [ha : sys.WF a] (h₁ : sys.simulate f a n = (b, r)) (h₂ : sys.tr b t = some c) : r = 0

@[simp]

theorem System.snd_simulate_add_one_eq_zero_iff {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : (sys.simulate f s (n + 1)).2 = 0 ↔ ∃ (s₁ : S) (s₂ : S), sys.simulate f s n = (s₁, 0) ∧ sys.tr s₁ (f s₁) = some s₂

@[simp]

theorem System.exi_trs_full_of_trs {S T : Type u} {sys : System S T} {a b : S} {ts ts' : List T} (h : sys.trs a ts = (b, ts')) : ∃ (ts₁ : List T), ts₁ <+: ts ∧ sys.trs a ts₁ = (b, [])

@[simp]

theorem System.exi_simulate_full_of_simulate {S T : Type u} {sys : System S T} {a b : S} {f : S → T} {n r : ℕ} (h : sys.simulate f a n = (b, r)) : ∃ (k : ℕ), sys.simulate f a k = (b, 0)