import Mt.Reservation
import Mt.Task.Impl

namespace Mt

/-- Monad to describe single threaded algorithms. Tasks can be iterated
  step by step until they finally complete or panic.

  `TaskM` is a monad, i.e. you can use the do-notation to write code:

  ```
  import Mt.Task.Basic
  open Mt

  abbrev spec : Spec :={
    State := Nat,
    Reservation := UnitReservation,
    validate :=λ _ _ => True
  }

  def sample_task : TaskM spec Bool :=do
    if (<- TaskM.atomic_read λ n => n) > 100 then
      -- reset to 100
      TaskM.atomic_read_modify λ _ => 100
      return false
    
    TaskM.atomic_assert λ n => n < 500
    
    TaskM.atomic_read_modify λ n => n + 7
    return true 
  ```

  Note: `TaskM` hat an associative bind operator, but it is not
  a lawful monad: Binding two `pure` cannot be simplified into
  a single pure, because it requires two iterations to complete.
-/
def TaskM: Spec → Type → Type
TaskM (spec: Spec
spec : Spec: Type 1
Spec) (T: Type
T : Type: Type 1
Type) : Type: Type 1
Type :=TaskM.impl.TaskM: Spec → Type → Type
TaskM.impl.TaskM spec: Spec
spec T: Type
T

/-- The result of a single iteration of `TaskM`.

  Independent of the result, the resulting shared state after
  the iteration can be retrieved using `IterationResult.state`
-/
inductive TaskM.IterationResult: Spec → Type → Type
TaskM.IterationResult (spec: Spec
spec : Spec: Type 1
Spec) (T: Type
T : Type: Type 1
Type)
| Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
Done : spec: Spec
spec.State: Spec → Type
State -> T: Type
T -> IterationResult: Spec → Type → Sort ?u.17
IterationResult spec: Spec
spec T: Type
T
| Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
Panic : spec: Spec
spec.State: Spec → Type
State -> String: Type
String -> IterationResult: Spec → Type → Sort ?u.17
IterationResult spec: Spec
spec T: Type
T
| Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
Running : spec: Spec
spec.State: Spec → Type
State -> (spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool) -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T -> IterationResult: Spec → Type → Sort ?u.17
IterationResult spec: Spec
spec T: Type
T

variable {spec: Spec
spec : Spec: Type 1
Spec}

def TaskM.IterationResult.state: {T : Type} → {spec : Spec} → IterationResult spec T → spec.State
TaskM.IterationResult.state {T: Type
T spec: Spec
spec} : IterationResult: Spec → Type → Type
IterationResult spec: ?m.1240
spec T: ?m.1237
T -> spec: ?m.1240
spec.State: Spec → Type
State
| Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
Done s: spec.State
s _ => s: spec.State
s
| Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
Panic s: spec.State
s _ => s: spec.State
s
| Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
Running s: spec.State
s .. => s: spec.State
s

instance TaskM.instMonad: {spec : Spec} → Monad (TaskM spec)
TaskM.instMonad : Monad: (Type ?u.1655 → Type ?u.1654) → Type (max (?u.1655 + 1) ?u.1654)
Monad (TaskM: Spec → Type → Type
TaskM spec: Spec
spec) where
  pure :=impl.TaskM.pure: {spec : Spec} → {T : Type} → T → impl.TaskM spec T
impl.TaskM.pure
  bind :=impl.TaskM.bind: {spec : Spec} → {U V : Type} → impl.TaskM spec U → (U → impl.TaskM spec V) → impl.TaskM spec V
impl.TaskM.bind

theorem TaskM.bind_assoc: ∀ {spec : Spec} {U V W : Type} (mu : TaskM spec U) (f : U → TaskM spec V) (g : V → TaskM spec W),
  (mu >>= fun u => f u >>= g) = mu >>= f >>= g
TaskM.bind_assoc {U: Type
U V: Type
V W: Type
W : Type: Type 1
Type}
  (mu: TaskM spec U
mu : TaskM: Spec → Type → Type
TaskM spec: Spec
spec U: Type
U)
  (f: U → TaskM spec V
f : U: Type
U -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec V: Type
V)
  (g: V → TaskM spec W
g : V: Type
V -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec W: Type
W) :
  mu: TaskM spec U
