Package m0-prog: M0 evaluator

Information

namem0-prog
version1.0
descriptionM0 evaluator
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksumc8343f0e5c93469a37e4d35f1619958d547ca43a
requiresbase
hol-base
hol-words
machine-code-hoare-logic
machine-code-hoare-logic-state
m0-model
m0-step
showData.Bool
Data.List
Data.Option
Data.Pair
Data.Unit
Function
HOL4
Number.Natural

Files

Defined Type Operators

Defined Constants

Theorems

d.
    m0_prog.m0_AIRCR_ENDIANNESS d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_AIRCR_ENDIANNESS, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_AIRCR_SYSRESETREQ d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_AIRCR_SYSRESETREQ, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_AIRCR_VECTCLRACTIVE d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_AIRCR_VECTCLRACTIVE, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_CONTROL_SPSEL d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_CONTROL_SPSEL, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_CONTROL_control'rst d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_CONTROL_control'rst, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_CONTROL_nPRIV d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_CONTROL_nPRIV, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_C d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_C, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_N d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_N, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_T d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_T, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_V d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_V, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_Z d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_Z, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_exception d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_exception, m0_prog.m0_d_exception d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_CCR d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_CCR, m0_prog.m0_d_CCR d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_CurrentMode d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_CurrentMode, m0_prog.m0_d_Mode d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PRIMASK d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PRIMASK, m0_prog.m0_d_PRIMASK d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_SHPR2 d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_SHPR2, m0_prog.m0_d_SHPR2 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_SHPR3 d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_SHPR3, m0_prog.m0_d_SHPR3 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_count d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_count, m0_prog.m0_d_num d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_pending d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_pending, m0_prog.m0_d_ARM_Exception_option d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_ExceptionNumber d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_PSR_ExceptionNumber, m0_prog.m0_d_word6 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_AIRCR_aircr'rst d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_AIRCR_aircr'rst, m0_prog.m0_d_word13 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_AIRCR_VECTKEY d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_AIRCR_VECTKEY, m0_prog.m0_d_word16 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_PSR_psr'rst d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_PSR_psr'rst, m0_prog.m0_d_word21 d)
         pred_set.EMPTY) pred_set.EMPTY

d.
    m0_prog.m0_VTOR d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_VTOR, m0_prog.m0_d_word32 d)
         pred_set.EMPTY) pred_set.EMPTY

pc.
    m0_prog.m0_PC pc =
    set_sep.STAR (m0_prog.m0_REG m0.RName_PC pc)
      (set_sep.cond (alignment.aligned 1 pc))

set_sep.SEP_HIDE m0_prog.m0_NZCV =
  set_sep.STAR
    (set_sep.STAR
       (set_sep.STAR (set_sep.SEP_HIDE m0_prog.m0_PSR_N)
          (set_sep.SEP_HIDE m0_prog.m0_PSR_Z))
       (set_sep.SEP_HIDE m0_prog.m0_PSR_C))
    (set_sep.SEP_HIDE m0_prog.m0_PSR_V)

m0_prog.M0_MODEL =
  (state.STATE m0_prog.m0_proj, state.NEXT_REL (=) m0_step.NextStateM0,
   m0_prog.m0_instr, (=), const )

bigend spsel.
    m0_prog.m0_CONFIG (bigend, spsel) =
    set_sep.STAR
      (set_sep.STAR (m0_prog.m0_exception m0.NoException)
         (m0_prog.m0_AIRCR_ENDIANNESS bigend))
      (m0_prog.m0_CONTROL_SPSEL spsel)

c d.
    m0_prog.m0_REG c d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_REG c, m0_prog.m0_d_word32 d)
         pred_set.EMPTY) pred_set.EMPTY

c d.
    m0_prog.m0_NVIC_IPR c d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_NVIC_IPR c, m0_prog.m0_d_IPR d)
         pred_set.EMPTY) pred_set.EMPTY

c d.
    m0_prog.m0_ExceptionActive c d =
    pred_set.INSERT
      (pred_set.INSERT
         (m0_prog.m0_c_ExceptionActive c, m0_prog.m0_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

c d.
    m0_prog.m0_MEM c d =
    pred_set.INSERT
      (pred_set.INSERT (m0_prog.m0_c_MEM c, m0_prog.m0_d_word8 d)
         pred_set.EMPTY) pred_set.EMPTY

dreg reg.
    m0_prog.m0_REGISTERS dreg reg =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λc.
               (pred_set.BIGUNION (m0_prog.m0_REG c (reg c)),
                bool.IN c dreg)))) pred_set.EMPTY

dmem mem.
    m0_prog.m0_MEMORY dmem mem =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λc.
               (pred_set.BIGUNION (m0_prog.m0_MEM c (mem c)),
                bool.IN c dmem)))) pred_set.EMPTY

words.word_add a (words.word_add (words.word_2comp b) c) =
  words.word_add (words.word_sub a b) c
  words.word_add a (words.word_2comp b) = words.word_sub a b

c d.
    bool.IN c dreg
    set_sep.STAR (m0_prog.m0_REG c d)
      (m0_prog.m0_REGISTERS (pred_set.DELETE dreg c) reg) =
    m0_prog.m0_REGISTERS dreg (combin.UPDATE c d reg)

c d.
    bool.IN c dmem
    set_sep.STAR (m0_prog.m0_MEM c d)
      (m0_prog.m0_MEMORY (pred_set.DELETE dmem c) mem) =
    m0_prog.m0_MEMORY dmem (combin.UPDATE c d mem)

