Package machine-code-hoare-logic: A Hoare logic for machine code

Information

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

Files

Defined Constants

Theorems

set_sep.precond = set_sep.cond

set_sep.sidecond = set_sep.cond

p. set_sep.SEP_IMP p p

x. address.ALIGNED (address.ADDR32 x)

s. set_sep.SEP_F s

s. set_sep.SEP_T s

x. address.CONTAINER x x

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

x. address.SING_SET x = pred_set.INSERT x pred_set.EMPTY

p. set_sep.SEP_IMP set_sep.emp p p pred_set.EMPTY

%%genvar%%3354.
    address.ALIGNED (words.word_2comp %%genvar%%3354)
    address.ALIGNED %%genvar%%3354

set_sep.SEP_EXISTS = λf s. y. f y s

x. set_sep.SEP_EQ x = λs. s = x

n x. address.GUARD n x x

p x. set_sep.SEP_IMP (p x) (set_sep.SEP_HIDE p)

p. set_sep.SEP_HIDE p = set_sep.SEP_EXISTS (λx. p x)

w.
    address.ADDR32 (words.word_2comp w) =
    words.word_2comp (address.ADDR32 w)

x. address.ADDR32 x = words.word_lsl (words.w2w x) (arithmetic.BIT2 0)

x c q. prog.SPEC x set_sep.SEP_F c q

x p c. prog.SPEC x p c p

x y. address.DUMMY_EQ x y x = y

x. set_sep.one x = λs. s = pred_set.INSERT x pred_set.EMPTY

c. set_sep.cond c = λs. s = pred_set.EMPTY c

n b. address.GUARD n b address.GUARD 0 b

p q. set_sep.SEP_DISJ p q = set_sep.SEP_DISJ q p

p q. set_sep.STAR p q = set_sep.STAR q p

set_sep.cond (c d) = set_sep.STAR (set_sep.cond c) (set_sep.cond d)

set_sep.SEP_EXISTS (λv. p v) s y. p y s

temporal.TEMPORAL model code (temporal.ALWAYS p)
  temporal.TEMPORAL model code p

w. words.word_mul (words.n2w (arithmetic.BIT2 0)) w = words.word_add w w

x. words.word_extract 1 0 (address.ADDR32 x) = words.n2w 0

x s. pred_set.INSERT x s = pred_set.UNION (address.SING_SET x) s

n. address.ADDR30 (words.n2w n) = words.n2w (n div arithmetic.BIT2 1)

n. address.ADDR32 (words.n2w n) = words.n2w (arithmetic.BIT2 1 * n)

x. address.ADDR32 x = words.n2w (arithmetic.BIT2 1 * words.w2n x)

a. address.ADDR32 a = words.n2w 0 a = words.n2w 0

a. words.word_and (address.ADDR32 a) (words.n2w 3) = words.n2w 0

x. address.ADDR30 x = words.n2w (words.w2n x div arithmetic.BIT2 1)

a.
    address.ALIGNED (words.word_sub a (words.n2w (arithmetic.BIT2 1)))
    address.ALIGNED a

w. words.word_extract 7 0 w = words.w2w w

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

g h. set_sep.SEP_IMP (set_sep.cond g) (set_sep.cond h) g h

x s. pred_set.UNION x (pred_set.UNION x s) = pred_set.UNION x s

x y.
    words.word_lo (address.ADDR32 x) (address.ADDR32 y) words.word_lo x y

x y.
    words.word_ls (address.ADDR32 x) (address.ADDR32 y) words.word_ls x y

n. address.ALIGNED (words.n2w n) n mod arithmetic.BIT2 1 = 0

p q. set_sep.SEP_DISJ p q = λs. p s q s

x. address.ALIGNED x words.word_and x (words.n2w 1) = words.n2w 0

(x. set_sep.SEP_IMP (p x) (q x))
  set_sep.SEP_IMP (set_sep.SEP_EXISTS p) (set_sep.SEP_EXISTS q)

f df. set_sep.fun2set (f, df) = pred_set.EMPTY df = pred_set.EMPTY

v w. address.word_mod v w = words.n2w (words.w2n v mod words.w2n w)

v w. words.word_xor v w = words.n2w 0 v = w

v w.
    address.ADDR32 (words.word_add v w) =
    words.word_add (address.ADDR32 v) (address.ADDR32 w)

v w.
    address.ADDR32 (words.word_sub v w) =
    words.word_sub (address.ADDR32 v) (address.ADDR32 w)

x y.
    address.ADDR30 (words.word_add (address.ADDR32 x) y) =
    words.word_add x (address.ADDR30 y)

x y.
    address.ALIGNED (words.word_or x y)
    address.ALIGNED x address.ALIGNED y

x y.
    address.ALIGNED x address.ALIGNED y
    address.ALIGNED (words.word_add x y)

x y.
    address.ALIGNED x address.ALIGNED y
    address.ALIGNED (words.word_sub x y)

x y z. address.CONTAINER x (if x then y else z) = y

n.
    words.word_and (words.n2w n) (words.n2w 1) =
    words.n2w (n mod arithmetic.BIT2 0)

p q. set_sep.SEP_IMP p q s. p s q s

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)

x. address.ALIGNED x words.word_and x (words.n2w 3) = words.n2w 0

p q. p = q set_sep.SEP_IMP p q set_sep.SEP_IMP q p

p.
    address.ALIGNED p
    k. p = words.word_mul k (words.n2w (arithmetic.BIT2 1))

temporal.SPEC_1 model pre code post err
  prog.SPEC model pre code (set_sep.SEP_DISJ post err)

x y z. address.CONTAINER (¬x) (if x then y else z) = z

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

x. address.ALIGNED x ¬fcp.fcp_index x 0 ¬fcp.fcp_index x 1

x. address.ADDR30 x = words.word_extract 31 (arithmetic.BIT2 0) x

m k.
    words.word_lsl (words.n2w m) k = words.n2w (m * arithmetic.BIT2 0 k)

p q.
    set_sep.SEP_IMP (set_sep.SEP_EXISTS (λv. p v)) q
    x. set_sep.SEP_IMP (p x) q

x y.
    address.ALIGNED x
    address.ALIGNED
      (words.word_add x (words.word_mul (words.n2w (arithmetic.BIT2 1)) y))

prog.SPEC model pre code post
  temporal.TEMPORAL model code
    (temporal.T_IMPLIES (temporal.NOW pre)
       (temporal.EVENTUALLY (temporal.NOW post)))

temporal.TEMPORAL model code (temporal.T_IMPLIES p1 (temporal.NEXT p2))
  temporal.TEMPORAL model code
    (temporal.T_IMPLIES p1 (temporal.EVENTUALLY p2))

%%genvar%%1520 c d. %%genvar%%1520 (c d) (%%genvar%%1520 c) d

n.
    words.word_and (words.n2w n) (words.n2w 3) =
    words.n2w (n mod arithmetic.BIT2 1)

x y z.
    pred_set.DIFF (pred_set.DIFF x y) z =
    pred_set.DIFF x (pred_set.UNION y z)

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

p q r. set_sep.SEP_IMP p q set_sep.SEP_IMP q r set_sep.SEP_IMP p r

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

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

p.
    address.ADDR32 (words.word_add p (words.n2w 1)) =
    words.word_add (address.ADDR32 p) (words.n2w (arithmetic.BIT2 1))

c p q.
    set_sep.SEP_IMP (set_sep.STAR p (set_sep.cond c)) q
    c set_sep.SEP_IMP p q

x.
    words.word_and x (words.n2w 3) = words.n2w 0
    address.ADDR32 (address.ADDR30 x) = x

f1 f2 g x. tailrec.TAILREC f1 f2 g x = f2 (while.WHILE g f1 x)

p c.
    set_sep.SEP_EXISTS (λv. set_sep.STAR (p v) (set_sep.cond c)) =
    set_sep.STAR (set_sep.SEP_EXISTS (λv. p v)) (set_sep.cond c)

w x.
    words.word_extract 1 0 (words.word_add (address.ADDR32 x) w) =
    words.word_extract 1 0 w

x.
    words.word_and x (words.n2w 3) = words.n2w 0 y. x = address.ADDR32 y

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

set_sep.one (a, x) (set_sep.fun2set (f, df)) f a = x bool.IN a df

