ink

structure Sample.State : Type

• x : Nat
• y : Nat

ink

structure Sample.Reservation : Type

• luft : Nat
• min_x : Mt.LowerBound

ink

instance Sample.instAddReservation : Add Sample.Reservation

Equations

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

ink

instance Sample.ReservationInstance : Mt.IsReservation Sample.Reservation

Equations

• Sample.ReservationInstance = Mt.IsReservation.mk { luft := Mt.IsReservation.empty, min_x := Mt.IsReservation.empty } Sample.ReservationInstance.proof_3

ink

def Sample.spec : Mt.Spec

Equations

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

ink

def Sample.thread1 : Mt.Thread Sample.spec

Equations

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

ink

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