structure Redeem (s : Γ) (a : A) (t0 t1 : T) (v : ℝ>0) : Prop

• exi : s.amms.init t0 t1
• hen0 : ↑v ≤ (s.mints.get a).get t0 t1
• nodrain : v < (s.mints.supply t0 t1).toPReal ⋯

theorem Redeem.nodrain_toNNReal {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (d : Redeem s a t0 t1 v) : ↑v < s.mints.supply t0 t1

noncomputable def Redeem.gain0 {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (d : Redeem s a t0 t1 v) : ℝ>0

Equations

• d.gain0 = v * s.amms.r0 t0 t1 ⋯ / (s.mints.supply t0 t1).toPReal ⋯

theorem Redeem.gain0_lt_r0 {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (r : Redeem s a t0 t1 v) : r.gain0 < s.amms.r0 t0 t1 ⋯

noncomputable def Redeem.gain1 {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (d : Redeem s a t0 t1 v) : ℝ>0

Equations

• d.gain1 = v * s.amms.r1 t0 t1 ⋯ / (s.mints.supply t0 t1).toPReal ⋯

theorem Redeem.gain1_lt_r1 {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (r : Redeem s a t0 t1 v) : r.gain1 < s.amms.r1 t0 t1 ⋯

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

Equations

• r.apply = { atoms := (s.atoms.add a t0 ↑r.gain0).add a t1 ↑r.gain1, mints := s.mints.sub a t0 t1 ⋯ ↑v ⋯, amms := (s.amms.sub_r0 t0 t1 ⋯ r.gain0 ⋯).sub_r1 t0 t1 ⋯ r.gain1 ⋯ }

@[simp]

theorem Redeem.atoms {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (r : Redeem s a t0 t1 v) : r.apply.atoms = (s.atoms.add a t0 ↑r.gain0).add a t1 ↑r.gain1

@[simp]

theorem Redeem.mints {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (r : Redeem s a t0 t1 v) : r.apply.mints = s.mints.sub a t0 t1 ⋯ ↑v ⋯

@[simp]

theorem Redeem.amms {s : Γ} {t0 t1 : T} {a : A} {v : ℝ>0} (r : Redeem s a t0 t1 v) : r.apply.amms = (s.amms.sub_r0 t0 t1 ⋯ r.gain0 ⋯).sub_r1 t0 t1 ⋯ r.gain1 ⋯