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 gt {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)

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

Equations

• ge a b = (eq a b || gt a b)

def flt_min {e s : Nat} (a b : PackedFloat e s) : PackedFloat e s

Equations

• flt_min a b = if (a.isNaN && b.isNaN) = true then PackedFloat.getNaN e s else if (b.isNaN || lt a b || a.isZero && b.isZero && a.isSignMinus) = true then a else b

def flt_max {e s : Nat} (a b : PackedFloat e s) : PackedFloat e s

Equations

• flt_max a b = if (a.isNaN && b.isNaN) = true then PackedFloat.getNaN e s else if (b.isNaN || gt a b || a.isZero && b.isZero && b.isSignMinus) = true then a else b

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

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