Package hol-monad: HOL monad theories

Information

namehol-monad
version1.1
descriptionHOL monad theories
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksum18a0db39c9736755cadb44129396c27ac35f5342
requiresbase
hol-base
showData.Bool
Data.List
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Constants

Theorems

state_transformer.UNIT = pair.CURRY id

errorStateMonad.UNIT = pair.CURRY Data.Option.some

state_transformer.JOIN = state_transformer.EXT id

state_transformer.EXT state_transformer.UNIT = id

state_transformer.MMAP id = id

errorStateMonad.MMAP id = id

state_transformer.sequence [] = state_transformer.UNIT []

errorStateMonad.sequence [] = errorStateMonad.UNIT []

errorStateMonad.ES_CHOICE errorStateMonad.ES_FAIL xM = xM

errorStateMonad.ES_CHOICE xM errorStateMonad.ES_FAIL = xM

errorStateMonad.BIND errorStateMonad.ES_FAIL fM = errorStateMonad.ES_FAIL

state_transformer.JOIN state_transformer.UNIT = id

errorStateMonad.JOIN errorStateMonad.UNIT = id

s. errorStateMonad.ES_FAIL s = Data.Option.none

state_transformer.mapM f [] = state_transformer.UNIT []

errorStateMonad.mapM f [] = errorStateMonad.UNIT []

state_transformer.EXT f state_transformer.UNIT = f

state_transformer.JOIN state_transformer.MMAP state_transformer.UNIT =
  id

errorStateMonad.JOIN errorStateMonad.MMAP errorStateMonad.UNIT = id

s. pair.UNCURRY state_transformer.UNIT s = s

k. state_transformer.BIND k state_transformer.UNIT = k

k. errorStateMonad.BIND k errorStateMonad.UNIT = k

state_transformer.EXT f =
  state_transformer.JOIN state_transformer.MMAP f

state_transformer.MMAP f =
  state_transformer.EXT (state_transformer.UNIT f)

state_transformer.BIND m f = state_transformer.EXT f m

x. snd state_transformer.UNIT x = id

z. state_transformer.JOIN z = state_transformer.BIND z id

z. errorStateMonad.JOIN z = errorStateMonad.BIND z id

x. state_transformer.UNIT x = λs. (x, s)

errorStateMonad.MCOMP g f = errorStateMonad.EXT g f

errorStateMonad.ES_APPLY (errorStateMonad.UNIT f) xM =
  errorStateMonad.MMAP f xM

state_transformer.JOIN state_transformer.MMAP state_transformer.JOIN =
  state_transformer.JOIN state_transformer.JOIN

errorStateMonad.JOIN errorStateMonad.MMAP errorStateMonad.JOIN =
  errorStateMonad.JOIN errorStateMonad.JOIN

x. fst state_transformer.UNIT x = const x

f. state_transformer.mapM f = state_transformer.sequence map f

f. errorStateMonad.mapM f = errorStateMonad.sequence map f

x. errorStateMonad.UNIT x = λs. Data.Option.some (x, s)

f. state_transformer.WRITE f = λs. (Data.Unit.(), f s)

f. state_transformer.READ f = λs. (f s, s)

errorStateMonad.ES_APPLY (errorStateMonad.UNIT f)
    (errorStateMonad.UNIT x) = errorStateMonad.UNIT (f x)

b.
    errorStateMonad.ES_GUARD b =
    if b then errorStateMonad.UNIT Data.Unit.()
    else errorStateMonad.ES_FAIL

f.
    errorStateMonad.MMAP f errorStateMonad.UNIT =
    errorStateMonad.UNIT f

f.
    state_transformer.MMAP f state_transformer.UNIT =
    state_transformer.UNIT f

f.
    state_transformer.EXT f state_transformer.JOIN =
    state_transformer.EXT (state_transformer.EXT f)

f. errorStateMonad.WRITE f = λs. Data.Option.some (Data.Unit.(), f s)

f. errorStateMonad.READ f = λs. Data.Option.some (f s, s)

k x. state_transformer.BIND (state_transformer.UNIT x) k = k x

k x. errorStateMonad.BIND (errorStateMonad.UNIT x) k = k x

g m. errorStateMonad.EXT g m = errorStateMonad.BIND m g

state_transformer.MCOMP g f =
  pair.CURRY (pair.UNCURRY g pair.UNCURRY f)