mu >>= (fun u: ?m.2694
u => (f: U → TaskM spec V
f u: ?m.2694
u) >>= g: V → TaskM spec W
g) = (mu: TaskM spec U
mu >>= f: U → TaskM spec V
f) >>= g: V → TaskM spec W
g :=by
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(mu >>= fun u => f u >>= g) = mu >>= f >>= gsimp only [Bind.bind: {m : Type ?u.2776 → Type ?u.2775} → [self : Bind m] → {α β : Type ?u.2776} → m α → (α → m β) → m β
Bind.bind]spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(impl.TaskM.bind mu fun u => impl.TaskM.bind (f u) g) = impl.TaskM.bind (impl.TaskM.bind mu f) g
  spec: Spec

U, V, W: Type

mu: TaskM spec U

f: U → TaskM spec V

g: V → TaskM spec W

(mu >>= fun u => f u >>= g) = mu >>= f >>= gexact impl.TaskM.bind_assoc: ∀ {spec : Spec} {U V W : Type} (mu : impl.TaskM spec U) (f : U → impl.TaskM spec V) (g : V → impl.TaskM spec W),
  (impl.TaskM.bind mu fun u => impl.TaskM.bind (f u) g) = impl.TaskM.bind (impl.TaskM.bind mu f) g
impl.TaskM.bind_assoc ..
Goals accomplished! 🐙

/-- Atomic `TaskM` primitive with read/write-access to the shared state.

  Additional to performing a read-modify operation, it returns a value.

  Example: Compare Exchange (https://en.wikipedia.org/wiki/Compare-and-swap)
 -/
def TaskM.atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
TaskM.atomic_read_modify_read {T: Type
T : Type: Type 1
Type}
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: Type
T × spec: Spec
spec.State: Spec → Type
State)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T :=impl.TaskM.atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → impl.TaskM spec T
impl.TaskM.atomic_read_modify_read f: spec.State → T × spec.State
f

/-- Atomic `TaskM` primitive to perform read-modify operations on the
  shared state. It does not return anything. -/
def TaskM.atomic_read_modify: (spec.State → spec.State) → TaskM spec Unit
TaskM.atomic_read_modify
  (f: spec.State → spec.State
f : spec: Spec
spec.State: Spec → Type
State -> spec: Spec
spec.State: Spec → Type
State) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec Unit: Type
Unit :=
  atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read λ s: ?m.2960
s => ⟨⟨⟩: PUnit
⟨⟩, f: spec.State → spec.State
f s: ?m.2960
s⟩

/-- Atomic `TaskM` primitive to perform read the shared state. It
  does not change anything -/
def TaskM.atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
TaskM.atomic_read {T: Type
T : Type: Type 1
Type}
  (f: spec.State → T
f : spec: Spec
spec.State: Spec → Type
State -> T: Type
T)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T :=
  atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read λ s: ?m.3046
s => match f: spec.State → T
f s: ?m.3046
s with
    | t: ?m.3049
t => ⟨t: ?m.3049
t, s: ?m.3046
s⟩

/-- Atomic `TaskM` primitive which throws an exception. The current thread
  panics and will be removed from the system -/
def TaskM.panic: {T : Type} → String → TaskM spec T
TaskM.panic {T: Type
T : Type: Type 1
Type} (msg: String
msg : String: Type
String) : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T :=
  impl.TaskM.panic: {spec : Spec} → {T : Type} → String → impl.TaskM spec T
impl.TaskM.panic msg: String
msg

/-- Atomic `TaskM` primitive to assert a given condition. The condition
  is checked atomically. If it returns `false`, the current thread panics. -/