b x y. (if b then x else y) b x ¬b y

n m k. n < k arithmetic.- n m mod k = arithmetic.- n m

n a b.
    words.word_lsl (words.word_add a b) n =
    words.word_add (words.word_lsl a n) (words.word_lsl b n)

n.
    words.word_and (words.n2w n) (words.n2w 7) =
    words.n2w (n mod arithmetic.BIT2 3)

p1 p2 q.
    set_sep.SEP_IMP (set_sep.SEP_DISJ p1 p2) q
    set_sep.SEP_IMP p1 q set_sep.SEP_IMP p2 q

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

x.
    address.ALIGNED x
    ¬(words.word_and (words.word_add x (words.n2w 1)) (words.n2w 1) =
       words.n2w 0)

p f seq. temporal.ALWAYS p f seq k. p f (λn. seq (n + k))

p f seq. temporal.EVENTUALLY p f seq k. p f (λn. seq (n + k))

x m.
    words.word_add (address.ADDR30 x) (words.n2w m) =
    address.ADDR30 (words.word_add x (words.n2w (arithmetic.BIT2 1 * m)))

x s p.
    set_sep.STAR (set_sep.one x) p s
    bool.IN x s p (pred_set.DELETE s 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.
    tailrec.SHORT_TAILREC_PRE f =
    tailrec.TAILREC_PRE (Data.Sum.destLeft (fst f))
      (Data.Sum.isLeft (fst f)) (snd f)

x.
    address.ALIGNED x
    words.word_and (words.word_add x (words.n2w (arithmetic.BIT2 0)))
      (words.n2w 3) = words.n2w (arithmetic.BIT2 0)

x.
    address.ALIGNED x
    words.word_and (words.word_add x (words.n2w 1)) (words.n2w 3) =
    words.n2w 1

a.
    (address.ALIGNED (words.word_add a (words.n2w 0))
     address.ALIGNED a)
    (address.ALIGNED (words.word_sub a (words.n2w 0)) address.ALIGNED a)

v df f.
    pred_set.SUBSET v (set_sep.fun2set (f, df))
    z. v = set_sep.fun2set (f, z)

q z.
    words.word_ror q
      (arithmetic.BIT2 3 *
       words.w2n (words.word_extract 1 0 (address.ADDR32 z))) = q

p q f seq. temporal.T_AND p q f seq p f seq q f seq

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.SUBSET u s v = pred_set.DIFF s u

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

(x. prog.SPEC m (P x) c (Q x))
  prog.SPEC m (set_sep.SEP_EXISTS (λx. P x)) c
    (set_sep.SEP_EXISTS (λx. Q x))

%%genvar%%3780 P.
    (i. ¬(i = %%genvar%%3780) ¬P i) ((i. P i) P %%genvar%%3780)

prog.SPEC m (set_sep.STAR p (set_sep.cond b)) c q
  prog.SPEC m (set_sep.STAR p (set_sep.cond b)) c
    (set_sep.STAR q (set_sep.cond b))

a h dh.
    pred_set.DELETE (set_sep.fun2set (h, dh)) (a, h a) =
    set_sep.fun2set (h, pred_set.DELETE dh a)

f x y.
    pred_set.DIFF (set_sep.fun2set (f, x)) (set_sep.fun2set (f, y)) =
    set_sep.fun2set (f, pred_set.DIFF x y)

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

f.
    tailrec.SHORT_TAILREC f =
    tailrec.TAILREC (Data.Sum.destLeft (fst f))
      (Data.Sum.destRight (fst f)) (Data.Sum.isLeft (fst f))

x.
    address.ALIGNED x
    words.word_and (words.word_add x (words.n2w 3)) (words.n2w 3) =
    words.n2w 3

x p c q. prog.SPEC x p c q c'. prog.SPEC x p (pred_set.UNION c c') q

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

p p' q q'.
    set_sep.SEP_IMP p p' set_sep.SEP_IMP q q'
    set_sep.SEP_IMP (set_sep.SEP_DISJ p q) (set_sep.SEP_DISJ p' q')

p p' q q'.
    set_sep.SEP_IMP p p' set_sep.SEP_IMP q q'
    set_sep.SEP_IMP (set_sep.STAR p q) (set_sep.STAR p' q')

p post f seq.
    temporal.T_OR_F p post f seq
    p f seq temporal.EVENTUALLY (temporal.NOW post) f seq

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

n m.
    words.word_sub (words.n2w n) (words.n2w m) =
    if n < m then words.word_2comp (words.n2w (arithmetic.- m n))
    else words.n2w (arithmetic.- n m)

f d a x. set_sep.fun2set (f, d) (a, x) f a = x bool.IN a d

x p c q.
    (y. prog.SPEC x (p y) c q)
    prog.SPEC x (set_sep.SEP_EXISTS (λy. p y)) c q

x p c q.
    prog.SPEC x p c q c'. pred_set.SUBSET c c' prog.SPEC x p c' q

x p c q. prog.SPEC x p c q r. set_sep.SEP_IMP q r prog.SPEC x p c r

x p c q. prog.SPEC x p c q r. set_sep.SEP_IMP r p prog.SPEC x r c q

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

f1 f2 g x.
    tailrec.TAILREC f1 f2 g x =
    if g x then tailrec.TAILREC f1 f2 g (f1 x) else f2 x

x.
    address.ALIGNED x
    ¬(words.word_add x (words.n2w (arithmetic.BIT2 1)) = words.n2w 0)
    words.word_lo x (words.word_add x (words.n2w (arithmetic.BIT2 1)))

x p c q g.
    prog.SPEC x (set_sep.STAR p (set_sep.cond g)) c q
    g prog.SPEC x p c q

f1 g p x.
    tailrec.TAILREC_PRE f1 g p x
    p x (g x tailrec.TAILREC_PRE f1 g p (f1 x))

w.
    words.word_and (words.word_add w (words.n2w n)) (words.n2w 3) =
    words.word_and (words.word_add w (words.n2w (n mod arithmetic.BIT2 1)))
      (words.n2w 3)

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

a x p f.
    set_sep.STAR (set_sep.one (a, x)) p (set_sep.fun2set (f, d))
    f a = x bool.IN a d

f g d.
    set_sep.fun2set (f, d) = set_sep.fun2set (g, d)
    a. bool.IN a d f a = g a

c s p.
    (set_sep.STAR (set_sep.cond c) p s c p s)
    (set_sep.STAR p (set_sep.cond c) s c p s)

model p c q err.
    (y. temporal.SPEC_1 model (p y) c q err)
    temporal.SPEC_1 model (set_sep.SEP_EXISTS (λy. p y)) c q err

w.
    ¬(w = words.n2w 0)
    v.
      v =
      words.word_add (words.word_mul (words.word_div v w) w)
        (address.word_mod v w) words.word_lo (address.word_mod v w) w

model p c r err.
    temporal.SPEC_1 model p c r err
    q. set_sep.SEP_IMP r q temporal.SPEC_1 model p c q err

model p c q err.
    temporal.SPEC_1 model p c q err
    r. set_sep.SEP_IMP r p temporal.SPEC_1 model r c q err

