import Mt.Reservation
import Mt.Thread

namespace SampleSimple

structure State: Type
State where
  x: State → Nat
x : Nat: Type
Nat
  y: State → Nat
y : Nat: Type
Nat

def spec: Mt.Spec
spec : Mt.Spec: Type 1
Mt.Spec :={
  State: Type
State
  Reservation :=Nat: Type
Nat
  validate := fun (luft: Nat
luft : Nat: Type
Nat) ⟨x: Nat
x, y: Nat
y⟩ => x: Nat
x ≥ y: Nat
y + luft: Nat
luft
}

open Mt
open Mt.TaskM

def thread1: Thread spec
thread1 : Thread: Spec → Type 1
Thread spec: Spec
spec :=mk_thread: {spec : Spec} → {T : Type} → TaskM spec T → Thread spec
mk_thread do
  -- increase x atomically
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.526
s => { s: ?m.526
s with x := s: ?m.526
s.x: State → Nat
x + 1: ?m.532
1 }
  
  -- increase y atomically
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.598
s => { s: ?m.598
s with y := s: ?m.598
s.y: State → Nat
y + 1: ?m.604
1 }

  atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert fun ⟨x: Nat
x, y: Nat
y⟩ => x: Nat
x ≥ y: Nat
y

theorem thread1_valid: Thread.valid thread1
thread1_valid : thread1: Thread spec
thread1.valid: {spec : Spec} → Thread spec → Prop
valid :=by
  
Thread.valid thread1rw [
Thread.valid thread1Thread.valid: {spec : Spec} → Thread spec → Prop
Thread.valid
valid thread1.task IsReservation.empty thread1.block_until fun x r => r = IsReservation.empty]
valid thread1.task IsReservation.empty thread1.block_until fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ _: ?m.1057
_ (luft: Nat
luft : Nat: Type
Nat) => luft: Nat
luft = 1: ?m.1063
1
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1.
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1 -- validate ++x
    ---------------
    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyapply valid_rm: ∀ {spec : Spec} {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rm
mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  Thread.block_until thread1 s = true →
    Spec.validate spec (env_r + IsReservation.empty) s →
      ∃ r',
        let s' := { x := s.x + 1, y := s.y };
        Spec.validate spec (env_r + r') s' ∧ r' = 1
    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyintro (env_luft: Nat
env_luft : Nat) ⟨x: Nat
x, y: Nat
y⟩ _: Thread.block_until thread1 { x := x, y := y } = true
_ initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }
initial_validenv_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

mu_valid.f_valid∃ r',
  let s' := { x := { x := x, y := y }.x + 1, y := { x := x, y := y }.y };
  Spec.validate spec (env_luft + r') s' ∧ r' = 1
    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyexists (1: ?m.1309
1 : Nat: Type
Nat)env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

mu_valid.f_validlet s' := { x := { x := x, y := y }.x + 1, y := { x := x, y := y }.y };
Spec.validate spec (env_luft + 1) s' ∧ 1 = 1
    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptysimp only [and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

mu_valid.f_validSpec.validate spec (env_luft + 1) { x := x + 1, y := y }

    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyhave : x: Nat
x ≥ y: Nat
y + env_luft: Nat
env_luft :=initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }
initial_validenv_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

this: x ≥ y + env_luft

mu_valid.f_validSpec.validate spec (env_luft + 1) { x := x + 1, y := y }
    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyshow x: Nat
x + 1: ?m.1771
1 ≥ y: Nat
y + env_luft: Nat
env_luft + 1: ?m.1789
1env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

this: x ≥ y + env_luft

mu_valid.f_validx + 1 ≥ y + env_luft + 1

    
mu_validvalid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x luft =>
  luft = 1
f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          atomic_assert fun x =>
              match x with
              | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyexact Nat.succ_le_succ: ∀ {n m : Nat}, n ≤ m → Nat.succ n ≤ Nat.succ m
Nat.succ_le_succ (env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

this: x ≥ y + env_luft

mu_valid.f_validx + 1 ≥ y + env_luft + 1by env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + IsReservation.empty) { x := x, y := y }

this: x ≥ y + env_luft

Nat.add (y + env_luft) 0 ≤ xassumption
Goals accomplished! 🐙)
Goals accomplished! 🐙
  
  
Thread.valid thread1intro (luft: Nat
luft : Nat) ⟨⟩ luft_def: luft = 1
luft_defluft: Nat

luft_def: luft = 1

f_validvalid
  (do
    atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
    atomic_assert fun x =>
        match x with
        | { x := x, y := y } => decide (x ≥ y))
  luft (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ _: ?m.2050
_ (luft: Nat
luft : Nat: Type
Nat) => luft: Nat
luft = 0: ?m.2056
0luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1.luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0 -- validate ++y knowing luft = 1
    --------------------------------
    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyapply valid_rm: ∀ {spec : Spec} {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rmluft: Nat

luft_def: luft = 1

f_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      ∃ r',
        let s' := { x := s.x, y := s.y + 1 };
        Spec.validate spec (env_r + r') s' ∧ r' = 0
    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyintro (env_luft: Nat
env_luft : Nat) ⟨x: Nat
x, y: Nat
y⟩ _: true = true
_ initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }
initial_validluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

f_valid.mu_valid.f_valid∃ r',
  let s' := { x := { x := x, y := y }.x, y := { x := x, y := y }.y + 1 };
  Spec.validate spec (env_luft + r') s' ∧ r' = 0
    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyexists (0: ?m.2280
0 : Nat: Type
Nat)luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

f_valid.mu_valid.f_validlet s' := { x := { x := x, y := y }.x, y := { x := x, y := y }.y + 1 };
Spec.validate spec (env_luft + 0) s' ∧ 0 = 0
    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptysimp only [and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 }

    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyrw [luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 }luft_def: luft = 1
luft_defluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 }]luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 } at initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }
initial_validluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 }

    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyhave : x: Nat
