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

Information

name	machine-code-hoare-logic
version	1.0
description	A Hoare logic for machine code
author	HOL developers <hol-developers@lists.sourceforge.net>
license	MIT
checksum	47ae51f61305fd7e712b1af8d4b8163d4b092f50
requires	base hol-base hol-words
show	Data.Bool Data.List Data.Pair Function HOL4 Number.Natural Relation

Files

Package tarball machine-code-hoare-logic-1.0.tgz
Theory source file machine-code-hoare-logic.thy (included in the package tarball)

Defined Constants

HOL4
- address
  - address.word_mod
  - address.ADDR30
  - address.ADDR32
  - address.ALIGNED
  - address.CONTAINER
  - address.DUMMY_EQ
  - address.GUARD
  - address.SING_SET
- prog
  - prog.rel_sequence
  - prog.CODE_POOL
  - prog.RUN
  - prog.SEP_REFINE
  - prog.SPEC
- set_sep
  - set_sep.cond
  - set_sep.emp
  - set_sep.fun2set
  - set_sep.one
  - set_sep.precond
  - set_sep.sidecond
  - set_sep.SEP_ARRAY
  - set_sep.SEP_DISJ
  - set_sep.SEP_EQ
  - set_sep.SEP_EXISTS
  - set_sep.SEP_F
  - set_sep.SEP_HIDE
  - set_sep.SEP_IMP
  - set_sep.SEP_T
  - set_sep.SPLIT
  - set_sep.STAR
- tailrec
  - tailrec.SHORT_TAILREC
  - tailrec.SHORT_TAILREC_PRE
  - tailrec.TAILREC
  - tailrec.TAILREC_PRE
- temporal
  - temporal.ALWAYS
  - temporal.EVENTUALLY
  - temporal.NEXT
  - temporal.NOW
  - temporal.SPEC_1
  - temporal.TEMPORAL
  - temporal.T_AND
  - temporal.T_IMPLIES
  - temporal.T_OR_F

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%%₃₃₅₄.
address.ALIGNED (words.word_2comp %%genvar%%₃₃₅₄) ⇔
address.ALIGNED %%genvar%%₃₃₅₄

⊦ 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 p₁ (temporal.NEXT p₂)) ⇒
temporal.TEMPORAL model code
(temporal.T_IMPLIES p₁ (temporal.EVENTUALLY p₂))

