Package machine-code-hoare-logic-state: Machine code Hoare logic state

Information

namemachine-code-hoare-logic-state
version1.0
descriptionMachine code Hoare logic state
authorHOL developers <hol-developers@lists.sourceforge.net>
licenseMIT
checksum6bd4c43462387d9d6c57c13447b5a598a3be51e3
requiresbase
hol-base
hol-words
machine-code-hoare-logic
showData.Bool
Data.List
Data.Option
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Constants

Theorems

relation.PreOrder (=)

x. set_sep.SEP_EQ x = pred_set.INSERT x pred_set.EMPTY

m. state.STATE m = state.SELECT_STATE m pred_set.UNIV

x c q. temporal_state.TEMPORAL_NEXT x set_sep.SEP_F c q

m d. state.FRAME_STATE m d = state.SELECT_STATE m (pred_set.COMPL d)

next. state.NEXT_REL (=) next = λs t. next s = some t

f x.
    pred_set.BIGUNION
      (pred_set.IMAGE f (pred_set.INSERT x pred_set.EMPTY)) = f x

instr c.
    prog.CODE_POOL instr c =
    pred_set.INSERT (pred_set.BIGUNION (pred_set.IMAGE instr c))
      pred_set.EMPTY

m x s. set_sep.emp (state.SELECT_STATE m x s) x = pred_set.EMPTY

m d s. state.SELECT_STATE m d s = set_sep.fun2set (m s, d)

(p. set_sep.STAR p (set_sep.cond ) = p)
  p. set_sep.STAR (set_sep.cond ) p = p

q = pred_set.UNION p1 p2 pred_set.DISJOINT p1 p2
  set_sep.STAR (set_sep.SEP_EQ p1) (set_sep.SEP_EQ p2) = set_sep.SEP_EQ q

f x y.
    pred_set.BIGUNION
      (pred_set.IMAGE f
         (pred_set.INSERT x (pred_set.INSERT y pred_set.EMPTY))) =
    pred_set.UNION (f x) (f y)

m x y s t. state.FRAME_STATE m x s = state.FRAME_STATE m y t x = y

r next s t. state.NEXT_REL r next s t u. r s u next u = some t

x p c q.
    temporal_state.TEMPORAL_NEXT x p c q
    r.
      temporal_state.TEMPORAL_NEXT x (set_sep.STAR p r) c
        (set_sep.STAR q r)

x p c q g.
    temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c q
    g temporal_state.TEMPORAL_NEXT x p c q

a b c.
    pred_set.DISJOINT a b
    set_sep.STAR (pred_set.INSERT (pred_set.UNION a b) pred_set.EMPTY) c =
    set_sep.STAR
      (set_sep.STAR (pred_set.INSERT a pred_set.EMPTY)
         (pred_set.INSERT b pred_set.EMPTY)) c

x p c q g.
    temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c q
    temporal_state.TEMPORAL_NEXT x (set_sep.STAR p (set_sep.cond g)) c
      (set_sep.STAR q (set_sep.cond g))

m s u v.
    set_sep.SPLIT (state.STATE m s) (u, v)
    y. u = state.SELECT_STATE m y s v = state.FRAME_STATE m y s

x p c q.
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) p)
      pred_set.EMPTY
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) q)
    temporal_state.TEMPORAL_NEXT x p c q

to_set next instr less avoid p c q.
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid) p c q
    temporal.TEMPORAL (to_set, next, instr, (=), const ) c
      (temporal.T_IMPLIES (temporal.NOW p)
         (temporal.NEXT (temporal.NOW q)))

to_set next instr less avoid p c q.
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid)
      (set_sep.STAR p (prog.CODE_POOL instr c)) pred_set.EMPTY
      (set_sep.STAR q (prog.CODE_POOL instr c))
    temporal_state.TEMPORAL_NEXT (to_set, next, instr, less, avoid) p c q

cd m p s x.
    set_sep.STAR (pred_set.INSERT cd pred_set.EMPTY) p
      (state.SELECT_STATE m x s)
    (c d. bool.IN (c, d) cd m s c = d)
    pred_set.SUBSET (pred_set.IMAGE fst cd) x
    p (state.SELECT_STATE m (pred_set.DIFF x (pred_set.IMAGE fst cd)) s)