x ≥ y: Nat
y + env_luft: Nat
env_luft + 1: ?m.2636
1 :=initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }
initial_validluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validSpec.validate spec (env_luft + 0) { x := x, y := y + 1 }
    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyshow x: Nat
x ≥ y: Nat
y + 1: ?m.2745
1 + env_luft: Nat
env_luftluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validx ≥ y + 1 + env_luft

    luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyrw [luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validx ≥ y + 1 + env_luftNat.add_right_comm: ∀ (n m k : Nat), n + m + k = n + k + m
Nat.add_right_commluft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validx ≥ y + env_luft + 1]luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validx ≥ y + env_luft + 1 luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.empty;luft: Nat

luft_def: luft = 1

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + 1) { x := x, y := y }

this: x ≥ y + env_luft + 1

f_valid.mu_valid.f_validx ≥ y + env_luft + 1 luft: Nat

luft_def: luft = 1

f_valid.mu_validvalid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) luft (fun x => true) fun x luft => luft = 0
luft: Nat

luft_def: luft = 1

f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.emptyassumption
Goals accomplished! 🐙
  
  
Thread.valid thread1clear luft: Nat
luft luft_def: luft = 1
luft_def
f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = 0 →
      valid
        (atomic_assert fun x =>
          match x with
          | { x := x, y := y } => decide (x ≥ y))
        r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1intro (luft: Nat
luft : Nat) ⟨⟩ luft_def: luft = 0
luft_defluft: Nat

luft_def: luft = 0

f_valid.f_validvalid
  (atomic_assert fun x =>
    match x with
    | { x := x, y := y } => decide (x ≥ y))
  luft (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_assert: ∀ {spec : Spec} {cond : spec.State → Bool} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  motive PUnit.unit r →
    (∀ (env_r : spec.Reservation) (s : spec.State),
        assuming s = true → Spec.validate spec (env_r + r) s → cond s = true) →
      valid (atomic_assert cond) r assuming motive
valid_assert (spec :=spec: Spec
spec) luft_def: luft = 0
luft_defluft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         true
  
Thread.valid thread1.luft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         true -- validate `assert x ≥ y`
    ----------------------------
    luft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         trueintro (env_luft: Nat
env_luft : Nat) ⟨x: Nat
x, y: Nat
y⟩ _: true = true
_ initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }
initial_validluft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

f_valid.f_valid(match { x := x, y := y } with
  | { x := x, y := y } => decide (x ≥ y)) =   true

    luft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         truehave : x: Nat
x ≥ y: Nat
y + (env_luft: Nat
env_luft + luft: Nat
luft) :=initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }
initial_validluft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

f_valid.f_valid(match { x := x, y := y } with
  | { x := x, y := y } => decide (x ≥ y)) =   true
    luft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         trueshow decide: (p : Prop) → [h : Decidable p] → Bool
decide (x: Nat
x ≥ y: Nat
y) = true: Bool
trueluft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

f_valid.f_validdecide (x ≥ y) = true

    luft: Nat

luft_def: luft = 0

f_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + luft) s →
      (match s with
        | { x := x, y := y } => decide (x ≥ y)) =         trueexact decide_eq_true: ∀ {p : Prop} [inst : Decidable p], p → decide p = true
decide_eq_true <| calc
      y: Nat
y ≤ y: Nat
y + (env_luft: Nat
env_luft + luft: Nat
luft) :=luft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

f_valid.f_validdecide (x ≥ y) = trueby luft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

y ≤ y + (env_luft + luft)simp_arith
Goals accomplished! 🐙
      _: ?m.3196
_ ≤ x: Nat
x                     :=luft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

f_valid.f_validdecide (x ≥ y) = trueby luft: Nat

luft_def: luft = 0

env_luft, x, y: Nat

initial_valid: Spec.validate spec (env_luft + luft) { x := x, y := y }

this: x ≥ y + (env_luft + luft)

y + (env_luft + luft) ≤ xassumption
Goals accomplished! 🐙

end SampleSimple