theorem System.Misc.aux₁ {S T : Type u} {sys : System S T} {s : S} {t : T} {s' : S} (h₁ : sys.validTr s t) (h₂ : sys.tr! s t = s') : sys.tr s t = some s'

theorem System.Misc.aux₂ {S T : Type u} {sys : System S T} {s : S} {t : T} (h₁ : ¬sys.validTr s t) : sys.tr! s t = s

theorem System.Misc.aux₃ {S T : Type u} {sys : System S T} {s : S} {ts : List T} : ∃ (s' : S) (rs : List T), sys.trs s ts = (s', rs) ∧ rs.length ≤ ts.length

theorem System.Misc.aux₅ {S T : Type u} {sys : System S T} {f : S → T} {s : S} {m : ℕ} : ∃ (s₂ : S) (l : ℕ), sys.simulate f s m = (s₂, l)

theorem System.Misc.cntrex₁ : ¬∀ (S T : Type) (sys : System S T) (f : S → T) (s : S) (n : ℕ), (∀ (s' : S), ¬sys.hasTr s') → ∃ (k : ℕ) (s' : S), sys.simulate f s n = (s', k) ∧ 0 < k

theorem System.Misc.aux₆ {S T : Type u} {sys : System S T} {a b c : S} (h₁ : sys.Reachable a b) (h₂ : sys.Reachable b c) : sys.Reachable a c

theorem System.Misc.aux₇ {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} {s' : S} (h₁ : sys.simulate f s n = (s', 0)) : sys.Reachable s s'

theorem System.Misc.cntrex₂ : ¬∀ (S T : Type) (sys : System S T) (a : sys.DecidableHasTr), ∃ (f : S → T), sys.SimFn f

theorem System.Misc.aux₈ {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : ∃! p : S × ℕ, sys.simulate f s n = (p.1, p.2)

theorem System.Misc.cntrex₃ : ¬∀ (α β : Type) (P : α → Prop), (¬∀ (x : α), P x) → ¬∀ (x : α) (x_1 : β), P x

theorem System.Misc.cntrex₄ : ¬∀ (S T : Type) (sys : System S T) (s : S), sys.Acyclic s → ∀ (f : S → T), sys.SimFn f → ∀ (n m : ℕ) (sn sm : S) (x y : ℕ), n < m → sys.simulate f s n = (sn, x) → sys.simulate f s m = (sm, y) → sn ≠ sm

theorem System.Misc.aux₉ {S T : Type u} {sys : System S T} {s : S} [h₁ : sys.Acyclic s] {f : S → T} [h₂ : sys.SimFn f] {n m : ℕ} {sn sm : S} (h₃ : n < m) : ∃ (x : ℕ) (y : ℕ), sys.simulate f s n = (sn, x) → sys.simulate f s m = (sm, y) → sn ≠ sm

theorem System.Misc.aux₁₀ {S T : Type u} {sys : System S T} {s : S} [h₁ : sys.Acyclic s] {f : S → T} [h₂ : sys.SimFn f] {n m : ℕ} {sn sm : S} (h₃ : n < m) : ∃ (x : ℕ), sys.simulate f s n = (sn, x) → sys.simulate f s m = (sm, x) → sn ≠ sm

theorem System.Misc.aux₁₁ {S T : Type u} {sys : System S T} {s : S} [h₁ : sys.Acyclic s] {f : S → T} [h₂ : sys.SimFn f] {n m : ℕ} {sn sm : S} (h₃ : n < m) {x : ℕ} (h₄ : sys.simulate f s n = (sn, x)) (h₅ : sys.simulate f s m = (sm, x)) : sn ≠ sm

theorem System.Misc.cntrex₅ : ¬∀ (S T : Type) (sys : System S T) [Finite S] {s : S} [sys.Acyclic s] {f : S → T} [sys.SimFn f], ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (k : ℕ), 0 < k ∧ ∀ (x : S), sys.simulate f s n = (x, k)

theorem System.Misc.cntrex₆ : ¬∀ (S T : Type) (sys : System S T) [Finite S] {s : S} [sys.Acyclic s] {f : S → T} [sys.SimFn f] {x : S}, ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (k : ℕ), 0 < k ∧ sys.simulate f s n = (x, k)

theorem System.Misc.cntrex₇ : ¬∀ (S T : Type) (sys : System S T) (a : S) (ts₁ ts₂ : List T) (b : S), (∀ t ∈ ts₁, sys.validTr b t) → sys.trs a (ts₁ ++ ts₂) = sys.trs (sys.trs a ts₁).1 ts₂

theorem System.Misc.aux₁₄ {S T : Type u} {sys : System S T} {a : S} {ts₁ ts₂ : List T} (h₁ : ∀ (a : S), ∀ t ∈ ts₁, sys.validTr a t) : sys.trs a (ts₁ ++ ts₂) = sys.trs (sys.trs a ts₁).1 ts₂

theorem System.Misc.aux₁₅ {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : sys.simulate f s (n + 1) = match sys.tr s (f s) with | none => (s, n + 1) | some s' => sys.simulate f s' n

theorem System.Misc.aux₁₆ : ∃! f : ℕ → ℕ, f 0 = 0 ∧ ∀ (n : ℕ), f (n + 1) = f (f n)