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

namespace Mt.Traced

structure TracedSystem: Spec → Type 1
TracedSystem (spec: Spec
spec : Spec: Type 1
Spec) where
  state: {spec : Spec} → TracedSystem spec → spec.State
state   : spec: Spec
spec.State: Spec → Type
State
  threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads : List: Type ?u.8 → Type ?u.8
List (TracedThread: Spec → Type 1
TracedThread spec: Spec
spec)

namespace TracedSystem

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 ThreadIndex: TracedSystem spec → Type
ThreadIndex (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) : Type: Type 1
Type :=Fin: Nat → Type
Fin s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.length: {α : Type ?u.410} → List α → Nat
length
def done: TracedSystem spec → Bool
done (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) : Bool: Type
Bool :=s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.length: {α : Type ?u.429} → List α → Nat
length = 0: ?m.435
0

def iterate: (s : TracedSystem spec) → ThreadIndex s → Thread.IterationResult spec
iterate (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) (idx: ThreadIndex s
idx : s: TracedSystem spec
s.ThreadIndex: {spec : Spec} → TracedSystem spec → Type
ThreadIndex) : Thread.IterationResult: Spec → Type 1
Thread.IterationResult spec: Spec
spec :=
  (s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.get: {α : Type ?u.537} → (as : List α) → Fin (List.length as) → α
get idx: ThreadIndex s
idx).iterate: {spec : Spec} → TracedThread spec → spec.State → Thread.IterationResult spec
iterate s: TracedSystem spec
s.state: {spec : Spec} → TracedSystem spec → spec.State
state

def update_thread: TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) (idx: Nat
idx : Nat: Type
Nat) (state: spec.State
state : spec: Spec
spec.State: Spec → Type
State)
  (r: spec.Reservation
r : spec: Spec
spec.Reservation: Spec → Type
Reservation) (cont: Thread spec
cont : Thread: Spec → Type 1
Thread spec: Spec
spec) : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec :={
  state: spec.State
state
  threads :=s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.set: {α : Type ?u.601} → List α → Nat → α → List α
set idx: Nat
idx ⟨cont: Thread spec
cont, r: spec.Reservation
r⟩
}

def remove_thread: TracedSystem spec → Nat → spec.State → TracedSystem spec
remove_thread (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) (idx: Nat
idx : Nat: Type
Nat) (state: spec.State
state : spec: Spec
spec.State: Spec → Type
State)
  : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec :={
  state: spec.State
state
  threads :=s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.eraseIdx: {α : Type ?u.686} → List α → Nat → List α
eraseIdx idx: Nat
idx
}

def reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
reservations (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) : spec: Spec
spec.Reservation: Spec → Type
Reservation :=
  s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.foldl: {α : Type ?u.739} → {β : Type ?u.738} → (α → β → α) → α → List β → α
foldl (λ env_r: ?m.748
env_r thread: ?m.751
thread => env_r: ?m.748
env_r + thread: ?m.751
thread.reservation: {spec : Spec} → 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

def other_reservations: TracedSystem spec → Nat → spec.Reservation
other_reservations (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) (idx: Nat
idx : Nat: Type
Nat) : spec: Spec
spec.Reservation: Spec → Type
Reservation :=
  (s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.eraseIdx: {α : Type ?u.931} → List α → Nat → List α
eraseIdx idx: Nat
idx).foldl: {α : Type ?u.938} → {β : Type ?u.937} → (α → β → α) → α → List β → α
foldl (λ env_r: ?m.947
env_r thread: ?m.950
thread => env_r: ?m.947
env_r + thread: ?m.950
thread.reservation: {spec : Spec} → 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

theorem decompose_reservations: ∀ (s : TracedSystem spec) (idx : ThreadIndex s),
  reservations s = other_reservations s idx.val + (List.get s.threads idx).reservation
decompose_reservations (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) (idx: ThreadIndex s
idx : s: TracedSystem spec
s.ThreadIndex: {spec : Spec} → TracedSystem spec → Type
ThreadIndex) :
  s: TracedSystem spec
s.reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
reservations = s: TracedSystem spec
s.other_reservations: {spec : Spec} → TracedSystem spec → Nat → spec.Reservation
other_reservations idx: ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val + (s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.get: {α : Type ?u.1100} → (as : List α) → Fin (List.length as) → α
get idx: ThreadIndex s
idx).reservation: {spec : Spec} → TracedThread spec → spec.Reservation
reservation :=
  System.Traced.decompose_reservation: ∀ {spec : Spec} (l : List (TracedThread spec)) (idx : Fin (List.length l)) (t : TracedThread spec),
  t = List.get l idx →
    System.Traced.sum_reservations l = System.Traced.sum_reservations (List.eraseIdx l idx.val) + t.reservation
System.Traced.decompose_reservation s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads idx: ThreadIndex s
idx _: TracedThread ?m.1152
_ rfl: ∀ {α : Sort ?u.1181} {a : α}, a = a
rfl

structure valid: {spec : Spec} → TracedSystem spec → Prop
valid (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) : Prop: Type
Prop where
  currently_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → Spec.validate spec (reservations s) s.state
currently_valid : spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate s: TracedSystem spec
s.reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
reservations s: TracedSystem spec
s.state: {spec : Spec} → TracedSystem spec → spec.State
state
  threads_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → ∀ (t : TracedThread spec), t ∈ s.threads → TracedThread.valid t
threads_valid : ∀ t: ?m.1214
t, t: ?m.1214
t ∈ s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads → t: ?m.1214
t.valid: {spec : Spec} → TracedThread spec → Prop
valid 

def to_system: TracedSystem spec → System spec
to_system (s: TracedSystem spec
s : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec) : System: Spec → Type 1
System spec: Spec
spec :={
  state := s: TracedSystem spec
s.state: {spec : Spec} → TracedSystem spec → spec.State
state
  threads := s: TracedSystem spec
s.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.map: {α : Type ?u.1263} → {β : Type ?u.1262} → (α → β) → List α → List β
map λ ⟨t: Thread spec
t, _⟩ => t: Thread spec
t
  panics := 0: ?m.1279
0
}

def mk_initial: System spec → TracedSystem spec
mk_initial (s: System spec
s : System: Spec → Type 1
System spec: Spec
spec) : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec :={
  state := s: System spec
s.state: {spec : Spec} → System spec → spec.State
state
  threads := s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads.map: {α : Type ?u.1484} → {β : Type ?u.1483} → (α → β) → List α → List β
map λ t: ?m.1493
t => ⟨t: ?m.1493
t, IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty⟩
}

theorem mk_initial.valid: ∀ {spec : Spec} (s : System spec),
  Spec.validate spec IsReservation.empty s.state →
    (∀ (t : Thread spec), t ∈ s.threads → Thread.valid t) → TracedSystem.valid (mk_initial s)
mk_initial.valid (s: System spec
s : System: Spec → Type 1
System spec: Spec
spec)
  (initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid : spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty s: System spec
s.state: {spec : Spec} → System spec → spec.State
state)
  (threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t
threads_valid : ∀ t: ?m.1583
t, t: ?m.1583
t ∈ s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads → t: ?m.1583
t.valid: {spec : Spec} → Thread spec → Prop
valid)
  : (mk_initial: {spec : Spec} → System spec → TracedSystem spec
mk_initial s: System spec
s).valid: {spec : Spec} → TracedSystem spec → Prop
valid :=by
  spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

TracedSystem.valid (mk_initial s)constructorspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid t
  spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

TracedSystem.valid (mk_initial s).spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid tsimp only [mk_initial: {spec : Spec} → System spec → TracedSystem spec
mk_initial]spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads })
  s.state
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid tinduction s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threadsspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_valid.nilSpec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) [] })
  s.state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.state
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid t.spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_valid.nilSpec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) [] })
  s.state spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_valid.nilSpec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) [] })
  s.state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.stateexact initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid
Goals accomplished! 🐙
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

currently_validSpec.validate spec (reservations (mk_initial s)) (mk_initial s).state
spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid t.spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.state spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.staterename_i head: ?m.1750
head tail: List ?m.1750
tail IH: ?m.1751 tail
IHspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head: Thread spec

tail: List (Thread spec)

IH: Spec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail })
  s.state

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head :: tail) })
  s.state
      spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.statesimp only [List.map: {α : Type ?u.1803} → {β : Type ?u.1802} → (α → β) → List α → List β
List.map, Traced.TracedSystem.reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
Traced.TracedSystem.reservations, List.foldl: {α : Type ?u.2099} → {β : Type ?u.2098} → (α → β → α) → α → List β → α
List.foldl, IsReservation.empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
IsReservation.empty_add]spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head: Thread spec

tail: List (Thread spec)

IH: Spec.validate spec
  (reservations
    { state := s.state, threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail })
  s.state

currently_valid.consSpec.validate spec
  (List.foldl (fun env_r thread => env_r + thread.reservation) IsReservation.empty
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail))
  s.state
      spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

head✝: Thread spec

tail✝: List (Thread spec)

currently_valid.consSpec.validate spec
  (reservations
    { state := s.state,
      threads := List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝) })
  s.stateexact IH: ?m.1751 tail
IH
Goals accomplished! 🐙
  spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

TracedSystem.valid (mk_initial s).spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid t spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid tintro t: TracedThread ?spec
t t_hyp: t ∈ ?s.threads
t_hypspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ (mk_initial s).threads

threads_validTracedThread.valid t
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid tsimp only [mk_initial: {spec : Spec} → System spec → TracedSystem spec
mk_initial] at t_hyp: t ∈ ?s.threads
t_hypspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

threads_validTracedThread.valid t
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid tcases Utils.List.eq_of_in_map: ∀ {U V : Type ?u.2831} {f : U → V} {l : List U} {v : V}, v ∈ List.map f l → ∃ u, u ∈ l ∧ v = f u
Utils.List.eq_of_in_map t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads
t_hypspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

w✝: Thread spec

threads_valid.introTracedThread.valid t
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid trename_i t_orig: ?m.2878
t_orig t_orig_hyp: ?m.2879 t_orig
t_orig_hypspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

t_orig: Thread spec

t_orig_hyp: t_orig ∈ s.threads ∧ t = { thread := t_orig, reservation := IsReservation.empty }

threads_valid.introTracedThread.valid t
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid trw [spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

t_orig: Thread spec

t_orig_hyp: t_orig ∈ s.threads ∧ t = { thread := t_orig, reservation := IsReservation.empty }

threads_valid.introTracedThread.valid tt_orig_hyp: ?m.2879 t_orig
t_orig_hyp.right: ∀ {a b : Prop}, a ∧ b → b
rightspec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

t_orig: Thread spec

t_orig_hyp: t_orig ∈ s.threads ∧ t = { thread := t_orig, reservation := IsReservation.empty }

threads_valid.introTracedThread.valid { thread := t_orig, reservation := IsReservation.empty }]spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

t: TracedThread spec

t_hyp: t ∈ List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads

t_orig: Thread spec

t_orig_hyp: t_orig ∈ s.threads ∧ t = { thread := t_orig, reservation := IsReservation.empty }

threads_valid.introTracedThread.valid { thread := t_orig, reservation := IsReservation.empty }
    spec: Spec

s: System spec

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

threads_valid∀ (t : TracedThread spec), t ∈ (mk_initial s).threads → TracedThread.valid texact threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t
threads_valid t_orig: ?m.2878
t_orig t_orig_hyp: ?m.2879 t_orig
t_orig_hyp.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙

