inductive Tx (sx : SX) (init : Γ) : Γ → Type

• empty {sx : SX} {init : Γ} : Tx sx init init
• create {sx : SX} {init : Γ} {t0 t1 : T} {a : A} {r0 r1 : ℝ>0} (s' : Γ) (rs : Tx sx init s') (d0 : Create s' t0 t1 a r0 r1) : Tx sx init d0.apply
• dep {sx : SX} {init : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (s' : Γ) (rs : Tx sx init s') (d : Deposit s' a t0 t1 v0) : Tx sx init d.apply
• red {sx : SX} {init : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (s' : Γ) (rs : Tx sx init s') (r : Redeem s' a t0 t1 v0) : Tx sx init r.apply
• swap {sx : SX} {init : Γ} {t0 t1 : T} {a : A} {v0 : ℝ>0} (s' : Γ) (rs : Tx sx init s') (sw : Swap sx s' a t0 t1 v0) : Tx sx init sw.apply

def validInit (s : Γ) : Prop

Equations

• validInit s = (s.amms = AMMs.empty ∧ s.mints = S₁.empty)

def reachable (sx : SX) (s : Γ) : Prop

Equations

• reachable sx s = ∃ (init : Γ) (x : Tx sx init s), validInit init

def concat {sx : SX} {init s' s'' : Γ} (t1 : Tx sx init s') (t2 : Tx sx s' s'') : Tx sx init s''

theorem AMMimpMintSupply {sx : SX} {s : Γ} {t0 t1 : T} (r : reachable sx s) (h : s.amms.init t0 t1) : 0 < s.mints.supply t0 t1

theorem SuppAMMimpMintSupply {sx : SX} {s : Γ} {t0 t1 : T} (r : reachable sx s) (h : 0 < s.mints.supply t0 t1) : s.amms.init t0 t1

theorem reachable_supply_iff_init {sx : SX} {s : Γ} {t0 t1 : T} (r : reachable sx s) : s.amms.init t0 t1 ↔ 0 < s.mints.supply t0 t1