structure System (S T : Type u) : Type u

• initial : Set S
• tr : S → T → Option S

theorem System.ext_iff {S T : Type u} {x y : System S T} : x = y ↔ x.initial = y.initial ∧ x.tr = y.tr

theorem System.ext {S T : Type u} {x y : System S T} (initial : x.initial = y.initial) (tr : x.tr = y.tr) : x = y

def System.validTr {S T : Type u} (sys : System S T) (s : S) (t : T) : Prop

Equations

• sys.validTr s t = ∃ (s' : S), sys.tr s t = some s'

def System.hasTr {S T : Type u} (sys : System S T) (s : S) : Prop

Equations

• sys.hasTr s = ∃ (t : T), sys.validTr s t

class System.DecidableHasTr {S T : Type u} (sys : System S T) : Type u

• h (s : S) : Decidable (sys.hasTr s)

class System.Initial {S T : Type u} (sys : System S T) (s : S) : Prop

• h : s ∈ sys.initial

class inductive System.Reachable {S T : Type u} (sys : System S T) : S → S → Prop

• refl {S T : Type u} {sys : System S T} {a : S} : sys.Reachable a a
• step {S T : Type u} {sys : System S T} {a b c : S} {t : T} : sys.tr a t = some b → sys.Reachable b c → sys.Reachable a c

class System.WF {S T : Type u} (sys : System S T) (s' : S) : Prop

• h : ∃ (s : S), sys.Initial s ∧ sys.Reachable s s'

class System.SimFn {S T : Type u} (sys : System S T) (f : S → T) : Prop

• h {s : S} [sys.WF s] : sys.hasTr s → sys.validTr s (f s)

def System.tr! {S T : Type u} (sys : System S T) (s : S) (t : T) : S

Equations

• sys.tr! s t = (sys.tr s t).getD s

def System.trs {S T : Type u} (sys : System S T) (s : S) : List T → S × List T

Equations

• sys.trs s [] = (s, [])
• sys.trs s (t :: ts) = match sys.tr s t with | none => (s, t :: ts) | some s₁ => sys.trs s₁ ts

def System.simulate {S T : Type u} (sys : System S T) (f : S → T) (s : S) : ℕ → S × ℕ

Equations

• sys.simulate f s 0 = (s, 0)
• sys.simulate f s n.succ = match sys.tr s (f s) with | none => (s, n + 1) | some s₁ => sys.simulate f s₁ n

def System.simp_path' {S T : Type u} (sys : System S T) (a : S) (ts : List T) : Prop

Equations

• sys.simp_path' a ts = ∀ (xs ys : List T), xs <+: ts → ys <+: ts → (sys.trs a xs).1 = (sys.trs a ys).1 → xs = ys

def System.simp_path {S T : Type u} (sys : System S T) (a : S) (ts : List T) (b : S) : Prop

Equations

• sys.simp_path a ts b = (sys.simp_path' a ts ∧ sys.trs a ts = (b, []))

class System.Acyclic {S T : Type u} (sys : System S T) (s : S) : Prop

• wf_s : sys.WF s
• h {a b : S} {t : T} : sys.Reachable s a → sys.tr a t = some b → ¬sys.Reachable b a

class System.Tree {S T : Type u} (sys : System S T) (s : S) : Prop

• wf_s : sys.WF s
• h {ts₁ ts₂ : List T} : sys.trs s ts₁ = sys.trs s ts₂ → ts₁ = ts₂