theorem System.sim_full_inj_of_acyclic {S T : Type u} {sys : System S T} {s : S} [ha : sys.Acyclic s] {f : S → T} [hf : sys.SimFn f] {n m : ℕ} : (sys.simulate f s n).2 = 0 → (sys.simulate f s m).2 = 0 → (sys.simulate f s n).1 = (sys.simulate f s m).1 → n = m

@[simp]

theorem System.reachable_fst_simulate {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : sys.Reachable s (sys.simulate f s n).1

theorem System.simFn_fn_set_of {S T : Type u} {sys : System S T} [DecidableEq S] {f : S → T} [hf : sys.SimFn f] {s : S} {t : T} (h : sys.validTr s t) : sys.SimFn (fn_set s t f)

theorem System.acyclic_of_reachable {S T : Type u} {sys : System S T} {a : S} [ha : sys.Acyclic a] {b : S} (h : sys.Reachable a b) : sys.Acyclic b

theorem System.simulate_fn_set_eq_of {S T : Type u} {sys : System S T} [DecidableEq S] {f : S → T} [hf : sys.SimFn f] {a b : S} {t : T} {n : ℕ} [ha : sys.WF a] (h₁ : sys.validTr b t) (h₂ : ∀ k < n, (sys.simulate f a k).1 ≠ b) : sys.simulate (fn_set b t f) a n = sys.simulate f a n

theorem System.simulate_snd_eq_zero_of_le_and_eq_zero {S T : Type u} {sys : System S T} {f : S → T} {a : S} {k n : ℕ} (h₁ : (sys.simulate f a n).2 = 0) (h₂ : k ≤ n) : (sys.simulate f a k).2 = 0

theorem System.simulate_snd_eq_zero_of_hasTr {S T : Type u} {sys : System S T} {f : S → T} [hf : sys.SimFn f] {a : S} {n : ℕ} [ha : sys.WF a] (h : sys.hasTr (sys.simulate f a n).1) : (sys.simulate f a n).2 = 0

theorem System.acyclic_of_tree {S T : Type u} {sys : System S T} {a : S} [ht : sys.Tree a] : sys.Acyclic a

instance System.instAcyclicOfTree {S T : Type u} {sys : System S T} {a : S} [ht : sys.Tree a] : sys.Acyclic a

theorem System.simulate_eq_of_tr_eq_none {S T : Type u} {sys : System S T} {f : S → T} {a : S} {n : ℕ} (h : sys.tr a (f a) = none) : sys.simulate f a n = (a, n)

theorem System.exi_trs_of_simulate_eq {S T : Type u} {sys : System S T} {f : S → T} {a : S} {n : ℕ} {r : S × ℕ} (h₁ : sys.simulate f a n = r) : ∃ (ts : List T), sys.trs a ts = (r.1, []) ∧ n = ts.length + r.2

theorem System.simulate_snd_eq_zero_of_tree_and_trs_eq {S T : Type u} {sys : System S T} {f : S → T} {a : S} [ht : sys.Tree a] {ts : List T} (h : sys.trs a ts = ((sys.simulate f a ts.length).1, [])) : (sys.simulate f a ts.length).2 = 0

theorem System.eq_of_tree_and_trs_eq {S T : Type u} {sys : System S T} {a : S} [ht : sys.Tree a] {ts₁ ts₂ : List T} {b : S} (hb : sys.trs a ts₁ = (b, [])) (hc : sys.trs a ts₂ = (b, [])) : ts₁ = ts₂

theorem System.trs_snd_eq_nil_of_prefix_and_eq_nil {S T : Type u} {sys : System S T} {a : S} {xs ys : List T} (h₁ : xs <+: ys) (h₂ : (sys.trs a ys).2 = []) : (sys.trs a xs).2 = []

theorem System.exi_simp_path_of_full_trs_eq {S T : Type u} {sys : System S T} {a b : S} {ts : List T} (h : sys.trs a ts = (b, [])) : ∃ (ts' : List T), sys.simp_path a ts' b

theorem System.exi_simp_path_of_reachable {S T : Type u} {sys : System S T} {a b : S} (h : sys.Reachable a b) : ∃ (ts : List T), sys.simp_path a ts b

theorem System.simp_path'_of_cons_and_tr_eq_some {S T : Type u} {sys : System S T} {a b : S} {t : T} {ts : List T} (h₁ : sys.simp_path' a (t :: ts)) (h₂ : sys.tr a t = some b) : sys.simp_path' b ts

theorem System.exi_trs_prefix_of_simulate_le {S T : Type u} {sys : System S T} {f : S → T} {a b c : S} {n m : ℕ} (h₁ : n ≤ m) (h₂ : sys.simulate f a n = (b, 0)) (h₃ : sys.simulate f a m = (c, 0)) : ∃ (xs : List T) (ys : List T), xs <+: ys ∧ xs.length = n ∧ ys.length = m ∧ sys.trs a xs = (b, []) ∧ sys.trs a ys = (c, [])

theorem System.hasTr_of_validTr {S T : Type u} {sys : System S T} {a : S} {t : T} (h : sys.validTr a t) : sys.hasTr a

@[simp]

theorem System.validTr_iff_of_simFn {S T : Type u} {sys : System S T} {f : S → T} [h : sys.SimFn f] {a : S} [ha : sys.WF a] : sys.validTr a (f a) ↔ sys.hasTr a

theorem System.snd_le_of_simulate_eq {S T : Type u} {sys : System S T} {f : S → T} {a b : S} {n m : ℕ} (h : sys.simulate f a n = (b, m)) : m ≤ n

theorem System.simulate_eq_of_simulate_add_eq_add {S T : Type u} {sys : System S T} {f : S → T} {a b : S} {n m k : ℕ} (h : sys.simulate f a (n + k) = (b, m + k)) : sys.simulate f a n = (b, m)

theorem System.simulate_sub_eq_of {S T : Type u} {sys : System S T} {f : S → T} {a b : S} {n m : ℕ} (h : sys.simulate f a n = (b, m)) : sys.simulate f a (n - m) = (b, 0)

theorem System.simulate_eq_of_iter_le {S T : Type u} {sys : System S T} {f : S → T} {n k : ℕ} (hk : k ≤ n) (g : ℕ → S) (h₁ : ∀ k < n, sys.validTr (g k) (f (g k))) (h₂ : ∀ k < n, sys.tr (g k) (f (g k)) = some (g (k + 1))) : sys.simulate f (g 0) k = (g k, 0)

theorem System.simulate_eq_of_iter {S T : Type u} {sys : System S T} {f : S → T} {n : ℕ} (g : ℕ → S) (h₁ : ∀ k < n, sys.validTr (g k) (f (g k))) (h₂ : ∀ k < n, sys.tr (g k) (f (g k)) = some (g (k + 1))) : sys.simulate f (g 0) n = (g n, 0)

theorem System.hasTr_trs_of_prefix {S T : Type u} {sys : System S T} {a b : S} {xs ys : List T} (h₁ : sys.trs a ys = (b, [])) (h₂ : xs <+: ys) (h₃ : xs ≠ ys) : sys.hasTr (sys.trs a xs).1

@[simp]

theorem System.not_validTr_iff {S T : Type u} {sys : System S T} {a : S} {t : T} : ¬sys.validTr a t ↔ sys.tr a t = none

theorem System.tr_trs_list_take_eq_some_of {S T : Type u} {sys : System S T} {ts : List T} {a : S} {n : ℕ} (h₁ : n < ts.length) (h₂ : (sys.trs a ts).2 = []) : sys.tr (sys.trs a (List.take n ts)).1 ts[n] = some (sys.trs a (List.take (n + 1) ts)).1

theorem System.validTr_trs_list_take_of {S T : Type u} {sys : System S T} {ts : List T} {a : S} {n : ℕ} (h₁ : n < ts.length) (h₂ : (sys.trs a ts).2 = []) : sys.validTr (sys.trs a (List.take n ts)).1 ts[n]

theorem System.wf_trs {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] {ts : List T} : sys.WF (sys.trs a ts).1

instance System.instWFFstListTrs {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] {ts : List T} : sys.WF (sys.trs a ts).1

theorem System.exi_simulate_of_simp_path {S T : Type u} {sys : System S T} [ht : Inhabited (S → T)] {a b : S} {ts : List T} [hs : sys.WF a] (h : sys.simp_path a ts b) : ∃ (f : S → T), sys.SimFn f ∧ ∀ k ≤ ts.length, sys.simulate f a k = ((sys.trs a (List.take k ts)).1, 0)

@[simp]

theorem System.simp_path_self_iff {S T : Type u} {sys : System S T} {a : S} {xs : List T} : sys.simp_path a xs a ↔ xs = []

@[simp]

theorem System.simp_path_nil_iff {S T : Type u} {sys : System S T} {a b : S} : sys.simp_path a [] b ↔ a = b

@[simp]

theorem System.simp_path_singleton_iff {S T : Type u} {sys : System S T} {a b : S} {t : T} : sys.simp_path a [t] b ↔ a ≠ b ∧ sys.tr a t = some b

theorem System.simp_path'_snoc_of {S T : Type u} {sys : System S T} (b c : S) {a : S} {ts : List T} {t : T} (h₁ : sys.simp_path a ts b) (h₂ : sys.tr b t = some c) (h₃ : ∀ (xs : List T), xs <+: ts → (sys.trs a xs).1 ≠ c) : sys.simp_path' a (ts ++ [t])

theorem System.simp_path_snoc_of {S T : Type u} {sys : System S T} {a b c : S} {ts : List T} {t : T} (h₁ : sys.simp_path a ts b) (h₂ : sys.tr b t = some c) (h₃ : ∀ (xs : List T), xs <+: ts → (sys.trs a xs).1 ≠ c) : sys.simp_path a (ts ++ [t]) c

@[simp]

theorem System.trs_snd_suffix {S T : Type u} {sys : System S T} {a : S} {xs : List T} : (sys.trs a xs).2 <:+ xs

theorem System.trs_snd_suffix_of_eq {S T : Type u} {sys : System S T} {a : S} {xs : List T} {r : S × List T} (h : sys.trs a xs = r) : r.2 <:+ xs

@[simp]

theorem System.trs_snd_length_le {S T : Type u} {sys : System S T} {a : S} {xs : List T} : (sys.trs a xs).2.length ≤ xs.length

theorem System.trs_snd_length_le_of_eq {S T : Type u} {sys : System S T} {a : S} {xs : List T} {r : S × List T} (h : sys.trs a xs = r) : r.2.length ≤ xs.length

theorem System.exi_trs_nil_of_trs_eq {S T : Type u} {sys : System S T} {a : S} {ts : List T} {r : S × List T} (hr : sys.trs a ts = r) : ∃ (xs : List T), xs <+: ts ∧ ∃ (b : S), sys.trs a xs = (b, [])

theorem System.simp_path'_of_prefix_simp_path' {S T : Type u} {sys : System S T} {a : S} {ts xs : List T} (h₁ : sys.simp_path' a ts) (h₂ : xs <+: ts) : sys.simp_path' a xs

theorem System.exi_simp_path_of_simp_path' {S T : Type u} {sys : System S T} {a : S} {ts : List T} (h : sys.simp_path' a ts) : ∃ (xs : List T), xs <+: ts ∧ ∃ (b : S), sys.simp_path a xs b ∧ b = (sys.trs a xs).1

@[simp]

theorem System.simp_path'_nil {S T : Type u} {sys : System S T} {a : S} : sys.simp_path' a []

theorem System.exi_simp_path_prefix_of_not_simp_path' {S T : Type u} {sys : System S T} {a : S} {ts : List T} (h₁ : ¬sys.simp_path' a ts) : ∃ (xs : List T) (t : T), xs ++ [t] <+: ts ∧ sys.simp_path' a xs ∧ ¬sys.simp_path' a (xs ++ [t])