y x w pc.
    pred_set.DISJOINT
      (m0_prog.m0_instr
         (words.word_add pc
            (words.word_add (words.w2w w) (words.n2w (arithmetic.BIT2 1))),
          m0_prog.data_to_thumb2 x))
      (m0_prog.m0_instr (pc, Data.Sum.left y))

n z c v.
    m0_prog.m0_NZCV (n, z, c, v) =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR (m0_prog.m0_PSR_N n) (m0_prog.m0_PSR_Z z))
         (m0_prog.m0_PSR_C c)) (m0_prog.m0_PSR_V v)

P.
    (a opc16. P (a, Data.Sum.left opc16))
    (a opc32. P (a, Data.Sum.right opc32)) v v1. P (v, v1)

prog.SPEC m (set_sep.STAR p1 (m0_prog.m0_PC pc)) code
    (set_sep.STAR p2 (m0_prog.m0_REG m0.RName_PC pc'))
  (alignment.aligned 1 pc alignment.aligned 1 pc')
  prog.SPEC m (set_sep.STAR p1 (m0_prog.m0_PC pc)) code
    (set_sep.STAR p2 (m0_prog.m0_PC pc'))

temporal_state.TEMPORAL_NEXT m (set_sep.STAR p1 (m0_prog.m0_PC pc)) code
    (set_sep.STAR p2 (m0_prog.m0_REG m0.RName_PC pc'))
  (alignment.aligned 1 pc alignment.aligned 1 pc')
  temporal_state.TEMPORAL_NEXT m (set_sep.STAR p1 (m0_prog.m0_PC pc)) code
    (set_sep.STAR p2 (m0_prog.m0_PC pc'))

c p q.
    (y s.
       set_sep.STAR p (prog.CODE_POOL m0_prog.m0_instr c)
         (state.SELECT_STATE m0_prog.m0_proj y s)
       v.
         m0_step.NextStateM0 s = some v
         set_sep.STAR q (prog.CODE_POOL m0_prog.m0_instr c)
           (state.SELECT_STATE m0_prog.m0_proj y v)
         state.FRAME_STATE m0_prog.m0_proj y s =
         state.FRAME_STATE m0_prog.m0_proj y v)
    prog.SPEC m0_prog.M0_MODEL p c q

c p q.
    (y s.
       set_sep.STAR p (prog.CODE_POOL m0_prog.m0_instr c)
         (state.SELECT_STATE m0_prog.m0_proj y s)
       v.
         m0_step.NextStateM0 s = some v
         set_sep.STAR q (prog.CODE_POOL m0_prog.m0_instr c)
           (state.SELECT_STATE m0_prog.m0_proj y v)
         state.FRAME_STATE m0_prog.m0_proj y s =
         state.FRAME_STATE m0_prog.m0_proj y v)
    temporal_state.TEMPORAL_NEXT m0_prog.M0_MODEL p c q

(a a'. m0_prog.m0_c_REG a = m0_prog.m0_c_REG a' a = a')
  (a a'. m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_NVIC_IPR a' a = a')
  (a a'. m0_prog.m0_c_MEM a = m0_prog.m0_c_MEM a' a = a')
  a a'.
    m0_prog.m0_c_ExceptionActive a = m0_prog.m0_c_ExceptionActive a'
    a = a'

w.
    m0_prog.data_to_thumb2 w =
    Data.Sum.right
      (words.word_concat (words.word_extract 15 (arithmetic.BIT2 3) w)
         (words.word_concat (words.word_extract 7 0 w)
            (words.word_concat
               (words.word_extract 31
                  (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w)
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w))))

a pc x y.
    words.word_lo (words.n2w 3) a
    words.word_lo a
      (words.n2w
         (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
                                                                                                   (arithmetic.BIT2
                                                                                                      0))))))))))))))))))))))))))))))))
    pred_set.DISJOINT
      (m0_prog.m0_instr (words.word_add pc a, m0_prog.data_to_thumb2 x))
      (m0_prog.m0_instr (pc, Data.Sum.left y))

(n m0_prog.m0_PSR_N = m0_prog.m0_PSR_N n)
  (¬n m0_prog.m0_PSR_N = m0_prog.m0_PSR_N n)
  (z m0_prog.m0_PSR_Z = m0_prog.m0_PSR_Z z)
  (¬z m0_prog.m0_PSR_Z = m0_prog.m0_PSR_Z z)
  (c m0_prog.m0_PSR_C = m0_prog.m0_PSR_C c)
  (¬c m0_prog.m0_PSR_C = m0_prog.m0_PSR_C c)
  (v m0_prog.m0_PSR_V = m0_prog.m0_PSR_V v)
  (¬v m0_prog.m0_PSR_V = m0_prog.m0_PSR_V v)

a i.
    m0_prog.m0_BE_WORD a i =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR
            (m0_prog.m0_MEM a
               (words.word_extract 31
                  (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) i))
            (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) i)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w (arithmetic.BIT2 0)))
            (words.word_extract 15 (arithmetic.BIT2 3) i)))
      (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
         (words.word_extract 7 0 i))

a i.
    m0_prog.m0_WORD a i =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR (m0_prog.m0_MEM a (words.word_extract 7 0 i))
            (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
               (words.word_extract 15 (arithmetic.BIT2 3) i)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w (arithmetic.BIT2 0)))
            (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
               (arithmetic.BIT2 7) i)))
      (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
         (words.word_extract 31
            (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) i))