state_transformer.EXT (state_transformer.MCOMP g f) =
  state_transformer.EXT g state_transformer.EXT f

f g.
    state_transformer.IGNORE_BIND f g = state_transformer.BIND f (λx. g)

f g. errorStateMonad.IGNORE_BIND f g = errorStateMonad.BIND f (λx. g)

k m.
    state_transformer.BIND k m =
    state_transformer.JOIN (state_transformer.MMAP m k)

g f. state_transformer.BIND g f = pair.UNCURRY f g

k m.
    errorStateMonad.BIND k m =
    errorStateMonad.JOIN (errorStateMonad.MMAP m k)

f m. state_transformer.EXT f m = pair.UNCURRY f m

g f. state_transformer.MCOMP g f = state_transformer.EXT g f

errorStateMonad.ES_CHOICE xM (errorStateMonad.ES_CHOICE yM zM) =
  errorStateMonad.ES_CHOICE (errorStateMonad.ES_CHOICE xM yM) zM

errorStateMonad.MCOMP f (errorStateMonad.MCOMP g h) =
  errorStateMonad.MCOMP (errorStateMonad.MCOMP f g) h

state_transformer.MCOMP f (state_transformer.MCOMP g h) =
  state_transformer.MCOMP (state_transformer.MCOMP f g) h

errorStateMonad.MCOMP g errorStateMonad.UNIT = g
  errorStateMonad.MCOMP errorStateMonad.UNIT f = f

errorStateMonad.IGNORE_BIND errorStateMonad.ES_FAIL xM =
  errorStateMonad.ES_FAIL
  errorStateMonad.IGNORE_BIND xM errorStateMonad.ES_FAIL =
  errorStateMonad.ES_FAIL

state_transformer.MCOMP g state_transformer.UNIT = g
  state_transformer.MCOMP state_transformer.UNIT f = f

f.
    errorStateMonad.MMAP f errorStateMonad.JOIN =
    errorStateMonad.JOIN errorStateMonad.MMAP (errorStateMonad.MMAP f)

f.
    state_transformer.MMAP f state_transformer.JOIN =
    state_transformer.JOIN
    state_transformer.MMAP (state_transformer.MMAP f)

f m.
    state_transformer.MMAP f m =
    state_transformer.BIND m (state_transformer.UNIT f)

f m.
    errorStateMonad.MMAP f m =
    errorStateMonad.BIND m (errorStateMonad.UNIT f)

f g.
    errorStateMonad.MMAP (f g) =
    errorStateMonad.MMAP f errorStateMonad.MMAP g

f g.
    state_transformer.MMAP (f g) =
    state_transformer.MMAP f state_transformer.MMAP g

g f.
    errorStateMonad.MCOMP g f =
    pair.CURRY (option.OPTION_MCOMP (pair.UNCURRY g) (pair.UNCURRY f))

errorStateMonad.IGNORE_BIND (errorStateMonad.ES_GUARD ) xM =
  errorStateMonad.ES_FAIL
  errorStateMonad.IGNORE_BIND (errorStateMonad.ES_GUARD ) xM = xM

state_transformer.MCOMP (state_transformer.UNIT g)
    (state_transformer.UNIT f) = state_transformer.UNIT (g f)

f g. fst state_transformer.MMAP f g = f (fst g)

errorStateMonad.BIND (errorStateMonad.ES_GUARD ) fM =
  errorStateMonad.ES_FAIL
  errorStateMonad.BIND (errorStateMonad.ES_GUARD ) fM = fM Data.Unit.()

f xM yM.
    errorStateMonad.ES_LIFT2 f xM yM =
    errorStateMonad.ES_APPLY (errorStateMonad.MMAP f xM) yM

fM xM.
    errorStateMonad.ES_APPLY fM xM =
    errorStateMonad.BIND fM
      (λf. errorStateMonad.BIND xM (λx. errorStateMonad.UNIT (f x)))

state_transformer.sequence =
  list.FOLDR
    (λm ms.
       state_transformer.BIND m
         (λx.
            state_transformer.BIND ms
              (λxs. state_transformer.UNIT (x :: xs))))
    (state_transformer.UNIT [])

errorStateMonad.sequence =
  list.FOLDR
    (λm ms.
       errorStateMonad.BIND m
         (λx.
            errorStateMonad.BIND ms (λxs. errorStateMonad.UNIT (x :: xs))))
    (errorStateMonad.UNIT [])