theorem System.exi_full_trs_of_simp_path' {S T : Type u} {sys : System S T} {a : S} {ts : List T} (h : sys.simp_path' a ts) : ∃ (b : S), sys.trs a ts = (b, [])

theorem System.trs_snd_eq_nil_of_simp_path'_and_prefix {S T : Type u} {sys : System S T} {a : S} {xs ts : List T} (h₁ : sys.simp_path' a ts) (h₂ : xs <+: ts) : (sys.trs a xs).2 = []

theorem System.simp_path'_snoc_iff {S T : Type u} {sys : System S T} {a : S} {ts : List T} {t : T} : sys.simp_path' a (ts ++ [t]) ↔ sys.simp_path' a ts ∧ ∀ (b : S), sys.trs a ts = (b, []) → ∀ (xs : List T), xs <+: ts → ∃ (c : S), sys.tr b t = some c ∧ sys.trs a xs ≠ (c, [])

theorem System.exi_cyclic_simulate_of_not_simp_path' {S T : Type u} {sys : System S T} {a : S} {ts : List T} [ha : sys.WF a] (h : ¬sys.simp_path' a ts) (hh : (sys.trs a ts).2 = []) : ∃ (f : S → T), sys.SimFn f ∧ ∃ (n : ℕ) (m : ℕ), n ≠ m ∧ (sys.simulate f a n).2 = 0 ∧ (sys.simulate f a m).2 = 0 ∧ (sys.simulate f a n).1 = (sys.simulate f a m).1

