import Mt.Thread.Basic
import Mt.Utils

namespace Mt.Traced

structure 
TracedThread: Spec → Type 1
TracedThread (
spec: Spec
spec : 
Spec: Type 1
Spec) where
  
thread: {spec : Spec} → TracedThread spec → Thread spec
thread : 
Thread: Spec → Type 1
Thread 
spec: Spec
spec
  
reservation: {spec : Spec} → TracedThread spec → spec.Reservation
reservation : 
spec: Spec
spec.
Reservation: Spec → Type
Reservation

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

namespace TracedThread

def 
T: TracedThread spec → Type
T (
t: TracedThread spec
t : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec) : 
Type: Type 1
Type :=
t: TracedThread spec
t.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
T: {spec : Spec} → Thread spec → Type
T
def 
block_until: TracedThread spec → spec.State → Bool
block_until (
t: TracedThread spec
t : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec) : 
spec: Spec
spec.
State: Spec → Type
State -> 
Bool: Type
Bool :=
t: TracedThread spec
t.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
block_until: {spec : Spec} → Thread spec → spec.State → Bool
block_until
def 
task: (t : TracedThread spec) → TaskM spec (T t)
task (
t: TracedThread spec
t : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec) : 
TaskM: Spec → Type → Type
TaskM 
spec: Spec
spec 
t: TracedThread spec
t.
T: {spec : Spec} → TracedThread spec → Type
T :=
t: TracedThread spec
t.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
task: {spec : Spec} → (self : Thread spec) → TaskM spec self.T
task
def 
iterate: TracedThread spec → spec.State → Thread.IterationResult spec
iterate (
t: TracedThread spec
t : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec) : 
spec: Spec
spec.
State: Spec → Type
State -> 
Thread.IterationResult: Spec → Type 1
Thread.IterationResult 
spec: Spec
spec :=
t: TracedThread spec
t.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
iterate: {spec : Spec} → Thread spec → spec.State → Thread.IterationResult spec
iterate

def 
valid: TracedThread spec → Prop
valid (
thread: TracedThread spec
thread : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec) : 
Prop: Type
Prop :=
  
thread: TracedThread spec
thread.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
task: {spec : Spec} → (self : Thread spec) → TaskM spec self.T
task.
valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid 
thread: TracedThread spec
thread.
reservation: {spec : Spec} → TracedThread spec → spec.Reservation
reservation
    
thread: TracedThread spec
thread.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
block_until: {spec : Spec} → Thread spec → spec.State → Bool
block_until
    (λ 
_: ?m.573
_ 
r: ?m.576
r => 
r: ?m.576
r = 
IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty)

theorem 
valid_elim: ∀ {thread : TracedThread spec},
  valid thread →
    ∀ (env_r : spec.Reservation) (s : spec.State),
      block_until thread s = true →
        Spec.validate spec (env_r + thread.reservation) s →
          ∃ r',
            let _discr := iterate thread s;
            match 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' ∧ valid { thread := cont, reservation := r' }
valid_elim {
thread: TracedThread spec
thread : 
TracedThread: Spec → Type 1
TracedThread 
spec: Spec
spec}
  (
is_valid: valid thread
is_valid : 
thread: TracedThread spec
thread.
valid: {spec : Spec} → TracedThread spec → Prop
valid)
  : ∀ 
env_r: ?m.615
env_r 
s: ?m.618
s,
    
thread: TracedThread spec
thread.
block_until: {spec : Spec} → TracedThread spec → spec.State → Bool
block_until 
s: ?m.618
s →
    
spec: Spec
spec.
validate: (self : Spec) → self.Reservation → self.State → Prop
validate (
env_r: ?m.615
env_r + 
thread: TracedThread spec
thread.
reservation: {spec : Spec} → TracedThread spec → spec.Reservation
reservation) 
s: ?m.618
s → ∃ 
r': spec.Reservation
r' : 
spec: Spec
spec.
Reservation: Spec → Type
Reservation,
    match 