m f u r.
    (b s a w. ¬(b = f a) m (u s a w) b = m (r s) b)
    a w s x.
      bool.IN (f a) x
      state.FRAME_STATE m x (u s a w) = state.FRAME_STATE m x (r s)

m next instr p q.
    prog.SPEC (state.STATE m, next, instr, (=), const ) p pred_set.EMPTY
      q
    y s seq.
      p (state.SELECT_STATE m y s) prog.rel_sequence next seq s
      k.
        q (state.SELECT_STATE m y (seq k))
        state.FRAME_STATE m y s = state.FRAME_STATE m y (seq k)

m next instr less avoid p q.
    temporal_state.TEMPORAL_NEXT (state.STATE m, next, instr, less, avoid)
      p pred_set.EMPTY q
    state y seq.
      p (state.SELECT_STATE m y (seq 0))
      prog.rel_sequence next seq state
      q (state.SELECT_STATE m y (seq 1))
      state.FRAME_STATE m y (seq 0) = state.FRAME_STATE m y (seq 1)

m next instr c p q.
    (y s.
       set_sep.STAR p (prog.CODE_POOL instr c) (state.SELECT_STATE m y s)
       v.
         next s = some v
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y v)
         state.FRAME_STATE m y s = state.FRAME_STATE m y v)
    prog.SPEC (state.STATE m, state.NEXT_REL (=) next, instr, (=), const )
      p c q

m next instr less avoid c p q.
    (y s.
       set_sep.STAR p (prog.CODE_POOL instr c) (state.SELECT_STATE m y s)
       v.
         next s = some v
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y v)
         state.FRAME_STATE m y s = state.FRAME_STATE m y v)
    temporal_state.TEMPORAL_NEXT
      (state.STATE m, state.NEXT_REL (=) next, instr, less, avoid) p c q

m next instr r p q.
    prog.SPEC (state.STATE m, next, instr, r, const ) p pred_set.EMPTY q
    y s t1 seq.
      p (state.SELECT_STATE m y t1) r t1 s
      prog.rel_sequence next seq s
      k t2.
        q (state.SELECT_STATE m y t2) r t2 (seq k)
        state.FRAME_STATE m y t1 = state.FRAME_STATE m y t2

x prefix postfix p c q m i a l1 l2.
    length l2 = length l1
    prog.SPEC x (set_sep.STAR p (set_sep.SEP_ARRAY m i a l1)) c
      (set_sep.STAR q (set_sep.SEP_ARRAY m i a l2))
    prog.SPEC x
      (set_sep.STAR p
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l1) @ postfix))) c
      (set_sep.STAR q
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l2) @ postfix)))

x prefix postfix p c q m i a l1 l2.
    length l2 = length l1
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR p (set_sep.SEP_ARRAY m i a l1)) c
      (set_sep.STAR q (set_sep.SEP_ARRAY m i a l2))
    temporal_state.TEMPORAL_NEXT x
      (set_sep.STAR p
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l1) @ postfix))) c
      (set_sep.STAR q
         (set_sep.SEP_ARRAY m i
            (words.word_sub a
               (words.word_mul (words.n2w (length prefix)) i))
            ((prefix @ l2) @ postfix)))

y x single_c map_c.
    (c d.
       single_c c d =
       pred_set.INSERT (pred_set.INSERT (x c, y d) pred_set.EMPTY)
         pred_set.EMPTY)
    (a b. x a = x b a = b)
    (df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc. (pred_set.BIGUNION (single_c c (f c)), bool.IN c df))))
         pred_set.EMPTY)
    f df c d.
      bool.IN c df
      set_sep.STAR (single_c c d) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

y x single_c map_c.
    (c d.
       single_c c d =
       pred_set.INSERT (pred_set.INSERT (x c, y d) pred_set.EMPTY)
         pred_set.EMPTY)
    (a b. x a = x b a = b)
    (df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc.
                  (pred_set.BIGUNION (single_c c (some (f c))),
                   bool.IN c df)))) pred_set.EMPTY)
    f df c d.
      bool.IN c df
      set_sep.STAR (single_c c (some d)) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