%%genvar%%1213 p c q q' y.
    prog.SPEC %%genvar%%1213 p c (set_sep.STAR q (q' y))
    prog.SPEC %%genvar%%1213 p c (set_sep.STAR q (set_sep.SEP_HIDE q'))

x p p' c q.
    (y. prog.SPEC x (set_sep.STAR p (p' y)) c q)
    prog.SPEC x (set_sep.STAR p (set_sep.SEP_HIDE p')) c q

set_sep.STAR p q (set_sep.fun2set (f, df))
  x y.
    p (set_sep.fun2set (f, pred_set.DIFF df y))
    q (set_sep.fun2set (f, pred_set.DIFF df x))

model pre code post err.
    temporal.SPEC_1 model pre code post err
    temporal.TEMPORAL model code
      (temporal.T_IMPLIES (temporal.NOW pre)
         (temporal.T_OR_F
            (temporal.NEXT (temporal.EVENTUALLY (temporal.NOW post))) err))

x p1 p2 c q.
    prog.SPEC x (set_sep.SEP_DISJ p1 p2) c q
    prog.SPEC x p1 c q prog.SPEC x p2 c q

model p c q g err.
    temporal.SPEC_1 model (set_sep.STAR p (set_sep.cond g)) c q err
    g temporal.SPEC_1 model p c q err

x p c q g.
    prog.SPEC x (set_sep.STAR p (set_sep.cond g)) c q
    prog.SPEC x (set_sep.STAR p (set_sep.cond g)) c
      (set_sep.STAR q (set_sep.cond g))

x p c1 m c2 q.
    prog.SPEC x p c1 m prog.SPEC x m c2 q
    prog.SPEC x p (pred_set.UNION c1 c2) q

model p c q err.
    temporal.SPEC_1 model p c q err
    r.
      temporal.SPEC_1 model (set_sep.STAR p r) c (set_sep.STAR q r)
        (set_sep.STAR err r)

%%genvar%%707 p c q.
    prog.SPEC %%genvar%%707 p c q
    r1 r2.
      set_sep.SEP_IMP r1 p set_sep.SEP_IMP q r2
      prog.SPEC %%genvar%%707 r1 c r2

x n m.
    words.word_add (words.word_sub x (words.n2w m)) (words.n2w n) =
    if n < m then words.word_sub x (words.n2w (arithmetic.- m n))
    else words.word_add x (words.n2w (arithmetic.- n m))

x n m.
    words.word_sub (words.word_add x (words.n2w n)) (words.n2w m) =
    if n < m then words.word_sub x (words.n2w (arithmetic.- m n))
    else words.word_add x (words.n2w (arithmetic.- n m))

a.
    address.ALIGNED a
    ¬address.ALIGNED (words.word_add a (words.n2w 1))
    ¬address.ALIGNED (words.word_add a (words.n2w (arithmetic.BIT2 0)))
    ¬address.ALIGNED (words.word_add a (words.n2w 3))

a b x y f g p.
    set_sep.STAR (set_sep.STAR (set_sep.one (a, x)) (set_sep.one (b, y))) p
      (set_sep.fun2set (f, g)) ¬(a = b)

w.
    (m.
       m < arithmetic.BIT2 127
       (words.w2w w = words.n2w m w = words.n2w m))
    words.w2w (words.w2w w) = w

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

y a x p f.
    set_sep.STAR (set_sep.one (a, x)) p (set_sep.fun2set (f, d))
    set_sep.STAR p (set_sep.one (a, y))
      (set_sep.fun2set (combin.UPDATE a y f, d))

step guard side.
    (R. wellFounded R x. guard x R (step x) x) (x. side x)
    x. tailrec.TAILREC_PRE step guard side x

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)

a x p f.
    set_sep.STAR (set_sep.one (a, x)) p (set_sep.fun2set (f, d))
    f a = x bool.IN a d p (set_sep.fun2set (f, pred_set.DELETE d a))

q p x y.
    (s. q s x = y)
    set_sep.STAR q (p x) = set_sep.STAR q (p y)
    set_sep.STAR (p x) q = set_sep.STAR (p y) q

a n.
    (address.ALIGNED (words.word_add a (words.n2w n))
     address.ALIGNED
       (words.word_add a (words.n2w (n mod arithmetic.BIT2 1))))
    (address.ALIGNED (words.word_sub a (words.n2w n))
     address.ALIGNED
       (words.word_sub a (words.n2w (n mod arithmetic.BIT2 1))))

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

x.
    ¬(words.word_add (address.ADDR32 x) (words.n2w 1) = words.n2w 0)
    ¬(words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 0)) =
       words.n2w 0)
    ¬(words.word_add (address.ADDR32 x) (words.n2w 3) = words.n2w 0)

f1 = f1' f2 = f2' g = g' s = s'
  tailrec.TAILREC f1 f2 g = tailrec.TAILREC f1' f2' g'
  tailrec.TAILREC_PRE f1 g s = tailrec.TAILREC_PRE f1' g' s'

words.n2w (arithmetic.BIT2 536870911) = words.n2w 0

x p c q1 q2 q3 q4.
    prog.SPEC x (set_sep.STAR q1 q3) c q2
    prog.SPEC x p c (set_sep.STAR q1 q4) set_sep.SEP_IMP q4 q3
    prog.SPEC x p c q2

b g x y.
    (b (if g then x else y) if g then b x else b y)
    ((if g then x else y) b if g then b x else b y)

b1 b2 h1 h2.
    (words.w2w b1 = words.w2w b2 b1 = b2)
    (words.w2w h1 = words.w2w h2 h1 = h2)
    words.w2w (words.w2w b1) = b1 words.w2w (words.w2w h1) = h1

x y.
    address.ALIGNED x
    (address.ALIGNED (words.word_add x y) address.ALIGNED y)
    (address.ALIGNED (words.word_sub x y) address.ALIGNED y)
    (address.ALIGNED (words.word_add y x) address.ALIGNED y)
    (address.ALIGNED (words.word_sub y x) address.ALIGNED y)

x y m n.
    words.word_add x (words.n2w n) = words.word_add y (words.n2w m)
    if n < m then
      x = words.word_sub (words.word_add y (words.n2w m)) (words.n2w n)
    else words.word_sub (words.word_add x (words.n2w n)) (words.n2w m) = y

p.
    a.
      p = words.word_add (address.ADDR32 a) (words.n2w 0)
      p = words.word_add (address.ADDR32 a) (words.n2w 1)
      p =
      words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0))
      p = words.word_add (address.ADDR32 a) (words.n2w 3)

f1 guard precondition x.
    tailrec.TAILREC_PRE f1 guard precondition x
    (k.
       (m. m < k guard (arithmetic.FUNPOW f1 m x))
       precondition (arithmetic.FUNPOW f1 k x))
    n. ¬guard (arithmetic.FUNPOW f1 n x)

x p1 p2 c1 m c2 q1 q2.
    prog.SPEC x p1 c1 (set_sep.SEP_DISJ q1 m)
    prog.SPEC x (set_sep.SEP_DISJ m p2) c2 q2
    prog.SPEC x (set_sep.SEP_DISJ p1 p2) (pred_set.UNION c1 c2)
      (set_sep.SEP_DISJ q1 q2)

(p i a. set_sep.SEP_ARRAY p i a [] = set_sep.emp)
  p i a x xs.
    set_sep.SEP_ARRAY p i a (x :: xs) =
    set_sep.STAR (p a x) (set_sep.SEP_ARRAY p i (words.word_add a i) xs)

x p c1 c2 q b1 b2.
    prog.SPEC x (set_sep.STAR p (set_sep.cond b1)) c1 q
    prog.SPEC x (set_sep.STAR p (set_sep.cond b2)) c2 q
    prog.SPEC x (set_sep.STAR p (set_sep.cond (b1 b2)))
      (pred_set.UNION c1 c2) q

f x.
    tailrec.SHORT_TAILREC f x =
    (if Data.Sum.isLeft (fst (f x)) then
       tailrec.SHORT_TAILREC f (Data.Sum.destLeft (fst (f x)))
     else Data.Sum.destRight (fst (f x)))
    (tailrec.SHORT_TAILREC_PRE f x
     snd (f x)
     (Data.Sum.isLeft (fst (f x))
      tailrec.SHORT_TAILREC_PRE f (Data.Sum.destLeft (fst (f x)))))

n m.
    words.word_add (words.n2w n) (words.n2w m) = words.n2w (n + m)
    words.word_add (words.word_add x (words.n2w n)) (words.n2w m) =
    words.word_add x (words.n2w (n + m))
    words.word_sub (words.word_sub x (words.n2w n)) (words.n2w m) =
    words.word_sub x (words.n2w (n + m))

x i j p c1 c2 q b.
    (b i prog.SPEC x p c1 q) (¬b j prog.SPEC x p c2 q)
    (if b then i else j) prog.SPEC x p (pred_set.UNION c1 c2) q

to_set next instr less allow p c q.
    prog.SPEC (to_set, next, instr, less, allow) p c q
    prog.RUN (to_set, next, instr, less, allow)
      (set_sep.STAR (prog.CODE_POOL instr c) p)
      (set_sep.STAR (prog.CODE_POOL instr c) q)

x.
    address.ADDR30 (address.ADDR32 x) = x
    address.ADDR30 (words.word_add (address.ADDR32 x) (words.n2w 0)) = x
    address.ADDR30 (words.word_add (address.ADDR32 x) (words.n2w 1)) = x
    address.ADDR30
      (words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 0))) =
    x
    address.ADDR30 (words.word_add (address.ADDR32 x) (words.n2w 3)) = x

x n.
    words.word_add x (words.n2w n) =
    if n < arithmetic.BIT2 0 31 then words.word_add x (words.n2w n)
    else
      words.word_sub x
        (words.n2w
           (arithmetic.- (arithmetic.BIT2 0 arithmetic.BIT2 15)
              (n mod arithmetic.BIT2 0 arithmetic.BIT2 15)))

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)

P.
    (x. tailrec.TAILREC_PRE f1 g p x p x g x P (f1 x) P x)
    (x. tailrec.TAILREC_PRE f1 g p x p x ¬g x P x)
    x. tailrec.TAILREC_PRE f1 g p x P x

x p p' c1 m c2 q q' b1 b2.
    (b1 prog.SPEC x (set_sep.STAR m q') c2 q)
    (b2 prog.SPEC x p c1 (set_sep.STAR m p')) b1 b2
    prog.SPEC x (set_sep.STAR p q') (pred_set.UNION c1 c2)
      (set_sep.STAR q p')

x n.
    words.word_add x (words.n2w n) =
    if n < arithmetic.BIT2 0 63 then words.word_add x (words.n2w n)
    else
      words.word_sub x
        (words.n2w
           (arithmetic.- (arithmetic.BIT2 0 arithmetic.BIT2 31)
              (n mod arithmetic.BIT2 0 arithmetic.BIT2 31)))

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)

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)

x p p' c1 m c2 q q' b1 b2 d.
    (b1 prog.SPEC x (set_sep.STAR m q') c2 q)
    (b2 prog.SPEC x p c1 (set_sep.SEP_DISJ (set_sep.STAR m p') d))
    b1 b2
    prog.SPEC x (set_sep.STAR p q') (pred_set.UNION c1 c2)
      (set_sep.SEP_DISJ (set_sep.STAR q p') (set_sep.STAR d q'))

prog.SPEC model pre code (set_sep.SEP_DISJ post err)
  bool.LET
    (λto_set.
       bool.LET
         (λinstr.
            bool.LET
              (λless.
                 (s r.
                    prog.SEP_REFINE
                      (set_sep.STAR
                         (set_sep.STAR pre (prog.CODE_POOL instr code)) r)
                      less to_set s
                    ¬prog.SEP_REFINE
                        (set_sep.STAR
                           (set_sep.STAR post (prog.CODE_POOL instr code))
                           r) less to_set s)
                 temporal.SPEC_1 model pre code post err)
              (fst (snd (snd (snd model))))) (fst (snd (snd model))))
    (fst model)

b c x y.
    (if b then if c then x else y else y) = (if b c then x else y)
    (if b then if c then y else x else y) = (if b ¬c then x else y)
    (if b then x else if c then x else y) = (if b c then x else y)
    (if b then x else if c then y else x) = if b ¬c then x else y

x y.
    words.word_add (words.word_2comp y) x = words.word_sub x y
    words.word_add x (words.word_2comp y) = words.word_sub x y
    words.word_add (words.word_mul (words.word_2comp (words.n2w 1)) y) x =
    words.word_sub x y
    words.word_add (words.word_mul y (words.word_2comp (words.n2w 1))) x =
    words.word_sub x y
    words.word_add x (words.word_mul (words.word_2comp (words.n2w 1)) y) =
    words.word_sub x y
    words.word_add x (words.word_mul y (words.word_2comp (words.n2w 1))) =
    words.word_sub x y

f1 f2 g p res res' c m.
    (x y. g x p x y = f1 x prog.SPEC m (res x) c (res y))
    (x y. ¬g x p x y = f2 x prog.SPEC m (res x) c (res' y))
    x.
      tailrec.TAILREC_PRE f1 g p x
      prog.SPEC m (res x) c (res' (tailrec.TAILREC f1 f2 g x))

x a.
    (address.ALIGNED
       (words.word_add a
          (words.word_mul (words.n2w (arithmetic.BIT2 1)) x))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_add (words.word_mul (words.n2w (arithmetic.BIT2 1)) x)
          a) address.ALIGNED a)
    (address.ALIGNED
       (words.word_add a
          (words.word_mul x (words.n2w (arithmetic.BIT2 1))))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_add (words.word_mul x (words.n2w (arithmetic.BIT2 1)))
          a) address.ALIGNED a)
    (address.ALIGNED (words.word_add a (words.n2w (arithmetic.BIT2 1)))
     address.ALIGNED a)
    (address.ALIGNED (words.word_add (words.n2w (arithmetic.BIT2 1)) a)
     address.ALIGNED a)

a.
    (words.word_and a (words.n2w 3) = words.n2w 0 address.ALIGNED a)
    (words.word_and (words.n2w 3) a = words.n2w 0 address.ALIGNED a)
    (words.n2w 0 = words.word_and a (words.n2w 3) address.ALIGNED a)
    (words.n2w 0 = words.word_and (words.n2w 3) a address.ALIGNED a)
    (words.w2n a mod arithmetic.BIT2 1 = 0 address.ALIGNED a)
    (0 = words.w2n a mod arithmetic.BIT2 1 address.ALIGNED a)

f res res' c m.
    (x y.
       Data.Sum.isLeft (fst (f x)) snd (f x)
       y = Data.Sum.destLeft (fst (f x)) prog.SPEC m (res x) c (res y))
    (x y.
       ¬Data.Sum.isLeft (fst (f x)) snd (f x)
       y = Data.Sum.destRight (fst (f x))
       prog.SPEC m (res x) c (res' y))
    x.
      tailrec.SHORT_TAILREC_PRE f x
      prog.SPEC m (res x) c (res' (tailrec.SHORT_TAILREC f x))

f1 f2 g p res res' c m.
    (z x y. g x p x y = f1 x prog.SPEC m (res z x) c (res z y))
    (z x y. ¬g x p x y = f2 x prog.SPEC m (res z x) c (res' z y))
    z x.
      tailrec.TAILREC_PRE f1 g p x
      prog.SPEC m (res z x) c (res' z (tailrec.TAILREC f1 f2 g x))

f res res' c m.
    (z x y.
       Data.Sum.isLeft (fst (f x)) snd (f x)
       y = Data.Sum.destLeft (fst (f x))
       prog.SPEC m (res z x) c (res z y))
    (z x y.
       ¬Data.Sum.isLeft (fst (f x)) snd (f x)
       y = Data.Sum.destRight (fst (f x))
       prog.SPEC m (res z x) c (res' z y))
    z x.
      tailrec.SHORT_TAILREC_PRE f x
      prog.SPEC m (res z x) c (res' z (tailrec.SHORT_TAILREC f x))

%%genvar%%3634 w x.
    (words.word_add %%genvar%%3634 w = words.word_add x w
     %%genvar%%3634 = x)
    (words.word_add w %%genvar%%3634 = words.word_add x w
     %%genvar%%3634 = x)
    (words.word_add %%genvar%%3634 w = words.word_add w x
     %%genvar%%3634 = x)
    (words.word_add w %%genvar%%3634 = words.word_add w x
     %%genvar%%3634 = x) (w = words.word_add x w x = words.n2w 0)
    (words.word_add %%genvar%%3634 w = w %%genvar%%3634 = words.n2w 0)
    (w = words.word_add w x x = words.n2w 0)
    (words.word_add w %%genvar%%3634 = w %%genvar%%3634 = words.n2w 0)

a b.
    (address.ADDR32 a = address.ADDR32 b a = b)
    (address.ADDR32 a = words.word_add (address.ADDR32 b) (words.n2w 0)
     a = b)
    (words.word_add (address.ADDR32 a) (words.n2w 0) = address.ADDR32 b
     a = b)
    (words.word_add (address.ADDR32 a) (words.n2w 0) =
     words.word_add (address.ADDR32 b) (words.n2w 0) a = b)
    (words.word_add (address.ADDR32 a) (words.n2w 1) =
     words.word_add (address.ADDR32 b) (words.n2w 1) a = b)
    (words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0)) =
     words.word_add (address.ADDR32 b) (words.n2w (arithmetic.BIT2 0))
     a = b)
    (words.word_add (address.ADDR32 a) (words.n2w 3) =
     words.word_add (address.ADDR32 b) (words.n2w 3) a = b)

x n p.
    words.word_add x (words.word_mul (words.n2w n) x) =
    words.word_mul (words.n2w (n + 1)) x
    words.word_add x (words.word_mul x (words.n2w n)) =
    words.word_mul (words.n2w (n + 1)) x
    words.word_add (words.word_mul (words.n2w n) x) x =
    words.word_mul (words.n2w (n + 1)) x
    words.word_add (words.word_mul (words.n2w n) x) x =
    words.word_mul (words.n2w (n + 1)) x
    words.word_add (words.word_add p x) (words.word_mul (words.n2w n) x) =
    words.word_add p (words.word_mul (words.n2w (n + 1)) x)
    words.word_add (words.word_add p x) (words.word_mul x (words.n2w n)) =
    words.word_add p (words.word_mul (words.n2w (n + 1)) x)
    words.word_add (words.word_add p (words.word_mul (words.n2w n) x)) x =
    words.word_add p (words.word_mul (words.n2w (n + 1)) x)
    words.word_add (words.word_add p (words.word_mul (words.n2w n) x)) x =
    words.word_add p (words.word_mul (words.n2w (n + 1)) x)

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

a x.
    (address.ALIGNED (words.n2w 0) )
    (address.ALIGNED (words.n2w (arithmetic.BIT2 (bit1 x))) )
    (address.ALIGNED (words.n2w (bit1 (arithmetic.BIT2 x))) )
    (address.ALIGNED (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 x)))
     ) (address.ALIGNED (words.n2w (bit1 (bit1 (bit1 x)))) )
    (address.ALIGNED (words.n2w (bit1 (bit1 (arithmetic.BIT2 x)))) )
    (address.ALIGNED (words.word_add a (words.n2w 0))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_add a (words.n2w (arithmetic.BIT2 (bit1 x))))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_add a (words.n2w (bit1 (arithmetic.BIT2 x))))
     address.ALIGNED (words.word_add a (words.n2w 1)))
    (address.ALIGNED
       (words.word_add a
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 x))))
     address.ALIGNED (words.word_add a (words.n2w (arithmetic.BIT2 0))))
    (address.ALIGNED
       (words.word_add a (words.n2w (bit1 (bit1 (bit1 x)))))
     address.ALIGNED (words.word_add a (words.n2w 3)))
    (address.ALIGNED
       (words.word_add a (words.n2w (bit1 (bit1 (arithmetic.BIT2 x)))))
     address.ALIGNED (words.word_add a (words.n2w 3)))
    (address.ALIGNED (words.word_sub a (words.n2w 0))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_sub a (words.n2w (arithmetic.BIT2 (bit1 x))))
     address.ALIGNED a)
    (address.ALIGNED
       (words.word_sub a (words.n2w (bit1 (arithmetic.BIT2 x))))
     address.ALIGNED (words.word_sub a (words.n2w 1)))
    (address.ALIGNED
       (words.word_sub a
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 x))))
     address.ALIGNED (words.word_sub a (words.n2w (arithmetic.BIT2 0))))
    (address.ALIGNED
       (words.word_sub a (words.n2w (bit1 (bit1 (bit1 x)))))
     address.ALIGNED (words.word_sub a (words.n2w 3)))
    (address.ALIGNED
       (words.word_sub a (words.n2w (bit1 (bit1 (arithmetic.BIT2 x)))))
     address.ALIGNED (words.word_sub a (words.n2w 3)))

a b.
    ¬(words.word_add (address.ADDR32 a) (words.n2w 0) =
       words.word_add (address.ADDR32 b) (words.n2w 1))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 0) =
       words.word_add (address.ADDR32 b) (words.n2w (arithmetic.BIT2 0)))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 0) =
       words.word_add (address.ADDR32 b) (words.n2w 3))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 1) =
       words.word_add (address.ADDR32 b) (words.n2w (arithmetic.BIT2 0)))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 1) =
       words.word_add (address.ADDR32 b) (words.n2w 3))
    ¬(words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0)) =
       words.word_add (address.ADDR32 b) (words.n2w 3))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 1) =
       words.word_add (address.ADDR32 b) (words.n2w 0))
    ¬(words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0)) =
       words.word_add (address.ADDR32 b) (words.n2w 0))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 3) =
       words.word_add (address.ADDR32 b) (words.n2w 0))
    ¬(words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0)) =
       words.word_add (address.ADDR32 b) (words.n2w 1))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 3) =
       words.word_add (address.ADDR32 b) (words.n2w 1))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 3) =
       words.word_add (address.ADDR32 b) (words.n2w (arithmetic.BIT2 0)))
    ¬(words.word_add (address.ADDR32 a) (words.n2w 1) = address.ADDR32 b)
    ¬(words.word_add (address.ADDR32 a) (words.n2w (arithmetic.BIT2 0)) =
       address.ADDR32 b)
    ¬(words.word_add (address.ADDR32 a) (words.n2w 3) = address.ADDR32 b)
    ¬(address.ADDR32 a = words.word_add (address.ADDR32 b) (words.n2w 1))
    ¬(address.ADDR32 a =
       words.word_add (address.ADDR32 b) (words.n2w (arithmetic.BIT2 0)))
    ¬(address.ADDR32 a = words.word_add (address.ADDR32 b) (words.n2w 3))

