@[instance_reducible]

instance System.instInhabited {S T : Type u} : Inhabited (System S T)

Equations

• System.instInhabited = { default := { initial := ∅, tr := default } }

noncomputable def System.dfltSimFn {S T : Type u} {sys : System S T} [Inhabited (S → T)] : S → T

Equations

• System.dfltSimFn s = if h : sys.hasTr s then Exists.choose h else default s

noncomputable def System.mkSimFn {S T : Type u} {sys : System S T} (f : S → T) : S → T

Equations

• System.mkSimFn f s = if h : sys.validTr s (f s) then f s else System.dfltSimFn s

@[simp]

instance System.instSimFnDfltSimFn {S T : Type u} {sys : System S T} [Inhabited (S → T)] : sys.SimFn dfltSimFn

theorem System.validTr_of_simFn_and_hasTr {S T : Type u} {sys : System S T} {s : S} {f : S → T} [hs : sys.WF s] [hf : sys.SimFn f] (h : sys.hasTr s) : sys.validTr s (f s)

@[simp]

instance System.instSimFnMkSimFn {S T : Type u} {sys : System S T} {f : S → T} : sys.SimFn (mkSimFn f)

@[simp]

theorem System.Reachable.refl' {S T : Type u} {sys : System S T} {a : S} : sys.Reachable a a

theorem System.Reachable.trans {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.validTr_of_eq_some {S T : Type u} {sys : System S T} {s : S} {t : T} {s₁ : S} (h : sys.tr s t = some s₁) : sys.validTr s t

theorem System.hasTr_of_eq_some {S T : Type u} {sys : System S T} {s : S} {t : T} {s₁ : S} (h : sys.tr s t = some s₁) : sys.hasTr s

theorem System.reachable_of_simulate' {S T : Type u} {sys : System S T} {f : S → T} {s₁ s₂ : S} {n : ℕ} (h : (sys.simulate f s₁ n).1 = s₂) : sys.Reachable s₁ s₂

theorem System.reachable_of_simulate {S T : Type u} {sys : System S T} {f : S → T} {s₁ s₂ : S} {n r : ℕ} (h : sys.simulate f s₁ n = (s₂, r)) : sys.Reachable s₁ s₂

theorem System.reachable_left {S T : Type u} {sys : System S T} {a b c : S} {t : T} (h₁ : sys.tr a t = some b) (h₂ : sys.Reachable b c) : sys.Reachable a c

theorem System.reachable_right {S T : Type u} {sys : System S T} {a b c : S} {t : T} (h₁ : sys.Reachable a b) (h₂ : sys.tr b t = some c) : sys.Reachable a c

theorem System.reachable_of_tr {S T : Type u} {sys : System S T} {a b : S} {t : T} (h : sys.tr a t = some b) : sys.Reachable a b

theorem System.hasTr_of_reachable_and_ne {S T : Type u} {sys : System S T} {s₁ s₂ : S} (h₁ : sys.Reachable s₁ s₂) (h₂ : s₁ ≠ s₂) : sys.hasTr s₁

theorem System.eq_of_reachable_and_not_hasTr {S T : Type u} {sys : System S T} {s₁ s₂ : S} (h₁ : sys.Reachable s₁ s₂) (h₂ : ¬sys.hasTr s₁) : s₁ = s₂

theorem System.exi_tr_right_of_reachable_and_ne {S T : Type u} {sys : System S T} {a b : S} (h₁ : sys.Reachable a b) (h₂ : a ≠ b) : ∃ (c : S) (t : T), sys.Reachable a c ∧ sys.tr c t = some b

theorem System.reachable_ind_left {S T : Type u} {sys : System S T} {P : (a b : S) → sys.Reachable a b → Prop} (h₁ : ∀ {a : S}, P a a ⋯) (h₂ : ∀ {a b c : S} {t : T} (hx : sys.tr a t = some b) (hy : sys.Reachable b c), P b c hy → P a c ⋯) {a b : S} (h : sys.Reachable a b) : P a b h

@[simp]

theorem System.trs_empty {S T : Type u} {sys : System S T} {s : S} : sys.trs s [] = (s, [])

@[simp]

theorem System.simulate_zero {S T : Type u} {sys : System S T} {f : S → T} {s : S} : sys.simulate f s 0 = (s, 0)

theorem System.reachable_of_trs' {S T : Type u} {sys : System S T} {a : S} {ts : List T} {r : S × List T} (h : sys.trs a ts = r) : sys.Reachable a r.1

theorem System.reachable_of_trs {S T : Type u} {sys : System S T} {a b : S} {ts r : List T} (h : sys.trs a ts = (b, r)) : sys.Reachable a b

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

theorem System.reachable_iff_exi_trs {S T : Type u} {sys : System S T} {a b : S} : sys.Reachable a b ↔ ∃ (ts : List T), sys.trs a ts = (b, [])

theorem System.trs_append {S T : Type u} {sys : System S T} {s : S} {xs ys : List T} : sys.trs s (xs ++ ys) = match sys.trs s xs with | (s₁, xs') => match sys.trs s₁ ys with | (s₂, ys') => if xs' ≠ [] then (s₁, xs' ++ ys) else (s₂, xs' ++ ys')