r m next instr c p q.
    relation.PreOrder r
    (y s t1.
       set_sep.STAR p (prog.CODE_POOL instr c)
         (state.SELECT_STATE m y t1) r t1 s
       v t2.
         set_sep.STAR p (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y s) next s = some v
         set_sep.STAR q (prog.CODE_POOL instr c)
           (state.SELECT_STATE m y t2) r t2 v
         state.FRAME_STATE m y t1 = state.FRAME_STATE m y t2)
    prog.SPEC (state.STATE m, state.NEXT_REL r next, instr, r, const ) p c
      q

P n x y single_c map_c.
    (c d.
       single_c c d =
       pred_set.INSERT
         (list.LIST_TO_SET (list.GENLIST (λi. (x c i, y d i)) n))
         pred_set.EMPTY)
    (a b i j.
       P a P b i < n j < n (x a i = x b j a = b i = j))
    (df f.
       map_c df f =
       pred_set.INSERT
         (pred_set.BIGUNION
            (pred_set.GSPEC
               (λc.
                  (pred_set.BIGUNION (single_c c (f c)),
                   bool.IN c df P c)))) pred_set.EMPTY)
    f df c d.
      bool.IN c df P c
      set_sep.STAR (single_c c d) (map_c (pred_set.DELETE df c) f) =
      map_c df (combin.UPDATE c d f)

External Type Operators

External Constants

Assumptions

pred_set.BIGUNION pred_set.EMPTY = pred_set.EMPTY

x. x = x

x. bool.IN x pred_set.UNIV

t. t

n. 0 n

bool.IN = λx f. f x

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. id x = x

s. set_sep.SEP_F s

t. t ¬t

(¬) = λt. t

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

set_sep.emp = λs. s = pred_set.EMPTY

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

¬(p q) p

x. x = x

t. ¬¬t t

f. pred_set.IMAGE f pred_set.EMPTY = pred_set.EMPTY

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

x. pred_set.BIGUNION (pred_set.INSERT x pred_set.EMPTY) = x

x y. const x y = x

x. set_sep.SEP_EQ x = λs. s = 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)

R. reflexive R x. R x x

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

R. relation.PreOrder R reflexive R transitive R

x y. x = y y = x

A B. A B B A

m n. m + n = n + m

v w. words.word_add v w = words.word_add w v

v w. words.word_mul v w = words.word_mul w v

x y. set_sep.STAR x y = set_sep.STAR y x

(¬A ) (A )

w.
    words.word_2comp w = words.word_mul (words.word_2comp (words.n2w 1)) w

x y. pred_set.INSERT y pred_set.EMPTY x x = y

A B. A B ¬A B

m n. m < n suc m n

m n. ¬(m < n) n m

v w. words.word_sub v w = words.word_add v (words.word_2comp w)

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

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

x. prog.RUN x p q prog.SPEC x p pred_set.EMPTY q

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

x y. some x = some y x = y

x s. bool.IN x (pred_set.COMPL s) ¬bool.IN x s

s t. pred_set.DISJOINT s t pred_set.INTER s t = pred_set.EMPTY

s P.
    pred_set.BIGUNION (pred_set.INSERT s P) =
    pred_set.UNION s (pred_set.BIGUNION P)

l1 l2. length (l1 @ l2) = length l1 + length l2

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

f v. (x. x = v f x) f v

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

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

instr c.
    prog.CODE_POOL instr c =
    λs. s = pred_set.BIGUNION (pred_set.IMAGE instr c)

p f seq. temporal.NOW p f seq f p (seq 0)

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

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

m n. m = n m n n m

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

list.LIST_TO_SET [] = pred_set.EMPTY
  list.LIST_TO_SET (h :: t) = pred_set.INSERT h (list.LIST_TO_SET t)

list.GENLIST f 0 = [] list.GENLIST f n = list.GENLIST_AUX f n []

(s. pred_set.UNION pred_set.EMPTY s = s)
  s. pred_set.UNION s pred_set.EMPTY = s

¬(¬A B) A ¬B

P Q. (x. P Q x) P x. Q x

Q P. (x. P x Q) (x. P x) Q

P Q. P (x. Q x) x. P Q x

P Q. (x. P x) Q x. P x Q

¬(A B) (A ) ¬B

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

t1 t2 t3. t1 t2 t3 t1 t2 t3

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

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

m n p. m n n p m p

