@[reducible, inline]

abbrev NatLog.y : HeyLo.Ident

Equations

• NatLog.y = { name := "y", type := HeyLo.Ty.Nat }

@[reducible, inline]

abbrev NatLog.c : HeyLo.Ident

Equations

• NatLog.c = { name := "c", type := HeyLo.Ty.Nat }

def NatLog : Conditions Encoding.wp

Equations

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

theorem NatLog.soundess : NatLog.sound