P.
    (a. P (m0_prog.m0_d_ARM_Exception_option a))
    (a. P (m0_prog.m0_d_exception a)) (a. P (m0_prog.m0_d_num a))
    (a. P (m0_prog.m0_d_SHPR3 a)) (a. P (m0_prog.m0_d_SHPR2 a))
    (a. P (m0_prog.m0_d_word32 a)) (a. P (m0_prog.m0_d_PRIMASK a))
    (a. P (m0_prog.m0_d_IPR a)) (a. P (m0_prog.m0_d_word8 a))
    (a. P (m0_prog.m0_d_Mode a)) (a. P (m0_prog.m0_d_CCR a))
    (a. P (m0_prog.m0_d_word21 a)) (a. P (m0_prog.m0_d_word6 a))
    (a. P (m0_prog.m0_d_word13 a)) (a. P (m0_prog.m0_d_word16 a))
    (a. P (m0_prog.m0_d_bool a)) x. P x

P.
    P m0_prog.m0_c_pending P m0_prog.m0_c_exception
    P m0_prog.m0_c_count P m0_prog.m0_c_VTOR P m0_prog.m0_c_SHPR3
    P m0_prog.m0_c_SHPR2 (a. P (m0_prog.m0_c_REG a))
    P m0_prog.m0_c_PRIMASK (a. P (m0_prog.m0_c_NVIC_IPR a))
    (a. P (m0_prog.m0_c_MEM a))
    (a. P (m0_prog.m0_c_ExceptionActive a)) P m0_prog.m0_c_CurrentMode
    P m0_prog.m0_c_CCR P m0_prog.m0_c_PSR_psr'rst
    P m0_prog.m0_c_PSR_Z P m0_prog.m0_c_PSR_V P m0_prog.m0_c_PSR_T
    P m0_prog.m0_c_PSR_N P m0_prog.m0_c_PSR_ExceptionNumber
    P m0_prog.m0_c_PSR_C P m0_prog.m0_c_CONTROL_nPRIV
    P m0_prog.m0_c_CONTROL_control'rst P m0_prog.m0_c_CONTROL_SPSEL
    P m0_prog.m0_c_AIRCR_aircr'rst P m0_prog.m0_c_AIRCR_VECTKEY
    P m0_prog.m0_c_AIRCR_VECTCLRACTIVE P m0_prog.m0_c_AIRCR_SYSRESETREQ
    P m0_prog.m0_c_AIRCR_ENDIANNESS x. P x

x.
    (o'. x = m0_prog.m0_d_ARM_Exception_option o')
    (e. x = m0_prog.m0_d_exception e) (n. x = m0_prog.m0_d_num n)
    (S'. x = m0_prog.m0_d_SHPR3 S') (S'. x = m0_prog.m0_d_SHPR2 S')
    (c. x = m0_prog.m0_d_word32 c) (P0. x = m0_prog.m0_d_PRIMASK P0)
    (I'. x = m0_prog.m0_d_IPR I') (c. x = m0_prog.m0_d_word8 c)
    (M. x = m0_prog.m0_d_Mode M) (C'. x = m0_prog.m0_d_CCR C')
    (c. x = m0_prog.m0_d_word21 c) (c. x = m0_prog.m0_d_word6 c)
    (c. x = m0_prog.m0_d_word13 c) (c. x = m0_prog.m0_d_word16 c)
    b. x = m0_prog.m0_d_bool b

