Theory "ieee"

Parents transc

Signature

Type	Arity
roundmode	0
float	0
ccode	0
Constant	Type
zerosign	:num # num -> num -> num # num # num -> num # num # num
wordlength	:num # num -> num
valof	:num # num -> num # num # num -> real
ulp	:num # num -> num # num # num -> real
topfloat	:num # num -> num # num # num
threshold	:num # num -> real
some_nan	:num # num -> num # num # num
sign	:num # num # num -> num
roundmode_size	:roundmode -> num
roundmode_case	:'a -> 'a -> 'a -> 'a -> roundmode -> 'a
roundmode2num	:roundmode -> num
round	:num # num -> roundmode -> real -> num # num # num
rem	:real -> real -> real
plus_zero	:num # num -> num # num # num
plus_infinity	:num # num -> num # num # num
num2roundmode	:num -> roundmode
num2ccode	:num -> ccode
minus_zero	:num # num -> num # num # num
minus_infinity	:num # num -> num # num # num
minus	:num # num -> num # num # num -> num # num # num
largest	:num # num -> real
is_zero	:num # num -> num # num # num -> bool
is_valid	:num # num -> num # num # num -> bool
is_single_extended	:num # num -> bool
is_single	:num # num -> bool
is_normal	:num # num -> num # num # num -> bool
is_nan	:num # num -> num # num # num -> bool
is_integral	:num # num -> num # num # num -> bool
is_infinity	:num # num -> num # num # num -> bool
is_finite	:num # num -> num # num # num -> bool
is_double_extended	:num # num -> bool
is_double	:num # num -> bool
is_denormal	:num # num -> num # num # num -> bool
is_closest	:('a -> real) -> ('a -> bool) -> real -> 'a -> bool
intround	:num # num -> roundmode -> real -> num # num # num
fsub	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fsqrt	:num # num -> roundmode -> num # num # num -> num # num # num
frem	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fracwidth	:num # num -> num
fraction	:num # num # num -> num
fneg	:num # num -> roundmode -> num # num # num -> num # num # num
fmul	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
flt	:num # num -> num # num # num -> num # num # num -> bool
float_sub	:float -> float -> float
float_sqrt	:float -> float
float_rem	:float -> float -> float
float_neg	:float -> float
float_mul	:float -> float -> float
float_lt	:float -> float -> bool
float_le	:float -> float -> bool
float_gt	:float -> float -> bool
float_ge	:float -> float -> bool
float_format	:num # num
float_eq	:float -> float -> bool
float_div	:float -> float -> float
float_add	:float -> float -> float
float_abs	:float -> float
float_To_zero	:roundmode
float	:num # num # num -> float
fle	:num # num -> num # num # num -> num # num # num -> bool
fintrnd	:num # num -> roundmode -> num # num # num -> num # num # num
fgt	:num # num -> num # num # num -> num # num # num -> bool
fge	:num # num -> num # num # num -> num # num # num -> bool
feq	:num # num -> num # num # num -> num # num # num -> bool
fdiv	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
fcompare	:num # num -> num # num # num -> num # num # num -> ccode
fadd	:num # num -> roundmode -> num # num # num -> num # num # num -> num # num # num
expwidth	:num # num -> num
exponent	:num # num # num -> num
encoding	:num # num -> num # num # num -> num
emax	:num # num -> num
defloat	:float -> num # num # num
closest	:('a -> real) -> ('a -> bool) -> ('a -> bool) -> real -> 'a
ccode_size	:ccode -> num
ccode_case	:'a -> 'a -> 'a -> 'a -> ccode -> 'a
ccode2num	:ccode -> num
bottomfloat	:num # num -> num # num # num
bias	:num # num -> num
Val	:float -> real
Un	:ccode
Ulp	:float -> real
To_pinfinity	:roundmode
To_ninfinity	:roundmode
To_nearest	:roundmode
Sign	:float -> num
ROUNDFLOAT	:float -> float
Plus_zero	:float
Plus_infinity	:float
Minus_zero	:float
Minus_infinity	:float
Lt	:ccode
Iszero	:float -> bool
Isnormal	:float -> bool
Isnan	:float -> bool
Isintegral	:float -> bool
Isdenormal	:float -> bool
Infinity	:float -> bool
Gt	:ccode
Fraction	:float -> num
Float	:real -> float
Finite	:float -> bool
Exponent	:float -> num
Eq	:ccode

Definitions

expwidth

|- !ew fw. expwidth (ew,fw) = ew

fracwidth

|- !ew fw. fracwidth (ew,fw) = fw

wordlength

|- !X. wordlength X = expwidth X + fracwidth X + 1

emax

|- !X. emax X = 2 ** expwidth X - 1

bias

|- !X. bias X = 2 ** (expwidth X - 1) - 1

is_single

|- !X. is_single X = (expwidth X = 8) /\ (wordlength X = 32)

is_double

|- !X. is_double X = (expwidth X = 11) /\ (wordlength X = 64)

is_single_extended

|- !X. is_single_extended X = expwidth X >= 11 /\ wordlength X >= 43

is_double_extended

|- !X. is_double_extended X = expwidth X >= 15 /\ wordlength X >= 79

sign

|- !s e f. sign (s,e,f) = s

exponent

|- !s e f. exponent (s,e,f) = e

fraction

|- !s e f. fraction (s,e,f) = f

is_nan

|- !X a. is_nan X a = (exponent a = emax X) /\ ~(fraction a = 0)

is_infinity

|- !X a. is_infinity X a = (exponent a = emax X) /\ (fraction a = 0)

is_normal

|- !X a. is_normal X a = 0 < exponent a /\ exponent a < emax X

is_denormal

|- !X a. is_denormal X a = (exponent a = 0) /\ ~(fraction a = 0)

is_zero

|- !X a. is_zero X a = (exponent a = 0) /\ (fraction a = 0)

is_valid

|- !X s e f.
     is_valid X (s,e,f) =
     s < SUC (SUC 0) /\ e < 2 ** expwidth X /\ f < 2 ** fracwidth X

is_finite

|- !X a.
     is_finite X a =
     is_valid X a /\ (is_normal X a \/ is_denormal X a \/ is_zero X a)

plus_infinity

|- !X. plus_infinity X = (0,emax X,0)

minus_infinity

|- !X. minus_infinity X = (1,emax X,0)

plus_zero

|- !X. plus_zero X = (0,0,0)

minus_zero

|- !X. minus_zero X = (1,0,0)

topfloat

|- !X. topfloat X = (0,emax X - 1,2 ** fracwidth X - 1)

bottomfloat

|- !X. bottomfloat X = (1,emax X - 1,2 ** fracwidth X - 1)

minus

|- !X a. minus X a = (1 - sign a,exponent a,fraction a)

encoding

|- !X s e f.
     encoding X (s,e,f) =
     s * 2 ** (wordlength X - 1) + e * 2 ** fracwidth X + f

valof

|- !X s e f.
     valof X (s,e,f) =
     (if e = 0 then
        ~1 pow s * (2 / 2 pow bias X) * (& f / 2 pow fracwidth X)
      else
        ~1 pow s * (2 pow e / 2 pow bias X) * (1 + & f / 2 pow fracwidth X))

largest

|- !X.
     largest X =
     2 pow (emax X - 1) / 2 pow bias X * (2 - inv (2 pow fracwidth X))

threshold

|- !X.
     threshold X =
     2 pow (emax X - 1) / 2 pow bias X * (2 - inv (2 pow SUC (fracwidth X)))

ulp

|- !X a. ulp X a = valof X (0,exponent a,1) - valof X (0,exponent a,0)

roundmode_TY_DEF

|- ?rep. TYPE_DEFINITION (\n. n < 4) rep

roundmode_BIJ

|- (!a. num2roundmode (roundmode2num a) = a) /\
   !r. (\n. n < 4) r = (roundmode2num (num2roundmode r) = r)

To_nearest

|- To_nearest = num2roundmode 0

float_To_zero

|- float_To_zero = num2roundmode 1

To_pinfinity

|- To_pinfinity = num2roundmode 2

To_ninfinity

|- To_ninfinity = num2roundmode 3

roundmode_size_def

|- !x. roundmode_size x = 0

roundmode_case

|- !v0 v1 v2 v3 x.
     (case x of
         To_nearest -> v0
      || float_To_zero -> v1
      || To_pinfinity -> v2
      || To_ninfinity -> v3) =
     (\m.
        (if m < 1 then
           v0
         else
           (if m < 2 then v1 else (if m = 2 then v2 else v3))))
       (roundmode2num x)

is_closest

|- !v s x a.
     is_closest v s x a =
     a IN s /\ !b. b IN s ==> abs (v a - x) <= abs (v b - x)

closest

|- !v p s x.
     closest v p s x =
     @a. is_closest v s x a /\ ((?b. is_closest v s x b /\ p b) ==> p a)

round_def

|- (!X x.
      round X To_nearest x =
      (if x <= ~threshold X then
         minus_infinity X
       else
         (if x >= threshold X then
            plus_infinity X
          else
            closest (valof X) (\a. EVEN (fraction a)) {a | is_finite X a}
              x))) /\
   (!X x.
      round X float_To_zero x =
      (if x < ~largest X then
         bottomfloat X
       else
         (if x > largest X then
            topfloat X
          else
            closest (valof X) (\x. T)
              {a | is_finite X a /\ abs (valof X a) <= abs x} x))) /\
   (!X x.
      round X To_pinfinity x =
      (if x < ~largest X then
         bottomfloat X
       else
         (if x > largest X then
            plus_infinity X
          else
            closest (valof X) (\x. T) {a | is_finite X a /\ valof X a >= x}
              x))) /\
   !X x.
     round X To_ninfinity x =
     (if x < ~largest X then
        minus_infinity X
      else
        (if x > largest X then
           topfloat X
         else
           closest (valof X) (\x. T) {a | is_finite X a /\ valof X a <= x} x))

is_integral

|- !X a. is_integral X a = is_finite X a /\ ?n. abs (valof X a) = & n

intround_def

|- (!X x.
      intround X To_nearest x =
      (if x <= ~threshold X then
         minus_infinity X
       else
         (if x >= threshold X then
            plus_infinity X
          else
            closest (valof X) (\a. ?n. EVEN n /\ (abs (valof X a) = & n))
              {a | is_integral X a} x))) /\
   (!X x.
      intround X float_To_zero x =
      (if x < ~largest X then
         bottomfloat X
       else
         (if x > largest X then
            topfloat X
          else
            closest (valof X) (\x. T)
              {a | is_integral X a /\ abs (valof X a) <= abs x} x))) /\
   (!X x.
      intround X To_pinfinity x =
      (if x < ~largest X then
         bottomfloat X
       else
         (if x > largest X then
            plus_infinity X
          else
            closest (valof X) (\x. T) {a | is_integral X a /\ valof X a >= x}
              x))) /\
   !X x.
     intround X To_ninfinity x =
     (if x < ~largest X then
        minus_infinity X
      else
        (if x > largest X then
           topfloat X
         else
           closest (valof X) (\x. T) {a | is_integral X a /\ valof X a <= x}
             x))

some_nan

|- !X. some_nan X = @a. is_nan X a

zerosign

|- !X s a.
     zerosign X s a =
     (if is_zero X a then
        (if s = 0 then plus_zero X else minus_zero X)
      else
        a)

rem

|- !x y.
     x rem y =
     (let n =
            closest I (\x. ?n. EVEN n /\ (abs x = & n)) {x | ?n. abs x = & n}
              (x / y)
      in
        x - n * y)

fintrnd

|- !X m a.
     fintrnd X m a =
     (if is_nan X a then
        some_nan X
      else
        (if is_infinity X a then
           a
         else
           zerosign X (sign a) (intround X m (valof X a))))

fadd

|- !X m a b.
     fadd X m a b =
     (if
        is_nan X a \/ is_nan X b \/
        is_infinity X a /\ is_infinity X b /\ ~(sign a = sign b)
      then
        some_nan X
      else
        (if is_infinity X a then
           a
         else
           (if is_infinity X b then
              b
            else
              zerosign X
                (if is_zero X a /\ is_zero X b /\ (sign a = sign b) then
                   sign a
                 else
                   (if m = To_ninfinity then 1 else 0))
                (round X m (valof X a + valof X b)))))

fsub

|- !X m a b.
     fsub X m a b =
     (if
        is_nan X a \/ is_nan X b \/
        is_infinity X a /\ is_infinity X b /\ (sign a = sign b)
      then
        some_nan X
      else
        (if is_infinity X a then
           a
         else
           (if is_infinity X b then
              minus X b
            else
              zerosign X
                (if is_zero X a /\ is_zero X b /\ ~(sign a = sign b) then
                   sign a
                 else
                   (if m = To_ninfinity then 1 else 0))
                (round X m (valof X a - valof X b)))))

fmul

|- !X m a b.
     fmul X m a b =
     (if
        is_nan X a \/ is_nan X b \/ is_zero X a /\ is_infinity X b \/
        is_infinity X a /\ is_zero X b
      then
        some_nan X
      else
        (if is_infinity X a \/ is_infinity X b then
           (if sign a = sign b then plus_infinity X else minus_infinity X)
         else
           zerosign X (if sign a = sign b then 0 else 1)
             (round X m (valof X a * valof X b))))

fdiv

|- !X m a b.
     fdiv X m a b =
     (if
        is_nan X a \/ is_nan X b \/ is_zero X a /\ is_zero X b \/
        is_infinity X a /\ is_infinity X b
      then
        some_nan X
      else
        (if is_infinity X a \/ is_zero X b then
           (if sign a = sign b then plus_infinity X else minus_infinity X)
         else
           (if is_infinity X b then
              (if sign a = sign b then plus_zero X else minus_zero X)
            else
              zerosign X (if sign a = sign b then 0 else 1)
                (round X m (valof X a / valof X b)))))

fsqrt

|- !X m a.
     fsqrt X m a =
     (if is_nan X a then
        some_nan X
      else
        (if is_zero X a \/ is_infinity X a /\ (sign a = 0) then
           a
         else
           (if sign a = 1 then
              some_nan X
            else
              zerosign X (sign a) (round X m (sqrt (valof X a))))))

frem

|- !X m a b.
     frem X m a b =
     (if is_nan X a \/ is_nan X b \/ is_infinity X a \/ is_zero X b then
        some_nan X
      else
        (if is_infinity X b then
           a
         else
           zerosign X (sign a) (round X m (valof X a rem valof X b))))

fneg

|- !X m a. fneg X m a = (1 - sign a,exponent a,fraction a)

ccode_TY_DEF

|- ?rep. TYPE_DEFINITION (\n. n < 4) rep

ccode_BIJ

|- (!a. num2ccode (ccode2num a) = a) /\
   !r. (\n. n < 4) r = (ccode2num (num2ccode r) = r)

Gt

|- Gt = num2ccode 0

Lt

|- Lt = num2ccode 1

Eq

|- Eq = num2ccode 2

Un

|- Un = num2ccode 3

ccode_size_def

|- !x. ccode_size x = 0

ccode_case

|- !v0 v1 v2 v3 x.
     (case x of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) =
     (\m.
        (if m < 1 then
           v0
         else
           (if m < 2 then v1 else (if m = 2 then v2 else v3)))) (ccode2num x)

fcompare

|- !X a b.
     fcompare X a b =
     (if is_nan X a \/ is_nan X b then
        Un
      else
        (if is_infinity X a /\ (sign a = 1) then
           (if is_infinity X b /\ (sign b = 1) then Eq else Lt)
         else
           (if is_infinity X a /\ (sign a = 0) then
              (if is_infinity X b /\ (sign b = 0) then Eq else Gt)
            else
              (if is_infinity X b /\ (sign b = 1) then
                 Gt
               else
                 (if is_infinity X b /\ (sign b = 0) then
                    Lt
                  else
                    (if valof X a < valof X b then
                       Lt
                     else
                       (if valof X a = valof X b then Eq else Gt)))))))

flt

|- !X a b. flt X a b = (fcompare X a b = Lt)

fle

|- !X a b. fle X a b = (fcompare X a b = Lt) \/ (fcompare X a b = Eq)

fgt

|- !X a b. fgt X a b = (fcompare X a b = Gt)

fge

|- !X a b. fge X a b = (fcompare X a b = Gt) \/ (fcompare X a b = Eq)

feq

|- !X a b. feq X a b = (fcompare X a b = Eq)

float_format

|- float_format = (8,23)

float_TY_DEF

|- ?rep. TYPE_DEFINITION (is_valid float_format) rep

float_tybij

|- (!a. float (defloat a) = a) /\
   !r. is_valid float_format r = (defloat (float r) = r)

Val

|- !a. Val a = valof float_format (defloat a)

Float

|- !x. Float x = float (round float_format To_nearest x)

Sign

|- !a. Sign a = sign (defloat a)

Exponent

|- !a. Exponent a = exponent (defloat a)

Fraction

|- !a. Fraction a = fraction (defloat a)

Ulp

|- !a. Ulp a = ulp float_format (defloat a)

Isnan

|- !a. Isnan a = is_nan float_format (defloat a)

Infinity

|- !a. Infinity a = is_infinity float_format (defloat a)

Isnormal

|- !a. Isnormal a = is_normal float_format (defloat a)

Isdenormal

|- !a. Isdenormal a = is_denormal float_format (defloat a)

Iszero

|- !a. Iszero a = is_zero float_format (defloat a)

Finite

|- !a. Finite a = Isnormal a \/ Isdenormal a \/ Iszero a

Isintegral

|- !a. Isintegral a = is_integral float_format (defloat a)

Plus_zero

|- Plus_zero = float (plus_zero float_format)

Minus_zero

|- Minus_zero = float (minus_zero float_format)

Minus_infinity

|- Minus_infinity = float (minus_infinity float_format)

Plus_infinity

|- Plus_infinity = float (plus_infinity float_format)

float_add

|- !a b. a + b = float (fadd float_format To_nearest (defloat a) (defloat b))

float_sub

|- !a b. a - b = float (fsub float_format To_nearest (defloat a) (defloat b))

float_mul

|- !a b. a * b = float (fmul float_format To_nearest (defloat a) (defloat b))

float_div

|- !a b. a / b = float (fdiv float_format To_nearest (defloat a) (defloat b))

float_rem

|- !a b.
     a float_rem b =
     float (frem float_format To_nearest (defloat a) (defloat b))

float_sqrt

|- !a. float_sqrt a = float (fsqrt float_format To_nearest (defloat a))

ROUNDFLOAT

|- !a. ROUNDFLOAT a = float (fintrnd float_format To_nearest (defloat a))

float_lt

|- !a b. a < b = flt float_format (defloat a) (defloat b)

float_le

|- !a b. a <= b = fle float_format (defloat a) (defloat b)

float_gt

|- !a b. a > b = fgt float_format (defloat a) (defloat b)

float_ge

|- !a b. a >= b = fge float_format (defloat a) (defloat b)

float_eq

|- !a b. a == b = feq float_format (defloat a) (defloat b)

float_neg

|- !a. ~a = float (fneg float_format To_nearest (defloat a))

float_abs

|- !a. float_abs a = (if a >= Plus_zero then a else ~a)

Theorems

num2roundmode_roundmode2num

|- !a. num2roundmode (roundmode2num a) = a

roundmode2num_num2roundmode

|- !r. r < 4 = (roundmode2num (num2roundmode r) = r)

num2roundmode_11

|- !r r'.
     r < 4 ==> r' < 4 ==> ((num2roundmode r = num2roundmode r') = (r = r'))

roundmode2num_11

|- !a a'. (roundmode2num a = roundmode2num a') = (a = a')

num2roundmode_ONTO

|- !a. ?r. (a = num2roundmode r) /\ r < 4

roundmode2num_ONTO

|- !r. r < 4 = ?a. r = roundmode2num a

num2roundmode_thm

|- (num2roundmode 0 = To_nearest) /\ (num2roundmode 1 = float_To_zero) /\
   (num2roundmode 2 = To_pinfinity) /\ (num2roundmode 3 = To_ninfinity)

roundmode2num_thm

|- (roundmode2num To_nearest = 0) /\ (roundmode2num float_To_zero = 1) /\
   (roundmode2num To_pinfinity = 2) /\ (roundmode2num To_ninfinity = 3)

roundmode_EQ_roundmode

|- !a a'. (a = a') = (roundmode2num a = roundmode2num a')

roundmode_case_def

|- (!v0 v1 v2 v3.
      (case To_nearest of
          To_nearest -> v0
       || float_To_zero -> v1
       || To_pinfinity -> v2
       || To_ninfinity -> v3) =
      v0) /\
   (!v0 v1 v2 v3.
      (case float_To_zero of
          To_nearest -> v0
       || float_To_zero -> v1
       || To_pinfinity -> v2
       || To_ninfinity -> v3) =
      v1) /\
   (!v0 v1 v2 v3.
      (case To_pinfinity of
          To_nearest -> v0
       || float_To_zero -> v1
       || To_pinfinity -> v2
       || To_ninfinity -> v3) =
      v2) /\
   !v0 v1 v2 v3.
     (case To_ninfinity of
         To_nearest -> v0
      || float_To_zero -> v1
      || To_pinfinity -> v2
      || To_ninfinity -> v3) =
     v3

datatype_roundmode

|- DATATYPE (roundmode To_nearest float_To_zero To_pinfinity To_ninfinity)

roundmode_distinct

|- ~(To_nearest = float_To_zero) /\ ~(To_nearest = To_pinfinity) /\
   ~(To_nearest = To_ninfinity) /\ ~(float_To_zero = To_pinfinity) /\
   ~(float_To_zero = To_ninfinity) /\ ~(To_pinfinity = To_ninfinity)

roundmode_case_cong

|- !M M' v0 v1 v2 v3.
     (M = M') /\ ((M' = To_nearest) ==> (v0 = v0')) /\
     ((M' = float_To_zero) ==> (v1 = v1')) /\
     ((M' = To_pinfinity) ==> (v2 = v2')) /\
     ((M' = To_ninfinity) ==> (v3 = v3')) ==>
     ((case M of
          To_nearest -> v0
       || float_To_zero -> v1
       || To_pinfinity -> v2
       || To_ninfinity -> v3) =
      case M' of
         To_nearest -> v0'
      || float_To_zero -> v1'
      || To_pinfinity -> v2'
      || To_ninfinity -> v3')

roundmode_nchotomy

|- !a.
     (a = To_nearest) \/ (a = float_To_zero) \/ (a = To_pinfinity) \/
     (a = To_ninfinity)

roundmode_Axiom

|- !x0 x1 x2 x3.
     ?f.
       (f To_nearest = x0) /\ (f float_To_zero = x1) /\
       (f To_pinfinity = x2) /\ (f To_ninfinity = x3)

roundmode_induction

|- !P.
     P To_nearest /\ P To_ninfinity /\ P To_pinfinity /\ P float_To_zero ==>
     !a. P a

num2ccode_ccode2num

|- !a. num2ccode (ccode2num a) = a

ccode2num_num2ccode

|- !r. r < 4 = (ccode2num (num2ccode r) = r)

num2ccode_11

|- !r r'. r < 4 ==> r' < 4 ==> ((num2ccode r = num2ccode r') = (r = r'))

ccode2num_11

|- !a a'. (ccode2num a = ccode2num a') = (a = a')

num2ccode_ONTO

|- !a. ?r. (a = num2ccode r) /\ r < 4

ccode2num_ONTO

|- !r. r < 4 = ?a. r = ccode2num a

num2ccode_thm

|- (num2ccode 0 = Gt) /\ (num2ccode 1 = Lt) /\ (num2ccode 2 = Eq) /\
   (num2ccode 3 = Un)

ccode2num_thm

|- (ccode2num Gt = 0) /\ (ccode2num Lt = 1) /\ (ccode2num Eq = 2) /\
   (ccode2num Un = 3)

ccode_EQ_ccode

|- !a a'. (a = a') = (ccode2num a = ccode2num a')

ccode_case_def

|- (!v0 v1 v2 v3.
      (case Gt of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) = v0) /\
   (!v0 v1 v2 v3.
      (case Lt of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) = v1) /\
   (!v0 v1 v2 v3.
      (case Eq of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) = v2) /\
   !v0 v1 v2 v3.
     (case Un of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) = v3

datatype_ccode

|- DATATYPE (ccode Gt Lt Eq Un)

ccode_distinct

|- ~(Gt = Lt) /\ ~(Gt = Eq) /\ ~(Gt = Un) /\ ~(Lt = Eq) /\ ~(Lt = Un) /\
   ~(Eq = Un)

ccode_case_cong

|- !M M' v0 v1 v2 v3.
     (M = M') /\ ((M' = Gt) ==> (v0 = v0')) /\ ((M' = Lt) ==> (v1 = v1')) /\
     ((M' = Eq) ==> (v2 = v2')) /\ ((M' = Un) ==> (v3 = v3')) ==>
     ((case M of Gt -> v0 || Lt -> v1 || Eq -> v2 || Un -> v3) =
      case M' of Gt -> v0' || Lt -> v1' || Eq -> v2' || Un -> v3')

ccode_nchotomy

|- !a. (a = Gt) \/ (a = Lt) \/ (a = Eq) \/ (a = Un)

ccode_Axiom

|- !x0 x1 x2 x3. ?f. (f Gt = x0) /\ (f Lt = x1) /\ (f Eq = x2) /\ (f Un = x3)

ccode_induction

|- !P. P Eq /\ P Gt /\ P Lt /\ P Un ==> !a. P a