thread: TracedThread spec
thread.
iterate: {spec : Spec} → TracedThread spec → spec.State → Thread.IterationResult spec
iterate 
s: ?m.618
s with
      | 
Thread.IterationResult.Done: {spec : Spec} → spec.State → Thread.IterationResult spec
Thread.IterationResult.Done 
s': spec.State
s' =>
          
spec: Spec
spec.
validate: (self : Spec) → self.Reservation → self.State → Prop
validate (
env_r: ?m.615
env_r + 
r': spec.Reservation
r') 
s': spec.State
s' ∧
          
r': spec.Reservation
r' = 
IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty
      | 
Thread.IterationResult.Panic: {spec : Spec} → spec.State → Thread.IterationResult spec
Thread.IterationResult.Panic .. => 
False: Prop
False
      | 
Thread.IterationResult.Running: {spec : Spec} → spec.State → Thread spec → Thread.IterationResult spec
Thread.IterationResult.Running 
s': spec.State
s' 
cont: Thread spec
cont =>
        (
spec: Spec
spec.
validate: (self : Spec) → self.Reservation → self.State → Prop
validate (
env_r: ?m.615
env_r + 
r': spec.Reservation
r') 
s': spec.State
s') ∧ 
TracedThread.valid: {spec : Spec} → TracedThread spec → Prop
TracedThread.valid ⟨
cont: Thread spec
cont, 
r': spec.Reservation
r'⟩ :=by
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }simp only []
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match 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' ∧ valid { thread := cont, reservation := r' } -- TODO: Remove
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }intro 
env_r: spec.Reservation
env_r 
s: spec.State
s 
bu_true: block_until thread s = true
bu_true 
initial_valid: Spec.validate spec (env_r + thread.reservation) s
initial_valid
spec: Spec

thread: TracedThread spec

is_valid: valid thread

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }rw [
spec: Spec

thread: TracedThread spec

is_valid: valid thread

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
valid: {spec : Spec} → TracedThread spec → Prop
valid,
spec: Spec

thread: TracedThread spec

is_valid: TaskM.valid thread.thread.task thread.reservation thread.thread.block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' } 
spec: Spec

thread: TracedThread spec

is_valid: valid thread

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
TaskM.valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
TaskM.valid
spec: Spec

thread: TracedThread spec

is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }]
spec: Spec

thread: TracedThread spec

is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' } at 
is_valid: valid thread
is_valid
spec: Spec

thread: TracedThread spec

is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }have :=
is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty
is_valid 
env_r: spec.Reservation
env_r 
s: spec.State
s 
bu_true: block_until thread s = true
bu_true 
initial_valid: Spec.validate spec (env_r + thread.reservation) s
initial_valid
spec: Spec

thread: TracedThread spec

is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

this: ∃ r',
  match h : TaskM.iterate thread.thread.task s with
  | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
  | TaskM.IterationResult.Panic a a_1 => False
  | TaskM.IterationResult.Running s' block_until cont =>
    Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }cases 
this: ?m.2083
this
spec: Spec

thread: TracedThread spec

is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

w✝: spec.Reservation

intro
∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }

  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }clear 
is_valid: ∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread.thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        match h : TaskM.iterate thread.thread.task s with
        | TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
        | TaskM.IterationResult.Panic a a_1 => False
        | TaskM.IterationResult.Running s' block_until cont =>
          Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty
is_valid
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

w✝: spec.Reservation

intro
∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' } 
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' };
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

w✝: spec.Reservation

intro
∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' } 
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }rename_i 
r': ?m.2116
r' 
is_valid: ?m.2117 r'
is_valid
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

intro
∃ r',
  match 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }exists 
r': ?m.2116
r'
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

intro
match 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }simp only [
iterate: {spec : Spec} → TracedThread spec → spec.State → Thread.IterationResult spec
iterate, 
Thread.iterate: {spec : Spec} → Thread spec → spec.State → Thread.IterationResult spec
Thread.iterate]
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