s.
    m0_prog.m0_proj s =
    λa.
      m0_prog.m0_component_CASE a
        (m0_prog.m0_d_ARM_Exception_option (m0.m0_state_pending s))
        (m0_prog.m0_d_exception (m0.m0_state_exception s))
        (m0_prog.m0_d_num (m0.m0_state_count s))
        (m0_prog.m0_d_word32 (m0.m0_state_VTOR s))
        (m0_prog.m0_d_SHPR3 (m0.m0_state_SHPR3 s))
        (m0_prog.m0_d_SHPR2 (m0.m0_state_SHPR2 s))
        (λv0. m0_prog.m0_d_word32 (m0.m0_state_REG s v0))
        (m0_prog.m0_d_PRIMASK (m0.m0_state_PRIMASK s))
        (λv1. m0_prog.m0_d_IPR (m0.m0_state_NVIC_IPR s v1))
        (λv2. m0_prog.m0_d_word8 (m0.m0_state_MEM s v2))
        (λv3. m0_prog.m0_d_bool (m0.m0_state_ExceptionActive s v3))
        (m0_prog.m0_d_Mode (m0.m0_state_CurrentMode s))
        (m0_prog.m0_d_CCR (m0.m0_state_CCR s))
        (m0_prog.m0_d_word21 (m0.PSR_psr'rst (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.PSR_Z (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.PSR_V (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.PSR_T (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.PSR_N (m0.m0_state_PSR s)))
        (m0_prog.m0_d_word6 (m0.PSR_ExceptionNumber (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.PSR_C (m0.m0_state_PSR s)))
        (m0_prog.m0_d_bool (m0.CONTROL_nPRIV (m0.m0_state_CONTROL s)))
        (m0_prog.m0_d_bool
           (m0.CONTROL_control'rst (m0.m0_state_CONTROL s)))
        (m0_prog.m0_d_bool (m0.CONTROL_SPSEL (m0.m0_state_CONTROL s)))
        (m0_prog.m0_d_word13 (m0.AIRCR_aircr'rst (m0.m0_state_AIRCR s)))
        (m0_prog.m0_d_word16 (m0.AIRCR_VECTKEY (m0.m0_state_AIRCR s)))
        (m0_prog.m0_d_bool (m0.AIRCR_VECTCLRACTIVE (m0.m0_state_AIRCR s)))
        (m0_prog.m0_d_bool (m0.AIRCR_SYSRESETREQ (m0.m0_state_AIRCR s)))
        (m0_prog.m0_d_bool (m0.AIRCR_ENDIANNESS (m0.m0_state_AIRCR s)))

x.
    x = m0_prog.m0_c_pending x = m0_prog.m0_c_exception
    x = m0_prog.m0_c_count x = m0_prog.m0_c_VTOR
    x = m0_prog.m0_c_SHPR3 x = m0_prog.m0_c_SHPR2
    (R'. x = m0_prog.m0_c_REG R') x = m0_prog.m0_c_PRIMASK
    (c. x = m0_prog.m0_c_NVIC_IPR c) (c. x = m0_prog.m0_c_MEM c)
    (c. x = m0_prog.m0_c_ExceptionActive c)
    x = m0_prog.m0_c_CurrentMode x = m0_prog.m0_c_CCR
    x = m0_prog.m0_c_PSR_psr'rst x = m0_prog.m0_c_PSR_Z
    x = m0_prog.m0_c_PSR_V x = m0_prog.m0_c_PSR_T
    x = m0_prog.m0_c_PSR_N x = m0_prog.m0_c_PSR_ExceptionNumber
    x = m0_prog.m0_c_PSR_C x = m0_prog.m0_c_CONTROL_nPRIV
    x = m0_prog.m0_c_CONTROL_control'rst x = m0_prog.m0_c_CONTROL_SPSEL
    x = m0_prog.m0_c_AIRCR_aircr'rst x = m0_prog.m0_c_AIRCR_VECTKEY
    x = m0_prog.m0_c_AIRCR_VECTCLRACTIVE
    x = m0_prog.m0_c_AIRCR_SYSRESETREQ x = m0_prog.m0_c_AIRCR_ENDIANNESS

m0_prog.m0_instr (a, Data.Sum.left opc16) =
  pred_set.INSERT
    (m0_prog.m0_c_MEM a, m0_prog.m0_d_word8 (words.word_extract 7 0 opc16))
    (pred_set.INSERT
       (m0_prog.m0_c_MEM (words.word_add a (words.n2w 1)),
        m0_prog.m0_d_word8
          (words.word_extract 15 (arithmetic.BIT2 3) opc16))
       pred_set.EMPTY)
  m0_prog.m0_instr (a, Data.Sum.right opc32) =
  pred_set.INSERT
    (m0_prog.m0_c_MEM a,
     m0_prog.m0_d_word8
       (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
          (arithmetic.BIT2 7) opc32))
    (pred_set.INSERT
       (m0_prog.m0_c_MEM (words.word_add a (words.n2w 1)),
        m0_prog.m0_d_word8
          (words.word_extract 31
             (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) opc32))
       (pred_set.INSERT
          (m0_prog.m0_c_MEM
             (words.word_add a (words.n2w (arithmetic.BIT2 0))),
           m0_prog.m0_d_word8 (words.word_extract 7 0 opc32))
          (pred_set.INSERT
             (m0_prog.m0_c_MEM (words.word_add a (words.n2w 3)),
              m0_prog.m0_d_word8
                (words.word_extract 15 (arithmetic.BIT2 3) opc32))
             pred_set.EMPTY)))

m0_prog.m0_instr =
  relation.WFREC (select R'. Relation.wellFounded R')
    (λm0_instr a'.
       pair.pair_CASE a'
         (λa v1.
            sum.sum_CASE v1
              (λopc16.
                 id
                   (pred_set.INSERT
                      (m0_prog.m0_c_MEM a,
                       m0_prog.m0_d_word8 (words.word_extract 7 0 opc16))
                      (pred_set.INSERT
                         (m0_prog.m0_c_MEM
                            (words.word_add a (words.n2w 1)),
                          m0_prog.m0_d_word8
                            (words.word_extract 15 (arithmetic.BIT2 3)
                               opc16)) pred_set.EMPTY)))
              (λopc32.
                 id
                   (pred_set.INSERT
                      (m0_prog.m0_c_MEM a,
                       m0_prog.m0_d_word8
                         (words.word_extract
                            (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                            (arithmetic.BIT2 7) opc32))
                      (pred_set.INSERT
                         (m0_prog.m0_c_MEM
                            (words.word_add a (words.n2w 1)),
                          m0_prog.m0_d_word8
                            (words.word_extract 31
                               (arithmetic.BIT2
                                  (bit1 (bit1 (arithmetic.BIT2 0))))
                               opc32))
                         (pred_set.INSERT
                            (m0_prog.m0_c_MEM
                               (words.word_add a
                                  (words.n2w (arithmetic.BIT2 0))),
                             m0_prog.m0_d_word8
                               (words.word_extract 7 0 opc32))
                            (pred_set.INSERT
                               (m0_prog.m0_c_MEM
                                  (words.word_add a (words.n2w 3)),
                                m0_prog.m0_d_word8
                                  (words.word_extract 15
                                     (arithmetic.BIT2 3) opc32))
                               pred_set.EMPTY)))))))

m0_prog.m0_component_size m0_prog.m0_c_pending = 0
  m0_prog.m0_component_size m0_prog.m0_c_exception = 0
  m0_prog.m0_component_size m0_prog.m0_c_count = 0
  m0_prog.m0_component_size m0_prog.m0_c_VTOR = 0
  m0_prog.m0_component_size m0_prog.m0_c_SHPR3 = 0
  m0_prog.m0_component_size m0_prog.m0_c_SHPR2 = 0
  (a.
     m0_prog.m0_component_size (m0_prog.m0_c_REG a) =
     1 + m0.RName_size a)
  m0_prog.m0_component_size m0_prog.m0_c_PRIMASK = 0
  (a. m0_prog.m0_component_size (m0_prog.m0_c_NVIC_IPR a) = 1)
  (a. m0_prog.m0_component_size (m0_prog.m0_c_MEM a) = 1)
  (a. m0_prog.m0_component_size (m0_prog.m0_c_ExceptionActive a) = 1)
  m0_prog.m0_component_size m0_prog.m0_c_CurrentMode = 0
  m0_prog.m0_component_size m0_prog.m0_c_CCR = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_psr'rst = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_Z = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_V = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_T = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_N = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_ExceptionNumber = 0
  m0_prog.m0_component_size m0_prog.m0_c_PSR_C = 0
  m0_prog.m0_component_size m0_prog.m0_c_CONTROL_nPRIV = 0
  m0_prog.m0_component_size m0_prog.m0_c_CONTROL_control'rst = 0
  m0_prog.m0_component_size m0_prog.m0_c_CONTROL_SPSEL = 0
  m0_prog.m0_component_size m0_prog.m0_c_AIRCR_aircr'rst = 0
  m0_prog.m0_component_size m0_prog.m0_c_AIRCR_VECTKEY = 0
  m0_prog.m0_component_size m0_prog.m0_c_AIRCR_VECTCLRACTIVE = 0
  m0_prog.m0_component_size m0_prog.m0_c_AIRCR_SYSRESETREQ = 0
  m0_prog.m0_component_size m0_prog.m0_c_AIRCR_ENDIANNESS = 0

f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
    fn.
      (a. fn (m0_prog.m0_d_ARM_Exception_option a) = f0 a)
      (a. fn (m0_prog.m0_d_exception a) = f1 a)
      (a. fn (m0_prog.m0_d_num a) = f2 a)
      (a. fn (m0_prog.m0_d_SHPR3 a) = f3 a)
      (a. fn (m0_prog.m0_d_SHPR2 a) = f4 a)
      (a. fn (m0_prog.m0_d_word32 a) = f5 a)
      (a. fn (m0_prog.m0_d_PRIMASK a) = f6 a)
      (a. fn (m0_prog.m0_d_IPR a) = f7 a)
      (a. fn (m0_prog.m0_d_word8 a) = f8 a)
      (a. fn (m0_prog.m0_d_Mode a) = f9 a)
      (a. fn (m0_prog.m0_d_CCR a) = f10 a)
      (a. fn (m0_prog.m0_d_word21 a) = f11 a)
      (a. fn (m0_prog.m0_d_word6 a) = f12 a)
      (a. fn (m0_prog.m0_d_word13 a) = f13 a)
      (a. fn (m0_prog.m0_d_word16 a) = f14 a)
      a. fn (m0_prog.m0_d_bool a) = f15 a

(a.
     m0_prog.m0_data_size (m0_prog.m0_d_ARM_Exception_option a) =
     1 + basicSize.option_size m0.ARM_Exception_size a)
  (a.
     m0_prog.m0_data_size (m0_prog.m0_d_exception a) =
     1 + m0.exception_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_num a) = 1 + a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_SHPR3 a) = 1 + m0.SHPR3_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_SHPR2 a) = 1 + m0.SHPR2_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word32 a) = 1)
  (a.
     m0_prog.m0_data_size (m0_prog.m0_d_PRIMASK a) =
     1 + m0.PRIMASK_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_IPR a) = 1 + m0.IPR_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word8 a) = 1)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_Mode a) = 1 + m0.Mode_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_CCR a) = 1 + m0.CCR_size a)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word21 a) = 1)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word6 a) = 1)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word13 a) = 1)
  (a. m0_prog.m0_data_size (m0_prog.m0_d_word16 a) = 1)
  a.
    m0_prog.m0_data_size (m0_prog.m0_d_bool a) = 1 + basicSize.bool_size a

