structure AMMs : Type

• res : T →₀ W₀
• distinct (t : T) : (self.res t) t = 0
• posres (t0 t1 : T) : (self.res t0) t1 ≠ 0 ↔ (self.res t1) t0 ≠ 0

def AMMs.empty : AMMs

Equations

• AMMs.empty = { res := 0, distinct := AMMs.empty.proof_1, posres := AMMs.empty.proof_2 }

def AMMs.init (amms : AMMs) (t0 t1 : T) : Prop

Equations

• amms.init t0 t1 = ((amms.res t0) t1 ≠ 0)

theorem AMMs.empty_uninit (t0 t1 : T) : ¬empty.init t0 t1

theorem AMMs.same_uninit (amms : AMMs) (t : T) : ¬amms.init t t

def AMMs.init.swap {amms : AMMs} {t0 t1 : T} (h : amms.init t0 t1) : amms.init t1 t0

Equations

• ⋯ = ⋯

def AMMs.init_swap_iff (amms : AMMs) (t0 t1 : T) : amms.init t0 t1 ↔ amms.init t1 t0

Equations

• ⋯ = ⋯

def AMMs.init.dif {amms : AMMs} {t0 t1 : T} (h : amms.init t0 t1) : t0 ≠ t1

Equations

• ⋯ = ⋯

theorem AMMs.init.samepair {amms : AMMs} {t0 t1 : T} (h : amms.init t0 t1) {t0' t1' : T} (same : samemint t0 t1 t0' t1') : amms.init t0' t1'

noncomputable def AMMs.initialize (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) : AMMs

Equations

• amms.initialize hdif r0 r1 = { res := (amms.res.update t0 (Finsupp.update (amms.res t0) t1 ↑r0)).update t1 (Finsupp.update (amms.res t1) t0 ↑r1), distinct := ⋯, posres := ⋯ }

@[simp]

theorem AMMs.initialize_init_diffpair (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (h : diffmint t0 t1 t0' t1') : (amms.initialize hdif r0 r1).init t0' t1' ↔ amms.init t0' t1'

@[simp]

theorem AMMs.initialize_init_not_diffpair (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (h : samemint t0 t1 t0' t1') : (amms.initialize hdif r0 r1).init t0' t1'

@[simp]

theorem AMMs.initialize_init_self (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) : (amms.initialize hdif r0 r1).init t0 t1

def AMMs.r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) : ℝ>0

Equations

• amms.r0 t0 t1 h = ⟨↑((amms.res t0) t1), ⋯⟩

def AMMs.r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) : ℝ>0

Equations

• amms.r1 t0 t1 h = ⟨↑((amms.res t1) t0), ⋯⟩

theorem AMMs.r0_reorder (amms : AMMs) (t1 t0 : T) (h : amms.init t1 t0) : amms.r0 t1 t0 h = amms.r1 t0 t1 ⋯

theorem AMMs.r1_reorder (amms : AMMs) (t1 t0 : T) (h : amms.init t1 t0) : amms.r1 t1 t0 h = amms.r0 t0 t1 ⋯

noncomputable instance decidableInit (amms : AMMs) (t0 t1 : T) : Decidable (amms.init t0 t1)

Equations

• decidableInit amms t0 t1 = id inferInstance

noncomputable def AMMs.add_r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) : AMMs

Equations

• amms.add_r0 t0 t1 h x = amms.initialize ⋯ (amms.r0 t0 t1 h + x) (amms.r1 t0 t1 h)

noncomputable def AMMs.sub_r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (nodrain : x < amms.r0 t0 t1 h) : AMMs

Equations

• amms.sub_r0 t0 t1 h x nodrain = amms.initialize ⋯ ((amms.r0 t0 t1 h).sub x nodrain) (amms.r1 t0 t1 h)

noncomputable def AMMs.add_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) : AMMs

Equations

• amms.add_r1 t0 t1 h x = amms.initialize ⋯ (amms.r0 t0 t1 h) (amms.r1 t0 t1 h + x)

noncomputable def AMMs.sub_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (nodrain : x < amms.r1 t0 t1 h) : AMMs

Equations

• amms.sub_r1 t0 t1 h x nodrain = amms.initialize ⋯ (amms.r0 t0 t1 h) ((amms.r1 t0 t1 h).sub x nodrain)

@[simp]

theorem AMMs.r0_of_initialize (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) : (amms.initialize hdif r0 r1).r0 t0 t1 ⋯ = r0

@[simp]

theorem AMMs.r1_of_initialize (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) : (amms.initialize hdif r0 r1).r1 t0 t1 ⋯ = r1

@[simp]

