Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
import Mt.Reservation
import Mt.Task
import Mt.Utils.Nat
import Mt.Thread

namespace Sample

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

structure 
Reservation: Type
Reservation where
  
luft: Reservation → Nat
luft  : 
Nat: Type
Nat               -- invariant : `x ≥ y + luft`
  
min_x: Reservation → Mt.LowerBound
min_x : 
Mt.LowerBound: Type
Mt.LowerBound     -- invariant : `x ≥ min_x`

-- [begin] this block will be provided by a `derive` handler in the future --
-----------------------------------------------------------------------------

instance: Add Reservation
instance : 
Add: Type ?u.642 → Type ?u.642
Add 
Reservation: Type
Reservation :=⟨fun ⟨
luft: Nat
luft, 
min_x: Mt.LowerBound
min_x⟩ ⟨
luft': Nat
luft', 
min_x': Mt.LowerBound
min_x'⟩ => ⟨
luft: Nat
luft + 
luft': Nat
luft', 
min_x: Mt.LowerBound
min_x + 
min_x': Mt.LowerBound
min_x'⟩⟩

private theorem 
Reservation.add_rw: ∀ (a b : Reservation), a + b = { luft := a.luft + b.luft, min_x := a.min_x + b.min_x }
Reservation.add_rw : ∀ 
a: Reservation
a 
b: Reservation
b : 
Reservation: Type
Reservation, 
a: Reservation
a + 
b: Reservation
b = ⟨
a: Reservation
a.
luft: Reservation → Nat
luft + 
b: Reservation
b.
luft: Reservation → Nat
luft, 
a: Reservation
a.
min_x: Reservation → Mt.LowerBound
min_x + 
b: Reservation
b.
min_x: Reservation → Mt.LowerBound
min_x⟩ :=
  
∀ (a b : Reservation), a + b = { luft := a.luft + b.luft, min_x := a.min_x + b.min_x }
a✝, b✝: Reservation

a✝ + b✝ = { luft := a✝.luft + b✝.luft, min_x := a✝.min_x + b✝.min_x }
∀ (a b : Reservation), a + b = { luft := a.luft + b.luft, min_x := a.min_x + b.min_x }
a✝, b✝: Reservation

a✝ + b✝ = { luft := a✝.luft + b✝.luft, min_x := a✝.min_x + b✝.min_x }
∀ (a b : Reservation), a + b = { luft := a.luft + b.luft, min_x := a.min_x + b.min_x }
Goals accomplished! 🐙


instance 
ReservationInstance: Mt.IsReservation Reservation
ReservationInstance : 
Mt.IsReservation: Type → Type
Mt.IsReservation 
Reservation: Type
Reservation where
  empty := ⟨
Mt.IsReservation.empty: {T : Type} → [self : Mt.IsReservation T] → T
Mt.IsReservation.empty, 
Mt.IsReservation.empty: {T : Type} → [self : Mt.IsReservation T] → T
Mt.IsReservation.empty⟩
  assoc :=
∀ (a b c : Reservation), a + b + c = a + (b + c)
a✝, b✝, c✝: Reservation

a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
∀ (a b c : Reservation), a + b + c = a + (b + c)
a✝, b✝, c✝: Reservation

a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
∀ (a b c : Reservation), a + b + c = a + (b + c)
Goals accomplished! 🐙

  comm :=
∀ (a b : Reservation), a + b = b + a
a✝, b✝: Reservation

a✝ + b✝ = b✝ + a✝
∀ (a b : Reservation), a + b = b + a
a✝, b✝: Reservation

a✝ + b✝ = b✝ + a✝
∀ (a b : Reservation), a + b = b + a
Goals accomplished! 🐙

  empty_add :=
∀ (t : Reservation), { luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } + t = t
t✝: Reservation

{ luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } + t✝ = t✝
∀ (t : Reservation), { luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } + t = t
t✝: Reservation

{ luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } + t✝ = t✝
∀ (t : Reservation), { luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } + t = t
Goals accomplished! 🐙


