import Mt.Thread.Traced
import Mt.System.Basic
import Mt.Utils.List

namespace Mt.System.Traced

open Utils

variable {spec: Spec
spec : Spec: Type 1
Spec}
local instance: {spec : Spec} → IsReservation spec.Reservation
instance : IsReservation: Type → Type
IsReservation spec: Spec
spec.Reservation: Spec → Type
Reservation :=spec: Spec
spec.is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation

def sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations (l: List (Traced.TracedThread spec)
l : List: Type ?u.28 → Type ?u.28
List (Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec)) : spec: Spec
spec.Reservation: Spec → Type
Reservation :=
  l: List (Traced.TracedThread spec)
l.foldl: {α : Type ?u.35} → {β : Type ?u.34} → (α → β → α) → α → List β → α
foldl (λ env_r: ?m.44
env_r thread: ?m.47
thread => env_r: ?m.44
env_r + thread: ?m.47
thread.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation) spec: Spec
spec.is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation.empty: {T : Type} → [self : IsReservation T] → T
empty 

private def sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' (start: ?m.219
start) (l: List (Traced.TracedThread spec)
l : List: Type ?u.222 → Type ?u.222
List (Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec)) :=
  l: List (Traced.TracedThread spec)
l.foldl: {α : Type ?u.231} → {β : Type ?u.230} → (α → β → α) → α → List β → α
foldl (λ env_r: ?m.240
env_r thread: ?m.243
thread => env_r: ?m.240
env_r + thread: ?m.243
thread.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation) start: ?m.219
start 

protected theorem sum_reservations.helper: ∀ {spec : Spec} (head : Traced.TracedThread spec) (l : List (Traced.TracedThread spec)),
  sum_reservations (head :: l) = head.reservation + sum_reservations l
sum_reservations.helper (head: Traced.TracedThread spec
head : Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec) (l: List (Traced.TracedThread spec)
l) :
  sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations (head: Traced.TracedThread spec
head :: l: ?m.415
l) = head: Traced.TracedThread spec
head.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation + sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations l: ?m.415
l :=by
  spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations lhave : ∀ l: List (Traced.TracedThread spec)
l : List: Type ?u.1679 → Type ?u.1679
List (Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec),
    sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations l: List (Traced.TracedThread spec)
l = sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty l: List (Traced.TracedThread spec)
l :=fun _: ?m.1691
_ => rfl: ∀ {α : Sort ?u.1693} {a : α}, a = a
rflspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

this: ∀ (l : List (Traced.TracedThread spec)), sum_reservations l = Mt.System.Traced.sum_reservations' IsReservation.empty l

sum_reservations (head :: l) = head.reservation + sum_reservations l
  spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations lsimp only [this: ∀ (l : List (Traced.TracedThread spec)), sum_reservations l = Mt.System.Traced.sum_reservations' IsReservation.empty l
this]spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

this: ∀ (l : List (Traced.TracedThread spec)), sum_reservations l = Mt.System.Traced.sum_reservations' IsReservation.empty l

Mt.System.Traced.sum_reservations' IsReservation.empty (head :: l) =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations l;spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

this: ∀ (l : List (Traced.TracedThread spec)), sum_reservations l = Mt.System.Traced.sum_reservations' IsReservation.empty l

Mt.System.Traced.sum_reservations' IsReservation.empty (head :: l) =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations lclear this: ∀ (l : List (Traced.TracedThread spec)), sum_reservations l = Mt.System.Traced.sum_reservations' IsReservation.empty l
thisspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' IsReservation.empty (head :: l) =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l
  spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations lsimp only [add: ∀ (r : spec.Reservation) (head : Traced.TracedThread spec) (tail : List (Traced.TracedThread spec)),
  Mt.System.Traced.sum_reservations' r (head :: tail) = Mt.System.Traced.sum_reservations' (r + head.reservation) tail
add, IsReservation.empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
IsReservation.empty_add]spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' head.reservation l =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l
  spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

sum_reservations (head :: l) = head.reservation + sum_reservations lrw [spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' head.reservation l =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty lassoc: ∀ (r : spec.Reservation) (l : List (Traced.TracedThread spec)),
  Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty l
assocspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l =   head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty l]
Goals accomplished! 🐙
where
  add: ∀ (r : spec.Reservation) (head : Traced.TracedThread spec) (tail : List (Traced.TracedThread spec)),
  Mt.System.Traced.sum_reservations' r (head :: tail) = Mt.System.Traced.sum_reservations' (r + head.reservation) tail
