Package m0-step: M0 step evaluator
Information
| name | m0-step |
| version | 1.0 |
| description | M0 step evaluator |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 59c7363aaa2835755ed6246dd56639a23e769ae3 |
| requires | base hol-base hol-words hol-string hol-integer hol-monad m0-model |
| show | Data.Bool Data.List Data.Option Data.Pair Data.Unit Function HOL4 Number.Natural |
Files
- Package tarball m0-step-1.0.tgz
- Theory source file m0-step.thy (included in the package tarball)
Defined Constants
- HOL4
- m0_step
- m0_step.reverse_endian
- m0_step.LDM1
- m0_step.LDM_UPTO
- m0_step.NextStateM0
- m0_step.R_name
- m0_step.STM1
- m0_step.STM_UPTO
- m0_step
Theorems
{¬(d = words.n2w 15)} ⊦ ¬(m0_step.R_name b d = m0.RName_PC)
⊦ ∀w. m0.BitCount w = words.bit_count w
⊦ ∀w. m0_step.reverse_endian (m0_step.reverse_endian w) = w
⊦ alignment.aligned 1 (words.word_concat w (words.n2w 0))
⊦ ∀x. fst (pair.SWAP x) = snd x
⊦ ∀w. words.bit_count w < 1 ⇔ w = words.n2w 0
⊦ ∀w1 w2.
bitstring.w2v w1 @ bitstring.w2v w2 =
bitstring.w2v (words.word_concat w1 w2)
⊦ ∀f s. state_transformer.FOR (n, n, f) s = f n s
⊦ ∀s0.
m0_step.NextStateM0 s0 =
bool.LET
(λs1.
if m0.m0_state_exception s1 = m0.NoException then some s1
else none) (m0.Next s0)
⊦ ∀b x. m0_step.R_name b x = m0.RName_PC ⇔ x = words.n2w 15
⊦ ∀x y carry_in.
m0.AddWithCarry (x, y, carry_in) =
words.add_with_carry (x, y, carry_in)
⊦ ∀w1 w2 w3.
bitstring.w2v w1 @ bitstring.w2v w2 @ bitstring.w2v w3 =
bitstring.w2v (words.word_concat w1 (words.word_concat w2 w3))
⊦ ∀r.
words.word_bit (arithmetic.BIT2 3) r ⇒
words.bit_count_upto (arithmetic.BIT2 3) r =
arithmetic.- (words.bit_count r) 1
⊦ ∀w.
m0.CountLeadingZeroBits w =
if w = words.n2w 0 then arithmetic.BIT2 3
else arithmetic.- 7 (words.w2n (words.word_log2 w))
⊦ ∀p b r s.
list.FOLDL (m0_step.LDM1 (m0_step.R_name p) b r s) (m0.m0_state_REG s)
(rich_list.COUNT_LIST (arithmetic.BIT2 3)) m0.RName_PC =
m0.m0_state_REG s m0.RName_PC
⊦ m0.DecodeRegShift (words.n2w 0) = m0.SRType_LSL ∧
m0.DecodeRegShift (words.n2w 1) = m0.SRType_LSR ∧
m0.DecodeRegShift (words.n2w (arithmetic.BIT2 0)) = m0.SRType_ASR ∧
m0.DecodeRegShift (words.n2w 3) = m0.SRType_ROR
⊦ ∀r.
words.word_sub (words.n2w (words.bit_count_upto 15 r))
(words.n2w (words.bit_count r)) =
if words.word_bit 15 r then words.word_2comp (words.n2w 1)
else words.n2w 0
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_add w (words.n2w (arithmetic.BIT2 1)))) (words.n2w 1) =
words.word_or (words.word_add w (words.n2w (arithmetic.BIT2 1)))
(words.n2w 1)
⊦ ∀l f b r s w mem.
list.FOLDL (m0_step.STM1 f b r (m0.m0_state_pcinc_fupd (const w) s))
mem l = list.FOLDL (m0_step.STM1 f b r s) mem l
⊦ ∀l f b r s w reg.
list.FOLDL (m0_step.LDM1 f b r (m0.m0_state_pcinc_fupd (const w) s))
reg l = list.FOLDL (m0_step.LDM1 f b r s) reg l
⊦ alignment.aligned (arithmetic.BIT2 0)
(words.word_add (alignment.align (arithmetic.BIT2 0) pc)
(words.w2w
(bitstring.v2w
(b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: ⊥ ::
[]))))
⊦ ∀x a b c d.
words.word_bit 0
(if x then
words.word_concat a (words.word_concat b (words.word_concat c d))
else
words.word_concat d
(words.word_concat c (words.word_concat b a))) ⇔
words.word_bit 0 (if x then d else a)
⊦ ∀w1 w2.
bitstring.field 7 0 (bitstring.w2v (words.word_concat w1 w2)) @
bitstring.field 15 (arithmetic.BIT2 3)
(bitstring.w2v (words.word_concat w1 w2)) =
bitstring.w2v (words.word_concat w2 w1)
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_sub (words.word_add w (words.n2w (arithmetic.BIT2 1)))
(words.n2w (arithmetic.BIT2 0)))) (words.n2w 1) =
words.word_or (words.word_add w (words.n2w (arithmetic.BIT2 0)))
(words.n2w 1)
⊦ ∀p a b c d.
alignment.aligned (arithmetic.BIT2 0)
(if p then
words.word_concat a (words.word_concat b (words.word_concat c d))
else
words.word_concat d
(words.word_concat c (words.word_concat b a))) ⇔
alignment.aligned (arithmetic.BIT2 0) (if p then d else a)
⊦ ∀i j f s.
i ≤ j ⇒
state_transformer.FOR (i, j, f) s =
((),
list.FOLDL (λx n. snd (f (n + i) x)) s
(rich_list.COUNT_LIST (arithmetic.- j i + 1)))
⊦ (∀w. m0.Aligned (w, 1) ⇔ alignment.aligned 0 w) ∧
(∀w. m0.Aligned (w, arithmetic.BIT2 0) ⇔ alignment.aligned 1 w) ∧
∀w.
m0.Aligned (w, arithmetic.BIT2 1) ⇔
alignment.aligned (arithmetic.BIT2 0) w
⊦ (∀w. m0.Align (w, 1) = alignment.align 0 w) ∧
(∀w. m0.Align (w, arithmetic.BIT2 0) = alignment.align 1 w) ∧
∀w.
m0.Align (w, arithmetic.BIT2 1) = alignment.align (arithmetic.BIT2 0) w
⊦ ∀imm2 w C s.
m0.Shift_C (w, m0.SRType_LSL, imm2, C) s =
((words.word_lsl w imm2,
(if imm2 = 0 then C
else
fcp.fcp_index (words.word_lsl (words.w2w w) imm2)
(arithmetic.BIT2 15))), s)
⊦ bitstring.v2w (⊥ :: ⊥ :: []) = words.n2w 0 ∧
bitstring.v2w (⊥ :: ⊤ :: []) = words.n2w 1 ∧
bitstring.v2w (⊤ :: ⊥ :: []) = words.n2w (arithmetic.BIT2 0) ∧
bitstring.v2w (⊤ :: ⊤ :: []) = words.n2w 3
⊦ ∀f i registers b s.
m0_step.STM_UPTO f i registers (b, s) =
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (i + 1) registers))),
m0.m0_state_MEM_fupd
(const
(list.FOLDL (m0_step.STM1 f b registers s) (m0.m0_state_MEM s)
(rich_list.COUNT_LIST (i + 1)))) s)
⊦ ∀f i registers b s.
m0_step.LDM_UPTO f i registers (b, s) =
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (i + 1) registers))),
m0.m0_state_REG_fupd
(const
(list.FOLDL (m0_step.LDM1 f b registers s) (m0.m0_state_REG s)
(rich_list.COUNT_LIST (i + 1)))) s)
⊦ ∀l r f g a b.
length l = length r ∧ a = b ∧
(∀i x. i < length l ⇒ f x (list.EL i l) = g x (list.EL i r)) ⇒
list.FOLDL f a l = list.FOLDL g b r
⊦ ∀w.
words.word_concat
(words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w)
(words.word_concat
(words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) w)
(words.word_concat (words.word_extract 15 (arithmetic.BIT2 3) w)
(words.word_extract 7 0 w))) = w
⊦ ∀w.
m0_step.reverse_endian w =
words.word_concat (words.word_extract 7 0 w)
(words.word_concat (words.word_extract 15 (arithmetic.BIT2 3) w)
(words.word_concat
(words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) w)
(words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w)))
{alignment.aligned (arithmetic.BIT2 0) sp}
⊦ words.word_and
(words.word_add sp (words.word_mul (words.n2w (arithmetic.BIT2 1)) a))
(words.n2w
(arithmetic.BIT2
(bit1
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
(arithmetic.BIT2
0)))))))))))))))))))))))))))))))) =
words.word_add sp (words.word_mul (words.n2w (arithmetic.BIT2 1)) a)
{m0.m0_state_exception s = m0.NoException}
⊦ m0.Fetch s = (m0.Thumb v, s) ∧
m0.DecodeThumb v
(m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 0))) s) =
(ast, m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 0))) s) ∧
(∀s. m0.Run ast s = f x s) ∧
f x (m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 0))) s) =
s1 ∧ m0.m0_state_exception s1 = m0.m0_state_exception s ⇒
m0_step.NextStateM0 s = some s1
{m0.m0_state_exception s = m0.NoException}
⊦ m0.Fetch s = (m0.Thumb2 v, s) ∧
m0.DecodeThumb2 v
(m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 1))) s) =
(ast, m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 1))) s) ∧
(∀s. m0.Run ast s = f x s) ∧
f x (m0.m0_state_pcinc_fupd (const (words.n2w (arithmetic.BIT2 1))) s) =
s1 ∧ m0.m0_state_exception s1 = m0.m0_state_exception s ⇒
m0_step.NextStateM0 s = some s1
⊦ alignment.aligned 1 pc ⇒
alignment.aligned 1
(words.word_add (words.word_add pc (words.n2w (arithmetic.BIT2 1)))
(bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: b23 ::
b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: b15 :: b14 ::
b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 ::
b3 :: b2 :: b1 :: ⊥ :: []))) ⇔ ⊤
⊦ ∀w1 w2 w3 w4.
bitstring.field 7 0
(bitstring.w2v
(words.word_concat w1
(words.word_concat w2 (words.word_concat w3 w4)))) @
bitstring.field 15 (arithmetic.BIT2 3)
(bitstring.w2v
(words.word_concat w1
(words.word_concat w2 (words.word_concat w3 w4)))) @
bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(bitstring.w2v
(words.word_concat w1
(words.word_concat w2 (words.word_concat w3 w4)))) @
bitstring.field 31 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v
(words.word_concat w1
(words.word_concat w2 (words.word_concat w3 w4)))) =
bitstring.w2v
(words.word_concat w4
(words.word_concat w3 (words.word_concat w2 w1)))
⊦ (if words.word_bit 0 registers then
(words.word_add b (words.n2w (arithmetic.BIT2 1)),
m0.m0_state_REG_fupd
(const
(combin.UPDATE (f (words.n2w 0))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_concat (m0.m0_state_MEM s b)
(words.word_concat
(m0.m0_state_MEM s (words.word_add b (words.n2w 1)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add b
(words.n2w (arithmetic.BIT2 0))))
(m0.m0_state_MEM s
(words.word_add b (words.n2w 3)))))
else
words.word_concat
(m0.m0_state_MEM s (words.word_add b (words.n2w 3)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add b
(words.n2w (arithmetic.BIT2 0))))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add b (words.n2w 1)))
(m0.m0_state_MEM s b)))) (m0.m0_state_REG s))) s)
else (b, s)) = m0_step.LDM_UPTO f 0 registers (b, s)
⊦ (∀s r i f b.
fst (m0_step.STM_UPTO f i r (b, s)) =
words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (i + 1) r)))) ∧
(∀s r i f b.
m0.m0_state_REG (snd (m0_step.STM_UPTO f i r (b, s))) =
m0.m0_state_REG s) ∧
(∀s r i f b.
m0.m0_state_CONTROL (snd (m0_step.STM_UPTO f i r (b, s))) =
m0.m0_state_CONTROL s) ∧
∀s r i f b.
m0.m0_state_AIRCR (snd (m0_step.STM_UPTO f i r (b, s))) =
m0.m0_state_AIRCR s
⊦ (∀s r i f b.
fst (m0_step.LDM_UPTO f i r (b, s)) =
words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (i + 1) r)))) ∧
(∀s r i f b.
m0.m0_state_MEM (snd (m0_step.LDM_UPTO f i r (b, s))) =
m0.m0_state_MEM s) ∧
(∀s r i f b.
m0.m0_state_CONTROL (snd (m0_step.LDM_UPTO f i r (b, s))) =
m0.m0_state_CONTROL s) ∧
∀s r i f b.
m0.m0_state_AIRCR (snd (m0_step.LDM_UPTO f i r (b, s))) =
m0.m0_state_AIRCR s
⊦ ∀a.
words.word_bit (words.w2n a)
(bitstring.v2w
(⊥ :: b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ⇔
b7 ∧ a = words.n2w 7 ∨
b6 ∧ a = words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)) ∨
b5 ∧ a = words.n2w (bit1 (arithmetic.BIT2 0)) ∨
b4 ∧ a = words.n2w (arithmetic.BIT2 1) ∨ b3 ∧ a = words.n2w 3 ∨
b2 ∧ a = words.n2w (arithmetic.BIT2 0) ∨ b1 ∧ a = words.n2w 1 ∨
b0 ∧ a = words.n2w 0
⊦ ∀w.
words.word_extract 7 0 (m0_step.reverse_endian w) =
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w ∧
words.word_extract 15 (arithmetic.BIT2 3) (m0_step.reverse_endian w) =
words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) w ∧
words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (m0_step.reverse_endian w) =
words.word_extract 15 (arithmetic.BIT2 3) w ∧
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(m0_step.reverse_endian w) = words.word_extract 7 0 w
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_add w
(words.sw2sw
(bitstring.v2w
(x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: ⊥ ::
[]))))) (words.n2w 0) =
words.word_add w
(bitstring.v2w
(x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 ::
x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 ::
x0 :: x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: ⊥ :: []))
⊦ ∀f b registers s r j.
m0_step.LDM1 f b registers s r j =
(if words.word_bit j registers then
combin.UPDATE (f (words.n2w j))
(bool.LET
(λa.
if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_concat (m0.m0_state_MEM s a)
(words.word_concat
(m0.m0_state_MEM s (words.word_add a (words.n2w 1)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add a
(words.n2w (arithmetic.BIT2 0))))
(m0.m0_state_MEM s
(words.word_add a (words.n2w 3)))))
else
words.word_concat
(m0.m0_state_MEM s (words.word_add a (words.n2w 3)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add a
(words.n2w (arithmetic.BIT2 0))))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add a (words.n2w 1)))
(m0.m0_state_MEM s a))))
(words.word_add b
(if j = 0 then words.n2w 0
else
words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto j registers)))))
else id) r
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_add w
(words.sw2sw
(bitstring.v2w
(x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 ::
x9 :: x10 :: ⊥ :: []))))) (words.n2w 0) =
words.word_add w
(bitstring.v2w
(x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 ::
x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x1 ::
x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: ⊥ :: []))
⊦ ∀b a amount w C s.
m0.Shift_C
(w, m0.DecodeRegShift (bitstring.v2w (a :: b :: [])), amount, C) s =
((if ¬a ∧ ¬b then
(words.word_lsl w amount,
(if amount = 0 then C
else
fcp.fcp_index (words.word_lsl (words.w2w w) amount)
(arithmetic.BIT2 15)))
else if ¬a ∧ b then
(words.word_lsr w amount,
(if amount = 0 then C
else
amount ≤ arithmetic.BIT2 15 ∧
words.word_bit (arithmetic.- amount 1) w))
else if a ∧ ¬b then
(words.word_asr w amount,
(if amount = 0 then C
else
words.word_bit
(arithmetic.- (min (arithmetic.BIT2 15) amount) 1) w))
else
(words.word_ror w amount,
(if amount = 0 then C
else words.word_msb (words.word_ror w amount)))), s)
⊦ (∀w.
bitstring.v2w
(bitstring.field 15 (arithmetic.BIT2 3)
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w))) =
words.word_extract 7 0 w) ∧
(∀w.
bitstring.v2w
(bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w)) =
words.word_extract 15 (arithmetic.BIT2 3) w) ∧
(∀w.
bitstring.v2w
(bitstring.field 7 0
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w))) =
words.word_extract 15 (arithmetic.BIT2 3) w) ∧
∀w.
bitstring.v2w (bitstring.field 7 0 (bitstring.w2v w)) =
words.word_extract 7 0 w
⊦ ∀b n.
m0_step.R_name b n =
bool.literal_case
(λv.
if v = words.n2w 0 then m0.RName_0
else if v = words.n2w 1 then m0.RName_1
else if v = words.n2w (arithmetic.BIT2 0) then m0.RName_2
else if v = words.n2w 3 then m0.RName_3
else if v = words.n2w (arithmetic.BIT2 1) then m0.RName_4
else if v = words.n2w (bit1 (arithmetic.BIT2 0)) then m0.RName_5
else if v = words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)) then
m0.RName_6
else if v = words.n2w 7 then m0.RName_7
else if v = words.n2w (arithmetic.BIT2 3) then m0.RName_8
else if v = words.n2w (bit1 (arithmetic.BIT2 1)) then m0.RName_9
else if v = words.n2w (arithmetic.BIT2 (arithmetic.BIT2 1)) then
m0.RName_10
else if v = words.n2w (bit1 (bit1 (arithmetic.BIT2 0))) then
m0.RName_11
else if v = words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
then m0.RName_12
else if v = words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))
then if b then m0.RName_SP_process else m0.RName_SP_main
else if v =
words.n2w
(arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))
then m0.RName_LR
else m0.RName_PC) n
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_add w
(words.sw2sw
(words.word_concat (bitstring.v2w (x0 :: []))
(words.word_concat (bitstring.v2w (x1 :: []))
(words.word_concat (bitstring.v2w (x2 :: []))
(words.word_concat
(bitstring.v2w
(x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: []))
(bitstring.v2w
(x9 :: x10 :: x11 :: x12 :: x13 :: x14 ::
x15 :: x16 :: x17 :: x18 :: x19 :: ⊥ ::
[]))))))))) (words.n2w 0) =
words.word_add w
(bitstring.v2w
(x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 ::
x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 ::
x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 :: ⊥ ::
[]))
⊦ (bitstring.v2w (⊥ :: b2 :: b1 :: b0 :: []) =
words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) ⇔ ⊥) ∧
(bitstring.v2w (b2 :: ⊥ :: b1 :: b0 :: []) =
words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) ⇔ ⊥) ∧
(bitstring.v2w (b2 :: b1 :: ⊤ :: b0 :: []) =
words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) ⇔ ⊥) ∧
(bitstring.v2w (b2 :: b1 :: b0 :: ⊥ :: []) =
words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) ⇔ ⊥) ∧
(bitstring.v2w (⊥ :: b2 :: b1 :: b0 :: []) = words.n2w 15 ⇔ ⊥) ∧
(bitstring.v2w (b2 :: ⊥ :: b1 :: b0 :: []) = words.n2w 15 ⇔ ⊥) ∧
(bitstring.v2w (b2 :: b1 :: ⊥ :: b0 :: []) = words.n2w 15 ⇔ ⊥) ∧
(bitstring.v2w (b2 :: b1 :: b0 :: ⊥ :: []) = words.n2w 15 ⇔ ⊥)
{alignment.aligned 1 w}
⊦ words.word_concat
(words.word_extract 31 1
(words.word_add w
(words.sw2sw
(words.word_concat (bitstring.v2w (x0 :: []))
(words.word_concat
(words.word_1comp
(words.word_xor (bitstring.v2w (x1a :: []))
(bitstring.v2w (x1b :: []))))
(words.word_concat
(words.word_1comp
(words.word_xor (bitstring.v2w (x2a :: []))
(bitstring.v2w (x2b :: []))))
(words.word_concat
(bitstring.v2w
(x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 ::
x10 :: x11 :: x12 :: []))
(bitstring.v2w
(x13 :: x14 :: x15 :: x16 :: x17 :: x18 ::
x19 :: x20 :: x21 :: x22 :: x23 :: ⊥ ::
[]))))))))) (words.n2w 0) =
words.word_add w
(bitstring.v2w
(x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: x0 :: (x1a ⇔ x1b) ::
(x2a ⇔ x2b) :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 ::
x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 ::
x20 :: x21 :: x22 :: x23 :: ⊥ :: []))
⊦ ∀b a imm5 w C s.
m0.Shift_C
(w, fst (m0.DecodeImmShift (bitstring.v2w (a :: b :: []), imm5)),
snd (m0.DecodeImmShift (bitstring.v2w (a :: b :: []), imm5)), C) s =
((if ¬a ∧ ¬b then
if imm5 = words.n2w 0 then (w, C)
else
(words.word_lsl w (words.w2n imm5),
fcp.fcp_index (words.word_lsl (words.w2w w) (words.w2n imm5))
(arithmetic.BIT2 15))
else if ¬a ∧ b then
if imm5 = words.n2w 0 then (words.n2w 0, words.word_msb w)
else
(words.word_lsr w (words.w2n imm5),
words.w2n imm5 ≤ arithmetic.BIT2 15 ∧
words.word_bit (arithmetic.- (words.w2n imm5) 1) w)
else if a ∧ ¬b then
if imm5 = words.n2w 0 then
(words.word_asr w (arithmetic.BIT2 15), words.word_msb w)
else
(words.word_asr w (words.w2n imm5),
words.word_bit
(arithmetic.- (min (arithmetic.BIT2 15) (words.w2n imm5)) 1)
w)
else if imm5 = words.n2w 0 then pair.SWAP (words.word_rrx (C, w))
else
(words.word_ror w (words.w2n imm5),
words.word_msb (words.word_ror w (words.w2n imm5)))), s)
⊦ ∀f b registers s m j.
m0_step.STM1 f b registers s m j =
(if words.word_bit j registers then
bool.LET
(bool.LET
(λa r.
combin.UPDATE (words.word_add a (words.n2w 3))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 7 0 r
else
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
r) ∘
(combin.UPDATE
(words.word_add a (words.n2w (arithmetic.BIT2 0)))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 15 (arithmetic.BIT2 3) r
else
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) r) ∘
(combin.UPDATE (words.word_add a (words.n2w 1))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) r
else words.word_extract 15 (arithmetic.BIT2 3) r) ∘
combin.UPDATE a
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
r
else words.word_extract 7 0 r))))
(words.word_add b
(if j = 0 then words.n2w 0
else
words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto j registers)))))
(m0.m0_state_REG s (f (words.n2w j)))
else id) m
⊦ (if words.word_bit 0 registers then
(words.word_add b (words.n2w (arithmetic.BIT2 1)),
m0.m0_state_MEM_fupd
(const
(combin.UPDATE (words.word_add b (words.n2w 3))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 7 0
(m0.m0_state_REG s (f (words.n2w 0)))
else
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(m0.m0_state_REG s (f (words.n2w 0))))
(combin.UPDATE
(words.word_add b (words.n2w (arithmetic.BIT2 0)))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 15 (arithmetic.BIT2 3)
(m0.m0_state_REG s (f (words.n2w 0)))
else
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(m0.m0_state_REG s (f (words.n2w 0))))
(combin.UPDATE (words.word_add b (words.n2w 1))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(m0.m0_state_REG s (f (words.n2w 0)))
else
words.word_extract 15 (arithmetic.BIT2 3)
(m0.m0_state_REG s (f (words.n2w 0))))
(combin.UPDATE b
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 31
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 0))))
(m0.m0_state_REG s (f (words.n2w 0)))
else
words.word_extract 7 0
(m0.m0_state_REG s (f (words.n2w 0))))
(m0.m0_state_MEM s)))))) s)
else (b, s)) = m0_step.STM_UPTO f 0 registers (b, s)
⊦ ∀n f registers b s.
n < arithmetic.BIT2 3 ⇒
(if words.word_bit (suc n) registers then
(words.word_add
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (n + 1) registers))))
(words.n2w (arithmetic.BIT2 1)),
m0.m0_state_REG_fupd
(const
(combin.UPDATE (f (words.n2w (suc n)))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_concat
(m0.m0_state_MEM s
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers)))))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers)))) (words.n2w 1)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers))))
(words.n2w (arithmetic.BIT2 0))))
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers))))
(words.n2w 3)))))
else
words.word_concat
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers)))) (words.n2w 3)))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers))))
(words.n2w (arithmetic.BIT2 0))))
(words.word_concat
(m0.m0_state_MEM s
(words.word_add
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers)))) (words.n2w 1)))
(m0.m0_state_MEM s
(words.word_add b
(words.word_mul
(words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers))))))))
(m0.m0_state_REG
(snd (m0_step.LDM_UPTO f n registers (b, s))))))
(snd (m0_step.LDM_UPTO f n registers (b, s))))
else m0_step.LDM_UPTO f n registers (b, s)) =
m0_step.LDM_UPTO f (suc n) registers (b, s)
⊦ bitstring.v2w (⊥ :: ⊥ :: ⊥ :: ⊥ :: []) = words.n2w 0 ∧
bitstring.v2w (⊥ :: ⊥ :: ⊥ :: ⊤ :: []) = words.n2w 1 ∧
bitstring.v2w (⊥ :: ⊥ :: ⊤ :: ⊥ :: []) = words.n2w (arithmetic.BIT2 0) ∧
bitstring.v2w (⊥ :: ⊥ :: ⊤ :: ⊤ :: []) = words.n2w 3 ∧
bitstring.v2w (⊥ :: ⊤ :: ⊥ :: ⊥ :: []) = words.n2w (arithmetic.BIT2 1) ∧
bitstring.v2w (⊥ :: ⊤ :: ⊥ :: ⊤ :: []) =
words.n2w (bit1 (arithmetic.BIT2 0)) ∧
bitstring.v2w (⊥ :: ⊤ :: ⊤ :: ⊥ :: []) =
words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)) ∧
bitstring.v2w (⊥ :: ⊤ :: ⊤ :: ⊤ :: []) = words.n2w 7 ∧
bitstring.v2w (⊤ :: ⊥ :: ⊥ :: ⊥ :: []) = words.n2w (arithmetic.BIT2 3) ∧
bitstring.v2w (⊤ :: ⊥ :: ⊥ :: ⊤ :: []) =
words.n2w (bit1 (arithmetic.BIT2 1)) ∧
bitstring.v2w (⊤ :: ⊥ :: ⊤ :: ⊥ :: []) =
words.n2w (arithmetic.BIT2 (arithmetic.BIT2 1)) ∧
bitstring.v2w (⊤ :: ⊥ :: ⊤ :: ⊤ :: []) =
words.n2w (bit1 (bit1 (arithmetic.BIT2 0))) ∧
bitstring.v2w (⊤ :: ⊤ :: ⊥ :: ⊥ :: []) =
words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))) ∧
bitstring.v2w (⊤ :: ⊤ :: ⊥ :: ⊤ :: []) =
words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) ∧
bitstring.v2w (⊤ :: ⊤ :: ⊤ :: ⊥ :: []) =
words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))) ∧
bitstring.v2w (⊤ :: ⊤ :: ⊤ :: ⊤ :: []) = words.n2w 15
⊦ ∀n f registers b s.
n < arithmetic.- (fcp.dimindex bool.the_value) 1 ⇒
(if words.word_bit (suc n) registers then
(words.word_add
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w (words.bit_count_upto (n + 1) registers))))
(words.n2w (arithmetic.BIT2 1)),
m0.m0_state_MEM_fupd
(const
(combin.UPDATE
(words.word_add
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n) registers))))
(words.n2w 3))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 7 0
(m0.m0_state_REG s (f (words.n2w (suc n))))
else
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(m0.m0_state_REG s (f (words.n2w (suc n)))))
(combin.UPDATE
(words.word_add
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n) registers))))
(words.n2w (arithmetic.BIT2 0)))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 15 (arithmetic.BIT2 3)
(m0.m0_state_REG s (f (words.n2w (suc n))))
else
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(m0.m0_state_REG s (f (words.n2w (suc n)))))
(combin.UPDATE
(words.word_add
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers)))) (words.n2w 1))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract
(bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(m0.m0_state_REG s (f (words.n2w (suc n))))
else
words.word_extract 15 (arithmetic.BIT2 3)
(m0.m0_state_REG s (f (words.n2w (suc n)))))
(combin.UPDATE
(words.word_add b
(words.word_mul (words.n2w (arithmetic.BIT2 1))
(words.n2w
(words.bit_count_upto (suc n)
registers))))
(if m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s) then
words.word_extract 31
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 0))))
(m0.m0_state_REG s (f (words.n2w (suc n))))
else
words.word_extract 7 0
(m0.m0_state_REG s (f (words.n2w (suc n)))))
(m0.m0_state_MEM
(snd
(m0_step.STM_UPTO f n registers
(b, s)))))))))
(snd (m0_step.STM_UPTO f n registers (b, s))))
else m0_step.STM_UPTO f n registers (b, s)) =
m0_step.STM_UPTO f (suc n) registers (b, s)
⊦ (∀w.
bitstring.v2w
(bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w) @
bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (bitstring.w2v w) @
bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v w))) = words.word_extract 7 0 w) ∧
(∀w.
bitstring.v2w
(bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v w)) =
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w) ∧
(∀w.
bitstring.v2w
(bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w) @
bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (bitstring.w2v w) @
bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v w))) =
words.word_extract 15 (arithmetic.BIT2 3) w) ∧
(∀w.
bitstring.v2w
(bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (bitstring.w2v w)) =
words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) w) ∧
(∀w.
bitstring.v2w
(bitstring.field 15 (arithmetic.BIT2 3)
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w) @
bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (bitstring.w2v w) @
bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v w))) =
words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) w) ∧
(∀w.
bitstring.v2w
(bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w)) =
words.word_extract 15 (arithmetic.BIT2 3) w) ∧
(∀w.
bitstring.v2w
(bitstring.field 7 0
(bitstring.field 7 0 (bitstring.w2v w) @
bitstring.field 15 (arithmetic.BIT2 3) (bitstring.w2v w) @
bitstring.field (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7) (bitstring.w2v w) @
bitstring.field 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.w2v w))) =
words.word_extract 31
(arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w) ∧
∀w.
bitstring.v2w (bitstring.field 7 0 (bitstring.w2v w)) =
words.word_extract 7 0 w
⊦ words.word_extract 31 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
(bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: b23 ::
b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: b15 :: b14 ::
b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 ::
b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: []) ∧
words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
(arithmetic.BIT2 7)
(bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: b23 ::
b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: b15 :: b14 ::
b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 ::
b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w
(b23 :: b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: []) ∧
words.word_extract 15 (arithmetic.BIT2 3)
(bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: b23 ::
b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: b15 :: b14 ::
b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 ::
b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w
(b15 :: b14 :: b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: []) ∧
words.word_extract 7 0
(bitstring.v2w
(b31 :: b30 :: b29 :: b28 :: b27 :: b26 :: b25 :: b24 :: b23 ::
b22 :: b21 :: b20 :: b19 :: b18 :: b17 :: b16 :: b15 :: b14 ::
b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 ::
b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: []) ∧
words.word_extract 15 (arithmetic.BIT2 3)
(bitstring.v2w
(b15 :: b14 :: b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 ::
b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w
(b15 :: b14 :: b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: []) ∧
words.word_extract 7 0
(bitstring.v2w
(b15 :: b14 :: b13 :: b12 :: b11 :: b10 :: b9 :: b8 :: b7 :: b6 ::
b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])
⊦ words.w2n (bitstring.v2w (b2 :: b1 :: b0 :: [])) =
words.w2n (bitstring.v2w (⊥ :: b2 :: b1 :: b0 :: [])) ∧
((words.word_lo (bitstring.v2w (b3 :: b2 :: b1 :: b0 :: []))
(words.n2w (arithmetic.BIT2 3)) ⇔ ¬b3) ∧
words.w2w (bitstring.v2w (b2 :: b1 :: b0 :: [])) =
bitstring.v2w (⊥ :: b2 :: b1 :: b0 :: []) ∧
words.word_concat (bitstring.v2w (b3 :: []))
(bitstring.v2w (b2 :: b1 :: b0 :: [])) =
bitstring.v2w (b3 :: b2 :: b1 :: b0 :: []) ∧
words.w2w
(bitstring.v2w (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) =
bitstring.v2w
(⊥ :: b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: []) ∧
words.word_concat (bitstring.v2w (b4 :: b3 :: b2 :: b1 :: b0 :: []))
(words.n2w 0) =
bitstring.v2w (b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: []) ∧
words.word_concat (bitstring.v2w (b4 :: b3 :: b2 :: b1 :: b0 :: []))
(words.n2w 0) =
bitstring.v2w (b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: ⊥ :: []) ∧
words.word_concat
(bitstring.v2w (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: []))
(words.n2w 0) =
bitstring.v2w (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: ⊥ :: []) ∧
words.word_concat
(bitstring.v2w (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: []))
(words.n2w 0) =
bitstring.v2w
(b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: []) ∧
words.word_concat
(bitstring.v2w (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: []))
(words.n2w 0) =
bitstring.v2w
(b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: ⊥ :: ⊥ :: []) ∧
words.word_concat
(bitstring.v2w
(b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 ::
[])) (words.n2w 0) =
bitstring.v2w
(b10 :: b9 :: b8 :: b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 ::
⊥ :: [])) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w 0 ⇔ ¬c ∧ ¬b ∧ ¬a) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w 1 ⇔ c ∧ ¬b ∧ ¬a) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w (arithmetic.BIT2 0) ⇔
¬c ∧ b ∧ ¬a) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w 3 ⇔ c ∧ b ∧ ¬a) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w (arithmetic.BIT2 1) ⇔
¬c ∧ ¬b ∧ a) ∧
(bitstring.v2w (a :: b :: c :: []) =
words.n2w (bit1 (arithmetic.BIT2 0)) ⇔ c ∧ ¬b ∧ a) ∧
(bitstring.v2w (a :: b :: c :: []) =
words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)) ⇔ ¬c ∧ b ∧ a) ∧
(bitstring.v2w (a :: b :: c :: []) = words.n2w 7 ⇔ c ∧ b ∧ a)
External Type Operators
- →
- bool
- Data
- List
- list
- Option
- option
- Pair
- ×
- Sum
- Data.Sum.+
- Unit
- unit
- List
- HOL4
- bool
- bool.itself
- fcp
- fcp.bit0
- fcp.bit1
- fcp.cart
- integer
- integer.int
- m0
- m0.exception
- m0.instruction
- m0.m0_state
- m0.AIRCR
- m0.ARM_Exception
- m0.CCR
- m0.CONTROL
- m0.IPR
- m0.MachineCode
- m0.Mode
- m0.PRIMASK
- m0.PSR
- m0.RName
- m0.SHPR2
- m0.SHPR3
- m0.SRType
- string
- string.char
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- head
- length
- map
- tail
- Option
- none
- some
- Pair
- ,
- fst
- snd
- Unit
- ()
- Bool
- Function
- const
- id
- ∘
- HOL4
- alignment
- alignment.align
- alignment.aligned
- arithmetic
- arithmetic.-
- arithmetic.BIT2
- arithmetic.DIV2
- bit
- bit.BIT
- bit.LOG2
- bit.MOD_2EXP_EQ
- bit.MOD_2EXP_MAX
- bitstring
- bitstring.bitify
- bitstring.field
- bitstring.fixwidth
- bitstring.replicate
- bitstring.shiftl
- bitstring.shiftr
- bitstring.testbit
- bitstring.v2n
- bitstring.v2w
- bitstring.w2v
- bitstring.zero_extend
- blast
- blast.bcarry
- blast.bsum
- blast.BCARRY
- blast.BSUM
- bool
- bool.literal_case
- bool.the_value
- bool.ARB
- bool.IN
- bool.LET
- combin
- combin.FAIL
- combin.UPDATE
- fcp
- fcp.dimindex
- fcp.fcp_index
- fcp.FCP
- integer
- integer.int_add
- integer.int_le
- integer.int_lt
- integer.int_mul
- integer.int_neg
- integer.int_of_num
- integer.int_sub
- integer.Num
- integer_word
- integer_word.w2i
- integer_word.INT_MIN
- list
- list.DROP
- list.EL
- list.FOLDL
- list.GENLIST
- list.LIST_TO_SET
- list.PAD_LEFT
- list.SNOC
- list.TAKE
- m0
- m0.m0_state_AIRCR
- m0.m0_state_AIRCR_fupd
- m0.m0_state_CCR
- m0.m0_state_CCR_fupd
- m0.m0_state_CONTROL
- m0.m0_state_CONTROL_fupd
- m0.m0_state_CurrentMode
- m0.m0_state_CurrentMode_fupd
- m0.m0_state_ExceptionActive
- m0.m0_state_ExceptionActive_fupd
- m0.m0_state_MEM
- m0.m0_state_MEM_fupd
- m0.m0_state_NVIC_IPR
- m0.m0_state_NVIC_IPR_fupd
- m0.m0_state_PRIMASK
- m0.m0_state_PRIMASK_fupd
- m0.m0_state_PSR
- m0.m0_state_PSR_fupd
- m0.m0_state_REG
- m0.m0_state_REG_fupd
- m0.m0_state_SHPR2
- m0.m0_state_SHPR2_fupd
- m0.m0_state_SHPR3
- m0.m0_state_SHPR3_fupd
- m0.m0_state_VTOR
- m0.m0_state_VTOR_fupd
- m0.m0_state_count
- m0.m0_state_count_fupd
- m0.m0_state_exception
- m0.m0_state_exception_fupd
- m0.m0_state_pcinc
- m0.m0_state_pcinc_fupd
- m0.m0_state_pending
- m0.m0_state_pending_fupd
- m0.raise'exception
- m0.AIRCR_ENDIANNESS
- m0.ASR_C
- m0.ASSERT
- m0.AddWithCarry
- m0.Align
- m0.Aligned
- m0.BitCount
- m0.CountLeadingZeroBits
- m0.Decode
- m0.DecodeImmShift
- m0.DecodeRegShift
- m0.DecodeThumb
- m0.DecodeThumb2
- m0.Fetch
- m0.HighestSetBit
- m0.LSL_C
- m0.LSR_C
- m0.MachineCode_CASE
- m0.Next
- m0.NoException
- m0.RName2num
- m0.RName_0
- m0.RName_1
- m0.RName_10
- m0.RName_11
- m0.RName_12
- m0.RName_2
- m0.RName_3
- m0.RName_4
- m0.RName_5
- m0.RName_6
- m0.RName_7
- m0.RName_8
- m0.RName_9
- m0.RName_LR
- m0.RName_PC
- m0.RName_SP_main
- m0.RName_SP_process
- m0.ROR_C
- m0.RRX_C
- m0.Run
- m0.SRType_ASR
- m0.SRType_CASE
- m0.SRType_LSL
- m0.SRType_LSR
- m0.SRType_ROR
- m0.SRType_RRX
- m0.Shift_C
- m0.Thumb
- m0.Thumb2
- marker
- marker.Abbrev
- numeral
- numeral.exactlog
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- numeral.internal_mult
- numeral.onecount
- numeral.texp_help
- numposrep
- numposrep.l2n
- numposrep.num_from_bin_list
- pair
- pair.SWAP
- pair.UNCURRY
- pred_set
- pred_set.EMPTY
- pred_set.FINITE
- pred_set.INSERT
- pred_set.UNIV
- prim_rec
- prim_rec.PRE
- rich_list
- rich_list.COUNT_LIST
- rich_list.COUNT_LIST_AUX
- state_transformer
- state_transformer.BIND
- state_transformer.FOR
- string
- string.CHR
- sum_num
- sum_num.SUM
- words
- words.add_with_carry
- words.bit_count
- words.bit_count_upto
- words.dimword
- words.n2w
- words.sw2sw
- words.w2n
- words.w2w
- words.word_1comp
- words.word_2comp
- words.word_H
- words.word_L
- words.word_T
- words.word_add
- words.word_and
- words.word_asr
- words.word_bit
- words.word_bits
- words.word_concat
- words.word_div
- words.word_extract
- words.word_ge
- words.word_gt
- words.word_hi
- words.word_hs
- words.word_join
- words.word_le
- words.word_len
- words.word_lo
- words.word_log2
- words.word_ls
- words.word_lsb
- words.word_lsl
- words.word_lsr
- words.word_lt
- words.word_mod
- words.word_msb
- words.word_mul
- words.word_or
- words.word_rol
- words.word_ror
- words.word_rrx
- words.word_sdiv
- words.word_slice
- words.word_sub
- words.word_xor
- words.BIT_SET
- words.INT_MAX
- words.INT_MIN
- words.UINT_MAX
- alignment
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- min
- mod
- odd
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ pred_set.FINITE pred_set.UNIV
⊦ words.word_msb words.word_L
⊦ 0 = 0
⊦ 0 < fcp.dimindex bool.the_value
⊦ 0 < words.dimword bool.the_value
⊦ 0 < words.INT_MIN bool.the_value
⊦ ∀x. x = x
⊦ ∀t. ⊥ ⇒ t
⊦ ∀v. v = ()
⊦ ∀n. 0 ≤ n
⊦ ∀m. m ≤ m
⊦ words.word_H = words.n2w (words.INT_MAX bool.the_value)
⊦ words.word_L = words.n2w (words.INT_MIN bool.the_value)
⊦ numposrep.num_from_bin_list = numposrep.l2n (arithmetic.BIT2 0)
⊦ bool.LET = λf x. f x
⊦ pred_set.FINITE pred_set.UNIV ⇔ pred_set.FINITE pred_set.UNIV
⊦ pred_set.FINITE pred_set.UNIV ⇔ pred_set.FINITE pred_set.UNIV
⊦ integer_word.w2i words.word_L = integer_word.INT_MIN bool.the_value
⊦ fcp.dimindex bool.the_value = 1
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 0
⊦ 1 = suc 0
⊦ words.INT_MIN bool.the_value < words.dimword bool.the_value
⊦ 1 < words.dimword bool.the_value
⊦ words.w2n (words.n2w 0) = 0
⊦ ¬¬p ⇒ p
⊦ ∀x. ¬bool.IN x pred_set.EMPTY
⊦ ∀x. id x = x
⊦ ∀t. t ∨ ¬t
⊦ ∀x. marker.Abbrev x ⇔ x
⊦ ∀b. ¬bit.BIT b 0
⊦ ∀n. ¬(n < n)
⊦ ∀n. 0 < suc n
⊦ (¬) = λt. t ⇒ ⊥
⊦ (∃) = λP. P ((select) P)
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (∃x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λP. P = λx. ⊤
⊦ fcp.dimindex bool.the_value = 3
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 (arithmetic.BIT2 0)
⊦ words.dimword bool.the_value = arithmetic.BIT2 1
⊦ integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0
⊦ words.word_2comp (words.n2w 1) = words.word_T
⊦ ¬(p ⇒ q) ⇒ p
⊦ ∀x. x = x ⇔ ⊤
⊦ ∀x. integer.int_neg (integer.int_neg x) = x
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. integer.Num (integer.int_of_num n) = n
⊦ ∀c. arithmetic.- c c = 0
⊦ ∀n. n * 0 = 0
⊦ ∀n. min n n = n
⊦ ∀w. words.word_len w = fcp.dimindex bool.the_value
⊦ ∀w. words.w2n w < words.dimword bool.the_value
⊦ ∀w. bitstring.v2w (bitstring.w2v w) = w
⊦ ∀w. words.n2w (words.w2n w) = w
⊦ words.word_H = words.word_sub words.word_L (words.n2w 1)
⊦ integer_word.INT_MIN bool.the_value =
integer.int_neg (integer.int_of_num (words.INT_MIN bool.the_value))
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 (arithmetic.BIT2 1)
⊦ fcp.dimindex bool.the_value = bit1 (arithmetic.BIT2 1)
⊦ words.dimword bool.the_value = arithmetic.BIT2 3
⊦ words.w2n (words.n2w 1) = 1
⊦ ¬(p ⇒ q) ⇒ ¬q
⊦ ¬(p ∨ q) ⇒ ¬p
⊦ ¬(p ∨ q) ⇒ ¬q
⊦ ∀A. A ⇒ ¬A ⇒ ⊥
⊦ ∀x. integer.int_add x (integer.int_of_num 0) = x
⊦ ∀x. numeral.iDUB x = x + x
⊦ ∀n. rich_list.COUNT_LIST n = list.GENLIST id n
⊦ ∀n. rich_list.COUNT_LIST n = rich_list.COUNT_LIST_AUX n []
⊦ ∀m. m * 1 = m
⊦ ∀q. q div 1 = q
⊦ ∀l. list.TAKE (length l) l = l
⊦ ∀w. words.word_lsb w ⇔ fcp.fcp_index w 0
⊦ ∀w. words.w2w w = words.n2w (words.w2n w)
⊦ ∀w. length (bitstring.w2v w) = fcp.dimindex bool.the_value
⊦ ∀x y. const x y = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ fcp.dimindex bool.the_value =
arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 (bit1 (arithmetic.BIT2 1))
⊦ words.dimword bool.the_value =
arithmetic.BIT2 0 * words.INT_MIN bool.the_value
⊦ words.dimword bool.the_value =
arithmetic.BIT2 0 ↑ fcp.dimindex bool.the_value
⊦ words.dimword bool.the_value = arithmetic.BIT2 7
⊦ words.INT_MAX bool.the_value =
arithmetic.- (words.INT_MIN bool.the_value) 1
⊦ arithmetic.- (words.dimword bool.the_value)
(words.INT_MIN bool.the_value) = words.INT_MIN bool.the_value
⊦ ∀t. t ⇒ ⊥ ⇔ t ⇔ ⊥
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀x. integer.int_mul (integer.int_of_num 0) x = integer.int_of_num 0
⊦ ∀x. integer.int_mul (integer.int_of_num 1) x = x
⊦ ∀n. arithmetic.DIV2 n = n div arithmetic.BIT2 0
⊦ ∀m. prim_rec.PRE m = arithmetic.- m 1
⊦ ∀m. suc m = m + 1
⊦ ∀n. suc n = 1 + n
⊦ ∀n. n ≤ 0 ⇔ n = 0
⊦ ∀m. arithmetic.- (suc m) 1 = m
⊦ ∀l. bitstring.v2n l = numposrep.num_from_bin_list (bitstring.bitify [] l)
⊦ ∀w.
words.bit_count w =
words.bit_count_upto (fcp.dimindex bool.the_value) w
⊦ ∀w. words.word_log2 w = words.n2w (bit.LOG2 (words.w2n w))
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀h t. head (h :: t) = h
⊦ ∀n v. length (bitstring.fixwidth n v) = n
⊦ ∀n. words.n2w n = fcp.FCP (λi. bit.BIT i n)
⊦ ∀v. bitstring.v2w v = fcp.FCP (λi. bitstring.testbit i v)
⊦ ∀f x. bool.literal_case f x = f x
⊦ ∀f x. bool.LET f x = f x
⊦ ∀P x. P x ⇒ P ((select) P)
⊦ ∀f n. length (list.GENLIST f n) = n
⊦ fcp.dimindex bool.the_value = arithmetic.BIT2 15
⊦ ∀n. words.w2n (words.n2w n) = n mod words.dimword bool.the_value
⊦ ∀n. arithmetic.BIT2 0 * n = n + n
⊦ ∀n. words.n2w (n mod words.dimword bool.the_value) = words.n2w n
⊦ ∀l. length l = 0 ⇔ l = []
⊦ ∀v.
bitstring.w2v (bitstring.v2w v) =
bitstring.fixwidth (fcp.dimindex bool.the_value) v
⊦ ∀x. ∃q r. x = (q, r)
⊦ ∀a. pair.SWAP a = (snd a, fst a)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1
⊦ ∀A B. A ∨ B ⇔ B ∨ A
⊦ ∀y x. integer.int_add x y = integer.int_add y x
⊦ ∀m n. m * n = n * m
⊦ ∀m n. m + n = n + m
⊦ ∀a c. arithmetic.- (a + c) c = a
⊦ ∀l f. length (map f l) = length l
⊦ ∀v w. words.word_add v w = words.word_add w v
⊦ ∀a b. words.word_and a b = words.word_and b a
⊦ ∀w. words.word_1comp w = fcp.FCP (λi. ¬fcp.fcp_index w i)
⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥
⊦ ∀n. bit1 n = n + (n + suc 0)
⊦ ∀n. 0 < n ⇒ 0 mod n = 0
⊦ ∀w.
words.word_1comp w = words.word_sub (words.word_2comp w) (words.n2w 1)
⊦ ∀w.
words.word_2comp w =
words.n2w (arithmetic.- (words.dimword bool.the_value) (words.w2n w))
⊦ ∀w.
words.word_2comp w = words.word_add (words.word_1comp w) (words.n2w 1)
⊦ ∀w.
words.word_2comp w = words.word_mul (words.word_2comp (words.n2w 1)) w
⊦ ∀w. words.bit_count w = 0 ⇔ w = words.n2w 0
⊦ ∀w. words.w2n w = 0 ⇔ w = words.n2w 0
⊦ ∀A B. A ⇒ B ⇔ ¬A ∨ B
⊦ ∀x y. integer.int_sub x y = integer.int_add x (integer.int_neg y)
⊦ ∀x y. ¬integer.int_le x y ⇔ integer.int_lt y x
⊦ ∀x y. integer.int_sub x (integer.int_neg y) = integer.int_add x y
⊦ ∀m n. m < n ⇔ suc m ≤ n
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. ¬(m ≤ n) ⇔ n < m
⊦ ∀n v. bitstring.zero_extend n v = list.PAD_LEFT ⊥ n v
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀v w. words.word_sub v w = words.word_add v (words.word_2comp w)
⊦ ∀v w. words.word_add (words.word_2comp w) v = words.word_sub v w
⊦ ∀v w. words.word_concat v w = words.w2w (words.word_join v w)
⊦ ∀g f. state_transformer.BIND g f = pair.UNCURRY f ∘ g
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ words.INT_MIN bool.the_value = arithmetic.BIT2 63
⊦ words.word_msb (words.n2w n) ⇔
words.INT_MIN bool.the_value ≤ n mod words.dimword bool.the_value
⊦ ∀i.
integer.int_of_num (integer.Num i) = i ⇔
integer.int_le (integer.int_of_num 0) i
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ ∀w.
words.word_msb w ⇔
fcp.fcp_index w (arithmetic.- (fcp.dimindex bool.the_value) 1)
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀x y. some x = some y ⇔ x = y
⊦ ∀x y.
integer.int_neg (integer.int_mul x y) =
integer.int_mul x (integer.int_neg y)
⊦ ∀x y.
integer.int_neg (integer.int_mul x y) =
integer.int_mul (integer.int_neg x) y
⊦ ∀a a'. a = a' ⇔ m0.RName2num a = m0.RName2num a'
⊦ ∀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
⊦ ∀n k. k < n ⇒ k mod n = k
⊦ ∀m n. ¬(m ≤ n) ⇔ suc n ≤ m
⊦ ∀m n. suc (m + n) = suc n + m
⊦ ∀m n. bool.IN m (list.LIST_TO_SET (rich_list.COUNT_LIST n)) ⇔ m < n
⊦ ∀m n. integer.int_of_num m = integer.int_of_num n ⇔ m = n
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n.
integer.int_le (integer.int_of_num m) (integer.int_of_num n) ⇔ m ≤ n
⊦ ∀m n.
integer.int_lt (integer.int_of_num m) (integer.int_of_num n) ⇔ m < n
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ ∀m n. arithmetic.- m n = 0 ⇔ m ≤ n
⊦ ∀n v.
words.word_lsl (bitstring.v2w v) n =
bitstring.v2w (bitstring.shiftl v n)
⊦ ∀p w. alignment.aligned p w ⇔ alignment.align p w = w
⊦ ∀v n. length (bitstring.shiftr v n) = arithmetic.- (length v) n
⊦ ∀w. ∃n. w = words.n2w n ∧ n < words.dimword bool.the_value
⊦ ∀f v. pair.UNCURRY f v = f (fst v) (snd v)
⊦ words.dimword bool.the_value = arithmetic.BIT2 127
⊦ ∀n.
words.word_msb (words.n2w n) ⇔
bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) n
⊦ ∀n.
n < words.INT_MIN bool.the_value ⇒
integer_word.w2i (words.n2w n) = integer.int_of_num n
⊦ ∀m. arithmetic.- 0 m = 0 ∧ arithmetic.- m 0 = m
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀f. id ∘ f = f ∧ f ∘ id = f
⊦ ∀x y.
integer.int_neg (integer.int_add x y) =
integer.int_add (integer.int_neg x) (integer.int_neg y)
⊦ ∀m n.
integer.int_add (integer.int_of_num m) (integer.int_of_num n) =
integer.int_of_num (m + n)
⊦ ∀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)
⊦ ∀n w. n = length w ⇒ bitstring.fixwidth n w = w
⊦ ∀l1 l2. length (l1 @ l2) = length l1 + length l2
⊦ ∀v m. bitstring.shiftr v m = list.TAKE (arithmetic.- (length v) m) v
⊦ fcp.dimindex bool.the_value =
if pred_set.FINITE pred_set.UNIV then
arithmetic.BIT2 0 * fcp.dimindex bool.the_value
else 1
⊦ ∀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
⊦ ∀l. l = [] ∨ ∃h t. l = h :: t
⊦ ∀f v. (∀x. x = v ⇒ f x) ⇔ f v
⊦ ∀w.
¬(w = words.n2w 0) ⇒
bit.LOG2 (words.w2n w) < fcp.dimindex bool.the_value
⊦ ∀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)
⊦ ∀x y.
integer.int_le x y ⇔
integer.int_le (integer.int_of_num 0)
(integer.int_add y (integer.int_neg x))
⊦ ∀x y.
integer.int_lt x y ⇔
integer.int_le (integer.int_add x (integer.int_of_num 1)) y
⊦ ∀x y. integer.int_le x y ∧ integer.int_le y x ⇔ x = y
⊦ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m
⊦ ∀v n. bitstring.shiftl v n = v @ bitstring.replicate (⊥ :: []) n
⊦ ∀a n.
words.word_lsl a n =
words.word_mul (words.n2w (arithmetic.BIT2 0 ↑ n)) a
⊦ ∀w n. fcp.dimindex bool.the_value ≤ n ⇒ words.word_lsr w n = words.n2w 0
⊦ ∀w.
∃v.
w = bitstring.v2w v ∧
marker.Abbrev (length v = fcp.dimindex bool.the_value)
⊦ ∀w n. m0.Aligned (w, n) ⇔ w = m0.Align (w, n)
⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
⊦ (∀n. P (integer.int_of_num n)) ⇔
∀x. integer.int_le (integer.int_of_num 0) x ⇒ P x
⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥
⊦ ∀h l v. length (bitstring.field h l v) = arithmetic.- (suc h) l
⊦ rich_list.COUNT_LIST 0 = [] ∧
∀n. rich_list.COUNT_LIST (suc n) = list.SNOC n (rich_list.COUNT_LIST n)
⊦ ∀a b. combin.UPDATE a b = λf c. if a = c then b else f c
⊦ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x
⊦ ∀n v. suc n = length v ⇒ bitstring.field n 0 v = v
⊦ ∀p w.
alignment.align p w =
words.word_slice (arithmetic.- (fcp.dimindex bool.the_value) 1) p w
⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q
⊦ ∀w b.
b < fcp.dimindex bool.the_value ⇒
(fcp.fcp_index w b ⇔ words.word_bit b w)
⊦ ∀w n. m0.Align (w, n) = words.n2w (n * (words.w2n w div n))
⊦ list.EL 0 = head ∧ list.EL (suc n) (l :: ls) = list.EL n ls
⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥
⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3
⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3
⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C
⊦ ∀z y x.
integer.int_add x (integer.int_add y z) =
integer.int_add (integer.int_add x y) z
⊦ ∀x y z. integer.int_add x z = integer.int_add y z ⇔ x = y
⊦ ∀m n p. m < arithmetic.- n p ⇔ m + p < n
⊦ ∀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. arithmetic.- (arithmetic.- m n) p = arithmetic.- 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
⊦ ∀n. n ≤ length l1 ⇒ list.TAKE n (l1 @ l2) = list.TAKE n l1
⊦ ∀n. 1 ↑ n = 1 ∧ n ↑ 1 = n
⊦ ∀l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3
⊦ ∀f g n. map f (list.GENLIST g n) = list.GENLIST (f ∘ g) n
⊦ ∀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_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 x. words.word_sub v w = words.word_sub x w ⇔ v = x
⊦ ∀x y.
words.word_add x y =
fcp.FCP (λi. blast.BSUM i (fcp.fcp_index x) (fcp.fcp_index y) ⊥)
⊦ ∀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)
⊦ ∀w.
integer_word.w2i w =
if words.word_msb w then
integer.int_neg (integer.int_of_num (words.w2n (words.word_2comp w)))
else integer.int_of_num (words.w2n w)
⊦ ∀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
⊦ ∀n x. 0 < n ⇒ (n + x) mod n = x mod n
⊦ ∀n x. 0 < n ⇒ (x + n) mod n = x mod n
⊦ ∀m n. 0 < n ⇒ (m = prim_rec.PRE n ⇔ suc m = n)
⊦ ∀x y. 0 < y ⇒ (x mod y = x ⇔ x < y)
⊦ ∀n i.
i < fcp.dimindex bool.the_value ⇒
(fcp.fcp_index (words.n2w n) i ⇔ bit.BIT i n)
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀n v.
words.word_bit n (bitstring.v2w v) ⇔
n < fcp.dimindex bool.the_value ∧ bitstring.testbit n v
⊦ ∀n f.
sum_num.SUM n f = list.FOLDL (λx n. f n + x) 0 (rich_list.COUNT_LIST n)
⊦ ∀n. all P (list.GENLIST f n) ⇔ ∀i. i < n ⇒ P (f i)
⊦ fcp.dimindex bool.the_value =
if pred_set.FINITE pred_set.UNIV then
arithmetic.BIT2 0 * fcp.dimindex bool.the_value + 1
else 1
⊦ fcp.dimindex bool.the_value =
if pred_set.FINITE pred_set.UNIV ∧ pred_set.FINITE pred_set.UNIV then
fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
else 1
⊦ 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 y c. blast.bsum x y c ⇔ (x ⇔ ¬y) ⇔ ¬c
⊦ ∀n w.
words.bit_count_upto n w =
sum_num.SUM n (λi. if fcp.fcp_index w i then 1 else 0)
⊦ ∀f n x. x < n ⇒ list.EL x (list.GENLIST f n) = f x
⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n
⊦ ∀v w.
words.word_xor v w =
fcp.FCP (λi. ¬(fcp.fcp_index v i ⇔ fcp.fcp_index w i))
⊦ ∀w.
m0.HighestSetBit w =
if w = words.n2w 0 then integer.int_neg (integer.int_of_num 1)
else integer_word.w2i (words.word_log2 w)
⊦ ∀w.
m0.CountLeadingZeroBits w =
integer.Num
(integer.int_sub
(integer.int_sub
(integer.int_of_num (words.word_len (words.n2w 0)))
(integer.int_of_num 1)) (m0.HighestSetBit w))
⊦ rich_list.COUNT_LIST 0 = [] ∧
∀n. rich_list.COUNT_LIST (suc n) = 0 :: map suc (rich_list.COUNT_LIST n)
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)
⊦ ∀m n. ¬(m = n) ⇔ suc m ≤ n ∨ suc n ≤ m
⊦ ∀v n.
words.word_mul v (words.n2w (n + 1)) =
words.word_add (words.word_mul v (words.n2w n)) v
⊦ words.INT_MAX bool.the_value < words.INT_MIN bool.the_value ∧
words.INT_MIN bool.the_value ≤ words.UINT_MAX bool.the_value ∧
words.UINT_MAX bool.the_value < words.dimword bool.the_value
⊦ ∀x y s. bool.IN x (pred_set.INSERT y s) ⇔ x = y ∨ bool.IN x s
⊦ ∀A B C. A ∨ B ∧ C ⇔ (A ∨ B) ∧ (A ∨ C)
⊦ ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)
⊦ ∀x y z.
integer.int_mul (integer.int_add x y) z =
integer.int_add (integer.int_mul x z) (integer.int_mul y z)
⊦ ∀m n p. m ≤ n ⇔ suc p * m ≤ suc p * n
⊦ ∀m n p. p * (m + n) = p * m + p * n
⊦ ∀m n p. (m + n) * p = m * p + n * p
⊦ ∀h l v.
bitstring.field h l v =
bitstring.fixwidth (arithmetic.- (suc h) l) (bitstring.shiftr v l)
⊦ ∀v w x.
words.word_mul v (words.word_add w x) =
words.word_add (words.word_mul v w) (words.word_mul v x)
⊦ ∀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)
⊦ ∀x y.
words.word_sub x y =
fcp.FCP (λi. blast.BSUM i (fcp.fcp_index x) ((¬) ∘ fcp.fcp_index y) ⊤)
⊦ ∀a. fcp.dimindex bool.the_value = 1 ⇒ a = words.n2w 0 ∨ a = words.n2w 1
⊦ ∀m n.
words.n2w m = words.n2w n ⇔
m mod words.dimword bool.the_value = n mod words.dimword bool.the_value
⊦ ∀b w.
words.word_bit b w ⇔
b ≤ arithmetic.- (fcp.dimindex bool.the_value) 1 ∧ fcp.fcp_index w b
⊦ ∀v w.
bitstring.v2w v = bitstring.v2w w ⇔
bitstring.fixwidth (fcp.dimindex bool.the_value) v =
bitstring.fixwidth (fcp.dimindex bool.the_value) w
⊦ ∀w n.
fcp.dimindex bool.the_value ≤ n ⇒
words.word_asr w n =
if words.word_msb w then words.word_T else words.n2w 0
⊦ ∀x y.
words.word_lo x y ⇔
¬blast.BCARRY (fcp.dimindex bool.the_value) (fcp.fcp_index x)
((¬) ∘ fcp.fcp_index y) ⊤
⊦ integer_word.w2i (words.n2w 1) =
if fcp.dimindex bool.the_value = 1 then
integer.int_neg (integer.int_of_num 1)
else integer.int_of_num 1
⊦ ∀x y c. blast.bcarry x y c ⇔ x ∧ y ∨ (x ∨ y) ∧ c
⊦ ∀state.
m0.Next state =
bool.LET
(pair.UNCURRY
(λv s.
bool.LET (pair.UNCURRY (λv s. m0.Run v s)) (m0.Decode v s)))
(m0.Fetch state)
⊦ ∀h a b. length b = suc h ⇒ bitstring.field h 0 (a @ b) = b
⊦ ∀v.
words.w2w (bitstring.v2w v) =
bitstring.v2w
(bitstring.fixwidth
(if fcp.dimindex bool.the_value < fcp.dimindex bool.the_value then
fcp.dimindex bool.the_value
else fcp.dimindex bool.the_value) v)
⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x
⊦ ∀w n.
words.bit_count_upto (suc n) w =
(if fcp.fcp_index w n then 1 else 0) + words.bit_count_upto n w
⊦ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h :: t)) ⇒ ∀l. P l
⊦ ∀f e x l. list.FOLDL f e (list.SNOC x l) = f (list.FOLDL f e l) x
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_le x y ⇒
(integer.int_le (integer.int_of_num 0) (integer.int_add c y) ⇔ ⊤)
⊦ ∀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. n * m = p * m ⇔ m = 0 ∨ n = p
⊦ ∀p w.
alignment.align p w =
words.n2w
((words.w2n w div arithmetic.BIT2 0 ↑ p) * arithmetic.BIT2 0 ↑ p)
⊦ ∀x y.
¬(words.word_msb x ⇔ words.word_msb y) ⇒
integer_word.w2i (words.word_add x y) =
integer.int_add (integer_word.w2i x) (integer_word.w2i y)
⊦ ∀v w.
words.word_join v w =
bool.LET
(bool.LET
(λcv cw.
words.word_or (words.word_lsl cv (fcp.dimindex bool.the_value))
cw) (words.w2w v)) (words.w2w w)
⊦ arithmetic.DIV2 0 = 0 ∧ (∀n. arithmetic.DIV2 (bit1 n) = n) ∧
∀n. arithmetic.DIV2 (arithmetic.BIT2 n) = suc n
⊦ ∀x y.
x = y ⇔
∀i.
i < fcp.dimindex bool.the_value ⇒
fcp.fcp_index x i = fcp.fcp_index y i
⊦ ∀w n.
words.word_lsr w n =
fcp.FCP
(λi. i + n < fcp.dimindex bool.the_value ∧ fcp.fcp_index w (i + n))
⊦ (∀l. rich_list.COUNT_LIST_AUX 0 l = l) ∧
∀n l.
rich_list.COUNT_LIST_AUX (suc n) l =
rich_list.COUNT_LIST_AUX n (n :: l)
⊦ (∀l. list.EL 0 l = head l) ∧ ∀l n. list.EL (suc n) l = list.EL n (tail l)
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ ∀p w.
alignment.aligned p w ⇔
p = 0 ∨ words.word_extract (arithmetic.- p 1) 0 w = words.n2w 0
⊦ ∀v i.
i < length v ⇒
(bitstring.testbit i v ⇔
list.EL (arithmetic.- (arithmetic.- (length v) 1) i) v)
⊦ ∀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)
⊦ numeral.iiSUC 0 = arithmetic.BIT2 0 ∧
numeral.iiSUC (bit1 n) = bit1 (suc n) ∧
numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n)
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_lt y (integer.int_neg x) ⇒
(integer.int_le (integer.int_of_num 0)
(integer.int_add (integer.int_neg c) y) ⇔ ⊥)
⊦ ∀n.
numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n) ∧
numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n) ∧
numeral.iDUB 0 = 0
⊦ ∀n.
words.INT_MIN bool.the_value ≤ n ∧ n < words.dimword bool.the_value ⇒
integer_word.w2i (words.n2w n) =
integer.int_neg
(integer.int_of_num (arithmetic.- (words.dimword bool.the_value) n))
⊦ ∀l1 n.
length l1 ≤ n ⇒
∀l2. list.DROP n (l1 @ l2) = list.DROP (arithmetic.- n (length l1)) l2
⊦ (∀f. sum_num.SUM 0 f = 0) ∧
∀m f. sum_num.SUM (suc m) f = sum_num.SUM m f + f m
⊦ (∀n. n ↑ 0 = 1) ∧ ∀m n. m ↑ suc n = m * m ↑ n
⊦ ∀i x y c.
blast.BSUM i x y c ⇔ blast.bsum (x i) (y i) (blast.BCARRY i x y c)
⊦ ∀v i.
fcp.fcp_index (bitstring.v2w v) i ⇔
if i < fcp.dimindex bool.the_value then bitstring.testbit i v
else combin.FAIL fcp.fcp_index index too large (bitstring.v2w v) i
⊦ ∀w n.
n < fcp.dimindex bool.the_value ⇒
(list.EL n (bitstring.w2v w) ⇔
fcp.fcp_index w
(arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1) n))
⊦ (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 v. const v ∘ f = const v) ∧ ∀f v. f ∘ const v = const (f v)
⊦ ∀b v.
bitstring.testbit b v ⇔
bool.LET (λn. b < n ∧ list.EL (arithmetic.- (arithmetic.- n 1) b) v)
(length v)
⊦ ∀n v.
bitstring.fixwidth n v =
bool.LET
(λl.
if l < n then bitstring.zero_extend n v
else list.DROP (arithmetic.- l n) v) (length v)
⊦ ∀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 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
⊦ ∀m n p. m = arithmetic.- n p ⇔ m + p = n ∨ m ≤ 0 ∧ n ≤ p
⊦ 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)
⊦ (∀P. all P [] ⇔ ⊤) ∧ ∀P h t. all P (h :: t) ⇔ P h ∧ all P t
⊦ list.EL (bit1 n) (l :: ls) = list.EL (prim_rec.PRE (bit1 n)) ls ∧
list.EL (arithmetic.BIT2 n) (l :: ls) = list.EL (bit1 n) ls
⊦ ∀mc.
m0.Decode mc =
λstate.
m0.MachineCode_CASE mc
(λh.
m0.DecodeThumb h
(m0.m0_state_pcinc_fupd
(const (words.n2w (arithmetic.BIT2 0))) state))
(λhs.
m0.DecodeThumb2 hs
(m0.m0_state_pcinc_fupd
(const (words.n2w (arithmetic.BIT2 1))) state))
⊦ ∀n.
even 0 ∧ even (arithmetic.BIT2 n) ∧ ¬even (bit1 n) ∧ ¬odd 0 ∧
¬odd (arithmetic.BIT2 n) ∧ odd (bit1 n)
⊦ ∀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))
⊦ ∀h l.
words.word_slice h l =
λw.
fcp.FCP
(λi.
l ≤ i ∧
i ≤ min h (arithmetic.- (fcp.dimindex bool.the_value) 1) ∧
fcp.fcp_index w i)
⊦ (∀a f f1. m0.MachineCode_CASE (m0.Thumb a) f f1 = f a) ∧
∀a f f1. m0.MachineCode_CASE (m0.Thumb2 a) f f1 = f1 a
⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)
⊦ (∀b. numposrep.l2n b [] = 0) ∧
∀b h t. numposrep.l2n b (h :: t) = h mod b + b * numposrep.l2n b t
⊦ ∀c w.
words.word_rrx (c, w) =
(words.word_lsb w,
fcp.FCP
(λi.
if i = arithmetic.- (fcp.dimindex bool.the_value) 1 then c
else fcp.fcp_index (words.word_lsr w 1) i))
⊦ ∀x carry_in.
m0.RRX_C (x, carry_in) =
(bitstring.v2w
((carry_in :: []) @
bitstring.field (arithmetic.- (words.word_len (words.n2w 0)) 1) 1
(bitstring.w2v x)), words.word_bit 0 x)
⊦ ∀w i.
i < fcp.dimindex bool.the_value ⇒
(fcp.fcp_index (words.sw2sw w) i ⇔
if i < fcp.dimindex bool.the_value ∨
fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
then fcp.fcp_index w i
else words.word_msb w)
⊦ ∀x y.
¬(integer_word.w2i (words.word_add x y) =
integer.int_add (integer_word.w2i x) (integer_word.w2i y)) ⇔
(words.word_msb x ⇔ words.word_msb y) ∧
¬(words.word_msb x ⇔ words.word_msb (words.word_add x y))
⊦ 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)
⊦ (∀f e. list.FOLDL f e [] = e) ∧
∀f e x l. list.FOLDL f e (x :: l) = list.FOLDL f (f e x) l
⊦ 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)
⊦ ∀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)
⊦ ∀h l a b.
l ≤ h ∧ length b ≤ l ⇒
bitstring.field h l (a @ b) =
bitstring.field (arithmetic.- h (length b)) (arithmetic.- l (length b))
a
⊦ (∀l1 l2 l3. l1 @ l2 = l1 @ l3 ⇔ l2 = l3) ∧
∀l1 l2 l3. l2 @ l1 = l3 @ l1 ⇔ l2 = l3
⊦ ∀w.
m0.BitCount w =
fst
(snd
(state_transformer.FOR
(0, arithmetic.- (words.word_len (words.n2w 0)) 1,
(λi state.
((),
(if words.word_bit i w then (fst state + 1, ())
else state)))) (0, ())))
⊦ ∀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 v.
length v ≤ fcp.dimindex bool.the_value ∧
fcp.dimindex bool.the_value = arithmetic.- (suc h) l ∧
fcp.dimindex bool.the_value < fcp.dimindex bool.the_value ⇒
words.word_extract h l (bitstring.v2w v) =
bitstring.v2w (bitstring.field h l v)
⊦ (∀x y c. blast.BCARRY 0 x y c ⇔ c) ∧
∀i x y c.
blast.BCARRY (suc i) x y c ⇔
blast.bcarry (x i) (y i) (blast.BCARRY i x y c)
⊦ ∀typ.
m0.DecodeRegShift typ =
bool.literal_case
(λv.
if v = words.n2w 0 then m0.SRType_LSL
else if v = words.n2w 1 then m0.SRType_LSR
else if v = words.n2w (arithmetic.BIT2 0) then m0.SRType_ASR
else if v = words.n2w 3 then m0.SRType_ROR
else bool.ARB) typ
⊦ 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
⊦ ∀v h l i.
i < arithmetic.- (suc h) l ⇒
(list.EL i (bitstring.field h l v) ⇔
suc h ≤ i + length v ∧
list.EL (arithmetic.- (i + length v) (suc h)) v)
⊦ (∀a. bitstring.bitify a [] = a) ∧
(∀l a. bitstring.bitify a (⊥ :: l) = bitstring.bitify (0 :: a) l) ∧
∀l a. bitstring.bitify a (⊤ :: l) = bitstring.bitify (1 :: a) l
⊦ ∀j i a.
state_transformer.FOR (i, j, a) =
if i = j then a i
else
state_transformer.BIND (a i)
(λu.
state_transformer.FOR
((if i < j then i + 1 else arithmetic.- i 1), j, a))
⊦ ∀v1 v2.
words.word_concat (bitstring.v2w v1) (bitstring.v2w v2) =
if pred_set.FINITE pred_set.UNIV ∧ pred_set.FINITE pred_set.UNIV then
bitstring.v2w
(bitstring.fixwidth
(min (fcp.dimindex bool.the_value)
(fcp.dimindex bool.the_value + fcp.dimindex bool.the_value))
(v1 @ bitstring.fixwidth (fcp.dimindex bool.the_value) v2))
else
combin.FAIL words.word_concat bad domain (bitstring.v2w v1)
(bitstring.v2w v2)
⊦ ∀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)
⊦ ∀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))
⊦ (∀m n.
words.word_add (words.word_2comp (words.n2w m))
(words.word_2comp (words.n2w n)) =
words.word_2comp (words.n2w (m + n))) ∧
∀m n.
words.word_add (words.n2w m) (words.word_2comp (words.n2w n)) =
if n ≤ m then words.n2w (arithmetic.- m n)
else words.word_2comp (words.n2w (arithmetic.- n m))
⊦ 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
⊦ (∀m n.
m < bit1 n ⇔
m = arithmetic.- (bit1 n) 1 ∨ m < arithmetic.- (bit1 n) 1) ∧
∀m n. m < arithmetic.BIT2 n ⇔ m = bit1 n ∨ m < bit1 n
⊦ ∀l l' b b' f f'.
l = l' ∧ b = b' ∧
(∀x a. bool.IN x (list.LIST_TO_SET l') ⇒ f a x = f' a x) ⇒
list.FOLDL f b l = list.FOLDL f' b' l'
⊦ (∀a b. bit.MOD_2EXP_EQ 0 a b ⇔ ⊤) ∧
(∀n a b.
bit.MOD_2EXP_EQ (suc n) a b ⇔
(odd a ⇔ odd b) ∧
bit.MOD_2EXP_EQ n (arithmetic.DIV2 a) (arithmetic.DIV2 b)) ∧
∀n a. bit.MOD_2EXP_EQ n a a ⇔ ⊤
⊦ (∀m n.
words.n2w m = words.n2w n ⇔
bit.MOD_2EXP_EQ (fcp.dimindex bool.the_value) m n) ∧
(∀n.
words.n2w n = words.word_2comp (words.n2w 1) ⇔
bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n) ∧
∀n.
words.word_2comp (words.n2w 1) = words.n2w n ⇔
bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n
⊦ (∀l. rich_list.COUNT_LIST_AUX 0 l = l) ∧
(∀n l.
rich_list.COUNT_LIST_AUX (bit1 n) l =
rich_list.COUNT_LIST_AUX (arithmetic.- (bit1 n) 1)
(arithmetic.- (bit1 n) 1 :: l)) ∧
∀n l.
rich_list.COUNT_LIST_AUX (arithmetic.BIT2 n) l =
rich_list.COUNT_LIST_AUX (bit1 n) (bit1 n :: l)
⊦ ∀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
⊦ ∀x y carry_in.
words.add_with_carry (x, y, carry_in) =
bool.LET
(λunsigned_sum.
bool.LET
(λresult.
bool.LET
(bool.LET
(λcarry_out overflow. (result, carry_out, overflow))
(¬(words.w2n result = unsigned_sum)))
((words.word_msb x ⇔ words.word_msb y) ∧
¬(words.word_msb x ⇔ words.word_msb result)))
(words.n2w unsigned_sum))
(words.w2n x + words.w2n y + if carry_in then 1 else 0)
⊦ ∀value typ amount carry_in.
m0.Shift_C (value, typ, amount, carry_in) =
λstate.
if amount = 0 then ((value, carry_in), state)
else
m0.SRType_CASE typ (m0.LSL_C (value, amount) state)
(m0.LSR_C (value, amount) state) (m0.ASR_C (value, amount) state)
(m0.ROR_C (value, amount) state)
(m0.RRX_C (value, carry_in), state)
⊦ ∀x y carry_in.
m0.AddWithCarry (x, y, carry_in) =
bool.LET
(λunsigned_sum.
bool.LET
(λresult.
(result, ¬(words.w2n result = unsigned_sum),
¬(integer_word.w2i result =
integer.int_add
(integer.int_add (integer_word.w2i x)
(integer_word.w2i y))
(if carry_in then integer.int_of_num 1
else integer.int_of_num 0))))
(words.n2w unsigned_sum))
(words.w2n x + words.w2n y + if carry_in then 1 else 0)
⊦ (∀m n. integer.int_of_num m = integer.int_of_num n ⇔ m = n) ∧
(∀x y. integer.int_neg x = integer.int_neg y ⇔ x = y) ∧
∀n m.
(integer.int_of_num n = integer.int_neg (integer.int_of_num m) ⇔
n = 0 ∧ m = 0) ∧
(integer.int_neg (integer.int_of_num n) = integer.int_of_num m ⇔
n = 0 ∧ m = 0)
⊦ (∀l. list.DROP 0 l = l) ∧ (∀n. list.DROP (bit1 n) [] = []) ∧
(∀n. list.DROP (arithmetic.BIT2 n) [] = []) ∧
(∀n h t.
list.DROP (bit1 n) (h :: t) = list.DROP (arithmetic.- (bit1 n) 1) t) ∧
∀n h t. list.DROP (arithmetic.BIT2 n) (h :: t) = list.DROP (bit1 n) t
⊦ ∀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)
⊦ ∀x shift.
m0.ROR_C (x, shift) =
λstate.
(bool.LET (λresult. (result, words.word_msb result))
(words.word_ror x shift),
(if shift = 0 then
snd
(m0.raise'exception
(m0.ASSERT
(string.CHR
(arithmetic.BIT2
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(arithmetic.BIT2
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(bit1
(bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))) ::
string.CHR (bit1 (bit1 (arithmetic.BIT2 7))) :: []))
state)
else state))
⊦ ∀m n p.
integer.int_sub p (integer.int_of_num 0) = p ∧
integer.int_sub (integer.int_of_num 0) p = integer.int_neg p ∧
integer.int_sub (integer.int_of_num m) (integer.int_of_num n) =
integer.int_add (integer.int_of_num m)
(integer.int_neg (integer.int_of_num n)) ∧
integer.int_sub (integer.int_neg (integer.int_of_num m))
(integer.int_of_num n) =
integer.int_add (integer.int_neg (integer.int_of_num m))
(integer.int_neg (integer.int_of_num n)) ∧
integer.int_sub (integer.int_of_num m)
(integer.int_neg (integer.int_of_num n)) =
integer.int_add (integer.int_of_num m) (integer.int_of_num n) ∧
integer.int_sub (integer.int_neg (integer.int_of_num m))
(integer.int_neg (integer.int_of_num n)) =
integer.int_add (integer.int_neg (integer.int_of_num m))
(integer.int_of_num n)
⊦ ∀x shift.
m0.ASR_C (x, shift) =
λstate.
((words.word_asr x shift,
words.word_bit
(arithmetic.- (min (words.word_len (words.n2w 0)) shift) 1) x),
(if shift = 0 then
snd
(m0.raise'exception
(m0.ASSERT
(string.CHR (bit1 (arithmetic.BIT2 15)) ::
string.CHR
(bit1
(bit1
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(arithmetic.BIT2
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(bit1
(bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))) ::
string.CHR (bit1 (bit1 (arithmetic.BIT2 7))) :: []))
state)
else state))
⊦ ∀x shift.
m0.LSL_C (x, shift) =
λstate.
((words.word_lsl x shift,
bitstring.testbit (words.word_len (words.n2w 0))
(bitstring.w2v x @ bitstring.replicate (⊥ :: []) shift)),
(if shift = 0 then
snd
(m0.raise'exception
(m0.ASSERT
(string.CHR
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 (arithmetic.BIT2 3)))) ::
string.CHR
(bit1
(bit1
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 (arithmetic.BIT2 3)))) ::
string.CHR
(bit1
(bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))) ::
string.CHR (bit1 (bit1 (arithmetic.BIT2 7))) :: []))
state)
else state))
⊦ ∀x shift.
m0.LSR_C (x, shift) =
λstate.
((words.word_lsr x shift,
shift ≤ words.word_len (words.n2w 0) ∧
words.word_bit (arithmetic.- shift 1) x),
(if shift = 0 then
snd
(m0.raise'exception
(m0.ASSERT
(string.CHR
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 (arithmetic.BIT2 3)))) ::
string.CHR
(bit1
(bit1
(arithmetic.BIT2
(bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(arithmetic.BIT2
(arithmetic.BIT2
(bit1 (bit1 (arithmetic.BIT2 1))))) ::
string.CHR
(bit1
(bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))) ::
string.CHR (bit1 (bit1 (arithmetic.BIT2 7))) :: []))
state)
else state))
⊦ ∀typ imm5.
m0.DecodeImmShift (typ, imm5) =
bool.literal_case
(λv.
if v = words.n2w 0 then (m0.SRType_LSL, words.w2n imm5)
else if v = words.n2w 1 then
(m0.SRType_LSR,
(if imm5 = words.n2w 0 then arithmetic.BIT2 15
else words.w2n imm5))
else if v = words.n2w (arithmetic.BIT2 0) then
(m0.SRType_ASR,
(if imm5 = words.n2w 0 then arithmetic.BIT2 15
else words.w2n imm5))
else if v = words.n2w 3 then
if imm5 = words.n2w 0 then (m0.SRType_RRX, 1)
else (m0.SRType_ROR, words.w2n imm5)
else bool.ARB) typ
⊦ ∀p n m.
integer.int_add (integer.int_of_num 0) p = p ∧
integer.int_add p (integer.int_of_num 0) = p ∧
integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
integer.int_of_num (n + m) ∧
integer.int_add (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) =
(if m ≤ n then integer.int_of_num (arithmetic.- n m)
else integer.int_neg (integer.int_of_num (arithmetic.- m n))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) =
(if n ≤ m then integer.int_of_num (arithmetic.- m n)
else integer.int_neg (integer.int_of_num (arithmetic.- n m))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) =
integer.int_neg (integer.int_of_num (n + m))
⊦ (∀v0 v1 v2 v3 v4. m0.SRType_CASE m0.SRType_LSL v0 v1 v2 v3 v4 = v0) ∧
(∀v0 v1 v2 v3 v4. m0.SRType_CASE m0.SRType_LSR v0 v1 v2 v3 v4 = v1) ∧
(∀v0 v1 v2 v3 v4. m0.SRType_CASE m0.SRType_ASR v0 v1 v2 v3 v4 = v2) ∧
(∀v0 v1 v2 v3 v4. m0.SRType_CASE m0.SRType_ROR v0 v1 v2 v3 v4 = v3) ∧
∀v0 v1 v2 v3 v4. m0.SRType_CASE m0.SRType_RRX v0 v1 v2 v3 v4 = v4
⊦ ∀p n m.
integer.int_add (integer.int_of_num 0) p = p ∧
integer.int_add p (integer.int_of_num 0) = p ∧
integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0 ∧
integer.int_neg (integer.int_neg p) = p ∧
integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
integer.int_of_num (numeral.iZ (n + m)) ∧
integer.int_add (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) =
(if m ≤ n then integer.int_of_num (arithmetic.- n m)
else integer.int_neg (integer.int_of_num (arithmetic.- m n))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) =
(if n ≤ m then integer.int_of_num (arithmetic.- m n)
else integer.int_neg (integer.int_of_num (arithmetic.- n m))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) =
integer.int_neg (integer.int_of_num (numeral.iZ (n + m)))
⊦ ∀m1 m2.
m1 = m2 ⇔
m0.m0_state_AIRCR m1 = m0.m0_state_AIRCR m2 ∧
m0.m0_state_CCR m1 = m0.m0_state_CCR m2 ∧
m0.m0_state_CONTROL m1 = m0.m0_state_CONTROL m2 ∧
m0.m0_state_CurrentMode m1 = m0.m0_state_CurrentMode m2 ∧
m0.m0_state_ExceptionActive m1 = m0.m0_state_ExceptionActive m2 ∧
m0.m0_state_MEM m1 = m0.m0_state_MEM m2 ∧
m0.m0_state_NVIC_IPR m1 = m0.m0_state_NVIC_IPR m2 ∧
m0.m0_state_PRIMASK m1 = m0.m0_state_PRIMASK m2 ∧
m0.m0_state_PSR m1 = m0.m0_state_PSR m2 ∧
m0.m0_state_REG m1 = m0.m0_state_REG m2 ∧
m0.m0_state_SHPR2 m1 = m0.m0_state_SHPR2 m2 ∧
m0.m0_state_SHPR3 m1 = m0.m0_state_SHPR3 m2 ∧
m0.m0_state_VTOR m1 = m0.m0_state_VTOR m2 ∧
m0.m0_state_count m1 = m0.m0_state_count m2 ∧
m0.m0_state_exception m1 = m0.m0_state_exception m2 ∧
m0.m0_state_pcinc m1 = m0.m0_state_pcinc m2 ∧
m0.m0_state_pending m1 = m0.m0_state_pending m2
⊦ 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))
⊦ ∀n m.
(integer.int_lt (integer.int_of_num 0) (integer.int_of_num (bit1 n)) ⇔
⊤) ∧
(integer.int_lt (integer.int_of_num 0)
(integer.int_of_num (arithmetic.BIT2 n)) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num 0) (integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_lt (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num n)) ⇔ ⊥) ∧
(integer.int_lt (integer.int_of_num n) (integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_lt
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num n) (integer.int_of_num m) ⇔
n < m) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_lt
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) ⇔ ⊥) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) ⇔ m < n)
⊦ m0.RName2num m0.RName_0 = 0 ∧ m0.RName2num m0.RName_1 = 1 ∧
m0.RName2num m0.RName_2 = arithmetic.BIT2 0 ∧
m0.RName2num m0.RName_3 = 3 ∧
m0.RName2num m0.RName_4 = arithmetic.BIT2 1 ∧
m0.RName2num m0.RName_5 = bit1 (arithmetic.BIT2 0) ∧
m0.RName2num m0.RName_6 = arithmetic.BIT2 (arithmetic.BIT2 0) ∧
m0.RName2num m0.RName_7 = 7 ∧
m0.RName2num m0.RName_8 = arithmetic.BIT2 3 ∧
m0.RName2num m0.RName_9 = bit1 (arithmetic.BIT2 1) ∧
m0.RName2num m0.RName_10 = arithmetic.BIT2 (arithmetic.BIT2 1) ∧
m0.RName2num m0.RName_11 = bit1 (bit1 (arithmetic.BIT2 0)) ∧
m0.RName2num m0.RName_12 = arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)) ∧
m0.RName2num m0.RName_SP_main =
bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)) ∧
m0.RName2num m0.RName_SP_process =
arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)) ∧
m0.RName2num m0.RName_LR = 15 ∧
m0.RName2num m0.RName_PC = arithmetic.BIT2 7
⊦ ∀n m.
(integer.int_le (integer.int_of_num 0) (integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num 0) (integer.int_of_num n) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num (bit1 n))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num (bit1 n)) (integer.int_of_num 0) ⇔
⊥) ∧
(integer.int_le (integer.int_of_num (arithmetic.BIT2 n))
(integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_le (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num n) (integer.int_of_num m) ⇔
n ≤ m) ∧
(integer.int_le (integer.int_of_num n)
(integer.int_neg (integer.int_of_num (bit1 m))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num n)
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 m))) ⇔ ⊥) ∧
(integer.int_le (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_le (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) ⇔ m ≤ n)
⊦ ∀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))
⊦ (∀m g f.
m0.m0_state_AIRCR_fupd f (m0.m0_state_AIRCR_fupd g m) =
m0.m0_state_AIRCR_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_CCR_fupd f (m0.m0_state_CCR_fupd g m) =
m0.m0_state_CCR_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_CONTROL_fupd f (m0.m0_state_CONTROL_fupd g m) =
m0.m0_state_CONTROL_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_CurrentMode_fupd f (m0.m0_state_CurrentMode_fupd g m) =
m0.m0_state_CurrentMode_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_ExceptionActive_fupd f
(m0.m0_state_ExceptionActive_fupd g m) =
m0.m0_state_ExceptionActive_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_MEM_fupd f (m0.m0_state_MEM_fupd g m) =
m0.m0_state_MEM_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_NVIC_IPR_fupd f (m0.m0_state_NVIC_IPR_fupd g m) =
m0.m0_state_NVIC_IPR_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_PRIMASK_fupd f (m0.m0_state_PRIMASK_fupd g m) =
m0.m0_state_PRIMASK_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_PSR_fupd f (m0.m0_state_PSR_fupd g m) =
m0.m0_state_PSR_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_REG_fupd f (m0.m0_state_REG_fupd g m) =
m0.m0_state_REG_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_SHPR2_fupd f (m0.m0_state_SHPR2_fupd g m) =
m0.m0_state_SHPR2_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_SHPR3_fupd f (m0.m0_state_SHPR3_fupd g m) =
m0.m0_state_SHPR3_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_VTOR_fupd f (m0.m0_state_VTOR_fupd g m) =
m0.m0_state_VTOR_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_count_fupd f (m0.m0_state_count_fupd g m) =
m0.m0_state_count_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_exception_fupd f (m0.m0_state_exception_fupd g m) =
m0.m0_state_exception_fupd (f ∘ g) m) ∧
(∀m g f.
m0.m0_state_pcinc_fupd f (m0.m0_state_pcinc_fupd g m) =
m0.m0_state_pcinc_fupd (f ∘ g) m) ∧
∀m g f.
m0.m0_state_pending_fupd f (m0.m0_state_pending_fupd g m) =
m0.m0_state_pending_fupd (f ∘ g) 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
⊦ (∀v.
words.word_2comp (bitstring.v2w v) =
words.word_2comp (words.n2w (bitstring.v2n v))) ∧
(∀v.
words.word_log2 (bitstring.v2w v) =
words.word_log2 (words.n2w (bitstring.v2n v))) ∧
(∀v n.
bitstring.v2w v = words.n2w n ⇔
words.n2w (bitstring.v2n v) = words.n2w n) ∧
(∀v n.
words.n2w n = bitstring.v2w v ⇔
words.n2w n = words.n2w (bitstring.v2n v)) ∧
(∀v w.
words.word_add (bitstring.v2w v) w =
words.word_add (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_add w (bitstring.v2w v) =
words.word_add w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_sub (bitstring.v2w v) w =
words.word_sub (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_sub w (bitstring.v2w v) =
words.word_sub w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_mul (bitstring.v2w v) w =
words.word_mul (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_mul w (bitstring.v2w v) =
words.word_mul w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_sdiv (bitstring.v2w v) w =
words.word_sdiv (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_sdiv w (bitstring.v2w v) =
words.word_sdiv w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_div (bitstring.v2w v) w =
words.word_div (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_div w (bitstring.v2w v) =
words.word_div w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_mod (bitstring.v2w v) w =
words.word_mod (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_mod w (bitstring.v2w v) =
words.word_mod w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_lt (bitstring.v2w v) w ⇔
words.word_lt (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_lt w (bitstring.v2w v) ⇔
words.word_lt w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_gt (bitstring.v2w v) w ⇔
words.word_gt (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_gt w (bitstring.v2w v) ⇔
words.word_gt w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_le (bitstring.v2w v) w ⇔
words.word_le (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_le w (bitstring.v2w v) ⇔
words.word_le w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_ge (bitstring.v2w v) w ⇔
words.word_ge (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_ge w (bitstring.v2w v) ⇔
words.word_ge w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_lo (bitstring.v2w v) w ⇔
words.word_lo (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_lo w (bitstring.v2w v) ⇔
words.word_lo w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_hi (bitstring.v2w v) w ⇔
words.word_hi (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_hi w (bitstring.v2w v) ⇔
words.word_hi w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_ls (bitstring.v2w v) w ⇔
words.word_ls (words.n2w (bitstring.v2n v)) w) ∧
(∀v w.
words.word_ls w (bitstring.v2w v) ⇔
words.word_ls w (words.n2w (bitstring.v2n v))) ∧
(∀v w.
words.word_hs (bitstring.v2w v) w ⇔
words.word_hs (words.n2w (bitstring.v2n v)) w) ∧
∀v w.
words.word_hs w (bitstring.v2w v) ⇔
words.word_hs w (words.n2w (bitstring.v2n v))
⊦ (∀m f.
m0.m0_state_AIRCR (m0.m0_state_CCR_fupd f m) = m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_MEM_fupd f m) = m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_PSR_fupd f m) = m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_REG_fupd f m) = m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_VTOR_fupd f m) = m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_count_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_exception_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_pending_fupd f m) =
m0.m0_state_AIRCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_AIRCR_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_CONTROL_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_CCR m) ∧
(∀m f. m0.m0_state_CCR (m0.m0_state_MEM_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_NVIC_IPR_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_PRIMASK_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f. m0.m0_state_CCR (m0.m0_state_PSR_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f. m0.m0_state_CCR (m0.m0_state_REG_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_SHPR2_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_SHPR3_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f. m0.m0_state_CCR (m0.m0_state_VTOR_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_count_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_exception_fupd f m) =
m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_pcinc_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_pending_fupd f m) = m0.m0_state_CCR m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_CCR_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_MEM_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_PSR_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_REG_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_count_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_exception_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_pending_fupd f m) =
m0.m0_state_CONTROL m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_CCR_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_MEM_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_PSR_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_REG_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_count_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_exception_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_pending_fupd f m) =
m0.m0_state_CurrentMode m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_CCR_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_MEM_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_PSR_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_REG_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_count_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_exception_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_pending_fupd f m) =
m0.m0_state_ExceptionActive m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_AIRCR_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f. m0.m0_state_MEM (m0.m0_state_CCR_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_CONTROL_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_NVIC_IPR_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_PRIMASK_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f. m0.m0_state_MEM (m0.m0_state_PSR_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f. m0.m0_state_MEM (m0.m0_state_REG_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_SHPR2_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_SHPR3_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f. m0.m0_state_MEM (m0.m0_state_VTOR_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_count_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_exception_fupd f m) =
m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_pcinc_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_pending_fupd f m) = m0.m0_state_MEM m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_CCR_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_MEM_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_PSR_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_REG_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_count_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_exception_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_pending_fupd f m) =
m0.m0_state_NVIC_IPR m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_CCR_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_MEM_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_PSR_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_REG_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_count_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_exception_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_pending_fupd f m) =
m0.m0_state_PRIMASK m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_AIRCR_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f. m0.m0_state_PSR (m0.m0_state_CCR_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_CONTROL_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_PSR m) ∧
(∀m f. m0.m0_state_PSR (m0.m0_state_MEM_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_NVIC_IPR_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_PRIMASK_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f. m0.m0_state_PSR (m0.m0_state_REG_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_SHPR2_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_SHPR3_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f. m0.m0_state_PSR (m0.m0_state_VTOR_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_count_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_exception_fupd f m) =
m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_pcinc_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_pending_fupd f m) = m0.m0_state_PSR m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_AIRCR_fupd f m) = m0.m0_state_REG m) ∧
(∀m f. m0.m0_state_REG (m0.m0_state_CCR_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_CONTROL_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_REG m) ∧
(∀m f. m0.m0_state_REG (m0.m0_state_MEM_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_NVIC_IPR_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_PRIMASK_fupd f m) = m0.m0_state_REG m) ∧
(∀m f. m0.m0_state_REG (m0.m0_state_PSR_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_SHPR2_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_SHPR3_fupd f m) = m0.m0_state_REG m) ∧
(∀m f. m0.m0_state_REG (m0.m0_state_VTOR_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_count_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_exception_fupd f m) =
m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_pcinc_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_pending_fupd f m) = m0.m0_state_REG m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_CCR_fupd f m) = m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_MEM_fupd f m) = m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_PSR_fupd f m) = m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_REG_fupd f m) = m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_VTOR_fupd f m) = m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_count_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_exception_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_pending_fupd f m) =
m0.m0_state_SHPR2 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_CCR_fupd f m) = m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_MEM_fupd f m) = m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_PSR_fupd f m) = m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_REG_fupd f m) = m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_VTOR_fupd f m) = m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_count_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_exception_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_pending_fupd f m) =
m0.m0_state_SHPR3 m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_AIRCR_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_CCR_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_MEM_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_PSR_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_REG_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_SHPR2_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_SHPR3_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_count_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_exception_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_pcinc_fupd f m) = m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_pending_fupd f m) =
m0.m0_state_VTOR m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_CCR_fupd f m) = m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_MEM_fupd f m) = m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_PSR_fupd f m) = m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_REG_fupd f m) = m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_VTOR_fupd f m) = m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_exception_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_pending_fupd f m) =
m0.m0_state_count m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_CCR_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_MEM_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_PSR_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_REG_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_count_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_pending_fupd f m) =
m0.m0_state_exception m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_CCR_fupd f m) = m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_MEM_fupd f m) = m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_PSR_fupd f m) = m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_REG_fupd f m) = m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_VTOR_fupd f m) = m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_count_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_exception_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_pending_fupd f m) =
m0.m0_state_pcinc m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_AIRCR_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_CCR_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_CONTROL_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_CurrentMode_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_ExceptionActive_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_MEM_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_NVIC_IPR_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_PRIMASK_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_PSR_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_REG_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_SHPR2_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_SHPR3_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_VTOR_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_count_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_exception_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_pending (m0.m0_state_pcinc_fupd f m) =
m0.m0_state_pending m) ∧
(∀m f.
m0.m0_state_AIRCR (m0.m0_state_AIRCR_fupd f m) =
f (m0.m0_state_AIRCR m)) ∧
(∀m f.
m0.m0_state_CCR (m0.m0_state_CCR_fupd f m) = f (m0.m0_state_CCR m)) ∧
(∀m f.
m0.m0_state_CONTROL (m0.m0_state_CONTROL_fupd f m) =
f (m0.m0_state_CONTROL m)) ∧
(∀m f.
m0.m0_state_CurrentMode (m0.m0_state_CurrentMode_fupd f m) =
f (m0.m0_state_CurrentMode m)) ∧
(∀m f.
m0.m0_state_ExceptionActive (m0.m0_state_ExceptionActive_fupd f m) =
f (m0.m0_state_ExceptionActive m)) ∧
(∀m f.
m0.m0_state_MEM (m0.m0_state_MEM_fupd f m) = f (m0.m0_state_MEM m)) ∧
(∀m f.
m0.m0_state_NVIC_IPR (m0.m0_state_NVIC_IPR_fupd f m) =
f (m0.m0_state_NVIC_IPR m)) ∧
(∀m f.
m0.m0_state_PRIMASK (m0.m0_state_PRIMASK_fupd f m) =
f (m0.m0_state_PRIMASK m)) ∧
(∀m f.
m0.m0_state_PSR (m0.m0_state_PSR_fupd f m) = f (m0.m0_state_PSR m)) ∧
(∀m f.
m0.m0_state_REG (m0.m0_state_REG_fupd f m) = f (m0.m0_state_REG m)) ∧
(∀m f.
m0.m0_state_SHPR2 (m0.m0_state_SHPR2_fupd f m) =
f (m0.m0_state_SHPR2 m)) ∧
(∀m f.
m0.m0_state_SHPR3 (m0.m0_state_SHPR3_fupd f m) =
f (m0.m0_state_SHPR3 m)) ∧
(∀m f.
m0.m0_state_VTOR (m0.m0_state_VTOR_fupd f m) =
f (m0.m0_state_VTOR m)) ∧
(∀m f.
m0.m0_state_count (m0.m0_state_count_fupd f m) =
f (m0.m0_state_count m)) ∧
(∀m f.
m0.m0_state_exception (m0.m0_state_exception_fupd f m) =
f (m0.m0_state_exception m)) ∧
(∀m f.
m0.m0_state_pcinc (m0.m0_state_pcinc_fupd f m) =
f (m0.m0_state_pcinc m)) ∧
∀m f.
m0.m0_state_pending (m0.m0_state_pending_fupd f m) =
f (m0.m0_state_pending m)