words.word_add (address.ADDR32 x) (words.n2w 0) = address.ADDR32 x
  words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 1)) =
  address.ADDR32 (words.word_add x (words.n2w 1))
  words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 3)) =
  address.ADDR32 (words.word_add x (words.n2w (arithmetic.BIT2 0)))
  words.word_add (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))) =
  address.ADDR32 (words.word_add x (words.n2w 3))
  words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 7)) =
  address.ADDR32 (words.word_add x (words.n2w (arithmetic.BIT2 1)))
  words.word_add (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 1)))) =
  address.ADDR32
    (words.word_add x (words.n2w (bit1 (arithmetic.BIT2 0))))
  words.word_add (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))) =
  address.ADDR32
    (words.word_add x (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0))))
  words.word_add (address.ADDR32 x)
    (words.n2w
       (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))) =
  address.ADDR32 (words.word_add x (words.n2w 7))
  words.word_add (address.ADDR32 x) (words.n2w (arithmetic.BIT2 15)) =
  address.ADDR32 (words.word_add x (words.n2w (arithmetic.BIT2 3)))
  words.word_add (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 3)))) =
  address.ADDR32
    (words.word_add x (words.n2w (bit1 (arithmetic.BIT2 1))))
  words.word_add (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 1))))) =
  address.ADDR32
    (words.word_add x (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 1))))
  words.word_sub (address.ADDR32 x) (words.n2w 0) =
  address.ADDR32 (words.word_sub x (words.n2w 0))
  words.word_sub (address.ADDR32 x) (words.n2w (arithmetic.BIT2 1)) =
  address.ADDR32 (words.word_sub x (words.n2w 1))
  words.word_sub (address.ADDR32 x) (words.n2w (arithmetic.BIT2 3)) =
  address.ADDR32 (words.word_sub x (words.n2w (arithmetic.BIT2 0)))
  words.word_sub (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))) =
  address.ADDR32 (words.word_sub x (words.n2w 3))
  words.word_sub (address.ADDR32 x) (words.n2w (arithmetic.BIT2 7)) =
  address.ADDR32 (words.word_sub x (words.n2w (arithmetic.BIT2 1)))
  words.word_sub (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 1)))) =
  address.ADDR32
    (words.word_sub x (words.n2w (bit1 (arithmetic.BIT2 0))))
  words.word_sub (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))) =
  address.ADDR32
    (words.word_sub x (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0))))
  words.word_sub (address.ADDR32 x)
    (words.n2w
       (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))) =
  address.ADDR32 (words.word_sub x (words.n2w 7))
  words.word_sub (address.ADDR32 x) (words.n2w (arithmetic.BIT2 15)) =
  address.ADDR32 (words.word_sub x (words.n2w (arithmetic.BIT2 3)))
  words.word_sub (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 3)))) =
  address.ADDR32
    (words.word_sub x (words.n2w (bit1 (arithmetic.BIT2 1))))
  words.word_sub (address.ADDR32 x)
    (words.n2w (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 1))))) =
  address.ADDR32
    (words.word_sub x (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 1))))