theorem mk_initial.cancels_to_system: ∀ {spec : Spec} {s : System spec}, s.panics = 0 → to_system (mk_initial s) = s
mk_initial.cancels_to_system {s: System spec
s : System: Spec → Type 1
System spec: Spec
spec}
  (no_panics_yet: s.panics = 0
no_panics_yet : s: System spec
s.panics: {spec : Spec} → System spec → Nat
panics = 0: ?m.2978
0)
  :
  (mk_initial: {spec : Spec} → System spec → TracedSystem spec
mk_initial s: System spec
s).to_system: {spec : Spec} → TracedSystem spec → System spec
to_system = s: System spec
s :=by
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = ssimp only [mk_initial: {spec : Spec} → System spec → TracedSystem spec
mk_initial, to_system: {spec : Spec} → TracedSystem spec → System spec
to_system]spec: Spec

s: System spec

no_panics_yet: s.panics = 0

{ state := s.state,
    threads :=
      List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads),
    panics := 0 } =   s
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = srw [spec: Spec

s: System spec

no_panics_yet: s.panics = 0

{ state := s.state,
    threads :=
      List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads),
    panics := 0 } =   sSystem.mk.injEq: ∀ {spec : Spec} (state : spec.State) (threads : List (Thread spec)) (panics : Nat) (state_1 : spec.State)
  (threads_1 : List (Thread spec)) (panics_1 : Nat),
  ({ state := state, threads := threads, panics := panics } =       { state := state_1, threads := threads_1, panics := panics_1 }) =     (state = state_1 ∧ threads = threads_1 ∧ panics = panics_1)
System.mk.injEqspec: Spec

s: System spec

no_panics_yet: s.panics = 0

s.state = s.state ∧   List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =       s.threads ∧     0 = s.panics]spec: Spec

s: System spec

no_panics_yet: s.panics = 0

s.state = s.state ∧   List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =       s.threads ∧     0 = s.panics
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = sconstructorspec: Spec

s: System spec

no_panics_yet: s.panics = 0

lefts.state = s.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

rightList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =     s.threads ∧   0 = s.panics
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = s.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

lefts.state = s.state spec: Spec

s: System spec

no_panics_yet: s.panics = 0

lefts.state = s.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

rightList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =     s.threads ∧   0 = s.panicsrfl
Goals accomplished! 🐙
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = sconstructorspec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.leftList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =   s.threads
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panics
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = s.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.leftList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =   s.threads spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.leftList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =   s.threads
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panicsinduction s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threadsspec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.left.nilList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) []) = []
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.leftList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =   s.threads
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panics.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.left.nilList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) []) = [] spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.left.nilList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) []) = []
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝rfl
Goals accomplished! 🐙
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.leftList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) s.threads) =   s.threads
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panics.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝ spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝rename_i head: ?m.3201
head tail: List ?m.3201
tail IH: ?m.3202 tail
IHspec: Spec

s: System spec

no_panics_yet: s.panics = 0

head: Thread spec

tail: List (Thread spec)

IH: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) = tail

right.left.consList.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head :: tail)) =   head :: tail
      spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝simp only [List.map: {α : Type ?u.3231} → {β : Type ?u.3230} → (α → β) → List α → List β
List.map]spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head: Thread spec

tail: List (Thread spec)

IH: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) = tail

right.left.conshead :: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) =   head :: tail
      spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head✝: Thread spec

tail✝: List (Thread spec)

right.left.consList.map (fun x => x.thread)
    (List.map (fun t => { thread := t, reservation := IsReservation.empty }) (head✝ :: tail✝)) =   head✝ :: tail✝rw [spec: Spec

s: System spec

no_panics_yet: s.panics = 0

head: Thread spec

tail: List (Thread spec)

IH: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) = tail

right.left.conshead :: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) =   head :: tailIH: ?m.3202 tail
IHspec: Spec

s: System spec

no_panics_yet: s.panics = 0

head: Thread spec

tail: List (Thread spec)

IH: List.map (fun x => x.thread) (List.map (fun t => { thread := t, reservation := IsReservation.empty }) tail) = tail

right.left.conshead :: tail = head :: tail]
Goals accomplished! 🐙
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

to_system (mk_initial s) = s.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panics spec: Spec

s: System spec

no_panics_yet: s.panics = 0

right.right0 = s.panicsexact no_panics_yet: s.panics = 0
no_panics_yet.symm: ∀ {α : Sort ?u.3302} {a b : α}, a = b → b = a
symm
Goals accomplished! 🐙

theorem valid_by_iteration: ∀ (s s' : System spec) {idx : System.ThreadIndex s} {ts : TracedSystem spec},
  s = to_system ts → valid ts → System.iterate s idx = s' → ∃ ts', to_system ts' = s' ∧ valid ts'
valid_by_iteration (s: System spec
s s': System spec
s' : System: Spec → Type 1
System spec: Spec
spec)
  {idx: System.ThreadIndex s
idx : s: System spec
s.ThreadIndex: {spec : Spec} → System spec → Type
ThreadIndex}
  {ts: TracedSystem spec
ts : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec}
  (has_traced_system: s = to_system ts
has_traced_system : s: System spec
s = ts: TracedSystem spec
ts.to_system: {spec : Spec} → TracedSystem spec → System spec
to_system)
  (ts_valid: valid ts
ts_valid : ts: TracedSystem spec
ts.valid: {spec : Spec} → TracedSystem spec → Prop
valid)
  (iteration: System.iterate s idx = s'
iteration : s: System spec
s.iterate: {spec : Spec} → (s : System spec) → System.ThreadIndex s → System spec
iterate idx: System.ThreadIndex s
idx = s': System spec
s')
  : ∃ ts': TracedSystem spec
ts' : TracedSystem: Spec → Type 1
TracedSystem spec: Spec
spec,
    ts': TracedSystem spec
ts'.to_system: {spec : Spec} → TracedSystem spec → System spec
to_system = s': System spec
s' ∧ ts': TracedSystem spec
ts'.valid: {spec : Spec} → TracedSystem spec → Prop
valid :=by
  
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'simp only [System.iterate: {spec : Spec} → (s : System spec) → System.ThreadIndex s → System spec
System.iterate] at iteration: System.iterate s idx = s'
iterationspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'cases blocked_until : (s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads.get: {α : Type ?u.4019} → (as : List α) → Fin (List.length as) → α
get idx: System.ThreadIndex s
idx).block_until: {spec : Spec} → Thread spec → spec.State → Bool
block_until s: System spec
s.state: {spec : Spec} → System spec → spec.State
statespec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

false∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

true∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

∃ ts', to_system ts' = s' ∧ valid ts'<;>spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

false∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

true∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'

∃ ts', to_system ts' = s' ∧ valid ts'simp only [blocked_until: Thread.block_until (List.get s.threads idx) s.state = false
blocked_until, ite_true: ∀ {α : Sort ?u.4435} (a b : α), (if True then a else b) = a
ite_true, ite_false: ∀ {α : Sort ?u.4443} (a b : α), (if False then a else b) = b
ite_false] at iteration: (if Thread.block_until (List.get s.threads idx) s.state = true then
    match Thread.iterate (List.get s.threads idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }
  else s) =   s'
iterationspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

iteration: s = s'

false∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

iteration: s = s'

false∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

iteration: s = s'

false∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

true∃ ts', to_system ts' = s' ∧ valid ts'exists ts: TracedSystem spec
tsspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

iteration: s = s'

falseto_system ts = s' ∧ valid ts
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = false

iteration: s = s'

false∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

true∃ ts', to_system ts' = s' ∧ valid ts'simp only [<- iteration: s = s'
iteration, has_traced_system: s = to_system ts
has_traced_system, ts_valid: valid ts
ts_valid]
Goals accomplished! 🐙
  
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'have ts_state_eq: ts.state = s.state
ts_state_eq : ts: TracedSystem spec
ts.state: {spec : Spec} → TracedSystem spec → spec.State
state = s: System spec
s.state: {spec : Spec} → System spec → spec.State
state :=spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

true∃ ts', to_system ts' = s' ∧ valid ts'by spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = s.staterw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = s.statehas_traced_system: s = to_system ts
has_traced_systemspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = (to_system ts).state]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = (to_system ts).state spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = s.state;spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = (to_system ts).state spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts.state = s.staterfl
Goals accomplished! 🐙

  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'let idx': ThreadIndex ts
idx' : ts: TracedSystem spec
ts.ThreadIndex: {spec : Spec} → TracedSystem spec → Type
ThreadIndex :=Utils.Fin.cast: {n m : Nat} → Fin n → n = m → Fin m
Utils.Fin.cast idx: System.ThreadIndex s
idx (spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

true∃ ts', to_system ts' = s' ∧ valid ts'by
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

List.length s.threads = List.length ts.threadsrw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

List.length s.threads = List.length ts.threadshas_traced_system: s = to_system ts
has_traced_systemspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

List.length (to_system ts).threads = List.length ts.threads]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

List.length (to_system ts).threads = List.length ts.threads
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

List.length s.threads = List.length ts.threadsexact List.length_map: ∀ {α : Type ?u.4910} {β : Type ?u.4909} (as : List α) (f : α → β), List.length (List.map f as) = List.length as
List.length_map ..
Goals accomplished! 🐙)spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

true∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'have get_idx': (List.get ts.threads idx').thread = List.get s.threads idx
get_idx' : (ts: TracedSystem spec
ts.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.get: {α : Type ?u.4949} → (as : List α) → Fin (List.length as) → α
get idx': ThreadIndex ts
idx').thread: {spec : Spec} → TracedThread spec → Thread spec
thread = s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads.get: {α : Type ?u.4957} → (as : List α) → Fin (List.length as) → α
get idx: System.ThreadIndex s
idx :=spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

true∃ ts', to_system ts' = s' ∧ valid ts'by
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

(List.get ts.threads idx').thread = List.get s.threads idxhave :=congrArg: ∀ {α : Sort ?u.4970} {β : Sort ?u.4969} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg System.threads: {spec : Spec} → System spec → List (Thread spec)
System.threads has_traced_system: s = to_system ts
has_traced_systemspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

this: s.threads = (to_system ts).threads

(List.get ts.threads idx').thread = List.get s.threads idx
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

(List.get ts.threads idx').thread = List.get s.threads idxrw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

this: s.threads = (to_system ts).threads

(List.get ts.threads idx').thread = List.get s.threads idxUtils.List.get_congr: ∀ {T : Type ?u.4983} {l l' : List T} (idx : Fin (List.length l)) (eq : l = l'),
  List.get l idx = List.get l' (Utils.Fin.cast idx (_ : List.length l = List.length l'))
Utils.List.get_congr idx: System.ThreadIndex s
idx this: ?m.4968
thisspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

this: s.threads = (to_system ts).threads

(List.get ts.threads idx').thread =   List.get (to_system ts).threads (Utils.Fin.cast idx (_ : List.length s.threads = List.length (to_system ts).threads))]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

this: s.threads = (to_system ts).threads

(List.get ts.threads idx').thread =   List.get (to_system ts).threads (Utils.Fin.cast idx (_ : List.length s.threads = List.length (to_system ts).threads))
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

(List.get ts.threads idx').thread = List.get s.threads idxsimp only [to_system: {spec : Spec} → TracedSystem spec → System spec
to_system, Utils.List.get_of_map: ∀ {U V : Type ?u.4997} {f : U → V} {l : List U} {idx : Fin (List.length (List.map f l))},
  List.get (List.map f l) idx = f (List.get l (Utils.Fin.cast idx (_ : List.length (List.map f l) = List.length l)))
Utils.List.get_of_map]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

this: s.threads = (to_system ts).threads

(List.get ts.threads (Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads))).thread =   (List.get ts.threads
      (Utils.Fin.cast (Utils.Fin.cast idx (_ : List.length s.threads = List.length (to_system ts).threads))
        (_ : List.length (List.map (fun x => x.thread) ts.threads) = List.length ts.threads))).thread
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

(List.get ts.threads idx').thread = List.get s.threads idxrfl
Goals accomplished! 🐙
  
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'let env_r: ?m.5181
env_r :=ts: TracedSystem spec
ts.other_reservations: {spec : Spec} → TracedSystem spec → Nat → spec.Reservation
other_reservations idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
valspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

true∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'have decompose: reservations ts = env_r + ?m.5201
decompose : ts: TracedSystem spec
ts.reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
reservations = env_r: ?m.5181
env_r + _: ?m.5200
_ :=ts: TracedSystem spec
ts.decompose_reservations: ∀ {spec : Spec} (s : TracedSystem spec) (idx : ThreadIndex s),
  reservations s = other_reservations s idx.val + (List.get s.threads idx).reservation
decompose_reservations idx': ThreadIndex ts
idx'spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

true∃ ts', to_system ts' = s' ∧ valid ts'

  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'have t_valid: ?m.5273
t_valid :=TracedThread.valid_elim: ∀ {spec : Spec} {thread : TracedThread spec},
  TracedThread.valid thread →
    ∀ (env_r : spec.Reservation) (s : spec.State),
      TracedThread.block_until thread s = true →
        Spec.validate spec (env_r + thread.reservation) s →
          ∃ r',
            let _discr := TracedThread.iterate thread s;
            match TracedThread.iterate thread s with
            | Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
            | Thread.IterationResult.Panic a => False
            | Thread.IterationResult.Running s' cont =>
              Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }
TracedThread.valid_elim
    (ts_valid: valid ts
ts_valid.threads_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → ∀ (t : TracedThread spec), t ∈ s.threads → TracedThread.valid t
threads_valid (ts: TracedSystem spec
ts.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.get: {α : Type ?u.5281} → (as : List α) → Fin (List.length as) → α
get idx': ThreadIndex ts
idx') (Utils.List.get_in: ∀ {T : Type ?u.5288} (l : List T) (idx : Fin (List.length l)), List.get l idx ∈ l
Utils.List.get_in ..))
    env_r: ?m.5181
env_r s: System spec
s.state: {spec : Spec} → System spec → spec.State
state
    (spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

true∃ ts', to_system ts' = s' ∧ valid ts'by
      spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

TracedThread.block_until (List.get ts.threads idx') s.state = truesimp only [TracedThread.block_until: {spec : Spec} → TracedThread spec → spec.State → Bool
TracedThread.block_until, get_idx': (List.get ts.threads idx').thread = List.get s.threads idx
get_idx']spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Thread.block_until (List.get s.threads idx) s.state = true
      spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

TracedThread.block_until (List.get ts.threads idx') s.state = trueexact blocked_until: Thread.block_until (List.get s.threads idx) s.state = true
blocked_until
Goals accomplished! 🐙)
    (spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

true∃ ts', to_system ts' = s' ∧ valid ts'by
      spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (env_r + (List.get ts.threads idx').reservation) s.staterw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (env_r + (List.get ts.threads idx').reservation) s.state<- decompose: reservations ts = env_r + (List.get ts.threads idx').reservation
decompose,spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (reservations ts) s.state spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (env_r + (List.get ts.threads idx').reservation) s.state<- ts_state_eq: ts.state = s.state
ts_state_eqspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (reservations ts) ts.state]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (reservations ts) ts.state
      spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

Spec.validate spec (env_r + (List.get ts.threads idx').reservation) s.stateexact ts_valid: valid ts
ts_valid.currently_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → Spec.validate spec (reservations s) s.state
currently_valid
Goals accomplished! 🐙)spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

t_valid: ∃ r',
  let _discr := TracedThread.iterate (List.get ts.threads idx') s.state;
  match TracedThread.iterate (List.get ts.threads idx') s.state with
  | Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
  | Thread.IterationResult.Panic a => False
  | Thread.IterationResult.Running s' cont =>
    Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'cases t_valid: ?m.5273
t_validspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

w✝: spec.Reservation

true.intro∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'rename_i r': ?m.5375
r' t_valid: ?m.5376 r'
t_validspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := TracedThread.iterate (List.get ts.threads idx') s.state;
match TracedThread.iterate (List.get ts.threads idx') s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'rw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := TracedThread.iterate (List.get ts.threads idx') s.state;
match TracedThread.iterate (List.get ts.threads idx') s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'TracedThread.iterate: {spec : Spec} → TracedThread spec → spec.State → Thread.IterationResult spec
TracedThread.iterate,spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get ts.threads idx').thread s.state;
match Thread.iterate (List.get ts.threads idx').thread s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := TracedThread.iterate (List.get ts.threads idx') s.state;
match TracedThread.iterate (List.get ts.threads idx') s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'get_idx': (List.get ts.threads idx').thread = List.get s.threads idx
get_idx'spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts']spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts' at t_valid: let _discr := Thread.iterate (List.get ts.threads idx').thread s.state;
match Thread.iterate (List.get ts.threads idx').thread s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }
t_validspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'

  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'cases h : (s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads.get: {α : Type ?u.5482} → (as : List α) → Fin (List.length as) → α
get idx: System.ThreadIndex s
idx).iterate: {spec : Spec} → Thread spec → spec.State → Thread.IterationResult spec
iterate s: System spec
s.state: {spec : Spec} → System spec → spec.State
statespec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Panic a✝

true.intro.Panic∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'<;>spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Panic a✝

true.intro.Panic∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro∃ ts', to_system ts' = s' ∧ valid ts'simp only [h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝
h] at iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'
iterationspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Panic a✝

true.intro.Panic∃ ts', to_system ts' = s' ∧ valid ts'<;>spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

iteration: (match Thread.iterate (List.get s.threads idx) s.state with
  | Thread.IterationResult.Done state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
  | Thread.IterationResult.Panic state =>
    { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics + 1 }
  | Thread.IterationResult.Running state thread =>
    { state := state, threads := List.set s.threads idx.val thread, panics := s.panics }) =   s'

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Panic a✝

true.intro.Panic∃ ts', to_system ts' = s' ∧ valid ts'simp only [h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Panic a✝
h] at t_valid: let _discr := Thread.iterate (List.get s.threads idx) s.state;
match Thread.iterate (List.get s.threads idx) s.state with
| Thread.IterationResult.Done s' => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| Thread.IterationResult.Panic a => False
| Thread.IterationResult.Running s' cont =>
  Spec.validate spec (env_r + r') s' ∧ TracedThread.valid { thread := cont, reservation := r' }
t_validspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'

  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'rename_i state: ?m.5522.State
statespec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'exists ts: TracedSystem spec
ts.remove_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → TracedSystem spec
remove_thread idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val state: ?m.5522.State
statespec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) = s' ∧ valid (remove_thread ts idx.val state)
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'rw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) = s' ∧ valid (remove_thread ts idx.val state)<- iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'
iterationspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) =     { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } ∧   valid (remove_thread ts idx.val state)]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) =     { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } ∧   valid (remove_thread ts idx.val state) spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts';spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) =     { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } ∧   valid (remove_thread ts idx.val state) spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'clear iteration: { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'
iteration s': System spec
s'spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system (remove_thread ts idx.val state) =     { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } ∧   valid (remove_thread ts idx.val state)
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'simp only [remove_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → TracedSystem spec
remove_thread]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Doneto_system { state := state, threads := List.eraseIdx ts.threads idx.val } =     { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } ∧   valid { state := state, threads := List.eraseIdx ts.threads idx.val }
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'constructorspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.leftto_system { state := state, threads := List.eraseIdx ts.threads idx.val } =   { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.leftto_system { state := state, threads := List.eraseIdx ts.threads idx.val } =   { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.leftto_system { state := state, threads := List.eraseIdx ts.threads idx.val } =   { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }simp only [to_system: {spec : Spec} → TracedSystem spec → System spec
to_system, has_traced_system: s = to_system ts
has_traced_system, System.mk.injEq: ∀ {spec : Spec} (state : spec.State) (threads : List (Thread spec)) (panics : Nat) (state_1 : spec.State)
  (threads_1 : List (Thread spec)) (panics_1 : Nat),
  ({ state := state, threads := threads, panics := panics } =       { state := state_1, threads := threads_1, panics := panics_1 }) =     (state = state_1 ∧ threads = threads_1 ∧ panics = panics_1)
System.mk.injEq, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.leftList.map (fun x => x.thread) (List.eraseIdx ts.threads idx.val) =   List.eraseIdx (List.map (fun x => x.thread) ts.threads) idx.val
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.leftto_system { state := state, threads := List.eraseIdx ts.threads idx.val } =   { state := state, threads := List.eraseIdx s.threads idx.val, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }exact Utils.List.erase_map_commutes: ∀ {U V : Type ?u.7798} (f : U → V) (l : List U) (idx : Nat),
  List.map f (List.eraseIdx l idx) = List.eraseIdx (List.map f l) idx
Utils.List.erase_map_commutes ..
Goals accomplished! 🐙
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done a✝

iteration: { state := a✝, threads := List.eraseIdx s.threads idx.val, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝ ∧ r' = IsReservation.empty

true.intro.Done∃ ts', to_system ts' = s' ∧ valid ts'
spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }rw [spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty
t_valid.right: ∀ {a b : Prop}, a ∧ b → b
right,spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + IsReservation.empty) state ∧   IsReservation.empty = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }IsReservation.toIsCommutative: {T : Type} → [self : IsReservation T] → Lean.IsCommutative HAdd.hAdd
IsReservation.toIsCommutative.comm: ∀ {α : Sort ?u.7834} {op : α → α → α} [self : Lean.IsCommutative op] (a b : α), op a b = op b a
comm,spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (IsReservation.empty + other_reservations ts idx.val) state ∧   IsReservation.empty = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }IsReservation.empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
IsReservation.empty_addspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val } at t_valid: Spec.validate spec (other_reservations ts idx.val + IsReservation.empty) state ∧   IsReservation.empty = IsReservation.empty
t_validspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }constructorspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.currently_validSpec.validate spec (reservations { state := state, threads := List.eraseIdx ts.threads idx.val })
  { state := state, threads := List.eraseIdx ts.threads idx.val }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.eraseIdx ts.threads idx.val }.threads → TracedThread.valid t
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.currently_validSpec.validate spec (reservations { state := state, threads := List.eraseIdx ts.threads idx.val })
  { state := state, threads := List.eraseIdx ts.threads idx.val }.state spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.currently_validSpec.validate spec (reservations { state := state, threads := List.eraseIdx ts.threads idx.val })
  { state := state, threads := List.eraseIdx ts.threads idx.val }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.eraseIdx ts.threads idx.val }.threads → TracedThread.valid texact t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty
t_valid.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ r' = IsReservation.empty

true.intro.Done.rightvalid { state := state, threads := List.eraseIdx ts.threads idx.val }.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.eraseIdx ts.threads idx.val }.threads → TracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.eraseIdx ts.threads idx.val }.threads → TracedThread.valid tintro t: TracedThread ?spec
t (t_hyp: t ∈ List.eraseIdx ts.threads idx.val
t_hyp : t ∈ ts.threads.eraseIdx idx.val)spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

t: TracedThread spec

t_hyp: t ∈ List.eraseIdx ts.threads idx.val

true.intro.Done.right.threads_validTracedThread.valid t
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Done state

t_valid: Spec.validate spec (other_reservations ts idx.val) state ∧ IsReservation.empty = IsReservation.empty

true.intro.Done.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.eraseIdx ts.threads idx.val }.threads → TracedThread.valid texact ts_valid: valid ts
ts_valid.threads_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → ∀ (t : TracedThread spec), t ∈ s.threads → TracedThread.valid t
threads_valid t: TracedThread ?spec
t <| Utils.List.erase_subset: ∀ {T : Type ?u.8020} {a : T} (l : List T) (idx : Nat), a ∈ List.eraseIdx l idx → a ∈ l
Utils.List.erase_subset _: List ?m.8021
_ _: Nat
_ t_hyp: t ∈ List.eraseIdx ts.threads idx.val
t_hyp
Goals accomplished! 🐙
  spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

iteration: System.iterate s idx = s'

∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts' spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'rename_i state: ?m.5522.State
state cont: Thread ?m.5522
contspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'exists ts: TracedSystem spec
ts.update_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val state: ?m.5522.State
state r': ?m.5375
r' cont: Thread ?m.5522
contspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) = s' ∧ valid (update_thread ts idx.val state r' cont)
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'rw [spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) = s' ∧ valid (update_thread ts idx.val state r' cont)<- iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'
iterationspec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) =     { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } ∧   valid (update_thread ts idx.val state r' cont)]spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) =     { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } ∧   valid (update_thread ts idx.val state r' cont) spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts';spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) =     { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } ∧   valid (update_thread ts idx.val state r' cont) spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'clear iteration: { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } = s'
iteration s': System spec
s'spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system (update_thread ts idx.val state r' cont) =     { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } ∧   valid (update_thread ts idx.val state r' cont)
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'simp only [update_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Runningto_system { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } =     { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } ∧   valid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'constructorspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.leftto_system { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } =   { state := state, threads := List.set s.threads idx.val cont, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.leftto_system { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } =   { state := state, threads := List.set s.threads idx.val cont, panics := s.panics } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.leftto_system { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } =   { state := state, threads := List.set s.threads idx.val cont, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }simp only [to_system: {spec : Spec} → TracedSystem spec → System spec
to_system, System.mk.injEq: ∀ {spec : Spec} (state : spec.State) (threads : List (Thread spec)) (panics : Nat) (state_1 : spec.State)
  (threads_1 : List (Thread spec)) (panics_1 : Nat),
  ({ state := state, threads := threads, panics := panics } =       { state := state_1, threads := threads_1, panics := panics_1 }) =     (state = state_1 ∧ threads = threads_1 ∧ panics = panics_1)
System.mk.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and, has_traced_system: s = to_system ts
has_traced_system, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.leftList.map (fun x => x.thread) (List.set ts.threads idx.val { thread := cont, reservation := r' }) =   List.set (List.map (fun x => x.thread) ts.threads) idx.val cont
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.leftto_system { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } =   { state := state, threads := List.set s.threads idx.val cont, panics := s.panics }
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }exact Utils.List.set_map_commutes: ∀ {U V : Type ?u.8555} (f : U → V) (l : List U) (idx : Nat) (new_val : U),
  List.map f (List.set l idx new_val) = List.set (List.map f l) idx (f new_val)
Utils.List.set_map_commutes ..
Goals accomplished! 🐙
    spec: Spec

s, s': System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running a✝¹ a✝

iteration: { state := a✝¹, threads := List.set s.threads idx.val a✝, panics := s.panics } = s'

t_valid: Spec.validate spec (other_reservations ts idx.val + r') a✝¹ ∧ TracedThread.valid { thread := a✝, reservation := r' }

true.intro.Running∃ ts', to_system ts' = s' ∧ valid ts'.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } } spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }constructorspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid t
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tlet ts': ?m.8584
ts' :=ts: TracedSystem spec
ts.update_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val state: ?m.5522.State
state r': ?m.5375
r' cont: Thread ?m.5522
contspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tshow spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate ts': ?m.8584
ts'.reservations: {spec : Spec} → TracedSystem spec → spec.Reservation
reservations ts': ?m.8584
ts'.state: {spec : Spec} → TracedSystem spec → spec.State
statespec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.state
        
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tlet idx'': ThreadIndex ts'
idx'' : ts': ?m.8584
ts'.ThreadIndex: {spec : Spec} → TracedSystem spec → Type
ThreadIndex :=⟨idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val, spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.stateby spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx.val < List.length ts'.threadscalc
          idx: System.ThreadIndex s
idx.val: {n : Nat} → Fin n → Nat
val < ts: TracedSystem spec
ts.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.length: {α : Type ?u.8635} → List α → Nat
length :=idx': ThreadIndex ts
idx'.isLt: ∀ {n : Nat} (self : Fin n), self.val < n
isLt
                _: ?m.8664
_ = ts': TracedSystem spec
ts'.threads: {spec : Spec} → TracedSystem spec → List (TracedThread spec)
threads.length: {α : Type ?u.8667} → List α → Nat
length :=Eq.symm: ∀ {α : Sort ?u.8672} {a b : α}, a = b → b = a
Eq.symm <| List.length_set: ∀ {α : Type ?u.8679} (as : List α) (i : Nat) (a : α), List.length (List.set as i a) = List.length as
List.length_set ..
Goals accomplished! 🐙⟩spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.state
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid thave decompose': ?m.8758
decompose' :=ts': ?m.8584
ts'.decompose_reservations: ∀ {spec : Spec} (s : TracedSystem spec) (idx : ThreadIndex s),
  reservations s = other_reservations s idx.val + (List.get s.threads idx).reservation
decompose_reservations idx'': ThreadIndex ts'
idx''spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.state

        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tconv at decompose' =>spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

env_r
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.staterhsspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationconv =>
            spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationarg 1spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

other_reservations ts' idx''.val
            spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationsimp only [other_reservations: {spec : Spec} → TracedSystem spec → Nat → spec.Reservation
other_reservations, update_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread, Utils.List.erase_set: ∀ {T : Type ?u.8855} (l : List T) (idx : Nat) (new_value : T),
  List.eraseIdx (List.set l idx new_value) idx = List.eraseIdx l idx
Utils.List.erase_set]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

List.foldl (fun env_r thread => env_r + thread.reservation) IsReservation.empty (List.eraseIdx ts.threads idx.val)
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationconv =>
            spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

List.foldl (fun env_r thread => env_r + thread.reservation) IsReservation.empty (List.eraseIdx ts.threads idx.val) +   (List.get ts'.threads idx'').reservationarg 2spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

(List.get ts'.threads idx'').reservation
            spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

List.foldl (fun env_r thread => env_r + thread.reservation) IsReservation.empty (List.eraseIdx ts.threads idx.val) +   (List.get ts'.threads idx'').reservationsimp only [update_thread: {spec : Spec} → TracedSystem spec → Nat → spec.State → spec.Reservation → Thread spec → TracedSystem spec
update_thread, Utils.List.get_of_set: ∀ {T : Type ?u.9002} (l : List T) (idx : Nat) (a : T) (isLt : idx < List.length (List.set l idx a)),
  List.get (List.set l idx a) { val := idx, isLt := isLt } = a
Utils.List.get_of_set]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

r'
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationarg 1spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

List.foldl (fun env_r thread => env_r + thread.reservation) IsReservation.empty (List.eraseIdx ts.threads idx.val)
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservationchange env_r: ?m.5181
env_rspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = other_reservations ts' idx''.val + (List.get ts'.threads idx'').reservation

env_r
        
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid trw [spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = env_r + r'

true.intro.Running.right.currently_validSpec.validate spec (reservations ts') ts'.statedecompose': reservations ts' = env_r + r'
decompose'spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = env_r + r'

true.intro.Running.right.currently_validSpec.validate spec (env_r + r') ts'.state]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

ts':= update_thread ts idx.val state r' cont: TracedSystem spec

idx'':= { val := idx.val, isLt := (_ : idx.val < List.length ts'.threads) }: ThreadIndex ts'

decompose': reservations ts' = env_r + r'

true.intro.Running.right.currently_validSpec.validate spec (env_r + r') ts'.state
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.currently_validSpec.validate spec
  (reservations { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } })
  { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.state
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid texact t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }
t_valid.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
      spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.rightvalid { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tintro t: TracedThread ?spec
t (t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }
t_hyp : t ∈ ts.threads.set idx.val ⟨cont, r'⟩)spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_validTracedThread.valid t
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid tcases Utils.List.set_subset: ∀ {T : Type ?u.9252} {a : T} (l : List T) (idx : Nat) (new_value : T),
  a ∈ List.set l idx new_value → a = new_value ∨ a ∈ l
Utils.List.set_subset _: List ?m.9253
_ _: Nat
_ _: ?m.9253
_ t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }
t_hypspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid t
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inrTracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_validTracedThread.valid t<;>spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid t
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inrTracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ List.set ts.threads idx.val { thread := cont, reservation := r' }

true.intro.Running.right.threads_validTracedThread.valid trename_i t_hyp: ?m.9293
t_hypspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ ts.threads

true.intro.Running.right.threads_valid.inrTracedThread.valid t
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid t.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid t
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ ts.threads

true.intro.Running.right.threads_valid.inrTracedThread.valid trw [spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid tt_hyp: ?m.9293
t_hypspec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid { thread := cont, reservation := r' }]spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid { thread := cont, reservation := r' }
          spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t = { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid.inlTracedThread.valid t
spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ ts.threads

true.intro.Running.right.threads_valid.inrTracedThread.valid texact t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }
t_valid.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙
        spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

true.intro.Running.right.threads_valid∀ (t : TracedThread spec),
  t ∈ { state := state, threads := List.set ts.threads idx.val { thread := cont, reservation := r' } }.threads →
    TracedThread.valid t.spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ ts.threads

true.intro.Running.right.threads_valid.inrTracedThread.valid t spec: Spec

s: System spec

idx: System.ThreadIndex s

ts: TracedSystem spec

has_traced_system: s = to_system ts

ts_valid: valid ts

blocked_until: Thread.block_until (List.get s.threads idx) s.state = true

ts_state_eq: ts.state = s.state

idx':= Utils.Fin.cast idx (_ : List.length s.threads = List.length ts.threads): ThreadIndex ts

get_idx': (List.get ts.threads idx').thread = List.get s.threads idx

env_r:= other_reservations ts idx.val: spec.Reservation

decompose: reservations ts = env_r + (List.get ts.threads idx').reservation

r': spec.Reservation

state: spec.State

cont: Thread spec

h: Thread.iterate (List.get s.threads idx) s.state = Thread.IterationResult.Running state cont

t_valid: Spec.validate spec (other_reservations ts idx.val + r') state ∧ TracedThread.valid { thread := cont, reservation := r' }

t: TracedThread spec

t_hyp: t ∈ ts.threads

true.intro.Running.right.threads_valid.inrTracedThread.valid texact ts_valid: valid ts
ts_valid.threads_valid: ∀ {spec : Spec} {s : TracedSystem spec}, valid s → ∀ (t : TracedThread spec), t ∈ s.threads → TracedThread.valid t
threads_valid t: TracedThread ?spec
t t_hyp: ?m.9294
t_hyp
Goals accomplished! 🐙

end TracedSystem

end Mt.Traced