a w c p q.
    prog.SPEC m0_prog.M0_MODEL
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR p
                  (m0_prog.m0_MEM a (words.word_extract 7 0 w)))
               (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (m0_prog.m0_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w))) c
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR q
                  (m0_prog.m0_MEM a (words.word_extract 7 0 w)))
               (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (m0_prog.m0_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w)))
    prog.SPEC m0_prog.M0_MODEL
      (set_sep.STAR
         (set_sep.cond
            (pred_set.DISJOINT
               (m0_prog.m0_instr (a, m0_prog.data_to_thumb2 w))
               (pred_set.BIGUNION (pred_set.IMAGE m0_prog.m0_instr c)))) p)
      (pred_set.INSERT (a, m0_prog.data_to_thumb2 w) c) q

a w c p q.
    temporal_state.TEMPORAL_NEXT m0_prog.M0_MODEL
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR p
                  (m0_prog.m0_MEM a (words.word_extract 7 0 w)))
               (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (m0_prog.m0_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w))) c
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR q
                  (m0_prog.m0_MEM a (words.word_extract 7 0 w)))
               (m0_prog.m0_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (m0_prog.m0_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (m0_prog.m0_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w)))
    temporal_state.TEMPORAL_NEXT m0_prog.M0_MODEL
      (set_sep.STAR
         (set_sep.cond
            (pred_set.DISJOINT
               (m0_prog.m0_instr (a, m0_prog.data_to_thumb2 w))
               (pred_set.BIGUNION (pred_set.IMAGE m0_prog.m0_instr c)))) p)
      (pred_set.INSERT (a, m0_prog.data_to_thumb2 w) c) q