-----------------------------------------------------------------------------
-- [end] --------------------------------------------------------------------

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

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.2140
s => { 
s: ?m.2140
s with x := 
s: ?m.2140
s.
x: State → Nat
x + 
1: ?m.2146
1 }
  
  -- increase y atomically
  
atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ 
s: ?m.2212
s => { 
s: ?m.2212
s with y := 
s: ?m.2212
s.
y: State → Nat
y + 
1: ?m.2218
1 }

  let 
py: ?m.2274
py <- 
atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read λ ⟨_, 
y: Nat
y⟩ => 
y: Nat
y
  let 
px: ?m.2297
px <- 
atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read λ ⟨
x: Nat
x, _⟩ => 
x: Nat
x

  
atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert fun 
_: ?m.2302
_ => 
px: ?m.2297
px ≥ 
py: ?m.2274
py

theorem 
thread1_valid: Thread.valid thread1
thread1_valid : 
thread1: Thread spec
thread1.
valid: {spec : Spec} → Thread spec → Prop
valid :=
Thread.valid thread1
Thread.valid thread1
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 thread1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
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'.luft = 1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

initial_valid: Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + 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 ({ luft := env_luft, min_x := env_min_x } + r') s' ∧ r'.luft = 1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid
let s' := { x := { x := x, y := y }.x + 1, y := { x := x, y := y }.y };
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 1, min_x := 0 }) s' ∧   { luft := 1, min_x := 0 }.luft = 1
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 1, min_x := 0 }) { x := x + 1, y := y }
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

this: x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0

mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 1, min_x := 0 }) { x := x + 1, y := y }
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

this: x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0

mu_valid.f_valid
x + 1 ≥ y + (env_luft + 1) ∧ x + 1 ≥ Nat.max env_min_x 0
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro
x + 1 ≥ y + (env_luft + 1) ∧ x + 1 ≥ Nat.max env_min_x 0
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro
x + 1 ≥ y + (env_luft + 1) ∧ x + 1 ≥ Nat.max env_min_x 0
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
x + 1 ≥ y + (env_luft + 1)
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
x + 1 ≥ y + (env_luft + 1)
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
x + 1 ≥ y + (env_luft + 1)
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
y + (env_luft + 1) ≤ x + 1
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
x + 1 ≥ y + (env_luft + 1)
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.left
y + (env_luft + 1) ≤ x + 1
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

Nat.add (y + env_luft) 0 ≤ x
Goals accomplished! 🐙
Goals accomplished! 🐙
mu_valid
valid (atomic_read_modify fun s => { x := s.x + 1, y := s.y }) IsReservation.empty thread1.block_until fun x r =>
  r.luft = 1