def TaskM.atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
TaskM.atomic_assert
  (cond: spec.State → Bool
cond : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec Unit: Type
Unit :=impl.TaskM.atomic_assert: {spec : Spec} → (spec.State → Bool) → impl.TaskM spec Unit
impl.TaskM.atomic_assert cond: spec.State → Bool
cond

/-- `TaskM` primitive which blocks the current thread until a given
  condition holds, and executes a read-modify-read operation afterwards.
  
  There are neither spurious wakeups nor race conditions: The system will
  only perform the read-modify-read operation if the provided condition
  holds. If it does not, the thread will block. -/
def TaskM.atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
TaskM.atomic_blocking_rmr
  (block_until: spec.State → Bool
block_until : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.3233
T × spec: Spec
spec.State: Spec → Type
State)
  : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: ?m.3233
T :=impl.TaskM.atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → impl.TaskM spec T
impl.TaskM.atomic_blocking_rmr block_until: spec.State → Bool
block_until f: spec.State → T × spec.State
f

/-- Iterate a given thread on a given state and provides an `IterationResult`.

  The task may complete or panic. If it is does not, it is still running
  and a continuation will be provided in the result -/
def TaskM.iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
TaskM.iterate {T: Type
T : Type: Type 1
Type} : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T ->
  spec: Spec
spec.State: Spec → Type
State -> IterationResult: Spec → Type → Type
IterationResult spec: Spec
spec T: Type
T :=
  λ p: ?m.3329
p s: ?m.3332
s => match p: ?m.3329
p s: ?m.3332
s with
  | impl.IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → impl.IterationResult spec T
impl.IterationResult.Done s': spec.State
s' t: T
t => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' t: T
t
  | impl.IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → impl.IterationResult spec T
impl.IterationResult.Panic s': spec.State
s' msg: String
msg => IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg
  | impl.IterationResult.Running: {spec : Spec} →
  {T : Type} →
    spec.State → (spec.State → Bool) → (spec.State → impl.IterationResult spec T) → impl.IterationResult spec T
impl.IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: spec.State → impl.IterationResult spec T
cont =>
      IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: spec.State → impl.IterationResult spec T
cont

/-- Iteration of `pure t` always completes with result `t` -/
theorem TaskM.iterate_pure: ∀ {T : Type} (s : spec.State) (t : T), iterate (pure t) s = IterationResult.Done s t
TaskM.iterate_pure {T: Type
T : Type: Type 1
Type} :
  ∀ (s: spec.State
s : spec: Spec
spec.State: Spec → Type
State) (t: T
t : T: Type
T),
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (pure: {f : Type ?u.3757 → Type ?u.3756} → [self : Pure f] → {α : Type ?u.3757} → α → f α
pure t: T
t) s: spec.State
s = IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s: spec.State
s t: T
t :=by spec: Spec

T: Type

∀ (s : spec.State) (t : T), iterate (pure t) s = IterationResult.Done s tintrosspec: Spec

T: Type

s✝: spec.State

t✝: T

iterate (pure t✝) s✝ = IterationResult.Done s✝ t✝ spec: Spec

T: Type

∀ (s : spec.State) (t : T), iterate (pure t) s = IterationResult.Done s t;spec: Spec

T: Type

s✝: spec.State

t✝: T

iterate (pure t✝) s✝ = IterationResult.Done s✝ t✝ spec: Spec

T: Type

∀ (s : spec.State) (t : T), iterate (pure t) s = IterationResult.Done s trfl
Goals accomplished! 🐙

/-- Iteration of `a >>= f` iterates `a` and returns a continuation.

  * If the `a` iteration has completed with result `t`, the next
    iteration will start work on `f t`
  * If the `a` iteration has not completed yet, the next iteration
    will continue.
  * If `a` has panicked, the exception is propagated.
 -/
theorem TaskM.iterate_bind: ∀ {spec : Spec} {U V : Type} (mu : TaskM spec U) (f : U → TaskM spec V) (s : spec.State),
  iterate (mu >>= f) s =     let _discr := iterate mu s;
    match iterate mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (cont >>= f)
TaskM.iterate_bind {U: Type
U V: Type
V : Type: Type 1
Type}
  (mu: TaskM spec U
mu : TaskM: Spec → Type → Type
TaskM spec: Spec
spec U: Type
U)
  (f: U → TaskM spec V
f : U: Type
U -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec V: Type
V)
  : ∀ (s: spec.State
s : spec: Spec
spec.State: Spec → Type
State),
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (mu: TaskM spec U
mu >>= f: U → TaskM spec V
f) s: spec.State
s = match iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate mu: TaskM spec U
mu s: spec.State
s with
    | IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' u: U
u => IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': spec.State
s' (λ _: ?m.3914
_ => true: Bool
true) (f: U → TaskM spec V
f u: U
u)
    | IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg => IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s': spec.State
s' msg: String
msg
    | IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until cont: TaskM spec U
cont =>
        IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': spec.State
s' block_until: spec.State → Bool
block_until (cont: TaskM spec U
cont >>= f: U → TaskM spec V
f) :=by
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