s t. s = t x. bool.IN x s bool.IN x t

s t. pred_set.SUBSET s t x. bool.IN x s bool.IN x t

v w x.
    words.word_add v (words.word_add w x) =
    words.word_add (words.word_add v w) x

f v. bool.IN v (pred_set.GSPEC f) x. (v, ) = f x

p q r.
    set_sep.STAR p (set_sep.STAR q r) = set_sep.STAR (set_sep.STAR p q) r

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

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

n m. arithmetic.- n m = if m < n then numeral.iSUB n m else 0

(w. words.word_add w (words.n2w 0) = w)
  w. words.word_add (words.n2w 0) w = w

x sos.
    bool.IN x (pred_set.BIGUNION sos) s. bool.IN x s bool.IN s sos

f x s.
    pred_set.IMAGE f (pred_set.INSERT x s) =
    pred_set.INSERT (f x) (pred_set.IMAGE f s)

bool.IN x (list.LIST_TO_SET (list.GENLIST f n)) m. m < n x = f m

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

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

p f seq. temporal.NEXT p f seq = p f (λn. seq (n + 1))

x y s. bool.IN x (pred_set.INSERT y s) x = y bool.IN x s

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

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

s t x. bool.IN x (pred_set.INTER s t) bool.IN x s bool.IN x t

s t x. bool.IN x (pred_set.UNION s t) bool.IN x s bool.IN x t

f d.
    set_sep.fun2set (f, d) = pred_set.GSPEC (λa. ((a, f a), bool.IN a d))

v w x.
    words.word_mul (words.word_add v w) x =
    words.word_add (words.word_mul v x) (words.word_mul w 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

s x y. bool.IN x (pred_set.DELETE s y) bool.IN x s ¬(x = y)

s t x. bool.IN x (pred_set.DIFF s t) bool.IN x s ¬bool.IN x t

P Q. (x. P x Q x) (x. P x) x. Q x

p s t.
    set_sep.STAR (set_sep.SEP_EQ t) p s
    p (pred_set.DIFF s t) pred_set.SUBSET t s

f a b c. combin.UPDATE a b f c = if a = c then b else f c

p q f seq. temporal.T_IMPLIES p q f seq p f seq q f seq

s u v.
    set_sep.SPLIT s (u, v) pred_set.UNION u v = s pred_set.DISJOINT u v

y s f. bool.IN y (pred_set.IMAGE f s) x. y = f x bool.IN x s

R. transitive R x y z. R x y R y z R x z

p less to_set state.
    prog.SEP_REFINE p less to_set state s. less s state p (to_set s)

p q. set_sep.STAR p q = λs. u v. set_sep.SPLIT s (u, v) p u q v

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

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

x p c q.
    prog.SPEC x p c q
    r. prog.SPEC x (set_sep.STAR p r) c (set_sep.STAR q r)

a y h dh.
    bool.IN (a, y) (set_sep.fun2set (h, dh)) h a = y bool.IN a dh

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

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

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

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

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

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

x p c q.
    prog.SPEC x (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) p)
      pred_set.EMPTY
      (set_sep.STAR (prog.CODE_POOL (fst (snd (snd x))) c) q)
    prog.SPEC x p c q

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

s t u.
    (pred_set.DISJOINT (pred_set.UNION s t) u
     pred_set.DISJOINT s u pred_set.DISJOINT t u)
    (pred_set.DISJOINT u (pred_set.UNION s t)
     pred_set.DISJOINT s u pred_set.DISJOINT t u)

xs ys p i a.
    set_sep.SEP_ARRAY p i a (xs @ ys) =
    set_sep.STAR (set_sep.SEP_ARRAY p i a xs)
      (set_sep.SEP_ARRAY p i
         (words.word_add a (words.word_mul (words.n2w (length xs)) i)) ys)

R seq state.
    prog.rel_sequence R seq state
    seq 0 = state
    n.
      if (x. R (seq n) x) then R (seq n) (seq (suc n))
      else seq (suc n) = seq n

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

(m n.
     words.word_add (words.word_2comp (words.n2w m))
       (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m + n)))
  m n.
    words.word_add (words.n2w m) (words.word_2comp (words.n2w n)) =
    if n m then words.n2w (arithmetic.- m n)
    else words.word_2comp (words.n2w (arithmetic.- n m))

