def f_lt {w e : Nat} (a b : FixedPoint w e) : Bool

Equations

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

def e_lt {w e : Nat} (a b : EFixedPoint w e) : Bool

Equations

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

def e_le {w e : Nat} (a b : EFixedPoint w e) : Bool

Equations

• e_le a b = (a.equal b || e_lt a b)

def lt {w e : Nat} (a b : PackedFloat w e) : Bool

Equations

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

def eq {w e : Nat} (a b : PackedFloat w e) : Bool

Equations

• eq a b = (decide ¬a.isNaN = true && decide ¬b.isNaN = true && (a.sign == b.sign && a.ex == b.ex && a.sig == b.sig || a.ex == 0 && b.ex == 0 && a.sig == 0 && b.sig == 0))

def le {w e : Nat} (a b : PackedFloat w e) : Bool

Equations

• le a b = (eq a b || lt a b)

theorem e_lt_nan {w e : Nat} (a : EFixedPoint w e) : ¬e_lt a (EFixedPoint.getNaN ⋯) = true

theorem nan_lt_e {w e : Nat} (a : EFixedPoint w e) : ¬e_lt (EFixedPoint.getNaN ⋯) a = true