⊦ ∀%%genvar%%₁₅₂₀ c d. %%genvar%%₁₅₂₀ ∧ (c ⇒ d) ⇒ (%%genvar%%₁₅₂₀ ⇒ 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

⊦ ∀f₁ f₂ g x. tailrec.TAILREC f₁ f₂ g x = f₂ (while.WHILE g f₁ 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)

⊦ ∀p₁ p₂ q.
set_sep.SEP_IMP (set_sep.SEP_DISJ p₁ p₂) q ⇔
set_sep.SEP_IMP p₁ q ∧ set_sep.SEP_IMP p₂ 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%%₃₇₈₀ P.
(∀i. ¬(i = %%genvar%%₃₇₈₀) ⇒ ¬P i) ⇒ ((∃i. P i) ⇔ P %%genvar%%₃₇₈₀)

⊦ 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

⊦ ∀f₁ f₂ g x.
tailrec.TAILREC f₁ f₂ g x =
if g x then tailrec.TAILREC f₁ f₂ g (f₁ x) else f₂ 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

⊦ ∀f₁ g p x.
tailrec.TAILREC_PRE f₁ g p x ⇔
p x ∧ (g x ⇒ tailrec.TAILREC_PRE f₁ g p (f₁ 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%%₁₂₁₃ p c q q' y.
prog.SPEC %%genvar%%₁₂₁₃ p c (set_sep.STAR q (q' y)) ⇒
prog.SPEC %%genvar%%₁₂₁₃ 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 p₁ p₂ c q.
prog.SPEC x (set_sep.SEP_DISJ p₁ p₂) c q ⇔
prog.SPEC x p₁ c q ∧ prog.SPEC x p₂ 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 c₁ m c₂ q.
prog.SPEC x p c₁ m ∧ prog.SPEC x m c₂ q ⇒
prog.SPEC x p (pred_set.UNION c₁ c₂) 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%%₇₀₇ p c q.
    prog.SPEC %%genvar%%₇₀₇ p c q ⇒
    ∀r₁ r₂.
      set_sep.SEP_IMP r₁ p ∧ set_sep.SEP_IMP q r₂ ⇒
      prog.SPEC %%genvar%%₇₀₇ r₁ c r₂

⊦ ∀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)

⊦ f₁ = f1' ∧ f₂ = f2' ∧ g = g' ∧ s = s' ⇒
tailrec.TAILREC f₁ f₂ g = tailrec.TAILREC f1' f2' g' ∧
tailrec.TAILREC_PRE f₁ g s = tailrec.TAILREC_PRE f1' g' s'

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

⊦ ∀x p c q₁ q₂ q₃ q₄.
    prog.SPEC x (set_sep.STAR q₁ q₃) c q₂ ⇒
    prog.SPEC x p c (set_sep.STAR q₁ q₄) ⇒ set_sep.SEP_IMP q₄ q₃ ⇒
    prog.SPEC x p c q₂

⊦ ∀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)

⊦ ∀b₁ b₂ h₁ h₂.
    (words.w2w b₁ = words.w2w b₂ ⇔ b₁ = b₂) ∧
    (words.w2w h₁ = words.w2w h₂ ⇔ h₁ = h₂) ∧
    words.w2w (words.w2w b₁) = b₁ ∧ words.w2w (words.w2w h₁) = h₁

⊦ ∀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)

⊦ ∀f₁ guard precondition x.
    tailrec.TAILREC_PRE f₁ guard precondition x ⇔
    (∀k.
       (∀m. m < k ⇒ guard (arithmetic.FUNPOW f₁ m x)) ⇒
       precondition (arithmetic.FUNPOW f₁ k x)) ∧
    ∃n. ¬guard (arithmetic.FUNPOW f₁ n x)

⊦ ∀x p₁ p₂ c₁ m c₂ q₁ q₂.
    prog.SPEC x p₁ c₁ (set_sep.SEP_DISJ q₁ m) ∧
    prog.SPEC x (set_sep.SEP_DISJ m p₂) c₂ q₂ ⇒
    prog.SPEC x (set_sep.SEP_DISJ p₁ p₂) (pred_set.UNION c₁ c₂)
      (set_sep.SEP_DISJ q₁ q₂)

⊦ (∀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 c₁ c₂ q b₁ b₂.
    prog.SPEC x (set_sep.STAR p (set_sep.cond b₁)) c₁ q ⇒
    prog.SPEC x (set_sep.STAR p (set_sep.cond b₂)) c₂ q ⇒
    prog.SPEC x (set_sep.STAR p (set_sep.cond (b₁ ∨ b₂)))
      (pred_set.UNION c₁ c₂) 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 c₁ c₂ q b.
(b ∧ i ⇒ prog.SPEC x p c₁ q) ⇒ (¬b ∧ j ⇒ prog.SPEC x p c₂ q) ⇒
(if b then i else j) ⇒ prog.SPEC x p (pred_set.UNION c₁ c₂) 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 f₁ g p x ∧ p x ∧ g x ∧ P (f₁ x) ⇒ P x) ∧
    (∀x. tailrec.TAILREC_PRE f₁ g p x ∧ p x ∧ ¬g x ⇒ P x) ⇒
    ∀x. tailrec.TAILREC_PRE f₁ g p x ⇒ P x

⊦ ∀x p p' c₁ m c₂ q q' b₁ b₂.
    (b₁ ⇒ prog.SPEC x (set_sep.STAR m q') c₂ q) ⇒
    (b₂ ⇒ prog.SPEC x p c₁ (set_sep.STAR m p')) ⇒ b₁ ∧ b₂ ⇒
    prog.SPEC x (set_sep.STAR p q') (pred_set.UNION c₁ c₂)
      (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' c₁ m c₂ q q' b₁ b₂ d.
    (b₁ ⇒ prog.SPEC x (set_sep.STAR m q') c₂ q) ⇒
    (b₂ ⇒ prog.SPEC x p c₁ (set_sep.SEP_DISJ (set_sep.STAR m p') d)) ⇒
    b₁ ∧ b₂ ⇒
    prog.SPEC x (set_sep.STAR p q') (pred_set.UNION c₁ c₂)
      (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

⊦ ∀f₁ f₂ g p res res' c m.
    (∀x y. g x ∧ p x ∧ y = f₁ x ⇒ prog.SPEC m (res x) c (res y)) ∧
    (∀x y. ¬g x ∧ p x ∧ y = f₂ x ⇒ prog.SPEC m (res x) c (res' y)) ⇒
    ∀x.
      tailrec.TAILREC_PRE f₁ g p x ⇒
      prog.SPEC m (res x) c (res' (tailrec.TAILREC f₁ f₂ 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))

⊦ ∀f₁ f₂ g p res res' c m.
    (∀z x y. g x ∧ p x ∧ y = f₁ x ⇒ prog.SPEC m (res z x) c (res z y)) ∧
    (∀z x y. ¬g x ∧ p x ∧ y = f₂ x ⇒ prog.SPEC m (res z x) c (res' z y)) ⇒
    ∀z x.
      tailrec.TAILREC_PRE f₁ g p x ⇒
      prog.SPEC m (res z x) c (res' z (tailrec.TAILREC f₁ f₂ 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%%₃₆₃₄ w x.
    (words.word_add %%genvar%%₃₆₃₄ w = words.word_add x w ⇔
     %%genvar%%₃₆₃₄ = x) ∧
    (words.word_add w %%genvar%%₃₆₃₄ = words.word_add x w ⇔
     %%genvar%%₃₆₃₄ = x) ∧
    (words.word_add %%genvar%%₃₆₃₄ w = words.word_add w x ⇔
     %%genvar%%₃₆₃₄ = x) ∧
    (words.word_add w %%genvar%%₃₆₃₄ = words.word_add w x ⇔
     %%genvar%%₃₆₃₄ = x) ∧ (w = words.word_add x w ⇔ x = words.n2w 0) ∧
    (words.word_add %%genvar%%₃₆₃₄ w = w ⇔ %%genvar%%₃₆₃₄ = words.n2w 0) ∧
    (w = words.word_add w x ⇔ x = words.n2w 0) ∧
    (words.word_add w %%genvar%%₃₆₃₄ = w ⇔ %%genvar%%₃₆₃₄ = 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

→
bool
Data
- List
  - list
- Pair
  - ×
- Sum
  - Data.Sum.+
- Unit
  - Data.Unit.unit
HOL4
- bool
  - bool.itself
- fcp
  - fcp.bit0
  - fcp.bit1
  - fcp.cart
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - length
- Pair
  - ,
  - fst
  - snd
- Sum
  - Data.Sum.destLeft
  - Data.Sum.destRight
  - Data.Sum.isLeft
  - Data.Sum.isRight
Function
- flip
- id
- ∘
- Combinator
  - Combinator.s
HOL4
- arithmetic
  - arithmetic.-
  - arithmetic.BIT2
  - arithmetic.DIV2
  - arithmetic.FUNPOW
- bit
  - bit.BIT
  - bit.BITS
  - bit.DIV_2EXP
  - bit.MOD_2EXP
  - bit.TIMES_2EXP
- bool
  - bool.the_value
  - bool.IN
  - bool.LET
- combin
  - combin.FAIL
  - combin.UPDATE
- fcp
  - fcp.dimindex
  - fcp.fcp_index
  - fcp.FCP
- numeral
  - numeral.exactlog
  - numeral.iDUB
  - numeral.iSUB
  - numeral.iZ
  - numeral.iiSUC
  - numeral.internal_mult
  - numeral.onecount
  - numeral.texp_help
- numeral_bit
  - numeral_bit.iDIV2
  - numeral_bit.iMOD_2EXP
  - numeral_bit.iSUC
  - numeral_bit.FDUB
  - numeral_bit.SFUNPOW
- pair
  - pair.UNCURRY
- pred_set
  - pred_set.BIGUNION
  - pred_set.DELETE
  - pred_set.DIFF
  - pred_set.DISJOINT
  - pred_set.EMPTY
  - pred_set.GSPEC
  - pred_set.IMAGE
  - pred_set.INSERT
  - pred_set.INTER
  - pred_set.SUBSET
  - pred_set.UNION
- prim_rec
  - prim_rec.wellfounded
  - prim_rec.PRE
- while
  - while.WHILE
- words
  - words.dimword
  - words.n2w
  - words.nzcv
  - words.w2n
  - words.w2w
  - words.word_2comp
  - words.word_T
  - words.word_add
  - words.word_and
  - words.word_asr
  - words.word_bits
  - words.word_div
  - words.word_extract
  - words.word_ge
  - words.word_gt
  - words.word_le
  - words.word_lo
  - words.word_ls
  - words.word_lsl
  - words.word_lsr
  - words.word_lt
  - words.word_msb
  - words.word_mul
  - words.word_or
  - words.word_rol
  - words.word_ror
  - words.word_sub
  - words.word_xor
  - words.BIT_SET
Number
- Natural
  - *
  - +
  - <
  - ≤
  - >
  - ≥
  - ↑
  - bit1
  - div
  - even
  - min
  - mod
  - odd
  - suc
  - zero
Relation
- wellFounded

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_₁ p_₂. P (p_₁, p_₂)

⊦ ∀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

⊦ ∀s₁ s₂.
pred_set.BIGUNION (pred_set.UNION s₁ s₂) =
pred_set.UNION (pred_set.BIGUNION s₁) (pred_set.BIGUNION s₂)

⊦ ∀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

⊦ (∨) = λt₁ t₂. ∀t. (t₁ ⇒ t) ⇒ (t₂ ⇒ t) ⇒ t

⊦ ∀t₁ t₂. (t₁ ⇒ t₂) ⇒ (t₂ ⇒ t₁) ⇒ (t₁ ⇔ t₂)

⊦ ∀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)

⊦ ∀t₁ t₂ t₃. t₁ ∧ t₂ ∧ t₃ ⇔ (t₁ ∧ t₂) ∧ t₃

⊦ ∀t₁ t₂ t₃. t₁ ⇒ t₂ ⇒ t₃ ⇔ t₁ ∧ t₂ ⇒ t₃

⊦ ∀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

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁ ∧ (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (t₁ ⇔ t₂) ⇔ t₁ ∧ t₂ ∨ ¬t₁ ∧ ¬t₂

⊦ ∀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

⊦ ∀f₀ f₁. ∃fn. fn [] = f₀ ∧ ∀a₀ a₁. fn (a₀ :: a₁) = f₁ a₀ a₁ (fn a₁)

⊦ ∀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) ∧ ∀l₁ l₂ h. (h :: l₁) @ l₂ = h :: l₁ @ l₂

⊦ ∀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)

⊦ ∀h₁ l₁ h₂ l₂ n.
bit.BITS h₂ l₂ (bit.BITS h₁ l₁ n) =
bit.BITS (min h₁ (h₂ + l₁)) (l₂ + l₁) 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