theorem System.exi_simulate_full_of_simulate_eq' {S T : Type u} {sys : System S T} {f : S → T} {a : S} {n : ℕ} {r : S × ℕ} (hr : sys.simulate f a n = r) : ∃ k ≤ n, sys.simulate f a k = (r.1, 0)

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

theorem System.exi_simulate_full_of_simulate_fst_eq {S T : Type u} {sys : System S T} {f : S → T} {a : S} {n : ℕ} {b : S} (hr : (sys.simulate f a n).1 = b) : ∃ k ≤ n, sys.simulate f a k = (b, 0)

theorem System.acyclic_def_sim_full_inj {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] : sys.Acyclic a ↔ ∀ (f : S → T) [sys.SimFn f] (n m : ℕ), (sys.simulate f a n).2 = 0 → (sys.simulate f a m).2 = 0 → (sys.simulate f a n).1 = (sys.simulate f a m).1 → n = m

theorem System.acyclic_iff_sim_inj {S T : Type u} {sys : System S T} {a : S} [sys.WF a] : sys.Acyclic a ↔ ∀ (f : S → T) [sys.SimFn f] (n m : ℕ), sys.simulate f a n = sys.simulate f a m → n = m

theorem System.exi_simulate_of_acyclic_and_trs_eq {S T : Type u} {sys : System S T} [ht : Inhabited (S → T)] {a : S} [ha : sys.Acyclic a] {ts : List T} {r : S × List T} (h₁ : sys.trs a ts = r) : ∃ (f : S → T), sys.SimFn f ∧ ∃ (n : ℕ), sys.simulate f a n = (r.1, 0) ∧ ts.length = n + r.2.length