theorem System.reachable_trs_aux {S T : Type u} {sys : System S T} {a b : S} {ts : List T} (h : sys.Reachable a b) : sys.Reachable a (sys.trs b ts).1

@[simp]

theorem System.reachable_trs {S T : Type u} {sys : System S T} {s : S} {ts : List T} : sys.Reachable s (sys.trs s ts).1

theorem System.simulate_add {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n m : ℕ} : sys.simulate f s (n + m) = 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')

@[simp]

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

@[simp]

theorem System.trs_append_full {S T : Type u} {sys : System S T} {s s₂ : S} {ts₁ ts₂ : List T} : sys.trs s (ts₁ ++ ts₂) = (s₂, []) ↔ ∃ (s₁ : S), sys.trs s ts₁ = (s₁, []) ∧ sys.trs s₁ ts₂ = (s₂, [])

@[simp]

theorem System.trs_cons_full {S T : Type u} {sys : System S T} {s s₂ : S} {t : T} {ts : List T} : sys.trs s (t :: ts) = (s₂, []) ↔ ∃ (s₁ : S), sys.tr s t = some s₁ ∧ sys.trs s₁ ts = (s₂, [])

@[simp]

theorem System.trs_snoc_full {S T : Type u} {sys : System S T} {s s₂ : S} {t : T} {ts : List T} : sys.trs s (ts ++ [t]) = (s₂, []) ↔ ∃ (s₁ : S), sys.trs s ts = (s₁, []) ∧ sys.tr s₁ t = some s₂

theorem System.reachable_ind_right {S T : Type u} {sys : System S T} {P : (a b : S) → sys.Reachable a b → Prop} (h₁ : ∀ {a : S}, P a a ⋯) (h₂ : ∀ {a b c : S} {t : T} (hx : sys.Reachable a b) (hy : sys.tr b t = some c), P a b hx → P a c ⋯) {a b : S} (h : sys.Reachable a b) : P a b h

@[simp]