add (r: spec.Reservation
r) (head: Traced.TracedThread spec
head : Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec) (tail: List (Traced.TracedThread spec)
tail)
    : sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' r: ?m.474
r (head: Traced.TracedThread spec
head::tail: ?m.479
tail) = sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' (r: ?m.474
r + head: Traced.TracedThread spec
head.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation) tail: ?m.479
tail :=by
    spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' r (head :: tail) = Mt.System.Traced.sum_reservations' (r + head.reservation) tailsimp only [sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations', List.foldl: {α : Type ?u.825} → {β : Type ?u.824} → (α → β → α) → α → List β → α
List.foldl]
Goals accomplished! 🐙

  assoc: ∀ (r : spec.Reservation) (l : List (Traced.TracedThread spec)),
  Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty l
assoc (r: spec.Reservation
r : spec: Spec
spec.Reservation: Spec → Type
Reservation) (l: List (Traced.TracedThread spec)
l)
    : sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' r: spec.Reservation
r l: ?m.740
l = r: spec.Reservation
r + sum_reservations': {spec : Spec} → spec.Reservation → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations' IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty l: ?m.740
l :=by
    spec: Spec

head: Traced.TracedThread spec

l✝: List (Traced.TracedThread spec)

r: spec.Reservation

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty lrevert r: spec.Reservation
rspec: Spec

head: Traced.TracedThread spec

l✝, l: List (Traced.TracedThread spec)

∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty l
    spec: Spec

head: Traced.TracedThread spec

l✝: List (Traced.TracedThread spec)

r: spec.Reservation

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty linduction l: List (Traced.TracedThread spec)
lspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

nil∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty []
spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)
    spec: Spec

head: Traced.TracedThread spec

l✝: List (Traced.TracedThread spec)

r: spec.Reservation

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty l.spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

nil∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty [] spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

nil∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty []
spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)intro r: spec.Reservation
rspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilMt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty []
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

nil∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty []
spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)show r: spec.Reservation
r = r: spec.Reservation
r + IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.emptyspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilr = r + IsReservation.empty
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

nil∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r [] = r + Mt.System.Traced.sum_reservations' IsReservation.empty []
spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)rw [spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilr = r + IsReservation.emptyIsReservation.toIsCommutative: {T : Type} → [self : IsReservation T] → Lean.IsCommutative HAdd.hAdd
IsReservation.toIsCommutative.comm: ∀ {α : Sort ?u.1526} {op : α → α → α} [self : Lean.IsCommutative op] (a b : α), op a b = op b a
comm,spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilr = IsReservation.empty + r spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilr = r + IsReservation.emptyIsReservation.empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
IsReservation.empty_addspec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

r: spec.Reservation

nilr = r]
Goals accomplished! 🐙
    spec: Spec

head: Traced.TracedThread spec

l✝: List (Traced.TracedThread spec)

r: spec.Reservation

l: List (Traced.TracedThread spec)

Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' IsReservation.empty l.spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝) spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)rename_i head: ?m.1409
head tail: List ?m.1409
tail IH: ?m.1410 tail
IHspec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head :: tail) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head :: tail)
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)intro r: spec.Reservation
rspec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consMt.System.Traced.sum_reservations' r (head :: tail) =   r + Mt.System.Traced.sum_reservations' IsReservation.empty (head :: tail)
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)simp only [add: ∀ (r : spec.Reservation) (head : Traced.TracedThread spec) (tail : List (Traced.TracedThread spec)),
  Mt.System.Traced.sum_reservations' r (head :: tail) = Mt.System.Traced.sum_reservations' (r + head.reservation) tail
add]spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consMt.System.Traced.sum_reservations' (r + head.reservation) tail =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tail
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)rw [spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consMt.System.Traced.sum_reservations' (r + head.reservation) tail =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tailIH: ?m.1410 tail
IH,spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tail spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consMt.System.Traced.sum_reservations' (r + head.reservation) tail =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tailIsReservation.toIsAssociative: {T : Type} → [self : IsReservation T] → Lean.IsAssociative HAdd.hAdd
IsReservation.toIsAssociative.assoc: ∀ {α : Sort ?u.1631} {op : α → α → α} [self : Lean.IsAssociative op] (a b c : α), op (op a b) c = op a (op b c)
assoc,spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail) =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tail spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consMt.System.Traced.sum_reservations' (r + head.reservation) tail =   r + Mt.System.Traced.sum_reservations' (IsReservation.empty + head.reservation) tailIsReservation.empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
IsReservation.empty_addspec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail) =   r + Mt.System.Traced.sum_reservations' head.reservation tail]spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail) =   r + Mt.System.Traced.sum_reservations' head.reservation tail
      spec: Spec