a b.
    (((words.word_msb (words.word_sub a b)
       ¬(words.word_msb a words.word_msb b)
       ¬(words.word_msb a words.word_msb (words.word_sub a b)))
      words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb b words.word_msb a)
       ¬(words.word_msb a words.word_msb (words.word_sub a b)))
      words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb a words.word_msb b)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a))
      words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb b words.word_msb a)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a))
      words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb a words.word_msb (words.word_sub a b))
       ¬(words.word_msb a words.word_msb b)) words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb a words.word_msb (words.word_sub a b))
       ¬(words.word_msb b words.word_msb a)) words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a)
       ¬(words.word_msb a words.word_msb b)) words.word_le b a)
     ((words.word_msb (words.word_sub a b)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a)
       ¬(words.word_msb b words.word_msb a)) words.word_le b a)
     ((¬(words.word_msb a words.word_msb b)
       ¬(words.word_msb a words.word_msb (words.word_sub a b))
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb b words.word_msb a)
       ¬(words.word_msb a words.word_msb (words.word_sub a b))
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb a words.word_msb b)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a)
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb b words.word_msb a)
       ¬(words.word_msb (words.word_sub a b) words.word_msb a)
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb a words.word_msb (words.word_sub a b))
       ¬(words.word_msb a words.word_msb b)
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb a words.word_msb (words.word_sub a b))
       ¬(words.word_msb b words.word_msb a)
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb (words.word_sub a b) words.word_msb a)
       ¬(words.word_msb a words.word_msb b)
       words.word_msb (words.word_sub a b)) words.word_le b a)
     ((¬(words.word_msb (words.word_sub a b) words.word_msb a)
       ¬(words.word_msb b words.word_msb a)
       words.word_msb (words.word_sub a b)) words.word_le b a))
    (words.word_ge a b words.word_le b a)
    (words.word_gt a b words.word_lt b a)
    (¬words.word_ls a b words.word_lo b a)
    (¬words.word_lo a b words.word_ls b a)
    (words.word_lo a b a = b words.word_ls a b)
    (¬words.word_lt a b words.word_le b a)
    (¬words.word_le a b words.word_lt b a)
    (words.word_lt a b a = b words.word_le a b)
    (a = b words.word_lt a b words.word_le a b)
    (words.word_lo a b a = b words.word_ls a b)
    (a = b words.word_lo a b words.word_ls a b)
    (words.word_ls b a ¬(a = b) words.word_lo b a)
    (¬(a = b) words.word_ls b a words.word_lo b a)
    (words.word_le b a ¬(a = b) words.word_lt b a)
    (¬(a = b) words.word_le b a words.word_lt b a)
    (words.word_sub v w = words.n2w 0 v = w)
    words.word_sub w (words.n2w 0) = w