f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19
    f20 f21 f22 f23 f24 f25 f26 f27.
    fn.
      fn m0_prog.m0_c_pending = f0 fn m0_prog.m0_c_exception = f1
      fn m0_prog.m0_c_count = f2 fn m0_prog.m0_c_VTOR = f3
      fn m0_prog.m0_c_SHPR3 = f4 fn m0_prog.m0_c_SHPR2 = f5
      (a. fn (m0_prog.m0_c_REG a) = f6 a) fn m0_prog.m0_c_PRIMASK = f7
      (a. fn (m0_prog.m0_c_NVIC_IPR a) = f8 a)
      (a. fn (m0_prog.m0_c_MEM a) = f9 a)
      (a. fn (m0_prog.m0_c_ExceptionActive a) = f10 a)
      fn m0_prog.m0_c_CurrentMode = f11 fn m0_prog.m0_c_CCR = f12
      fn m0_prog.m0_c_PSR_psr'rst = f13 fn m0_prog.m0_c_PSR_Z = f14
      fn m0_prog.m0_c_PSR_V = f15 fn m0_prog.m0_c_PSR_T = f16
      fn m0_prog.m0_c_PSR_N = f17
      fn m0_prog.m0_c_PSR_ExceptionNumber = f18
      fn m0_prog.m0_c_PSR_C = f19 fn m0_prog.m0_c_CONTROL_nPRIV = f20
      fn m0_prog.m0_c_CONTROL_control'rst = f21
      fn m0_prog.m0_c_CONTROL_SPSEL = f22
      fn m0_prog.m0_c_AIRCR_aircr'rst = f23
      fn m0_prog.m0_c_AIRCR_VECTKEY = f24
      fn m0_prog.m0_c_AIRCR_VECTCLRACTIVE = f25
      fn m0_prog.m0_c_AIRCR_SYSRESETREQ = f26
      fn m0_prog.m0_c_AIRCR_ENDIANNESS = f27