head: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r (head✝ :: tail✝) =     r + Mt.System.Traced.sum_reservations' IsReservation.empty (head✝ :: tail✝)rw [spec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail) =   r + Mt.System.Traced.sum_reservations' head.reservation tailIH: ?m.1410 tail
IH head: ?m.1409
head.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservationspec: Spec

head✝: Traced.TracedThread spec

l: List (Traced.TracedThread spec)

head: Traced.TracedThread spec

tail: List (Traced.TracedThread spec)

IH: ∀ (r : spec.Reservation),
  Mt.System.Traced.sum_reservations' r tail = r + Mt.System.Traced.sum_reservations' IsReservation.empty tail

r: spec.Reservation

consr + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail) =   r + (head.reservation + Mt.System.Traced.sum_reservations' IsReservation.empty tail)]
Goals accomplished! 🐙

protected theorem decompose_reservation: ∀ (l : List (Traced.TracedThread spec)) (idx : Fin (List.length l)) (t : Traced.TracedThread spec),
  t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation
decompose_reservation (l: List (Traced.TracedThread spec)
l : List: Type ?u.1948 → Type ?u.1948
List (Traced.TracedThread: Spec → Type 1
Traced.TracedThread spec: Spec
spec)) (idx: Fin (List.length l)
idx : Fin: Nat → Type
Fin l: List (Traced.TracedThread spec)
l.length: {α : Type ?u.1951} → List α → Nat
length) t: ?m.1958
t :
  t: ?m.1958
t = l: List (Traced.TracedThread spec)
l.get: {α : Type ?u.1963} → (as : List α) → Fin (List.length as) → α
get idx: Fin (List.length l)
idx →
  sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations l: List (Traced.TracedThread spec)
l = sum_reservations: {spec : Spec} → List (Traced.TracedThread spec) → spec.Reservation
sum_reservations (l: List (Traced.TracedThread spec)
l.eraseIdx: {α : Type ?u.1978} → List α → Nat → List α
eraseIdx idx: Fin (List.length l)
idx.val: {n : Nat} → Fin n → Nat
val) + t: ?m.1958
t.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation :=by
  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationintro t_def: t = List.get l idx
t_defspec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation;spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationrw [spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationt_def: t = List.get l idx
t_defspec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + (List.get l idx).reservation]spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + (List.get l idx).reservation  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation;spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t_def: t = List.get l idx

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + (List.get l idx).reservation spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationclear t_def: t = List.get l idx
t_defspec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + (List.get l idx).reservation
  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationrevert idx: Fin (List.length l)
idxspec: Spec

l: List (Traced.TracedThread spec)

t: Traced.TracedThread spec

∀ (idx : Fin (List.length l)),
  sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + (List.get l idx).reservation

  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservationinduction l: List (Traced.TracedThread spec)
lspec: Spec

t: Traced.TracedThread spec

nil∀ (idx : Fin (List.length [])),
  sum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservation
  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation.spec: Spec

t: Traced.TracedThread spec

nil∀ (idx : Fin (List.length [])),
  sum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation spec: Spec

t: Traced.TracedThread spec

nil∀ (idx : Fin (List.length [])),
  sum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationintro idx: Fin (List.length [])
idxspec: Spec

t: Traced.TracedThread spec

idx: Fin (List.length [])

nilsum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
    spec: Spec

t: Traced.TracedThread spec

nil∀ (idx : Fin (List.length [])),
  sum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationhave : idx: Fin (List.length [])
idx.val: {n : Nat} → Fin n → Nat
val < 0: ?m.2079
0 :=idx: Fin (List.length [])
idx.isLt: ∀ {n : Nat} (self : Fin n), self.val < n
isLtspec: Spec

t: Traced.TracedThread spec

idx: Fin (List.length [])

this: idx.val < 0

nilsum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
    spec: Spec

t: Traced.TracedThread spec

nil∀ (idx : Fin (List.length [])),
  sum_reservations [] = sum_reservations (List.eraseIdx [] idx.val) + (List.get [] idx).reservation
spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationcontradiction
Goals accomplished! 🐙
  spec: Spec

l: List (Traced.TracedThread spec)

idx: Fin (List.length l)

t: Traced.TracedThread spec

t = List.get l idx → sum_reservations l = sum_reservations (List.eraseIdx l idx.val) + t.reservation.spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservation spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationintro idx: Fin (List.length (head✝ :: tail✝))
idxspec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

idx: Fin (List.length (head✝ :: tail✝))

conssum_reservations (head✝ :: tail✝) =   sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservation
    spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationrename_i thread: ?m.2058
thread threads: List ?m.2058
threads IH: ?m.2059 threads
IHspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

conssum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) idx.val) + (List.get (thread :: threads) idx).reservation
    spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservationcases h : idx: Fin (List.length (thread :: threads))
