structure Create (s : Γ) (t0 t1 : T) (a : A) (v0 v1 : ℝ>0) : Prop

• hdif : t0 ≠ t1
• hnin : ¬s.amms.init t0 t1
• hen0 : ↑v0 ≤ (s.atoms.get a) t0
• hen1 : ↑v1 ≤ (s.atoms.get a) t1

noncomputable def Create.apply {t0 t1 : T} {a : A} {v0 v1 : ℝ>0} {s : Γ} (v : Create s t0 t1 a v0 v1) : Γ

Equations

• v.apply = { atoms := (s.atoms.sub a t0 ↑v0 ⋯).sub a t1 ↑v1 ⋯, mints := s.mints.add a t0 t1 ⋯ ↑v0, amms := s.amms.initialize ⋯ v0 v1 }

@[simp]

theorem Create.supply_minted_diff' {t0 t1 : T} {a : A} {r0 r1 : ℝ>0} {s : Γ} (v : Create s t0 t1 a r0 r1) (t0' t1' : T) (hdifp : diffmint t0 t1 t0' t1') : v.apply.mints.supply t0' t1' = s.mints.supply t0' t1'

@[simp]

theorem Create.supply_minted_diff {t0 t1 : T} {a : A} {r0 r1 : ℝ>0} {s : Γ} (v : Create s t0 t1 a r0 r1) (t0' t1' : T) (hdifp : diffmint t0 t1 t0' t1') : v.apply.mintsupply t0' t1' = s.mintsupply t0' t1'

@[simp]

theorem Create.init_same {s : Γ} {t0 t1 : T} {a : A} {r0 r1 : ℝ>0} (v : Create s t0 t1 a r0 r1) (t0' t1' : T) (same : samemint t0 t1 t0' t1') : v.apply.amms.init t0' t1'

@[simp]

theorem Create.init_diff_iff {t0 t1 : T} {a : A} {r0 r1 : ℝ>0} {s : Γ} (v : Create s t0 t1 a r0 r1) (t0' t1' : T) (hdifp : diffmint t0 t1 t0' t1') : v.apply.amms.init t0' t1' ↔ s.amms.init t0' t1'