External Type Operators

External Constants

Assumptions

0 = 0

0 < fcp.dimindex bool.the_value

0 < words.dimword bool.the_value

pred_set.BIGUNION pred_set.EMPTY = pred_set.EMPTY

x. x = x

t. t

n. 0 n

m. m m

s. pred_set.SUBSET pred_set.EMPTY s

bool.IN = λx f. f x

bool.LET = λf x. f x

fcp.dimindex bool.the_value = arithmetic.BIT2 0

1 = suc 0

1 < words.dimword bool.the_value

arithmetic.DIV2 (bit1 x) = x

words.w2n (words.n2w 0) = 0

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. id x = x

t. t ¬t

n. ¬(n < 0)

n. ¬(n < n)

(¬) = λt. t

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

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

arithmetic.BIT2 0 = suc 1

words.word_2comp (words.n2w 1) = words.word_T

¬(p q) p

x. x = x

c. arithmetic.- c c = 0

n. n * 0 = 0

n. min n n = n

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

s. pred_set.UNION s s = s

w. words.n2w (words.w2n w) = w

w. words.word_2comp (words.word_2comp w) = w

R. wellFounded R prim_rec.wellfounded R

flip = λf x y. f y x

fcp.dimindex bool.the_value = arithmetic.BIT2 3

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

q. q div 1 = q

x. ¬Data.Sum.isLeft x Data.Sum.isRight x

w. words.w2w w = words.n2w (words.w2n w)

w. words.word_sub w w = words.n2w 0

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

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

() = λp q. p q p

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))

t. t t

t. (t ) (t )

n. arithmetic.DIV2 n = n div arithmetic.BIT2 0

m. suc m = m + 1

n. suc n = 1 + n

n. n 0 n = 0

x.
    numeral_bit.FDUB numeral_bit.iDIV2 x =
    numeral_bit.iDIV2 (numeral_bit.iDIV2 x)

a. arithmetic.- (suc a) a = 1

m. arithmetic.- (suc m) 1 = m

x. (fst x, snd x) = x

x y. fst (x, y) = x

x y. snd (x, y) = y

n. words.n2w n = fcp.FCP (λi. bit.BIT i n)

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

fcp.dimindex bool.the_value = arithmetic.BIT2 15

¬( ) ¬( )

n. words.w2n (words.n2w n) = n mod words.dimword bool.the_value

n. ¬(n = 0) 0 < n

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

n. words.n2w (n mod words.dimword bool.the_value) = words.n2w n

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

x y. x = y y = x

A B. A B B A

m n. m * n = n * m

m n. m + n = n + m

s t. pred_set.INTER s t = pred_set.INTER t s

s t. pred_set.UNION s t = pred_set.UNION t s

a b. words.word_ge a b words.word_le b a

a b. words.word_gt a b words.word_lt b a

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

a b. words.word_and a b = words.word_and b a

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

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

(¬A ) (A )

n. bit1 n = n + (n + suc 0)

n. 0 < n 0 mod n = 0

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

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

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

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

a b. words.word_lo a b ¬(a = b)

a b. words.word_lt a b ¬(a = b)

a b. ¬words.word_le a b words.word_lt b a

a b. ¬words.word_lo a b words.word_ls b a

a b. ¬words.word_ls a b words.word_lo b a

a b. ¬words.word_lt a b words.word_le b a

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

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

n. odd n n mod arithmetic.BIT2 0 = 1

n. arithmetic.BIT2 n = n + (n + suc (suc 0))

i. i < fcp.dimindex bool.the_value ¬fcp.fcp_index (words.n2w 0) i

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

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

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

(x'. P x') p_1 p_2. P (p_1, p_2)

i n. bit.BIT i n bool.IN i (words.BIT_SET 0 n)

h l. words.word_extract h l = words.w2w words.word_bits h l

m n. 0 < n m mod n < n

n k. k < n k mod n = k

m n. ¬(m n) suc n m

s x.
    pred_set.DELETE s x =
    pred_set.DIFF s (pred_set.INSERT x pred_set.EMPTY)

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

a b. words.word_lo a b words.w2n a < words.w2n b

a b. words.word_ls a b words.w2n a words.w2n b

w. n. w = words.n2w n n < words.dimword bool.the_value

words.dimword bool.the_value = arithmetic.BIT2 127

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

n. min n 0 = 0 min 0 n = 0

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

f. id f = f f id = f

w.
    words.w2w w =
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 w

x n. bit.MOD_2EXP x n = n mod arithmetic.BIT2 0 x

x n. bit.TIMES_2EXP x n = n * arithmetic.BIT2 0 x

m n. words.word_add (words.n2w m) (words.n2w n) = words.n2w (m + n)

m n. words.word_mul (words.n2w m) (words.n2w n) = words.n2w (m * n)

v w. words.word_div v w = words.n2w (words.w2n v div words.w2n w)

w v. words.word_sub v w = words.n2w 0 v = w

s1 s2.
    pred_set.BIGUNION (pred_set.UNION s1 s2) =
    pred_set.UNION (pred_set.BIGUNION s1) (pred_set.BIGUNION s2)

h l w. words.word_bits h l w = words.word_extract h l w

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

n.
    words.word_2comp (words.n2w n) =
    words.n2w
      (arithmetic.- (words.dimword bool.the_value)
         (n mod words.dimword bool.the_value))

i. i < fcp.dimindex bool.the_value fcp.fcp_index (fcp.FCP g) i = g i

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

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

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

m n. m = n m n n m

b n. bit.BIT b n bit.BITS b b n = 1

n q. 0 < n q * n div n = q

n. 0 < n k. k * n mod n = 0