theorem AMMs.r0_of_initialize_diffpair (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (hinit : amms.init t0' t1') (difp : diffmint t0 t1 t0' t1') : (amms.initialize hdif r0 r1).r0 t0' t1' ⋯ = amms.r0 t0' t1' hinit

@[simp]

theorem AMMs.r1_of_initialize_diffpair (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (hinit : amms.init t0' t1') (difp : diffmint t0 t1 t0' t1') : (amms.initialize hdif r0 r1).r1 t0' t1' ⋯ = amms.r1 t0' t1' hinit

@[simp]

theorem AMMs.init_of_add_r0 (amms : AMMs) (t0 t1 t0' t1' : T) (h : amms.init t0 t1) (x : ℝ>0) : (amms.add_r0 t0 t1 h x).init t0' t1' ↔ amms.init t0' t1'

@[simp]

theorem AMMs.init_of_add_r1 (amms : AMMs) (t0 t1 t0' t1' : T) (h : amms.init t0 t1) (x : ℝ>0) : (amms.add_r1 t0 t1 h x).init t0' t1' ↔ amms.init t0' t1'

@[simp]

theorem AMMs.init_of_sub_r0 (amms : AMMs) (t0 t1 t0' t1' : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) : (amms.sub_r0 t0 t1 h x h').init t0' t1' ↔ amms.init t0' t1'

@[simp]

theorem AMMs.init_of_sub_r1 (amms : AMMs) (t0 t1 t0' t1' : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) : (amms.sub_r1 t0 t1 h x h').init t0' t1' ↔ amms.init t0' t1'

@[simp]

theorem AMMs.r0_of_add_r0 (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) : (amms.add_r0 t0 t1 h x).r0 t0 t1 ⋯ = x + amms.r0 t0 t1 h

@[simp]

theorem AMMs.r0_of_add_r0_diff (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (h' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.add_r0 t0 t1 h x).r0 t0' t1' ⋯ = amms.r0 t0' t1' h'

@[simp]

theorem AMMs.r0_of_add_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) : (amms.add_r1 t0 t1 h x).r0 t0 t1 ⋯ = amms.r0 t0 t1 h

@[simp]

theorem AMMs.r0_of_add_r1_diff (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (h' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.add_r1 t0 t1 h x).r0 t0' t1' ⋯ = amms.r0 t0' t1' h'

@[simp]

theorem AMMs.r1_of_add_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) : (amms.add_r1 t0 t1 h x).r1 t0 t1 ⋯ = x + amms.r1 t0 t1 h

@[simp]

theorem AMMs.r1_of_add_r1_diff (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (h' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.add_r1 t0 t1 h x).r1 t0' t1' ⋯ = amms.r1 t0' t1' h'

@[simp]

theorem AMMs.r1_of_add_r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) : (amms.add_r0 t0 t1 h x).r1 t0 t1 ⋯ = amms.r1 t0 t1 h

@[simp]

theorem AMMs.r1_of_add_r0_diff (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (h' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.add_r0 t0 t1 h x).r1 t0' t1' ⋯ = amms.r1 t0' t1' h'

@[simp]

theorem AMMs.r0_of_sub_r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) : (amms.sub_r0 t0 t1 h x h').r0 t0 t1 ⋯ = (amms.r0 t0 t1 h).sub x h'

@[simp]

theorem AMMs.r0_of_sub_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) : (amms.sub_r1 t0 t1 h x h').r0 t0 t1 ⋯ = amms.r0 t0 t1 h

@[simp]

theorem AMMs.r1_of_sub_r1 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) : (amms.sub_r1 t0 t1 h x h').r1 t0 t1 ⋯ = (amms.r1 t0 t1 h).sub x h'

@[simp]

theorem AMMs.r1_of_sub_r0 (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) : (amms.sub_r0 t0 t1 h x h').r1 t0 t1 ⋯ = amms.r1 t0 t1 h

@[simp]

theorem AMMs.r0_of_sub_r0_diff (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) (t0' t1' : T) (h'' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.sub_r0 t0 t1 h x h').r0 t0' t1' ⋯ = amms.r0 t0' t1' h''

@[simp]

theorem AMMs.r0_of_sub_r1_diff (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) (t0' t1' : T) (h'' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.sub_r1 t0 t1 h x h').r0 t0' t1' ⋯ = amms.r0 t0' t1' h''

@[simp]

theorem AMMs.r1_of_sub_r1_diff (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) (t0' t1' : T) (h'' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.sub_r1 t0 t1 h x h').r1 t0' t1' ⋯ = amms.r1 t0' t1' h''

@[simp]

theorem AMMs.r1_of_sub_r0_diff (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) (t0' t1' : T) (h'' : amms.init t0' t1') (hdiff : diffmint t0 t1 t0' t1') : (amms.sub_r0 t0 t1 h x h').r1 t0' t1' ⋯ = amms.r1 t0' t1' h''