f.
    state_transformer.WIDEN f =
    pair.UNCURRY
      (λs1 s2. bool.LET (pair.UNCURRY (λr s3. (r, s1, s3))) (f s2))

xM yM s.
    errorStateMonad.ES_CHOICE xM yM s =
    option.option_CASE (xM s) (yM s) (λv1. Data.Option.some v1)

k m n.
    state_transformer.BIND k (λa. state_transformer.BIND (m a) n) =
    state_transformer.BIND (state_transformer.BIND k m) n

k m n.
    errorStateMonad.BIND k (λa. errorStateMonad.BIND (m a) n) =
    errorStateMonad.BIND (errorStateMonad.BIND k m) n

state_transformer.mapM f (x :: xs) =
  state_transformer.BIND (f x)
    (λy.
       state_transformer.BIND (state_transformer.mapM f xs)
         (λys. state_transformer.UNIT (y :: ys)))

errorStateMonad.mapM f (x :: xs) =
  errorStateMonad.BIND (f x)
    (λy.
       errorStateMonad.BIND (errorStateMonad.mapM f xs)
         (λys. errorStateMonad.UNIT (y :: ys)))

v f.
    state_transformer.NARROW v f =
    λs. bool.LET (pair.UNCURRY (λr s1. (r, snd s1))) (f (v, s))

g b.
    state_transformer.MWHILE g b =
    state_transformer.BIND g
      (λgv.
         if gv then
           state_transformer.IGNORE_BIND b (state_transformer.MWHILE g b)
         else state_transformer.UNIT Data.Unit.())

f.
    errorStateMonad.WIDEN f =
    pair.UNCURRY
      (λs1 s2.
         option.option_CASE (f s2) Data.Option.none
           (λv. pair.pair_CASE v (λr s3. Data.Option.some (r, s1, s3))))

g f s0.
    errorStateMonad.BIND g f s0 =
    option.option_CASE (g s0) Data.Option.none
      (λv. pair.pair_CASE v (λb s. f b s))

v f.
    errorStateMonad.NARROW v f =
    λs.
      option.option_CASE (f (v, s)) Data.Option.none
        (λv. pair.pair_CASE v (λr s1. Data.Option.some (r, snd s1)))

(a.
     state_transformer.FOREACH ([], a) =
     state_transformer.UNIT Data.Unit.())
  t h a.
    state_transformer.FOREACH (h :: t, a) =
    state_transformer.BIND (a h) (λu. state_transformer.FOREACH (t, a))

(a.
     errorStateMonad.FOREACH ([], a) = errorStateMonad.UNIT Data.Unit.())
  t h a.
    errorStateMonad.FOREACH (h :: t, a) =
    errorStateMonad.BIND (a h) (λu. errorStateMonad.FOREACH (t, a))

P.
    (a. P ([], a)) (h t a. P (t, a) P (h :: t, a)) v v1. P (v, v1)

P.
    (a. P ([], a)) (h t a. P (t, a) P (h :: t, a)) v v1. P (v, v1)

j i a.
    state_transformer.FOR (i, j, a) =
    if i = j then a i
    else
      state_transformer.BIND (a i)
        (λu.
           state_transformer.FOR
             ((if i < j then i + 1 else arithmetic.- i 1), j, a))

j i a.
    errorStateMonad.FOR (i, j, a) =
    if i = j then a i
    else
      errorStateMonad.BIND (a i)
        (λu.
           errorStateMonad.FOR
             ((if i < j then i + 1 else arithmetic.- i 1), j, a))

state_transformer.FOREACH =
  relation.WFREC (select R. wellFounded R h a t. R (t, a) (h :: t, a))
    (λFOREACH a'.
       pair.pair_CASE a'
         (λv a.
            list.list_CASE v (id (state_transformer.UNIT Data.Unit.()))
              (λh t.
                 id (state_transformer.BIND (a h) (λu. FOREACH (t, a))))))

errorStateMonad.FOREACH =
  relation.WFREC (select R. wellFounded R h a t. R (t, a) (h :: t, a))
    (λFOREACH a'.
       pair.pair_CASE a'
         (λv a.
            list.list_CASE v (id (errorStateMonad.UNIT Data.Unit.()))
              (λh t.
                 id (errorStateMonad.BIND (a h) (λu. FOREACH (t, a))))))

P.
    (i j a.
       (¬(i = j) P ((if i < j then i + 1 else arithmetic.- i 1), j, a))
       P (i, j, a)) v v1 v2. P (v, v1, v2)