a n.
    words.word_lsl a n =
    words.word_mul (words.n2w (arithmetic.BIT2 0 n)) a

a b. words.word_le a b words.word_lt a b a = b

a b. words.word_ls a b words.word_lo a b a = b

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

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

¬(¬A B) A ¬B

h l n. h < l bit.BITS h l n = 0

R. prim_rec.wellfounded R ¬f. n. R (f (suc n)) (f n)

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

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

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

m n. m < suc n m = n m < n

h n. bit.BITS h 0 n = n mod arithmetic.BIT2 0 suc h

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

¬(A B) (A ) ¬B

x s t.
    pred_set.UNION (pred_set.INSERT x s) t =
    pred_set.INSERT x (pred_set.UNION s t)

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. arithmetic.- m n p m n + p

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

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

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

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

m n p. m < n n < p m < p

m n p. m n n p m p

n. 1 n = 1 n 1 = n

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

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

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

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

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

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

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

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

v w.
    words.word_and v w =
    fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

v w.
    words.word_or v w = fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

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

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

x y. 0 < y (x mod y = x x < y)

n. 0 < n k. k mod n mod n = k mod n

length [] = 0 h t. length (h :: t) = suc (length t)

(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

n. ¬(n mod arithmetic.BIT2 0 = 0) n mod arithmetic.BIT2 0 = 1

P. P 0 (n. P n P (suc n)) k. P k

v w.
    words.word_xor v w =
    fcp.FCP (λi. ¬(fcp.fcp_index v i fcp.fcp_index w i))

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

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

w h.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    words.word_bits h 0 w = w

a b.
    words.word_and a b = words.n2w 0
    words.word_add a b = words.word_or a b

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

x s t.
    pred_set.SUBSET (pred_set.INSERT x s) t
    bool.IN x t pred_set.SUBSET s t

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

P Q R. P Q R (P R) (Q R)

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

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

h l n.
    bit.BITS h l n =
    bit.MOD_2EXP (arithmetic.- (suc h) l) (bit.DIV_2EXP l n)

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

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

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

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

n r. r < n q. (q * n + r) mod n = r

n a b.
    words.word_lsl (words.word_add a b) n =
    words.word_add (words.word_lsl a n) (words.word_lsl b n)

n. 0 < n n div n = 1 n mod n = 0

f s t.
    pred_set.IMAGE f (pred_set.UNION s t) =
    pred_set.UNION (pred_set.IMAGE f s) (pred_set.IMAGE f t)

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

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)

v w x.
    words.word_mul (words.word_sub w x) v =
    words.word_sub (words.word_mul w v) (words.word_mul x v)

(x. bit.MOD_2EXP x 0 = 0)
  x n. bit.MOD_2EXP x n = numeral_bit.iMOD_2EXP x n

m n.
    words.n2w m = words.n2w n
    m mod words.dimword bool.the_value = n mod words.dimword bool.the_value

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)

P g x. while.WHILE P g x = if P x then while.WHILE P g (g x) else x

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) (i. P i) x. Q x

(n. bit.DIV_2EXP n 0 = 0)
  n x. bit.DIV_2EXP n x = numeral_bit.SFUNPOW numeral_bit.iDIV2 n x

(n. bit.TIMES_2EXP n 0 = 0)
  n x. bit.TIMES_2EXP n x = numeral_bit.SFUNPOW numeral.iDUB n x

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

a b.
    words.word_ge a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. n v))))
      (words.nzcv a b)

P. P [] (t. P t h. P (h :: t)) l. P l

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

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

m n p. m * n < m * p 0 < m n < p

m n p. m * n m * p m = 0 n p

n. 0 < n q r. (q * n + r) mod n = r mod n

a b.
    words.w2w (words.word_add a b) =
    words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) 0
      (words.word_add (words.w2w a) (words.w2w b))

words.dimword bool.the_value = arithmetic.BIT2 32767

x y.
    x = y
    i.
      i < fcp.dimindex bool.the_value
      fcp.fcp_index x i = fcp.fcp_index y i

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

k n. 0 < n r q. k = q * n + r r < n

w i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.w2w w) i
     i < fcp.dimindex bool.the_value fcp.fcp_index w i)

h l n.
    bit.BITS h l n =
    n mod arithmetic.BIT2 0 suc h div arithmetic.BIT2 0 l

n. 0 < n x r. (x * n + r) div n = x + r div n

n.
    numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
    numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
    numeral.iDUB 0 = 0

n i.
    fcp.fcp_index (words.n2w n) i
    if i < fcp.dimindex bool.the_value then bit.BIT i n
    else combin.FAIL fcp.fcp_index index too large (words.n2w n) i

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

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

min 0 x = 0 min x 0 = 0 min x y = if x < y then x else y

f0 f1. fn. fn [] = f0 a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)

n.
    words.w2w (words.n2w n) =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
      words.n2w n
    else
      words.n2w
        (bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 n)

w n.
    words.word_lsl w n =
    fcp.FCP
      (λi.
         i < fcp.dimindex bool.the_value n i
         fcp.fcp_index w (arithmetic.- i n))

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

n k q. (r. k = q * n + r r < n) k div n = q

n k r. (q. k = q * n + r r < n) k mod n = r

(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)

(l. [] @ l = l) l1 l2 h. (h :: l1) @ l2 = h :: l1 @ l2

h l n.
    bit.BITS h l n =
    n div arithmetic.BIT2 0 l mod
    arithmetic.BIT2 0 arithmetic.- (suc h) l

m n. 0 < n 0 < m x. x mod n * m mod n = x mod n

n. 0 < n j k. (j mod n + k mod n) mod n = (j + k) mod 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)

n. 0 < n k. k = (k div n) * n + k mod n k mod n < n

n m.
    words.word_lsl (words.n2w m) n =
    if arithmetic.- (fcp.dimindex bool.the_value) 1 < n then words.n2w 0
    else words.n2w (m * arithmetic.BIT2 0 n)

h1 l1 h2 l2 n.
    bit.BITS h2 l2 (bit.BITS h1 l1 n) =
    bit.BITS (min h1 (h2 + l1)) (l2 + l1) n

n.
    even 0 even (arithmetic.BIT2 n) ¬even (bit1 n) ¬odd 0
    ¬odd (arithmetic.BIT2 n) odd (bit1 n)

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

h l.
    words.word_bits h l =
    λw.
      fcp.FCP
        (λi.
           i + l min h (arithmetic.- (fcp.dimindex bool.the_value) 1)
           fcp.fcp_index w (i + l))

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

numeral.texp_help 0 acc = arithmetic.BIT2 acc
  numeral.texp_help (bit1 n) acc =
  numeral.texp_help (prim_rec.PRE (bit1 n)) (bit1 acc)
  numeral.texp_help (arithmetic.BIT2 n) acc =
  numeral.texp_help (bit1 n) (bit1 acc)

numeral.exactlog 0 = 0 (n. numeral.exactlog (bit1 n) = 0)
  n.
    numeral.exactlog (arithmetic.BIT2 n) =
    bool.LET (λx. if x = 0 then 0 else bit1 x) (numeral.onecount n 0)

(x. numeral.onecount 0 x = x)
  (n x. numeral.onecount (bit1 n) x = numeral.onecount n (suc x))
  n x. numeral.onecount (arithmetic.BIT2 n) x = 0

arithmetic.BIT2 0 0 = 1
  arithmetic.BIT2 0 bit1 n =
  numeral.texp_help (prim_rec.PRE (bit1 n)) 0
  arithmetic.BIT2 0 arithmetic.BIT2 n = numeral.texp_help (bit1 n) 0

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

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

n i.
    words.BIT_SET i n =
    if n = 0 then pred_set.EMPTY
    else if odd n then
      pred_set.INSERT i (words.BIT_SET (suc i) (n div arithmetic.BIT2 0))
    else words.BIT_SET (suc i) (n div arithmetic.BIT2 0)

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

(m n.
     words.word_mul (words.n2w m) (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m * n)))
  m n.
    words.word_mul (words.word_2comp (words.n2w m))
      (words.word_2comp (words.n2w n)) = words.n2w (m * n)

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

n m p. (min m n < p m < p n < p) (p < min m n p < m p < n)

n m p. (min m n p m p n p) (p min m n p m p n)