f_valid
∀ (r' : spec.Reservation),
  Unit →
    r'.luft = 1 →
      valid
        (do
          atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
Nat.max env_min_x 0 ≤ x + 1
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
x + 1 ≥ Nat.max env_min_x 0
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

mu_valid.f_valid.intro.right
Nat.max env_min_x 0 ≤ x + 1
env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

Nat.max env_min_x 0 ≤ x
Goals accomplished! 🐙
Goals accomplished! 🐙
Thread.valid thread1
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid
valid
  (do
    atomic_read_modify fun s => { x := s.x, y := s.y + 1 }
    let py ←
      atomic_read fun x =>
          match x with
          | { x := x, y := y } => y
    let px ←
      atomic_read fun x =>
          match x with
          | { x := x, y := y } => x
    atomic_assert fun x => decide (px ≥ py))
  { luft := luft, min_x := min_x } (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

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

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

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 := luft, min_x := min_x }) s →
      ∃ r',
        let s' := { x := s.x, y := s.y + 1 };
        Spec.validate spec (env_r + r') s' ∧ True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

initial_valid: Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := luft, min_x := min_x }) { 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 ({ luft := env_luft, min_x := env_min_x } + r') s' ∧ True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

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

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

this: x ≥ y + env_luft + 1 ∧ x ≥ env_min_x + min_x

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

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

this: x ≥ y + env_luft + 1 ∧ x ≥ env_min_x + min_x

f_valid.mu_valid.f_valid
x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro
x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro
x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.right
x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro
x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.right
x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro
x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.mu_valid
valid (atomic_read_modify fun s => { x := s.x, y := s.y + 1 }) { luft := luft, min_x := min_x } (fun x => true)
  fun x x => True
luft: Nat

min_x: LowerBound

luft_def: { luft := luft, min_x := min_x }.luft = 1

f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft + 1
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft + 1
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft + 1
luft: Nat

min_x: LowerBound

luft_def: luft = 1

env_luft: Nat

env_min_x: LowerBound

x, y: Nat

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

f_valid.mu_valid.f_valid.intro.left
x ≥ y + 1 + env_luft
Goals accomplished! 🐙
Thread.valid thread1
f_valid.f_valid
∀ (r' : spec.Reservation),
  Unit →
    True →
      valid
        (do
          let py ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => y
          let px ←
            atomic_read fun x =>
                match x with
                | { x := x, y := y } => x
          atomic_assert fun x => decide (px ≥ py))
        r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

f_valid.f_valid
valid
  (do
    let py ←
      atomic_read fun x =>
          match x with
          | { x := x, y := y } => y
    let px ←
      atomic_read fun x =>
          match x with
          | { x := x, y := y } => x
    atomic_assert fun x => decide (px ≥ py))
  { luft := luft, min_x := min_x } (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + { luft := luft, min_x := min_x }) s →
      ∃ r',
        let t :=
          match s with
          | { x := x, y := y } => y;
        Spec.validate spec (env_r + r') s ∧           match r' with
          | { luft := luft, min_x := min_x } => min_x = t
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid
∃ r',
  let t :=
    match { x := x, y := y } with
    | { x := x, y := y } => y;
  Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + r') { x := x, y := y } ∧     match r' with
    | { luft := luft, min_x := min_x } => min_x = t
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid
let t :=
  match { x := x, y := y } with
  | { x := x, y := y } => y;
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := y }) { x := x, y := y } ∧   match { luft := 0, min_x := y } with
  | { luft := luft, min_x := min_x } => min_x = t
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := y }) { x := x, y := y }
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

this: x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x

f_valid.f_valid.mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := y }) { x := x, y := y }
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

this: x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x

f_valid.f_valid.mu_valid.f_valid
x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro
x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro
x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

y + env_luft ≤ y + (env_luft + luft)
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

y + (env_luft + luft) ≤ x
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => y)
  { luft := luft, min_x := min_x } (fun x => true) fun y x =>
  match x with
  | { luft := luft, min_x := min_x } => min_x = y
luft: Nat

min_x: LowerBound

f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
Nat.max env_min_x y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
env_min_x ≤ x ∧ y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
env_min_x ≤ x ∧ y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

h: x ≥ Nat.max env_min_x min_x

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.left
env_min_x ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ Nat.max env_min_x y
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

y ≤ y + (env_luft + luft)
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.mu_valid.f_valid.intro.right.right
y ≤ x
luft: Nat

min_x: LowerBound

env_luft, env_min_x, x, y: Nat

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

y + (env_luft + luft) ≤ x
Goals accomplished! 🐙
Thread.valid thread1
f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : LowerBound),
  (match r' with
    | { luft := luft, min_x := min_x } => min_x = u) →
    valid
      (do
        let px ←
          atomic_read fun x =>
              match x with
              | { x := x, y := y } => x
        atomic_assert fun x => decide (px ≥ u))
      r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid
valid
  (do
    let px ←
      atomic_read fun x =>
          match x with
          | { x := x, y := y } => x
    atomic_assert fun x => decide (px ≥ py))
  { luft := luft, min_x := min_x } (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

f_valid.f_valid.f_valid.mu_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + { luft := luft, min_x := min_x }) s →
      ∃ r',
        let t :=
          match s with
          | { x := x, y := y } => x;
        Spec.validate spec (env_r + r') s ∧ t ≥ py ∧ r' = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid
∃ r',
  let t :=
    match { x := x, y := y } with
    | { x := x, y := y } => x;
  Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + r') { x := x, y := y } ∧     t ≥ py ∧ r' = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid
let t :=
  match { x := x, y := y } with
  | { x := x, y := y } => x;
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := 0 }) { x := x, y := y } ∧   t ≥ py ∧ { luft := 0, min_x := 0 } = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := 0 }) { x := x, y := y } ∧ x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x

f_valid.f_valid.f_valid.mu_valid.f_valid
Spec.validate spec ({ luft := env_luft, min_x := env_min_x } + { luft := 0, min_x := 0 }) { x := x, y := y } ∧ x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x

f_valid.f_valid.f_valid.mu_valid.f_valid
(x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0) ∧ x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro
(x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0) ∧ x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro
(x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0) ∧ x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left
x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
x ≥ y + env_luft
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

y + env_luft ≤ y + (env_luft + luft)
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.left
y + env_luft ≤ x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

y + (env_luft + luft) ≤ x
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ env_min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ env_min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

h: x ≥ Nat.max env_min_x min_x

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ env_min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.left.right
x ≥ Nat.max env_min_x 0
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.mu_valid
valid
  (atomic_read fun x =>
    match x with
    | { x := x, y := y } => x)
  { luft := luft, min_x := min_x } (fun x => true) fun x r => x ≥ py ∧ r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: match { luft := luft, min_x := min_x } with
| { luft := luft, min_x := min_x } => min_x = py

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

this: x ≥ min_x

x ≥ py
Goals accomplished! 🐙
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

h: x ≥ Nat.max env_min_x min_x

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ min_x
luft: Nat

min_x: LowerBound

py: Nat

min_x_def: min_x = py

env_luft, env_min_x, x, y: Nat

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

f_valid.f_valid.f_valid.mu_valid.f_valid.intro.right
x ≥ py
Goals accomplished! 🐙
Thread.valid thread1
py: Nat

f_valid.f_valid.f_valid.f_valid
∀ (r' : spec.Reservation) (u : Nat),
  u ≥ py ∧ r' = IsReservation.empty →
    valid (atomic_assert fun x => decide (u ≥ py)) r' (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
valid (atomic_assert fun x => decide (px ≥ py)) { luft := luft, min_x := min_x } (fun x => true) fun x r =>
  r = IsReservation.empty
Thread.valid thread1
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
valid (atomic_assert fun x => decide (px ≥ py)) { luft := luft, min_x := min_x } (fun x => true) fun x r =>
  r = IsReservation.empty
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
valid (atomic_assert fun x => decide (px ≥ py)) IsReservation.empty (fun x => true) fun x r => r = IsReservation.empty
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
valid (atomic_assert fun x => decide (px ≥ py)) IsReservation.empty (fun x => true) fun x r => r = IsReservation.empty
Thread.valid thread1
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true → Spec.validate spec (env_r + IsReservation.empty) s → decide (px ≥ py) = true
Thread.valid thread1
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true → Spec.validate spec (env_r + IsReservation.empty) s → decide (px ≥ py) = true
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true → Spec.validate spec (env_r + IsReservation.empty) s → decide (px ≥ py) = true
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

env_r✝: spec.Reservation

s✝: spec.State

f_valid.f_valid.f_valid.f_valid
decide (px ≥ py) = true
py, luft: Nat

min_x: LowerBound

px: Nat

px_gt_py: px ≥ py

final_check: { luft := luft, min_x := min_x } = IsReservation.empty

f_valid.f_valid.f_valid.f_valid
∀ (env_r : spec.Reservation) (s : spec.State),
  true = true → Spec.validate spec (env_r + IsReservation.empty) s → decide (px ≥ py) = true
Goals accomplished! 🐙


end Sample