structure S₁ : Type

• map : A →₀ W₁

def S₁.empty : S₁

Equations

• S₁.empty = { map := 0 }

def S₁.get (s : S₁) (a : A) : W₁

Equations

• s.get a = s.map a

@[simp]

theorem S₁.map_eq_get (s : S₁) : ⇑s.map = s.get

noncomputable def S₁.add (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) : S₁

Equations

• s.add a t0 t1 hdif x = { map := s.map.update a ((s.map a).add t0 t1 hdif x) }

@[simp]

theorem S₁.get_add_self (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) : (s.add a t0 t1 hdif x).get a = (s.get a).add t0 t1 hdif x

@[simp]

theorem S₁.get_add_diff (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (a' : A) (hdiff : a ≠ a') : (s.add a t0 t1 hdif x).get a' = s.get a'

noncomputable def S₁.sub (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ ((s.get a).bal t0) t1) : S₁

Equations

• s.sub a t0 t1 hdif x h = { map := s.map.update a ((s.map a).sub t0 t1 hdif x h) }

@[simp]

theorem S₁.get_sub_self (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ ((s.get a).bal t0) t1) : (s.sub a t0 t1 hdif x h).get a = (s.get a).sub t0 t1 hdif x h

@[simp]

theorem S₁.get_sub_diff (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ ((s.get a).bal t0) t1) (a' : A) (hdiff : a ≠ a') : (s.sub a t0 t1 hdif x h).get a' = s.get a'

noncomputable def S₁.drain (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) : S₁

Equations

• s.drain a t0 t1 hdif = { map := s.map.update a ((s.map a).drain t0 t1 hdif) }

@[simp]

theorem S₁.get_drain_self (w : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) : (w.drain a t0 t1 hdif).get a = (w.get a).drain t0 t1 hdif

@[simp]

theorem S₁.get_drain_diff (w : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (a' : A) (hdiff : a ≠ a') : (w.drain a t0 t1 hdif).get a' = w.get a'

def S₁.supply (s : S₁) (t0 t1 : T) : NNReal

Equations

• s.supply t0 t1 = s.map.sum fun (x : A) (w : W₁) => w.get t0 t1

@[simp]

theorem S₁.supply_of_empty (t0 t1 : T) : empty.supply t0 t1 = 0

theorem S₁.supply_reorder (s : S₁) (t1 t0 : T) : s.supply t1 t0 = s.supply t0 t1

theorem S₁.supply_samepair (s : S₁) (t0 t1 t0' t1' : T) (samepair : samemint t0 t1 t0' t1') : s.supply t0 t1 = s.supply t0' t1'

theorem S₁.supply_destroy (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) : s.supply t0 t1 = (s.drain a t0 t1 hdif).supply t0 t1 + (s.get a).get t0 t1

theorem S₁.get_pos_imp_supp_pos (w : S₁) (t0 t1 : T) (a : A) (h : 0 < (w.get a).get t0 t1) : 0 < w.supply t0 t1

@[simp]

theorem S₁.supply_of_add_self (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) : (s.add a t0 t1 hdif x).supply t0 t1 = s.supply t0 t1 + x

@[simp]

theorem S₁.supply_of_add_diff (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (t0' t1' : T) (hdiffp : diffmint t0 t1 t0' t1') : (s.add a t0 t1 hdif x).supply t0' t1' = s.supply t0' t1'

@[simp]

theorem S₁.supply_of_sub_self (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ (s.get a).get t0 t1) : (s.sub a t0 t1 hdif x h).supply t0 t1 = s.supply t0 t1 - x

@[simp]

theorem S₁.supply_of_sub_diff (s : S₁) (a : A) (t0 t1 : T) (hdif : t0 ≠ t1) (x : NNReal) (h : x ≤ ((s.get a).bal t0) t1) (t0' t1' : T) (hdiffp : diffmint t0 t1 t0' t1') : (s.sub a t0 t1 hdif x h).supply t0' t1' = s.supply t0' t1'