Package m0-step: M0 step evaluator

Information

namem0-step
version1.0
descriptionM0 step evaluator
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksum59c7363aaa2835755ed6246dd56639a23e769ae3
requiresbase
hol-base
hol-words
hol-string
hol-integer
hol-monad
m0-model
showData.Bool
Data.List
Data.Option
Data.Pair
Data.Unit
Function
HOL4
Number.Natural

Files

Defined Constants

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

External Constants

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)