(a a'.
     m0_prog.m0_d_ARM_Exception_option a =
     m0_prog.m0_d_ARM_Exception_option a' a = a')
  (a a'. m0_prog.m0_d_exception a = m0_prog.m0_d_exception a' a = a')
  (a a'. m0_prog.m0_d_num a = m0_prog.m0_d_num a' a = a')
  (a a'. m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_SHPR3 a' a = a')
  (a a'. m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_SHPR2 a' a = a')
  (a a'. m0_prog.m0_d_word32 a = m0_prog.m0_d_word32 a' a = a')
  (a a'. m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_PRIMASK a' a = a')
  (a a'. m0_prog.m0_d_IPR a = m0_prog.m0_d_IPR a' a = a')
  (a a'. m0_prog.m0_d_word8 a = m0_prog.m0_d_word8 a' a = a')
  (a a'. m0_prog.m0_d_Mode a = m0_prog.m0_d_Mode a' a = a')
  (a a'. m0_prog.m0_d_CCR a = m0_prog.m0_d_CCR a' a = a')
  (a a'. m0_prog.m0_d_word21 a = m0_prog.m0_d_word21 a' a = a')
  (a a'. m0_prog.m0_d_word6 a = m0_prog.m0_d_word6 a' a = a')
  (a a'. m0_prog.m0_d_word13 a = m0_prog.m0_d_word13 a' a = a')
  (a a'. m0_prog.m0_d_word16 a = m0_prog.m0_d_word16 a' a = a')
  a a'. m0_prog.m0_d_bool a = m0_prog.m0_d_bool a' a a'

M M' f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
    M = M' (a. M' = m0_prog.m0_d_ARM_Exception_option a f a = f' a)
    (a. M' = m0_prog.m0_d_exception a f1 a = f1' a)
    (a. M' = m0_prog.m0_d_num a f2 a = f2' a)
    (a. M' = m0_prog.m0_d_SHPR3 a f3 a = f3' a)
    (a. M' = m0_prog.m0_d_SHPR2 a f4 a = f4' a)
    (a. M' = m0_prog.m0_d_word32 a f5 a = f5' a)
    (a. M' = m0_prog.m0_d_PRIMASK a f6 a = f6' a)
    (a. M' = m0_prog.m0_d_IPR a f7 a = f7' a)
    (a. M' = m0_prog.m0_d_word8 a f8 a = f8' a)
    (a. M' = m0_prog.m0_d_Mode a f9 a = f9' a)
    (a. M' = m0_prog.m0_d_CCR a f10 a = f10' a)
    (a. M' = m0_prog.m0_d_word21 a f11 a = f11' a)
    (a. M' = m0_prog.m0_d_word6 a f12 a = f12' a)
    (a. M' = m0_prog.m0_d_word13 a f13 a = f13' a)
    (a. M' = m0_prog.m0_d_word16 a f14 a = f14' a)
    (a. M' = m0_prog.m0_d_bool a f15 a = f15' a)
    m0_prog.m0_data_CASE M f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14
      f15 =
    m0_prog.m0_data_CASE M' f' f1' f2' f3' f4' f5' f6' f7' f8' f9' f10'
      f11' f12' f13' f14' f15'

M M' v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
    v17 v18 v19 v20 v21 v22 v23.
    M = M' (M' = m0_prog.m0_c_pending v = v')
    (M' = m0_prog.m0_c_exception v1 = v1')
    (M' = m0_prog.m0_c_count v2 = v2')
    (M' = m0_prog.m0_c_VTOR v3 = v3')
    (M' = m0_prog.m0_c_SHPR3 v4 = v4')
    (M' = m0_prog.m0_c_SHPR2 v5 = v5')
    (a. M' = m0_prog.m0_c_REG a f a = f' a)
    (M' = m0_prog.m0_c_PRIMASK v6 = v6')
    (a. M' = m0_prog.m0_c_NVIC_IPR a f1 a = f1' a)
    (a. M' = m0_prog.m0_c_MEM a f2 a = f2' a)
    (a. M' = m0_prog.m0_c_ExceptionActive a f3 a = f3' a)
    (M' = m0_prog.m0_c_CurrentMode v7 = v7')
    (M' = m0_prog.m0_c_CCR v8 = v8')
    (M' = m0_prog.m0_c_PSR_psr'rst v9 = v9')
    (M' = m0_prog.m0_c_PSR_Z v10 = v10')
    (M' = m0_prog.m0_c_PSR_V v11 = v11')
    (M' = m0_prog.m0_c_PSR_T v12 = v12')
    (M' = m0_prog.m0_c_PSR_N v13 = v13')
    (M' = m0_prog.m0_c_PSR_ExceptionNumber v14 = v14')
    (M' = m0_prog.m0_c_PSR_C v15 = v15')
    (M' = m0_prog.m0_c_CONTROL_nPRIV v16 = v16')
    (M' = m0_prog.m0_c_CONTROL_control'rst v17 = v17')
    (M' = m0_prog.m0_c_CONTROL_SPSEL v18 = v18')
    (M' = m0_prog.m0_c_AIRCR_aircr'rst v19 = v19')
    (M' = m0_prog.m0_c_AIRCR_VECTKEY v20 = v20')
    (M' = m0_prog.m0_c_AIRCR_VECTCLRACTIVE v21 = v21')
    (M' = m0_prog.m0_c_AIRCR_SYSRESETREQ v22 = v22')
    (M' = m0_prog.m0_c_AIRCR_ENDIANNESS v23 = v23')
    m0_prog.m0_component_CASE M v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10
      v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 =
    m0_prog.m0_component_CASE M' v' v1' v2' v3' v4' v5' f' v6' f1' f2' f3'
      v7' v8' v9' v10' v11' v12' v13' v14' v15' v16' v17' v18' v19' v20'
      v21' v22' v23'

(a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_ARM_Exception_option a) f f1 f2 f3
       f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 = f a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_exception a) f f1 f2 f3 f4 f5 f6 f7
       f8 f9 f10 f11 f12 f13 f14 f15 = f1 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_num a) f f1 f2 f3 f4 f5 f6 f7 f8 f9
       f10 f11 f12 f13 f14 f15 = f2 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_SHPR3 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f3 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_SHPR2 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f4 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word32 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f5 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_PRIMASK a) f f1 f2 f3 f4 f5 f6 f7
       f8 f9 f10 f11 f12 f13 f14 f15 = f6 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_IPR a) f f1 f2 f3 f4 f5 f6 f7 f8 f9
       f10 f11 f12 f13 f14 f15 = f7 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word8 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f8 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_Mode a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f9 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_CCR a) f f1 f2 f3 f4 f5 f6 f7 f8 f9
       f10 f11 f12 f13 f14 f15 = f10 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word21 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f11 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word6 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f12 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word13 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f13 a)
  (a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word16 a) f f1 f2 f3 f4 f5 f6 f7 f8
       f9 f10 f11 f12 f13 f14 f15 = f14 a)
  a f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15.
    m0_prog.m0_data_CASE (m0_prog.m0_d_bool a) f f1 f2 f3 f4 f5 f6 f7 f8 f9
      f10 f11 f12 f13 f14 f15 = f15 a

(a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_exception a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_num a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_SHPR3 a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_SHPR2 a'))
  (a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word32 a'))
  (a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_CCR a'))
  (a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word6 a'))
  (a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word13 a'))
  (a' a.
     ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_ARM_Exception_option a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_num a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_SHPR3 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_SHPR2 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word32 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_exception a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_SHPR3 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_SHPR2 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word32 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_num a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_SHPR2 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word32 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR3 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word32 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_SHPR2 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_PRIMASK a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_word32 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_IPR a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_PRIMASK a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_word8 a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_IPR a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_Mode a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_word8 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_CCR a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_Mode a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_CCR a = m0_prog.m0_d_word21 a'))
  (a' a. ¬(m0_prog.m0_d_CCR a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_CCR a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_CCR a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_CCR a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_word21 a = m0_prog.m0_d_word6 a'))
  (a' a. ¬(m0_prog.m0_d_word21 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_word21 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_word21 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_word6 a = m0_prog.m0_d_word13 a'))
  (a' a. ¬(m0_prog.m0_d_word6 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_word6 a = m0_prog.m0_d_bool a'))
  (a' a. ¬(m0_prog.m0_d_word13 a = m0_prog.m0_d_word16 a'))
  (a' a. ¬(m0_prog.m0_d_word13 a = m0_prog.m0_d_bool a'))
  a' a. ¬(m0_prog.m0_d_word16 a = m0_prog.m0_d_bool a')

(v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_pending v v1 v2 v3 v4 v5 f v6
       f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = v)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_exception v v1 v2 v3 v4 v5 f v6
       f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = v1)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_count v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v2)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_VTOR v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v3)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_SHPR3 v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v4)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_SHPR2 v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v5)
  (a v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
     v17 v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE (m0_prog.m0_c_REG a) v v1 v2 v3 v4 v5 f v6
       f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = f a)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PRIMASK v v1 v2 v3 v4 v5 f v6
       f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = v6)
  (a v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
     v17 v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE (m0_prog.m0_c_NVIC_IPR a) v v1 v2 v3 v4 v5 f
       v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = f1 a)
  (a v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
     v17 v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE (m0_prog.m0_c_MEM a) v v1 v2 v3 v4 v5 f v6
       f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = f2 a)
  (a v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
     v17 v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE (m0_prog.m0_c_ExceptionActive a) v v1 v2 v3
       v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = f3 a)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_CurrentMode v v1 v2 v3 v4 v5 f
       v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = v7)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_CCR v v1 v2 v3 v4 v5 f v6 f1 f2
       f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v8)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_psr'rst v v1 v2 v3 v4 v5 f
       v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
       v22 v23 = v9)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_Z v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v10)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_V v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v11)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_T v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v12)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_N v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v13)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_ExceptionNumber v v1 v2 v3
       v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = v14)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_PSR_C v v1 v2 v3 v4 v5 f v6 f1
       f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
       v23 = v15)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_CONTROL_nPRIV v v1 v2 v3 v4 v5
       f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20
       v21 v22 v23 = v16)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_CONTROL_control'rst v v1 v2 v3
       v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = v17)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_CONTROL_SPSEL v v1 v2 v3 v4 v5
       f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20
       v21 v22 v23 = v18)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_AIRCR_aircr'rst v v1 v2 v3 v4
       v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = v19)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_AIRCR_VECTKEY v v1 v2 v3 v4 v5
       f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20
       v21 v22 v23 = v20)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_AIRCR_VECTCLRACTIVE v v1 v2 v3
       v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = v21)
  (v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
     v18 v19 v20 v21 v22 v23.
     m0_prog.m0_component_CASE m0_prog.m0_c_AIRCR_SYSRESETREQ v v1 v2 v3 v4
       v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19
       v20 v21 v22 v23 = v22)
  v v1 v2 v3 v4 v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
    v18 v19 v20 v21 v22 v23.
    m0_prog.m0_component_CASE m0_prog.m0_c_AIRCR_ENDIANNESS v v1 v2 v3 v4
      v5 f v6 f1 f2 f3 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20
      v21 v22 v23 = v23