P.
    (i j a.
       (¬(i = j) P ((if i < j then i + 1 else arithmetic.- i 1), j, a))
       P (i, j, a)) v v1 v2. P (v, v1, v2)

state_transformer.FOR =
  relation.WFREC
    (select R.
       wellFounded R
       a j i.
         ¬(i = j)
         R ((if i < j then i + 1 else arithmetic.- i 1), j, a) (i, j, a))
    (λFOR a'.
       pair.pair_CASE a'
         (λi v1.
            pair.pair_CASE v1
              (λj a.
                 id
                   (if i = j then a i
                    else
                      state_transformer.BIND (a i)
                        (λu.
                           FOR
                             ((if i < j then i + 1 else arithmetic.- i 1),
                              j, a))))))

errorStateMonad.FOR =
  relation.WFREC
    (select R.
       wellFounded R
       a j i.
         ¬(i = j)
         R ((if i < j then i + 1 else arithmetic.- i 1), j, a) (i, j, a))
    (λFOR a'.
       pair.pair_CASE a'
         (λi v1.
            pair.pair_CASE v1
              (λj a.
                 id
                   (if i = j then a i
                    else
                      errorStateMonad.BIND (a i)
                        (λu.
                           FOR
                             ((if i < j then i + 1 else arithmetic.- i 1),
                              j, a))))))

External Type Operators

External Constants

Assumptions

wellFounded (<)

prim_rec.measure = relation.inv_image (<)

t. t

n. 0 n

m. wellFounded (prim_rec.measure m)

x. id x = x

t. t ¬t

x. marker.Abbrev x x

(¬) = λt. t

() = λP. P ((select) P)

a. x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

arithmetic.BIT2 0 = suc 1

arithmetic.FUNPOW f 0 x = x

¬(p q) p

x. ¬(Data.Option.none = Data.Option.some x)

x. x = x

f. pair.CURRY (pair.UNCURRY f) = f

f. pair.UNCURRY (pair.CURRY f) = f

¬(p q) ¬q

A. A ¬A

t. ¬t t

x y. const x y = x

() = λp q. p q p

t. t t

t. (t ) (t )

n. suc n = 1 + n

x. (fst x, snd x) = x

x y. fst (x, y) = x

x y. snd (x, y) = y

f x. bool.LET f x = f x

P x. P x P ((select) P)

f (λx. g x) = λx. f (g x)

flip (λx. f x) y = λx. f x y

pair.pair_CASE (x, y) f = f x y

n. arithmetic.BIT2 0 * n = n + n

x. q r. x = (q, r)

x y. x = y y = x

m n. m + n = n + m

R f. wellFounded R wellFounded (relation.inv_image R f)

P (bool.LET f v) = bool.LET (P f) v

bool.LET f v x = bool.LET (flip f x) v

(¬A ) (A )

Combinator.s f (λx. g x) = λx. f x (g x)

f g. f g = λx. f (g x)

A B. A B ¬A B

m n. m < n suc m n

m n. ¬(m < n) n m

m. m = 0 n. m = suc n

opt. opt = Data.Option.none x. opt = Data.Option.some x

() = λp q. (λf. f p q) = λf. f

option.OPTION_MCOMP f (option.OPTION_MCOMP g h) =
  option.OPTION_MCOMP (option.OPTION_MCOMP f g) h

option.OPTION_MCOMP g Data.Option.some = g
  option.OPTION_MCOMP Data.Option.some f = f

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

x y. Data.Option.some x = Data.Option.some y x = y

A B. ¬(A B) A ¬B

m n. suc m = suc n m = n

m n. suc m < suc n m < n

p f. pair.pair_CASE p f = f (fst p) (snd p)

f v. pair.UNCURRY f v = f (fst v) (snd v)

m. arithmetic.- 0 m = 0 arithmetic.- m 0 = m

f g x. (f g) x = f (g x)

f. id f = f f id = f

f x y. flip f x y = f y x

R f. relation.inv_image R f = λx y. R (f x) (f y)

l. l = [] h t. l = h :: t

f g. f = g x. f x = g x

f g. (x. f x = g x) f = g

P a. (x. x = a P x) P a

g f m. option.OPTION_MCOMP g f m = option.OPTION_BIND (f m) g

f x y. pair.UNCURRY f (x, y) = f x y

f x y. pair.CURRY f x y = f (x, y)