a.
    words.word_or words.word_T a = words.word_T
    words.word_or a words.word_T = words.word_T
    words.word_or (words.n2w 0) a = a words.word_or a (words.n2w 0) = a
    words.word_or a a = a

words.dimword bool.the_value = arithmetic.BIT2 536870911

a.
    words.word_and words.word_T a = a words.word_and a words.word_T = a
    words.word_and (words.n2w 0) a = words.n2w 0
    words.word_and a (words.n2w 0) = words.n2w 0 words.word_and a a = a

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)

h l n w.
    h < fcp.dimindex bool.the_value
    words.word_extract h l (words.word_lsl w n) =
    if n h then
      words.word_lsl
        (words.word_extract (arithmetic.- h n) (arithmetic.- l n) w)
        (arithmetic.- n l)
    else words.n2w 0

words.dimword bool.the_value = arithmetic.BIT2 2147483647

(a. words.word_lsl a 0 = a) (a. words.word_asr a 0 = a)
  (a. words.word_lsr a 0 = a) (a. words.word_rol a 0 = a)
  a. words.word_ror a 0 = a

f g.
    (n. g (suc n) = f n (suc n))
    (n. g (bit1 n) = f (arithmetic.- (bit1 n) 1) (bit1 n))
    n. g (arithmetic.BIT2 n) = f (bit1 n) (arithmetic.BIT2 n)

w h l m n.
    words.word_extract h l (words.word_extract m n w) =
    words.word_extract
      (min m
         (min (h + n)
            (min (arithmetic.- (fcp.dimindex bool.the_value) 1)
               (arithmetic.- (fcp.dimindex bool.the_value + n) 1))))
      (l + n) w

n m.
    numeral.internal_mult 0 n = 0 numeral.internal_mult n 0 = 0
    numeral.internal_mult (bit1 n) m =
    numeral.iZ (numeral.iDUB (numeral.internal_mult n m) + m)
    numeral.internal_mult (arithmetic.BIT2 n) m =
    numeral.iDUB (numeral.iZ (numeral.internal_mult n m + m))

n m.
    0 * n = 0 n * 0 = 0
    bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m)
    arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))

prim_rec.PRE 0 = 0 prim_rec.PRE 1 = 0
  (n.
     prim_rec.PRE (bit1 (bit1 n)) =
     arithmetic.BIT2 (prim_rec.PRE (bit1 n)))
  (n.
     prim_rec.PRE (bit1 (arithmetic.BIT2 n)) = arithmetic.BIT2 (bit1 n))
  n. prim_rec.PRE (arithmetic.BIT2 n) = bit1 n

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

words.word_extract h l (words.n2w n) =
  if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
    words.n2w
      (bit.BITS (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l n)
  else
    words.n2w
      (bit.BITS
         (min (min h (arithmetic.- (fcp.dimindex bool.the_value) 1))
            (arithmetic.- (fcp.dimindex bool.the_value) 1 + l)) l n)

(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)

numeral_bit.iDIV2 0 = 0 numeral_bit.iDIV2 (numeral_bit.iSUC 0) = 0
  numeral_bit.iDIV2 (bit1 n) = n
  numeral_bit.iDIV2 (numeral_bit.iSUC (bit1 n)) = numeral_bit.iSUC n
  numeral_bit.iDIV2 (arithmetic.BIT2 n) = numeral_bit.iSUC n
  numeral_bit.iDIV2 (numeral_bit.iSUC (arithmetic.BIT2 n)) =
  numeral_bit.iSUC n numeral_bit.iSUC n = suc n

a b.
    words.nzcv a b =
    bool.LET
      (λq.
         bool.LET
           (λr.
              (words.word_msb r, r = words.n2w 0,
               bit.BIT (fcp.dimindex bool.the_value) q b = words.n2w 0,
               ¬(words.word_msb a words.word_msb b)
               ¬(words.word_msb r words.word_msb a))) (words.n2w q))
      (words.w2n a + words.w2n (words.word_2comp b))

(x. numeral_bit.SFUNPOW numeral_bit.iDIV2 0 x = x)
  (y. numeral_bit.SFUNPOW numeral_bit.iDIV2 y 0 = 0)
  (n x.
     numeral_bit.SFUNPOW numeral_bit.iDIV2 (bit1 n) x =
     numeral_bit.SFUNPOW (numeral_bit.FDUB numeral_bit.iDIV2) n
       (numeral_bit.iDIV2 x))
  n x.
    numeral_bit.SFUNPOW numeral_bit.iDIV2 (arithmetic.BIT2 n) x =
    numeral_bit.SFUNPOW (numeral_bit.FDUB numeral_bit.iDIV2) n
      (numeral_bit.iDIV2 (numeral_bit.iDIV2 x))

numeral_bit.FDUB (numeral_bit.FDUB f) 0 = 0
  (x.
     numeral_bit.FDUB (numeral_bit.FDUB f) (numeral_bit.iSUC x) =
     numeral_bit.FDUB f (numeral_bit.FDUB f (numeral_bit.iSUC x)))
  (x.
     numeral_bit.FDUB (numeral_bit.FDUB f) (bit1 x) =
     numeral_bit.FDUB f (numeral_bit.FDUB f (bit1 x)))
  x.
    numeral_bit.FDUB (numeral_bit.FDUB f) (arithmetic.BIT2 x) =
    numeral_bit.FDUB f (numeral_bit.FDUB f (arithmetic.BIT2 x))

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

f.
    (x. numeral_bit.SFUNPOW (numeral_bit.FDUB f) 0 x = x)
    (y. numeral_bit.SFUNPOW (numeral_bit.FDUB f) y 0 = 0)
    (n x.
       numeral_bit.SFUNPOW (numeral_bit.FDUB f) (bit1 n) x =
       numeral_bit.SFUNPOW (numeral_bit.FDUB (numeral_bit.FDUB f)) n
         (numeral_bit.FDUB f x))
    n x.
      numeral_bit.SFUNPOW (numeral_bit.FDUB f) (arithmetic.BIT2 n) x =
      numeral_bit.SFUNPOW (numeral_bit.FDUB (numeral_bit.FDUB f)) n
        (numeral_bit.FDUB f (numeral_bit.FDUB f x))

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)

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

(h l w.
     fcp.dimindex bool.the_value fcp.dimindex bool.the_value + l
     fcp.dimindex bool.the_value h
     words.word_extract h l w =
     words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) l
       w)
  h l w.
    fcp.dimindex bool.the_value + l < fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value + l h
    words.word_extract h l w =
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value + l) 1) l
      w

words.dimword bool.the_value = arithmetic.BIT2 9223372036854775807

0 * n = 0 n * 0 = 0
  bit1 x * bit1 y = numeral.internal_mult (bit1 x) (bit1 y)
  bit1 x * arithmetic.BIT2 y =
  bool.LET
    (λn.
       if odd n then
         numeral.texp_help (arithmetic.DIV2 n) (prim_rec.PRE (bit1 x))
       else numeral.internal_mult (bit1 x) (arithmetic.BIT2 y))
    (numeral.exactlog (arithmetic.BIT2 y))
  arithmetic.BIT2 x * bit1 y =
  bool.LET
    (λm.
       if odd m then
         numeral.texp_help (arithmetic.DIV2 m) (prim_rec.PRE (bit1 y))
       else numeral.internal_mult (arithmetic.BIT2 x) (bit1 y))
    (numeral.exactlog (arithmetic.BIT2 x))
  arithmetic.BIT2 x * arithmetic.BIT2 y =
  bool.LET
    (λm.
       bool.LET
         (λn.
            if odd m then
              numeral.texp_help (arithmetic.DIV2 m)
                (prim_rec.PRE (arithmetic.BIT2 y))
            else if odd n then
              numeral.texp_help (arithmetic.DIV2 n)
                (prim_rec.PRE (arithmetic.BIT2 x))
            else
              numeral.internal_mult (arithmetic.BIT2 x)
                (arithmetic.BIT2 y))
         (numeral.exactlog (arithmetic.BIT2 y)))
    (numeral.exactlog (arithmetic.BIT2 x))

b n m.
    numeral.iSUB b 0 x = 0 numeral.iSUB n 0 = n
    numeral.iSUB (bit1 n) 0 = numeral.iDUB n
    numeral.iSUB (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (bit1 m) = bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) 0 = bit1 n
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB 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