¬(m0_prog.m0_c_pending = m0_prog.m0_c_exception)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_count)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_VTOR)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_SHPR3)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_SHPR2)
  (a. ¬(m0_prog.m0_c_pending = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_pending = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_pending = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_pending = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_pending = m0_prog.m0_c_AIRCR_ENDIANNESS)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_count)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_VTOR)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_SHPR3)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_SHPR2)
  (a. ¬(m0_prog.m0_c_exception = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_exception = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_exception = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_exception = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_exception = m0_prog.m0_c_AIRCR_ENDIANNESS)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_VTOR)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_SHPR3)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_SHPR2)
  (a. ¬(m0_prog.m0_c_count = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_count = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_count = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_count = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_count = m0_prog.m0_c_AIRCR_ENDIANNESS)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_SHPR3)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_SHPR2)
  (a. ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_VTOR = m0_prog.m0_c_AIRCR_ENDIANNESS)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_SHPR2)
  (a. ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_SHPR3 = m0_prog.m0_c_AIRCR_ENDIANNESS)
  (a. ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_REG a))
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PRIMASK)
  (a. ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_SHPR2 = m0_prog.m0_c_AIRCR_ENDIANNESS)
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PRIMASK))
  (a' a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_NVIC_IPR a'))
  (a' a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_MEM a'))
  (a' a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_ExceptionActive a'))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_CurrentMode))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_CCR))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_psr'rst))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_Z))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_V))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_T))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_N))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_ExceptionNumber))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_PSR_C))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_CONTROL_nPRIV))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_CONTROL_control'rst))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_CONTROL_SPSEL))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_AIRCR_aircr'rst))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_AIRCR_VECTKEY))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_AIRCR_VECTCLRACTIVE))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_AIRCR_SYSRESETREQ))
  (a. ¬(m0_prog.m0_c_REG a = m0_prog.m0_c_AIRCR_ENDIANNESS))
  (a. ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_NVIC_IPR a))
  (a. ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_MEM a))
  (a. ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_ExceptionActive a))
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_CurrentMode)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_CCR)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_psr'rst)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_Z)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_V)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_T)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_N)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_ExceptionNumber)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_PSR_C)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_CONTROL_nPRIV)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_CONTROL_control'rst)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_CONTROL_SPSEL)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_AIRCR_aircr'rst)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_AIRCR_VECTKEY)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_AIRCR_VECTCLRACTIVE)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_AIRCR_SYSRESETREQ)
  ¬(m0_prog.m0_c_PRIMASK = m0_prog.m0_c_AIRCR_ENDIANNESS)
  (a' a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_MEM a'))
  (a' a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_ExceptionActive a'))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_CurrentMode))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_CCR))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_psr'rst))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_Z))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_V))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_T))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_N))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_ExceptionNumber))
  (a. ¬(m0_prog.m0_c_NVIC_IPR a = m0_prog.m0_c_PSR_C))