theorem System.exi_simp_path_of_trs_eq {S T : Type u} {sys : System S T} {a : S} {ts : List T} {r : S × List T} (h : sys.trs a ts = r) : ∃ (ts' : List T), sys.simp_path a ts' r.1

theorem System.exi_simulate_of_trs_eq {S T : Type u} {sys : System S T} [ht : Inhabited (S → T)] {a : S} {ts : List T} {r : S × List T} [ha : sys.WF a] (h₁ : sys.trs a ts = r) : ∃ (f : S → T), sys.SimFn f ∧ ∃ (n : ℕ), sys.simulate f a n = (r.1, 0)

theorem System.exi_simulate_of_reachable {S T : Type u} {sys : System S T} {a b : S} [ha : sys.WF a] [ht : Inhabited (S → T)] (h : sys.Reachable a b) : ∃ (f : S → T), sys.SimFn f ∧ ∃ (n : ℕ), sys.simulate f a n = (b, 0)

theorem System.reachable_iff_exi_simulate {S T : Type u} {sys : System S T} [hi : Inhabited (S → T)] {a b : S} [ha : sys.WF a] : sys.Reachable a b ↔ ∃ (f : S → T), sys.SimFn f ∧ ∃ (n : ℕ), sys.simulate f a n = (b, 0)

theorem System.simulate_fst_eq_fst_of_snd_ne_zero {S T : Type u} {sys : System S T} {f : S → T} {a : S} {n m : ℕ} (h₁ : (sys.simulate f a n).2 ≠ 0) (h₂ : (sys.simulate f a m).2 ≠ 0) : (sys.simulate f a n).1 = (sys.simulate f a m).1

theorem System.simp_path'_iff_nodup {S T : Type u} {sys : System S T} {a : S} {ts : List T} : sys.simp_path' a ts ↔ (List.map (fun (xs : List T) => (sys.trs a xs).1) ts.inits).Nodup

theorem System.full_trs_inj_of_acyclic {S T : Type u} {sys : System S T} {a : S} [h : sys.Acyclic a] {xs ys : List T} (hx : xs <+: ys) (h₁ : (sys.trs a xs).2 = []) (h₂ : (sys.trs a ys).2 = []) (h₃ : (sys.trs a xs).1 = (sys.trs a ys).1) : xs = ys

theorem System.acyclic_of_full_trs_inj {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] (h : ∀ (xs ys : List T), xs <+: ys → (sys.trs a xs).2 = [] → (sys.trs a ys).2 = [] → (sys.trs a xs).1 = (sys.trs a ys).1 → xs = ys) : sys.Acyclic a

theorem System.acyclic_def_full_trs_inj {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] : sys.Acyclic a ↔ ∀ (xs ys : List T), xs <+: ys → (sys.trs a xs).2 = [] → (sys.trs a ys).2 = [] → (sys.trs a xs).1 = (sys.trs a ys).1 → xs = ys

@[simp]

theorem System.trs_take_length_sub_eq {S T : Type u} {sys : System S T} {a : S} {xs : List T} : sys.trs a (List.take (xs.length - (sys.trs a xs).2.length) xs) = ((sys.trs a xs).1, [])

theorem System.trs_snd_eq_nil_of_trs_eq_of_prefix_and_and_ne {S T : Type u} {sys : System S T} {a : S} {xs ys : List T} (h₁ : sys.trs a xs = sys.trs a ys) (h₂ : xs <+: ys) (h₃ : xs ≠ ys) : (sys.trs a xs).2 = []

theorem System.trs_inj_of_acyclic {S T : Type u} {sys : System S T} {a : S} [h : sys.Acyclic a] {xs ys : List T} (hx : xs <+: ys) (h₁ : sys.trs a xs = sys.trs a ys) : xs = ys

theorem System.acyclic_of_trs_inj {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] (h : ∀ (xs ys : List T), xs <+: ys → sys.trs a xs = sys.trs a ys → xs = ys) : sys.Acyclic a

theorem System.acyclic_def_trs_inj {S T : Type u} {sys : System S T} {a : S} [ha : sys.WF a] : sys.Acyclic a ↔ ∀ (xs ys : List T), xs <+: ys → sys.trs a xs = sys.trs a ys → xs = ys

theorem System.acyclic_of_tr {S T : Type u} {sys : System S T} {a : S} [ha : sys.Acyclic a] {t : T} {b : S} (h₁ : sys.tr a t = some b) : sys.Acyclic b

theorem System.simulate_succ_snd_eq_zero_of_tr_and_eq_zero {S T : Type u} {sys : System S T} {f : S → T} {a b : S} {n : ℕ} (h₁ : (sys.simulate f b n).2 = 0) (h₂ : sys.tr a (f a) = some b) : (sys.simulate f a (n + 1)).2 = 0

theorem System.simulate_snd_eq_zero_of_tr_and_eq_zero {S T : Type u} {sys : System S T} {f : S → T} {a b : S} {n : ℕ} (h₁ : (sys.simulate f b n).2 = 0) (h₂ : sys.tr a (f a) = some b) : (sys.simulate f a n).2 = 0

theorem System.simulate_finset_card_eq_of_acyclic {S T : Type u} {sys : System S T} [hs : DecidableEq S] {f : S → T} [hf : sys.SimFn f] {a : S} [ha : sys.Acyclic a] {n : ℕ} (h₁ : (sys.simulate f a n).2 = 0) : (Finset.mkRaw fun (k : Fin (n + 1)) => (sys.simulate f a ↑k).1).card = n + 1

theorem System.simulate_exi_snd_pos_of_finite' {S T : Type u} {sys : System S T} [hs : Fintype S] {a : S} [ha : sys.Acyclic a] {f : S → T} [hf : sys.SimFn f] : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (k : ℕ), 0 < k ∧ ∃ (x : S), sys.simulate f a n = (x, k)

theorem System.simulate_exi_snd_pos_of_finite {S T : Type u} {sys : System S T} [h₁ : Fintype S] {s : S} [h₂ : sys.Acyclic s] {f : S → T} [h₃ : sys.SimFn f] : ∃ (x : S) (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (k : ℕ), 0 < k ∧ sys.simulate f s n = (x, k)

@[simp]

theorem System.wf_fst_simulate {S T : Type u} {sys : System S T} {s : S} {f : S → T} {n : ℕ} [hs : sys.WF s] : sys.WF (sys.simulate f s n).1

instance System.instWFFstNatSimulate {S T : Type u} {sys : System S T} {s : S} {f : S → T} {n : ℕ} [hs : sys.WF s] : sys.WF (sys.simulate f s n).1

theorem System.wf_of_simulate' {S T : Type u} {sys : System S T} {s : S} {f : S → T} {n : ℕ} {r : S × ℕ} [hs : sys.WF s] (h : sys.simulate f s n = r) : sys.WF r.1

theorem System.wf_of_simulate {S T : Type u} {sys : System S T} {s s₁ : S} {f : S → T} {n r : ℕ} [hs : sys.WF s] (h : sys.simulate f s n = (s₁, r)) : sys.WF s₁

theorem System.simulate_add_eq_left_iff {S T : Type u} {sys : System S T} {f : S → T} [hf : sys.SimFn f] {a b : S} {n m : ℕ} [ha : sys.WF a] : sys.simulate f a (n + m) = (b, n) ↔ sys.simulate f a m = (b, 0) ∧ (sys.validTr b (f b) → n = 0)

theorem System.simulate_add_eq_right_iff {S T : Type u} {sys : System S T} {f : S → T} [hf : sys.SimFn f] {a b : S} {n m : ℕ} [ha : sys.WF a] : sys.simulate f a (n + m) = (b, m) ↔ sys.simulate f a n = (b, 0) ∧ (sys.validTr b (f b) → m = 0)

@[simp]

theorem System.not_hasTr_iff {S T : Type u} {sys : System S T} {a : S} : ¬sys.hasTr a ↔ ∀ (t : T), sys.tr a t = none

theorem System.tr_eq_none_iff_of_simFn {S T : Type u} {sys : System S T} {f : S → T} {a : S} [hf : sys.SimFn f] [ha : sys.WF a] : sys.tr a (f a) = none ↔ ¬sys.hasTr a

theorem System.false_of_tr_eq_none_and_some_of_simFn {S T : Type u} {sys : System S T} {f g : S → T} {a b : S} [hf : sys.SimFn f] [hg : sys.SimFn g] [ha : sys.WF a] (h₁ : sys.tr a (f a) = none) (h₂ : sys.tr a (g a) = some b) : False

theorem System.tree_iff_full_trs {S T : Type u} {sys : System S T} {s : S} : sys.Tree s ↔ sys.WF s ∧ ∀ {ts₁ ts₂ : List T} {s' : S}, sys.trs s ts₁ = (s', []) → sys.trs s ts₂ = (s', []) → ts₁ = ts₂

@[simp]

theorem System.trs_eq_self_nil_iff_of_tree {S T : Type u} {sys : System S T} {s : S} {ts : List T} [hs : sys.Tree s] : sys.trs s ts = (s, []) ↔ ts = []

theorem System.simulate_congr_rel {S T : Type u} {sys : System S T} {f g : S → T} {r : S → S → Prop} {a₁ a₂ : S} {n : ℕ} [hf : sys.SimFn f] [hg : sys.SimFn g] [ha₁ : sys.WF a₁] [ha₂ : sys.WF a₂] (h₁ : r a₁ a₂) (h₂ : ∀ k < n, ∀ (b₁ b₂ : S), sys.simulate f a₁ k = (b₁, 0) → sys.simulate g a₂ k = (b₂, 0) → r b₁ b₂ → (sys.hasTr b₁ ↔ sys.hasTr b₂) ∧ ∀ (c₁ c₂ : S), sys.tr b₁ (f b₁) = some c₁ → sys.tr b₂ (g b₂) = some c₂ → r c₁ c₂) : ∃ (b : S), r (sys.simulate f a₁ n).1 b ∧ sys.simulate g a₂ n = (b, (sys.simulate f a₁ n).2)

theorem System.simulate_congr_rel_full {S T : Type u} {sys : System S T} {f g : S → T} {r : S → S → Prop} {a₁ a₂ b₁ : S} {n : ℕ} [hf : sys.SimFn f] [hg : sys.SimFn g] [ha₁ : sys.WF a₁] [ha₂ : sys.WF a₂] (h₂ : sys.simulate f a₁ n = (b₁, 0)) (h₁ : r a₁ a₂) (h₃ : ∀ k < n, ∀ (b₁ b₂ c₁ : S), sys.simulate f a₁ k = (b₁, 0) → sys.simulate g a₂ k = (b₂, 0) → r b₁ b₂ → sys.tr b₁ (f b₁) = some c₁ → ∃ (c₂ : S), sys.tr b₂ (g b₂) = some c₂ ∧ r c₁ c₂) : ∃ (b₂ : S), sys.simulate g a₂ n = (b₂, 0) ∧ r b₁ b₂

theorem System.simulate_congr_rel' {S T : Type u} {sys : System S T} {f g : S → T} {r : S → S → Prop} {a₁ a₂ : S} {n : ℕ} [hf : sys.SimFn f] [hg : sys.SimFn g] [ha₁ : sys.WF a₁] [ha₂ : sys.WF a₂] (h₂ : (sys.simulate f a₁ n).2 = 0) (h₁ : r a₁ a₂) (h₃ : ∀ k < n, ∀ (b₁ b₂ c₁ : S), sys.simulate f a₁ k = (b₁, 0) → sys.simulate g a₂ k = (b₂, 0) → r b₁ b₂ → sys.tr b₁ (f b₁) = some c₁ → ∃ (c₂ : S), sys.tr b₂ (g b₂) = some c₂ ∧ r c₁ c₂) : (sys.simulate g a₂ n).2 = 0

theorem System.simulate_congr {S T : Type u} {sys : System S T} {f g : S → T} {a : S} {n : ℕ} [hf : sys.SimFn f] [hg : sys.SimFn g] [ha : sys.WF a] (h : ∀ k < n, ∀ (b : S), sys.simulate f a k = (b, 0) → sys.simulate g a k = (b, 0) → sys.hasTr b → f b = g b) : sys.simulate f a n = sys.simulate g a n

theorem System.not_reachable_of_acyclic_and_simulate_and_lt {S T : Type u} {sys : System S T} {a b : S} {f : S → T} {k n : ℕ} [ha : sys.Acyclic a] (h₁ : sys.simulate f a n = (b, 0)) (h₂ : k < n) : ¬sys.Reachable b (sys.simulate f a k).1

theorem System.not_hasTr_of_snd_simulate_ne_zero {S T : Type u} {sys : System S T} {a : S} {n : ℕ} {f : S → T} {r : S × ℕ} [ha : sys.WF a] [hf : sys.SimFn f] (h₁ : sys.simulate f a n = r) (h₂ : r.2 ≠ 0) : ¬sys.hasTr r.1

theorem System.false_of_acyclic_and_reachable_and_tr {S T : Type u} {sys : System S T} {a b : S} {t : T} [ha : sys.Acyclic a] (h₁ : sys.Reachable a b) (h₂ : sys.tr b t = some a) : False

theorem System.fst_simulate_ind {S T : Type u} {sys : System S T} {f : S → T} {s : S} {p : S → Prop} (h : ∀ (n : ℕ) (s' : S), sys.simulate f s n = (s', 0) → p s') (n : ℕ) : p (sys.simulate f s n).1