() = λt1 t2. t. (t1 t) (t2 t) t

t1 t2. (t1 t2) (t2 t1) (t1 t2)

m n. m = n m n n m

bool.LET f v () (Combinator.s (() (marker.Abbrev flip (=) v)) f)

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

¬(A B) (A ) ¬B

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

m n p. m < arithmetic.- n p m + p < n

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. arithmetic.- (arithmetic.- m n) p = arithmetic.- m (n + p)

m n p. m + n m + p n p

m n p. m n n p m p

f g h. f (g h) = f g h

P. (x. y. P x y) f. x. P x (f x)

t1 t2. (if then t1 else t2) = t1 (if then t1 else t2) = t2

t1 t2. (t1 t2) t1 t2 ¬t1 ¬t2

(t. ¬¬t t) (¬ ) (¬ )

m n. ¬(m = n) suc m n suc n m

m n p. m n suc p * m suc p * n

m n p. p * (m + n) = p * m + p * n

m n p. (m + n) * p = m * p + n * p

(f. option.OPTION_BIND Data.Option.none f = Data.Option.none)
  x f. option.OPTION_BIND (Data.Option.some x) f = f x

b f g x. (if b then f else g) x = if b then f x else g x

f b x y. f (if b then x else y) = if b then f x else f y

f R y z. R y z relation.RESTRICT f R z y = f y

(t1 t2. (if then t1 else t2) = t1)
  t1 t2. (if then t1 else t2) = t2

m n p. arithmetic.- m n < p m < n + p 0 < p

x y a b. (x, y) = (a, b) x = a y = b

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

R. wellFounded R P. (x. (y. R y x P y) P x) x. P x

(v f. option.option_CASE Data.Option.none v f = v)
  x v f. option.option_CASE (Data.Option.some x) v f = f x

x x' y y'. (x x') (x' (y y')) (x y x' y')

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
  n. suc (arithmetic.BIT2 n) = bit1 (suc n)

P (arithmetic.- a b) d. (b = a + d P 0) (a = b + d P d)

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

M R f.
    f = relation.WFREC R M wellFounded R
    x. f x = M (relation.RESTRICT f R x) x

(f. map f [] = []) f h t. map f (h :: t) = f h :: map f t

P P' Q Q'. (Q (P P')) (P' (Q Q')) (P Q P' Q')

(f x. arithmetic.FUNPOW f 0 x = x)
  f n x. arithmetic.FUNPOW f (suc n) x = arithmetic.FUNPOW f n (f x)

(v f. list.list_CASE [] v f = v)
  a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

(f. list.list_size f [] = 0)
  f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)

Q P.
    (n. P n) (n. (m. m < n ¬P m) P n Q n) Q (while.LEAST P)

(f e. list.FOLDR f e [] = e)
  f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

0 + m = m m + 0 = m suc m + n = suc (m + n) m + suc n = suc (m + n)

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

P Q x x' y y'.
    (P Q) (Q x = x') (¬Q y = y')
    (if P then x else y) = if Q then x' else y'

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

m n.
    0 * m = 0 m * 0 = 0 1 * m = m m * 1 = m suc m * n = m * n + n
    m * suc n = m + m * n

n m.
    (0 n ) (bit1 n 0 ) (arithmetic.BIT2 n 0 )
    (bit1 n bit1 m n m) (bit1 n arithmetic.BIT2 m n m)
    (arithmetic.BIT2 n bit1 m ¬(m n))
    (arithmetic.BIT2 n arithmetic.BIT2 m n m)

n m.
    (0 < bit1 n ) (0 < arithmetic.BIT2 n ) (n < 0 )
    (bit1 n < bit1 m n < m)
    (arithmetic.BIT2 n < arithmetic.BIT2 m n < m)
    (bit1 n < arithmetic.BIT2 m ¬(m < n))
    (arithmetic.BIT2 n < bit1 m n < m)

n m.
    numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
    numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
    numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
    suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
    suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (0 + n) = numeral.iiSUC n
    numeral.iiSUC (n + 0) = numeral.iiSUC n
    numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (numeral.iiSUC (n + m))

(n. 0 + n = n) (n. n + 0 = n) (n m. n + m = numeral.iZ (n + m))
  (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
  (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
  (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
  (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
  (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
  prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
  (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
  (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
  (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
  (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
  (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
  (n. odd n odd n) (n. even n even n) ¬odd 0 even 0