idx.val: {n : Nat} → Fin n → Nat
valspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation
spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservation
    spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservation.spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation
spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationhave : idx: Fin (List.length (thread :: threads))
idx = Fin.mk: {n : Nat} → (val : Nat) → val < n → Fin n
Fin.mk 0: ?m.2250
0 (spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservationby spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

0 < List.length (thread :: threads)simp_arith
Goals accomplished! 🐙) :=Fin.eq_of_val_eq: ∀ {n : Nat} {i j : Fin n}, i.val = j.val → i = j
Fin.eq_of_val_eq h: idx.val = Nat.zero
hspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

this: idx =   { val := 0,
    isLt :=
      (_ :
        Nat.Linear.ExprCnstr.denote [List.length threads]
          { eq := false, lhs := Nat.Linear.Expr.add (Nat.Linear.Expr.num 0) (Nat.Linear.Expr.num 1),
            rhs := Nat.Linear.Expr.add (Nat.Linear.Expr.var 0) (Nat.Linear.Expr.num 1) }) }

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation
spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationsimp only [this: idx = { val := 0, isLt := ?m.2252 }
this, List.get: {α : Type ?u.2628} → (as : List α) → Fin (List.length as) → α
List.get, List.eraseIdx: {α : Type ?u.3337} → List α → Nat → List α
List.eraseIdx, sum_reservations.helper: ∀ {spec : Spec} (head : Traced.TracedThread spec) (l : List (Traced.TracedThread spec)),
  sum_reservations (head :: l) = head.reservation + sum_reservations l
sum_reservations.helper]spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

this: idx =   { val := 0,
    isLt :=
      (_ :
        Nat.Linear.ExprCnstr.denote [List.length threads]
          { eq := false, lhs := Nat.Linear.Expr.add (Nat.Linear.Expr.num 0) (Nat.Linear.Expr.num 1),
            rhs := Nat.Linear.Expr.add (Nat.Linear.Expr.var 0) (Nat.Linear.Expr.num 1) }) }

cons.zerothread.reservation + sum_reservations threads = sum_reservations threads + thread.reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

h: idx.val = Nat.zero

cons.zerosum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) Nat.zero) + (List.get (thread :: threads) idx).reservation
spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationexact IsReservation.toIsCommutative: {T : Type} → [self : IsReservation T] → Lean.IsCommutative HAdd.hAdd
IsReservation.toIsCommutative.comm: ∀ {α : Sort ?u.4156} {op : α → α → α} [self : Lean.IsCommutative op] (a b : α), op a b = op b a
comm _: ?m.4157
_ _: ?m.4157
_
Goals accomplished! 🐙
    spec: Spec

t, head✝: Traced.TracedThread spec

tail✝: List (Traced.TracedThread spec)

cons∀ (idx : Fin (List.length (head✝ :: tail✝))),
  sum_reservations (head✝ :: tail✝) =     sum_reservations (List.eraseIdx (head✝ :: tail✝) idx.val) + (List.get (head✝ :: tail✝) idx).reservation.spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservation spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationrename_i n: Nat
nspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n: Nat

h: idx.val = Nat.succ n

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n)) + (List.get (thread :: threads) idx).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationhave idx_ok: n + 1 < List.length (thread :: threads)
idx_ok : n: Nat
n + 1: ?m.4186
1 < (thread: ?m.2058
thread :: threads: List ?m.2058
threads).length: {α : Type ?u.4199} → List α → Nat
length :=calc
        n: Nat
n + 1: ?m.4253
1 = idx: Fin (List.length (thread :: threads))
idx.val: {n : Nat} → Fin n → Nat
val :=h: idx.val = Nat.succ n
h.symm: ∀ {α : Sort ?u.4288} {a b : α}, a = b → b = a
symm
        _: ?m.4299
_ < _: ?m.4302
_ :=idx: Fin (List.length (thread :: threads))
idx.isLt: ∀ {n : Nat} (self : Fin n), self.val < n
isLtspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n: Nat

h: idx.val = Nat.succ n