∀ (s : spec.State),
  iterate (mu >>= f) s =     let _discr := iterate mu s;
    match iterate mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (cont >>= f)intro s: spec.State
sspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

iterate (mu >>= f) s =   let _discr := iterate mu s;
  match iterate mu s with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (cont >>= f)
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

∀ (s : spec.State),
  iterate (mu >>= f) s =     let _discr := iterate mu s;
    match iterate mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (cont >>= f)simp only [Bind.bind: {m : Type ?u.4143 → Type ?u.4142} → [self : Bind m] → {α β : Type ?u.4143} → m α → (α → m β) → m β
Bind.bind, iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate, impl.TaskM.bind: {spec : Spec} → {U V : Type} → impl.TaskM spec U → (U → impl.TaskM spec V) → impl.TaskM spec V
impl.TaskM.bind]spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match
    match h : mu s with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match mu s with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)
  spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

∀ (s : spec.State),
  iterate (mu >>= f) s =     let _discr := iterate mu s;
    match iterate mu s with
    | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
    | IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (cont >>= f)cases mu: TaskM spec U
mu s: spec.State
sspec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: U

Done(match
    match h : impl.IterationResult.Done a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Done a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: String

Panic(match
    match h : impl.IterationResult.Panic a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Panic a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec U

Running(match
    match h : impl.IterationResult.Running a✝² a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Running a✝² a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f) spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match
    match h : mu s with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match mu s with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)<;>spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: U

Done(match
    match h : impl.IterationResult.Done a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Done a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝¹: spec.State

a✝: String

Panic(match
    match h : impl.IterationResult.Panic a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Panic a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)
spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s, a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec U

Running(match
    match h : impl.IterationResult.Running a✝² a✝¹ a✝ with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match impl.IterationResult.Running a✝² a✝¹ a✝ with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f) spec: Spec

U, V: Type

mu: TaskM spec U

f: U → TaskM spec V

s: spec.State

(match
    match h : mu s with
    | impl.IterationResult.Done s' u => impl.IterationResult.Running s' (fun x => true) (f u)
    | impl.IterationResult.Panic s' msg => impl.IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont =>
      impl.IterationResult.Running s' block_until (impl.TaskM.bind cont f) with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   match
    match mu s with
    | impl.IterationResult.Done s' t => IterationResult.Done s' t
    | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
    | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont with
  | IterationResult.Done s' u => IterationResult.Running s' (fun x => true) (f u)
  | IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | IterationResult.Running s' block_until cont => IterationResult.Running s' block_until (impl.TaskM.bind cont f)rfl
Goals accomplished! 🐙

/-- Iteration of a read-modify-read-operation will perform the read modify
  and complete with the computed result. -/
theorem TaskM.iterate_rmr: ∀ {T : Type} (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t
TaskM.iterate_rmr {T: Type
T : Type: Type 1
Type}
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: Type
T × spec: Spec
spec.State: Spec → Type
State)
  : ∀ s: ?m.7722
s,
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read f: spec.State → T × spec.State
f) s: ?m.7722
s = match f: spec.State → T × spec.State
f s: ?m.7722
s with
    | ⟨t: T
t, s': spec.State
s'⟩ => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': spec.State
s' t: T
t :=by spec: Spec

T: Type

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' tintrosspec: Spec

T: Type

f: spec.State → T × spec.State

s✝: spec.State

iterate (atomic_read_modify_read f) s✝ =   let _discr := f s✝;
  match f s✝ with
  | (t, s') => IterationResult.Done s' t spec: Spec

T: Type

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t;spec: Spec

T: Type

f: spec.State → T × spec.State

s✝: spec.State

iterate (atomic_read_modify_read f) s✝ =   let _discr := f s✝;
  match f s✝ with
  | (t, s') => IterationResult.Done s' t spec: Spec

T: Type

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' trfl
Goals accomplished! 🐙

/-- Iteration of a read-modify operation will perform the read modify
  operation and complete with `Unit.unit` -/
theorem TaskM.iterate_rm: ∀ (f : spec.State → spec.State) (s : spec.State),
  iterate (atomic_read_modify f) s =     let s' := f s;
    IterationResult.Done s' PUnit.unit
TaskM.iterate_rm
  (f: spec.State → spec.State
f : spec: Spec
spec.State: Spec → Type
State -> spec: Spec
spec.State: Spec → Type
State)
  : ∀ s: ?m.7888
s,
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify f: spec.State → spec.State
f) s: ?m.7888
s = match f: spec.State → spec.State
f s: ?m.7888
s with
    | s': ?m.7904
s' => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s': ?m.7904
s' ⟨⟩: PUnit
⟨⟩ :=by
  spec: Spec

f: spec.State → spec.State

∀ (s : spec.State),
  iterate (atomic_read_modify f) s =     let s' := f s;
    IterationResult.Done s' PUnit.unitapply iterate_rmr: ∀ {spec : Spec} {T : Type} (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t
iterate_rmr
Goals accomplished! 🐙

/-- Iteration of a read operation will compute a value based on the
  current shared state and complete with the result -/
theorem TaskM.iterate_read: ∀ {spec : Spec} {T : Type} (f : spec.State → T × spec.Reservation) (s : spec.State),
  iterate (atomic_read f) s =     let t := f s;
    IterationResult.Done s t
TaskM.iterate_read
  (f: spec.State → T × spec.Reservation
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.8188
T × spec: Spec
spec.Reservation: Spec → Type
Reservation)
  : ∀ s: ?m.8198
s,
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read f: spec.State → T × spec.Reservation
f) s: ?m.8198
s = match f: spec.State → T × spec.Reservation
f s: ?m.8198
s with
    | t: ?m.8217
t => IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s: ?m.8198
s t: ?m.8217
t :=by
  spec: Spec

T: Type

f: spec.State → T × spec.Reservation

∀ (s : spec.State),
  iterate (atomic_read f) s =     let t := f s;
    IterationResult.Done s tapply iterate_rmr: ∀ {spec : Spec} {T : Type} (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_read_modify_read f) s =     let _discr := f s;
    match f s with
    | (t, s') => IterationResult.Done s' t
iterate_rmr
Goals accomplished! 🐙

/-- Iteration of a panic will fail -/
theorem TaskM.iterate_panic: ∀ {spec : Spec} {T : Type} (msg : String) (s : spec.State), iterate (panic msg) s = IterationResult.Panic s msg
TaskM.iterate_panic {T: Type
T : Type: Type 1
Type} (msg: String
msg : String: Type
String)
  : ∀ (s: spec.State
s : spec: Spec
spec.State: Spec → Type
State),
    iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (panic: {spec : Spec} → {T : Type} → String → TaskM spec T
panic (T :=T: Type
T) msg: String
msg) s: spec.State
s = IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s: spec.State
s msg: String
msg :=by
  spec: Spec

T: Type

msg: String

∀ (s : spec.State), iterate (panic msg) s = IterationResult.Panic s msgintrosspec: Spec

T: Type

msg: String

s✝: spec.State

iterate (panic msg) s✝ = IterationResult.Panic s✝ msg spec: Spec

T: Type

msg: String

∀ (s : spec.State), iterate (panic msg) s = IterationResult.Panic s msg;spec: Spec

T: Type

msg: String

s✝: spec.State

iterate (panic msg) s✝ = IterationResult.Panic s✝ msg spec: Spec

T: Type

msg: String

∀ (s : spec.State), iterate (panic msg) s = IterationResult.Panic s msgrfl
Goals accomplished! 🐙

/-- Iteration of an assertion will atomically check the condition
  and succeed or fail depending on the result. -/
theorem TaskM.iterate_assert: ∀ {spec : Spec} (cond : spec.State → Bool) (s : spec.State),
  iterate (atomic_assert cond) s =     if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
TaskM.iterate_assert
  (cond: spec.State → Bool
cond : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  : ∀ s: ?m.8539
s,
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert cond: spec.State → Bool
cond) s: ?m.8539
s = if cond: spec.State → Bool
cond s: ?m.8539
s then
    IterationResult.Done: {spec : Spec} → {T : Type} → spec.State → T → IterationResult spec T
IterationResult.Done s: ?m.8539
s ⟨⟩: PUnit
⟨⟩
  else
    IterationResult.Panic: {spec : Spec} → {T : Type} → spec.State → String → IterationResult spec T
IterationResult.Panic s: ?m.8539
s "Assertion failed": String
"Assertion failed" :=by
  spec: Spec

cond: spec.State → Bool

∀ (s : spec.State),
  iterate (atomic_assert cond) s =     if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"intro s: spec.State
sspec: Spec

cond: spec.State → Bool

s: spec.State

iterate (atomic_assert cond) s =   if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
  spec: Spec

cond: spec.State → Bool

∀ (s : spec.State),
  iterate (atomic_assert cond) s =     if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"simp only [atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert, impl.TaskM.atomic_assert: {spec : Spec} → (spec.State → Bool) → impl.TaskM spec Unit
impl.TaskM.atomic_assert, iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate]spec: Spec

cond: spec.State → Bool

s: spec.State

(match
    if cond s = true then impl.IterationResult.Done s PUnit.unit
    else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
  spec: Spec

cond: spec.State → Bool

∀ (s : spec.State),
  iterate (atomic_assert cond) s =     if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"cases cond: spec.State → Bool
cond s: spec.State
sspec: Spec

cond: spec.State → Bool

s: spec.State

false(match
    if false = true then impl.IterationResult.Done s PUnit.unit
    else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if false = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
spec: Spec

cond: spec.State → Bool

s: spec.State

true(match
    if true = true then impl.IterationResult.Done s PUnit.unit else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if true = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" spec: Spec

cond: spec.State → Bool

s: spec.State

(match
    if cond s = true then impl.IterationResult.Done s PUnit.unit
    else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"<;>spec: Spec

cond: spec.State → Bool

s: spec.State

false(match
    if false = true then impl.IterationResult.Done s PUnit.unit
    else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if false = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"
spec: Spec

cond: spec.State → Bool

s: spec.State

true(match
    if true = true then impl.IterationResult.Done s PUnit.unit else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if true = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed" spec: Spec

cond: spec.State → Bool

s: spec.State

(match
    if cond s = true then impl.IterationResult.Done s PUnit.unit
    else impl.IterationResult.Panic s "Assertion failed" with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   if cond s = true then IterationResult.Done s PUnit.unit else IterationResult.Panic s "Assertion failed"simp only [ite_false: ∀ {α : Sort ?u.9809} (a b : α), (if False then a else b) = b
ite_false, ite_true: ∀ {α : Sort ?u.9817} (a b : α), (if True then a else b) = a
ite_true]
Goals accomplished! 🐙

/-- Iteration of a `atomic_blocking_rmr` operation will always
  return a continuation.
  
  The `IterationResult` contains the blocking predicate and
  the desired read-modify-read operation. The caller should ensure
  that the read-modify-operation is only iterated when the blocking
  predicate holds. -/
theorem TaskM.iterate_blocking_rmr: ∀ {spec : Spec} {T : Type} (block_until : spec.State → Bool) (f : spec.State → T × spec.State) (s : spec.State),
  iterate (atomic_blocking_rmr block_until f) s = IterationResult.Running s block_until (atomic_read_modify_read f)
TaskM.iterate_blocking_rmr
  (block_until: spec.State → Bool
block_until : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool)
  (f: spec.State → T × spec.State
f : spec: Spec
spec.State: Spec → Type
State -> T: ?m.9923
T × spec: Spec
spec.State: Spec → Type
State)
  : ∀ s: ?m.9937
s,
  iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate (atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
atomic_blocking_rmr block_until: spec.State → Bool
block_until f: spec.State → T × spec.State
f) s: ?m.9937
s = IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s: ?m.9937
s
    block_until: spec.State → Bool
block_until (atomic_read_modify_read: {spec : Spec} → {T : Type} → (spec.State → T × spec.State) → TaskM spec T
atomic_read_modify_read f: spec.State → T × spec.State
f) :=by spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_blocking_rmr block_until f) s = IterationResult.Running s block_until (atomic_read_modify_read f)introsspec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

s✝: spec.State

iterate (atomic_blocking_rmr block_until f) s✝ = IterationResult.Running s✝ block_until (atomic_read_modify_read f) spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_blocking_rmr block_until f) s = IterationResult.Running s block_until (atomic_read_modify_read f);spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

s✝: spec.State

iterate (atomic_blocking_rmr block_until f) s✝ = IterationResult.Running s✝ block_until (atomic_read_modify_read f) spec: Spec

T: Type

block_until: spec.State → Bool

f: spec.State → T × spec.State

∀ (s : spec.State),
  iterate (atomic_blocking_rmr block_until f) s = IterationResult.Running s block_until (atomic_read_modify_read f)rfl
Goals accomplished! 🐙

/-- Well founded relation on `TaskM` fulfilled by continuations with their parents.

  It can be used to perform well founded recursion `TaskM` without using the
  implementation details of `TaskM`. Whenever `TaskM.iterate` returns a
  continuation, the continuation will be *smaller* according to this
  relation.
  -/
inductive TaskM.is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
TaskM.is_direct_cont {T: Type
T : Type: Type 1
Type} : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T -> TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T -> Prop: Type
Prop
| running: ∀ {spec : Spec} {T : Type} {p cont : TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool},
  iterate p s = IterationResult.Running s' block_until cont → is_direct_cont cont p
running
    {p: TaskM spec T
p cont: TaskM spec T
cont : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T}
    {s: ?m.10035
s s': ?m.10038
s'}
    {block_until: spec.State → Bool
block_until : spec: Spec
spec.State: Spec → Type
State -> Bool: Type
Bool}
    (iteration: iterate p s = IterationResult.Running s' block_until cont
iteration : p: TaskM spec T
p.iterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iterate s: ?m.10035
s = IterationResult.Running: {spec : Spec} → {T : Type} → spec.State → (spec.State → Bool) → TaskM spec T → IterationResult spec T
IterationResult.Running s': ?m.10038
s' block_until: spec.State → Bool
block_until cont: TaskM spec T
cont)
    : is_direct_cont: {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont cont: TaskM spec T
cont p: TaskM spec T
p 

/-- See `TaskM.is_direct_cont` -/
theorem TaskM.is_direct_cont_wf: ∀ {spec : Spec} {T : Type}, WellFounded is_direct_cont
TaskM.is_direct_cont_wf {T: Type
T : Type: Type 1
Type} :
  WellFounded: {α : Sort ?u.10114} → (α → α → Prop) → Prop
WellFounded (@is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont spec: Spec
spec T: Type
T) :=by
  spec: Spec

T: Type

WellFounded is_direct_contconstructorspec: Spec

T: Type

h∀ (a : TaskM spec T), Acc is_direct_cont a spec: Spec

T: Type

WellFounded is_direct_cont;spec: Spec

T: Type

h∀ (a : TaskM spec T), Acc is_direct_cont a spec: Spec

T: Type

WellFounded is_direct_contintro (p: impl.TaskM spec T
p : impl.TaskM spec T)spec: Spec

T: Type

p: impl.TaskM spec T

hAcc is_direct_cont p

  spec: Spec

T: Type

WellFounded is_direct_continduction p: impl.TaskM spec T
p using WellFounded.induction: ∀ {α : Sort u} {r : α → α → Prop},
  WellFounded r → ∀ {C : α → Prop} (a : α), (∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
WellFounded.inductionspec: Spec

T: Type

p: impl.TaskM spec T

h.hwfWellFounded ?m.10203
spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝
  spec: Spec

T: Type

WellFounded is_direct_cont.spec: Spec

T: Type

p: impl.TaskM spec T

h.hwfWellFounded ?m.10203 spec: Spec

T: Type

p: impl.TaskM spec T

h.hwfWellFounded ?m.10203
spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝exact impl.TaskM.is_direct_cont.wf: ∀ {spec : Spec} {T : Type}, WellFounded impl.TaskM.is_direct_cont
impl.TaskM.is_direct_cont.wf
Goals accomplished! 🐙
  spec: Spec

T: Type

WellFounded is_direct_cont.spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝ spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝clear p: impl.TaskM spec T
pspec: Spec

T: Type

x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝ spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝;spec: Spec

T: Type

x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝ spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝rename_i p: ?m.10202
p IH: ∀ (y : ?m.10202), ?m.10203 y p → ?m.10205 y
IHspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

h.hAcc is_direct_cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝constructorspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

h.h.h∀ (y : TaskM spec T), is_direct_cont y p → Acc is_direct_cont y spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝;spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

h.h.h∀ (y : TaskM spec T), is_direct_cont y p → Acc is_direct_cont y spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝intro cont: ?α
cont is_cont: ?r cont ?x
is_contspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

is_cont: is_direct_cont cont p

h.h.hAcc is_direct_cont cont
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝apply IH: ∀ (y : ?m.10202), ?m.10203 y p → ?m.10205 y
IHspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

is_cont: is_direct_cont cont p

h.h.h.aimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝cases is_cont: ?r cont ?x
is_contspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s✝, s'✝: spec.State

block_until✝: spec.State → Bool

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝rename_i s: ?m.10280.State
s s': ?m.10280.State
s' block_until: ?m.10280.State → Bool
block_until iteration: iterate p s = IterationResult.Running s' block_until cont
iterationspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: iterate p s = IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝rw [spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: iterate p s = IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont piterate: {spec : Spec} → {T : Type} → TaskM spec T → spec.State → IterationResult spec T
iteratespec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p]spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p at iteration: iterate p s = IterationResult.Running s' block_until cont
iterationspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝cases h : p: ?m.10202
p s: ?m.10280.State
sspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: T

h: p s = impl.IterationResult.Done a✝¹ a✝

h.h.h.a.running.Doneimpl.TaskM.is_direct_cont cont p
spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: String

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont p
spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont p<;>spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: T

h: p s = impl.IterationResult.Done a✝¹ a✝

h.h.h.a.running.Doneimpl.TaskM.is_direct_cont cont p
spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: String

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont p
spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h.h.h.a.runningimpl.TaskM.is_direct_cont cont prw [spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont ph: p s = impl.IterationResult.Panic a✝¹ a✝
hspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

iteration: (match impl.IterationResult.Running a✝² a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p]spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝¹: spec.State

a✝: String

iteration: (match impl.IterationResult.Panic a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont p at iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont
iterationspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

iteration: (match impl.IterationResult.Running a✝² a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: String

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont p<;>spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝¹: spec.State

a✝: String

iteration: (match impl.IterationResult.Panic a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

iteration: (match p s with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

a✝¹: spec.State

a✝: String

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont ptry spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝¹: spec.State

a✝: String

iteration: (match impl.IterationResult.Panic a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont

h: p s = impl.IterationResult.Panic a✝¹ a✝

h.h.h.a.running.Panicimpl.TaskM.is_direct_cont cont pcontradiction
Goals accomplished! 🐙
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝injection iteration: (match impl.IterationResult.Running a✝² a✝¹ a✝ with
  | impl.IterationResult.Done s' t => IterationResult.Done s' t
  | impl.IterationResult.Panic s' msg => IterationResult.Panic s' msg
  | impl.IterationResult.Running s' block_until cont => IterationResult.Running s' block_until cont) =   IterationResult.Running s' block_until cont
iterationspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝rename_i cont'_def: a✝ = cont
cont'_defspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝;spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝rw [spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ a✝

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont pcont'_def: a✝ = cont
cont'_defspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ cont

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p]spec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ cont

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p at h: p s = impl.IterationResult.Running a✝² a✝¹ a✝
hspec: Spec

T: Type

p: impl.TaskM spec T

IH: ∀ (y : impl.TaskM spec T), impl.TaskM.is_direct_cont y p → Acc is_direct_cont y

cont: TaskM spec T

s, s': spec.State

block_until: spec.State → Bool

a✝²: spec.State

a✝¹: spec.State → Bool

a✝: spec.State → impl.IterationResult spec T

h: p s = impl.IterationResult.Running a✝² a✝¹ cont

cont'_def: a✝ = cont

h.h.h.a.running.Runningimpl.TaskM.is_direct_cont cont p
    spec: Spec

T: Type

p, x✝: impl.TaskM spec T

h.hAcc is_direct_cont x✝exact ⟨h: p s = impl.IterationResult.Running a✝² a✝¹ cont
h⟩
Goals accomplished! 🐙

instance TaskM.instWf: {spec : Spec} → {T : Type} → WellFoundedRelation (TaskM spec T)
TaskM.instWf {T: Type
T : Type: Type 1
Type} :
  WellFoundedRelation: Sort ?u.10763 → Sort (max 1 ?u.10763)
WellFoundedRelation (TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T) where
  rel :=is_direct_cont: {spec : Spec} → {T : Type} → TaskM spec T → TaskM spec T → Prop
is_direct_cont
  wf  :=is_direct_cont_wf: ∀ {spec : Spec} {T : Type}, WellFounded is_direct_cont
is_direct_cont_wf

end Mt