P Q.
    ((x. P x) Q x. P x Q) ((x. P x) Q x. P x Q)
    (Q (x. P x) x. Q P x)

(p if q then r else s)
  (p q ¬s) (p ¬r ¬q) (p ¬r ¬s) (¬q r ¬p)
  (q s ¬p)

f.
    (x y z. f x (f y z) = f (f x y) z) (x y. f x y = f y x)
    x y z. f x (f y z) = f y (f x z)

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

to_set next instr less allow c exp.
    temporal.TEMPORAL (to_set, next, instr, less, allow) c exp
    state seq r.
      prog.rel_sequence next seq state
      bool.LET (λf. exp f seq)
        (λp state.
           prog.SEP_REFINE
             (set_sep.STAR (set_sep.STAR p (prog.CODE_POOL instr c)) r)
             less to_set state allow state)

(f l. list.GENLIST_AUX f 0 l = l)
  (f n l.
     list.GENLIST_AUX f (bit1 n) l =
     list.GENLIST_AUX f (arithmetic.- (bit1 n) 1)
       (f (arithmetic.- (bit1 n) 1) :: l))
  f n l.
    list.GENLIST_AUX f (arithmetic.BIT2 n) l =
    list.GENLIST_AUX f (bit1 n) (f (bit1 n) :: l)

to_set next instr less allow p q.
    prog.RUN (to_set, next, instr, less, allow) p q
    state r.
      prog.SEP_REFINE (set_sep.STAR p r) less to_set state allow state
      seq.
        prog.rel_sequence next seq state
        i.
          prog.SEP_REFINE (set_sep.STAR q r) less to_set (seq i)
          allow (seq i)

v w.
    words.word_mul (words.n2w 0) v = words.n2w 0
    words.word_mul v (words.n2w 0) = words.n2w 0
    words.word_mul (words.n2w 1) v = v
    words.word_mul v (words.n2w 1) = v
    words.word_mul (words.word_add v (words.n2w 1)) w =
    words.word_add (words.word_mul v w) w
    words.word_mul v (words.word_add w (words.n2w 1)) =
    words.word_add v (words.word_mul v w)

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)

p q t c c'.
    set_sep.STAR (set_sep.SEP_EXISTS (λv. p v)) q =
    set_sep.SEP_EXISTS (λv. set_sep.STAR (p v) q)
    set_sep.STAR q (set_sep.SEP_EXISTS (λv. p v)) =
    set_sep.SEP_EXISTS (λv. set_sep.STAR q (p v))
    set_sep.SEP_DISJ (set_sep.SEP_EXISTS (λv. p v)) q =
    set_sep.SEP_EXISTS (λv. set_sep.SEP_DISJ (p v) q)
    set_sep.SEP_DISJ q (set_sep.SEP_EXISTS (λv. p v)) =
    set_sep.SEP_EXISTS (λv. set_sep.SEP_DISJ q (p v))
    set_sep.SEP_EXISTS (λv. q) = q
    set_sep.SEP_EXISTS (λv. set_sep.STAR (p v) (set_sep.cond (v = x))) =
    p x set_sep.SEP_DISJ q set_sep.SEP_F = q
    set_sep.SEP_DISJ set_sep.SEP_F q = q
    set_sep.STAR set_sep.SEP_F q = set_sep.SEP_F
    set_sep.STAR q set_sep.SEP_F = set_sep.SEP_F
    set_sep.SEP_DISJ r r = r
    set_sep.STAR q (set_sep.SEP_DISJ r t) =
    set_sep.SEP_DISJ (set_sep.STAR q r) (set_sep.STAR q t)
    set_sep.STAR (set_sep.SEP_DISJ r t) q =
    set_sep.SEP_DISJ (set_sep.STAR r q) (set_sep.STAR t q)
    set_sep.SEP_DISJ (set_sep.cond c) (set_sep.cond c') =
    set_sep.cond (c c')
    set_sep.STAR (set_sep.cond c) (set_sep.cond c') =
    set_sep.cond (c c') set_sep.cond = set_sep.emp
    set_sep.cond = set_sep.SEP_F set_sep.STAR set_sep.emp q = q
    set_sep.STAR q set_sep.emp = q

(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