theorem System.simulate_snd_le {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : (sys.simulate f s n).2 ≤ n

theorem System.simulate_snd_mono {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n m : ℕ} (h : n ≤ m) : (sys.simulate f s n).2 ≤ (sys.simulate f s m).2

@[simp]

theorem System.simulate_sub_simulate_snd_eq {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} : sys.simulate f s (n - (sys.simulate f s n).2) = ((sys.simulate f s n).1, 0)

theorem System.simFn_def {S T : Type u} {sys : System S T} {f : S → T} : sys.SimFn f ↔ ∀ {s : S} [sys.WF s], sys.hasTr s → sys.validTr s (f s)

theorem System.acyclic_def {S T : Type u} {sys : System S T} {s : S} : sys.Acyclic s ↔ sys.WF s ∧ ∀ {a b : S} {t : T}, sys.Reachable s a → sys.tr a t = some b → ¬sys.Reachable b a

theorem System.tree_def {S T : Type u} {sys : System S T} {s : S} : sys.Tree s ↔ sys.WF s ∧ ∀ {ts₁ ts₂ : List T}, sys.trs s ts₁ = sys.trs s ts₂ → ts₁ = ts₂

theorem System.wf_def {S T : Type u} {sys : System S T} {b : S} : sys.WF b ↔ ∃ (a : S), sys.Initial a ∧ sys.Reachable a b

theorem System.wf_of_initial {S T : Type u} {sys : System S T} {s : S} [sys.Initial s] : sys.WF s

@[simp]

instance System.instWFOfInitial {S T : Type u} {sys : System S T} {s : S} [sys.Initial s] : sys.WF s

theorem System.wf_of_reachable {S T : Type u} {sys : System S T} {a b : S} [ha : sys.WF a] (hb : sys.Reachable a b) : sys.WF b

theorem System.initial_def {S T : Type u} {sys : System S T} {a : S} : sys.Initial a ↔ a ∈ sys.initial

theorem System.validTr_iff_isSome {S T : Type u} {sys : System S T} {s : S} {t : T} : sys.validTr s t ↔ (sys.tr s t).isSome = true

theorem System.hasTr_iff {S T : Type u} {sys : System S T} {s : S} : sys.hasTr s ↔ ∃ (t : T) (s' : S), sys.tr s t = some s'

@[instance_reducible]

instance System.instDecidableValidTr {S T : Type u} {sys : System S T} {s : S} {t : T} : Decidable (sys.validTr s t)

Equations

• System.instDecidableValidTr = match h : sys.tr s t with | none => isFalse ⋯ | some val => isTrue ⋯

theorem System.reachable_of_fst_trs {S T : Type u} {sys : System S T} {a : S} {ts : List T} {b : S} (h : (sys.trs a ts).1 = b) : sys.Reachable a b

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

theorem System.wf_of_trs {S T : Type u} {sys : System S T} {a b : S} {ts r : List T} [ha : sys.WF a] (h : sys.trs a ts = (b, r)) : sys.WF b

theorem System.wf_of_acyclic {S T : Type u} {sys : System S T} {a : S} [ha : sys.Acyclic a] : sys.WF a

theorem System.wf_of_tree {S T : Type u} {sys : System S T} {a : S} [ha : sys.Tree a] : sys.WF a

instance System.instWFOfAcyclic {S T : Type u} {sys : System S T} {a : S} [ha : sys.Acyclic a] : sys.WF a

instance System.instWFOfTree {S T : Type u} {sys : System S T} {a : S} [ha : sys.Tree a] : sys.WF a

theorem System.simulate_eq_of_not_hasTr {S T : Type u} {sys : System S T} {f : S → T} {s : S} {n : ℕ} (h : ¬sys.hasTr s) : sys.simulate f s n = (s, n)

class System.WFTrans {S T : Type u} (sys : System S T) (t : T) : Prop

• h : ∃ (s : S), sys.WF s ∧ sys.validTr s t

theorem System.WFTrans_def {S T : Type u} {sys : System S T} {t : T} : sys.WFTrans t ↔ ∃ (s : S), sys.WF s ∧ sys.validTr s t

theorem System.wfTrans_of_validTr {S T : Type u} {sys : System S T} {s : S} {t : T} [hs : sys.WF s] (h : sys.validTr s t) : sys.WFTrans t

theorem System.wfTrans_of_tr {S T : Type u} {sys : System S T} {s s' : S} {t : T} [hs : sys.WF s] (h : sys.tr s t = some s') : sys.WFTrans t

theorem System.simulate_snd_le_of_eq {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {r n : ℕ} (h : sys.simulate f s n = (s', r)) : r ≤ n

theorem System.simulate_snd_ne_zero_of {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {r n m : ℕ} (h : sys.simulate f s n = (s', r)) (hr : r ≠ 0) (hm : n ≤ m) : (sys.simulate f s m).2 ≠ 0

@[simp]

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

@[simp]

theorem System.snd_trs_append_eq_nil_iff {S T : Type u} {sys : System S T} {s : S} {ts₁ ts₂ : List T} : (sys.trs s (ts₁ ++ ts₂)).2 = [] ↔ ∃ (s₁ : S) (s₂ : S), sys.trs s ts₁ = (s₁, []) ∧ sys.trs s₁ ts₂ = (s₂, [])

@[simp]

theorem System.snd_trs_cons_eq_nil_iff {S T : Type u} {sys : System S T} {s : S} {t : T} {ts : List T} : (sys.trs s (t :: ts)).2 = [] ↔ ∃ (s₁ : S), sys.tr s t = some s₁ ∧ (sys.trs s₁ ts).2 = []

@[simp]

theorem System.snd_trs_snoc_eq_nil_iff {S T : Type u} {sys : System S T} {s : S} {t : T} {ts : List T} : (sys.trs s (ts ++ [t])).2 = [] ↔ ∃ (s₁ : S) (s₂ : S), sys.trs s ts = (s₁, []) ∧ sys.tr s₁ t = some s₂

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem System.simulate_one_of_snd_succ {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {r : ℕ} : sys.simulate f s 1 = (s', r.succ) ↔ sys.tr s (f s) = none ∧ s = s' ∧ r = 0

theorem System.simulate_one_of_snd_add_one {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {r : ℕ} : sys.simulate f s 1 = (s', r + 1) ↔ sys.tr s (f s) = none ∧ s = s' ∧ r = 0

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), sys.tr s (f s) = some s₁ ∧ (sys.simulate f s₁ n).2 = 0

@[simp]

theorem System.simulate_eq_snd_add_right_iff {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {n r : ℕ} : sys.simulate f s n = (s', n + r) ↔ r = 0 ∧ s = s' ∧ (n = 0 ∨ sys.tr s (f s) = none)

@[simp]

theorem System.simulate_eq_snd_add_left_iff {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {n r : ℕ} : sys.simulate f s n = (s', r + n) ↔ r = 0 ∧ s = s' ∧ (n = 0 ∨ sys.tr s (f s) = none)

@[simp]

theorem System.simulate_eq_same_iff {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {n : ℕ} : sys.simulate f s n = (s', n) ↔ s = s' ∧ (n = 0 ∨ sys.tr s (f s) = none)

@[simp]

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

theorem System.tr_eq_none_of_simulate_eq {S T : Type u} {sys : System S T} {f : S → T} {s s' : S} {n r : ℕ} (h : sys.simulate f s n = (s', r + 1)) : sys.tr s' (f s') = none