ink

structure SampleSimple.State : Type

• x : Nat
• y : Nat

ink

def SampleSimple.spec : Mt.Spec

Equations

• SampleSimple.spec = Mt.Spec.mk SampleSimple.State Nat fun luft x => match x with | { x := x, y := y } => x ≥ y + luft

ink

def SampleSimple.thread1 : Mt.Thread SampleSimple.spec

Equations

• One or more equations did not get rendered due to their size.

ink

theorem SampleSimple.thread1_valid : Mt.Thread.valid SampleSimple.thread1