idx_ok: n + 1 < List.length (thread :: threads)

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n)) + (List.get (thread :: threads) idx).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationhave : idx: Fin (List.length (thread :: threads))
idx = Fin.mk: {n : Nat} → (val : Nat) → val < n → Fin n
Fin.mk (n: Nat
n + 1: ?m.4396
1) idx_ok: n + 1 < List.length (thread :: threads)
idx_ok :=Fin.eq_of_val_eq: ∀ {n : Nat} {i j : Fin n}, i.val = j.val → i = j
Fin.eq_of_val_eq h: idx.val = Nat.succ n
hspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n: Nat

h: idx.val = Nat.succ n

idx_ok: n + 1 < List.length (thread :: threads)

this: idx = { val := n + 1, isLt := idx_ok }

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n)) + (List.get (thread :: threads) idx).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationsimp only [this: idx = { val := n + 1, isLt := idx_ok }
this, List.get: {α : Type ?u.4444} → (as : List α) → Fin (List.length as) → α
List.get, List.eraseIdx: {α : Type ?u.4470} → List α → Nat → List α
List.eraseIdx, sum_reservations.helper: ∀ {spec : Spec} (head : Traced.TracedThread spec) (l : List (Traced.TracedThread spec)),
  sum_reservations (head :: l) = head.reservation + sum_reservations l
sum_reservations.helper]spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n: Nat

h: idx.val = Nat.succ n

idx_ok: n + 1 < List.length (thread :: threads)

this: idx = { val := n + 1, isLt := idx_ok }

cons.succthread.reservation + sum_reservations threads =   thread.reservation + sum_reservations (List.eraseIdx threads n) +     (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationclear this: idx = { val := n + 1, isLt := idx_ok }
this h: idx.val = Nat.succ n
h idx: Fin (List.length (thread :: threads))
idxspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

n: Nat

idx_ok: n + 1 < List.length (thread :: threads)

cons.succthread.reservation + sum_reservations threads =   thread.reservation + sum_reservations (List.eraseIdx threads n) +     (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationrw [spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

n: Nat

idx_ok: n + 1 < List.length (thread :: threads)

cons.succthread.reservation + sum_reservations threads =   thread.reservation + sum_reservations (List.eraseIdx threads n) +     (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservationIsReservation.toIsAssociative: {T : Type} → [self : IsReservation T] → Lean.IsAssociative HAdd.hAdd
IsReservation.toIsAssociative.assoc: ∀ {α : Sort ?u.4588} {op : α → α → α} [self : Lean.IsAssociative op] (a b c : α), op (op a b) c = op a (op b c)
assocspec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

n: Nat

idx_ok: n + 1 < List.length (thread :: threads)

cons.succthread.reservation + sum_reservations threads =   thread.reservation +     (sum_reservations (List.eraseIdx threads n) +       (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservation)]spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

n: Nat

idx_ok: n + 1 < List.length (thread :: threads)

cons.succthread.reservation + sum_reservations threads =   thread.reservation +     (sum_reservations (List.eraseIdx threads n) +       (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservation)
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationapply congrArg: ∀ {α : Sort ?u.4612} {β : Sort ?u.4611} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg (thread: ?m.2058
thread.reservation: {spec : Spec} → Traced.TracedThread spec → spec.Reservation
reservation + .)spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

n: Nat

idx_ok: n + 1 < List.length (thread :: threads)

cons.succsum_reservations threads =   sum_reservations (List.eraseIdx threads n) +     (List.get threads { val := n, isLt := (_ : Nat.succ n ≤ List.length threads) }).reservation
      spec: Spec

t, thread: Traced.TracedThread spec

threads: List (Traced.TracedThread spec)

IH: ∀ (idx : Fin (List.length threads)),
  sum_reservations threads = sum_reservations (List.eraseIdx threads idx.val) + (List.get threads idx).reservation

idx: Fin (List.length (thread :: threads))

n✝: Nat

h: idx.val = Nat.succ n✝

cons.succsum_reservations (thread :: threads) =   sum_reservations (List.eraseIdx (thread :: threads) (Nat.succ n✝)) + (List.get (thread :: threads) idx).reservationexact IH: ?m.2059 threads
IH <| Fin.mk: {n : Nat} → (val : Nat) → val < n → Fin n
Fin.mk n: Nat
n (Nat.le_of_succ_le_succ: ∀ {n m : Nat}, Nat.succ n ≤ Nat.succ m → n ≤ m
Nat.le_of_succ_le_succ idx_ok: n + 1 < List.length (thread :: threads)
idx_ok)
Goals accomplished! 🐙
  
end Mt.System.Traced