intro
match
  match TaskM.iterate thread.1.task s with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
  
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }cases h : 
TaskM.iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → TaskM.IterationResult spec T
TaskM.iterate 
thread: TracedThread spec
thread.
thread: {spec : Spec} → TracedThread spec → Thread spec
thread.
task: {spec : Spec} → (self : Thread spec) → TaskM spec self.T
task 
s: spec.State
s
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Done a✝¹ a✝

intro.Done
match
  match TaskM.IterationResult.Done a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: String

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Panic a✝¹ a✝

intro.Panic
match
  match TaskM.IterationResult.Panic a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Running a✝² a✝¹ a✝

intro.Running
match
  match TaskM.IterationResult.Running a✝² a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
  
spec: Spec

thread: TracedThread spec

is_valid: valid thread

∀ (env_r : spec.Reservation) (s : spec.State),
  block_until thread s = true →
    Spec.validate spec (env_r + thread.reservation) s →
      ∃ r',
        let _discr := iterate thread s;
        match 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' ∧ valid { thread := cont, reservation := r' }all_goals 
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Done a✝¹ a✝

intro.Done
match
  match TaskM.IterationResult.Done a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: String

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Panic a✝¹ a✝

intro.Panic
match
  match TaskM.IterationResult.Panic a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Running a✝² a✝¹ a✝

intro.Running
match
  match TaskM.IterationResult.Running a✝² a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }(
    
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Done a✝¹ a✝

intro.Done
match
  match TaskM.IterationResult.Done a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }rw [
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec thread.thread.T

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Running a✝² a✝¹ a✝

intro.Running
match
  match TaskM.IterationResult.Running a✝² a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Panic a✝¹ a✝
h
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

a✝¹: spec.State

a✝: String

is_valid: match h : TaskM.IterationResult.Panic a✝¹ a✝ with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Panic a✝¹ a✝

intro.Panic
match
  match TaskM.IterationResult.Panic a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }]
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec thread.thread.T

is_valid: match h : TaskM.IterationResult.Running a✝² a✝¹ a✝ with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Running a✝² a✝¹ a✝

intro.Running
match
  match TaskM.IterationResult.Running a✝² a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' } at 
is_valid: ?m.2117 r'
is_valid
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: TaskM spec thread.thread.T

is_valid: match h : TaskM.IterationResult.Running a✝² a✝¹ a✝ with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Running a✝² a✝¹ a✝

intro.Running
match
  match TaskM.IterationResult.Running a✝² a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }
    
spec: Spec

thread: TracedThread spec

env_r: spec.Reservation

s: spec.State

bu_true: block_until thread s = true

initial_valid: Spec.validate spec (env_r + thread.reservation) s

r': spec.Reservation

is_valid: match h : TaskM.iterate thread.thread.task s with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty

a✝¹: spec.State

a✝: String

h: TaskM.iterate thread.thread.task s = TaskM.IterationResult.Panic a✝¹ a✝

intro.Panic
match
  match TaskM.IterationResult.Panic a✝¹ a✝ with
  | TaskM.IterationResult.Done state' a => Thread.IterationResult.Done state'
  | TaskM.IterationResult.Panic state' a => Thread.IterationResult.Panic state'
  | TaskM.IterationResult.Running state' block_until task =>
    Thread.IterationResult.Running state' { T := thread.1.T, block_until := block_until, task := task } 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' ∧ valid { thread := cont, reservation := r' }exact 
is_valid: match h : TaskM.IterationResult.Running a✝² a✝¹ a✝ with
| TaskM.IterationResult.Done s' t => Spec.validate spec (env_r + r') s' ∧ r' = IsReservation.empty
| TaskM.IterationResult.Panic a a_1 => False
| TaskM.IterationResult.Running s' block_until cont =>
  Spec.validate spec (env_r + r') s' ∧ TaskM.valid cont r' block_until fun x r => r = IsReservation.empty
is_valid
Goals accomplished! 🐙
  )
Goals accomplished! 🐙

end TracedThread

end Mt.Traced