Package m0-prog: M0 evaluator

Information

Files

• Package tarball m0-prog-1.0.tgz
• Theory source file m0-prog.thy (included in the package tarball)

Defined Type Operators

• HOL4
  • m0_prog
    • m0_prog.m0_component
    • m0_prog.m0_data

Defined Constants

• HOL4
  • m0_prog
    • m0_prog.data_to_thumb2
    • m0_prog.m0_AIRCR_ENDIANNESS
    • m0_prog.m0_AIRCR_SYSRESETREQ
    • m0_prog.m0_AIRCR_VECTCLRACTIVE
    • m0_prog.m0_AIRCR_VECTKEY
    • m0_prog.m0_AIRCR_aircr'rst
    • m0_prog.m0_BE_WORD
    • m0_prog.m0_CCR
    • m0_prog.m0_CONFIG
    • m0_prog.m0_CONTROL_SPSEL
    • m0_prog.m0_CONTROL_control'rst
    • m0_prog.m0_CONTROL_nPRIV
    • m0_prog.m0_CurrentMode
    • m0_prog.m0_ExceptionActive
    • m0_prog.m0_MEM
    • m0_prog.m0_MEMORY
    • m0_prog.m0_NVIC_IPR
    • m0_prog.m0_NZCV
    • m0_prog.m0_PC
    • m0_prog.m0_PRIMASK
    • m0_prog.m0_PSR_C
    • m0_prog.m0_PSR_ExceptionNumber
    • m0_prog.m0_PSR_N
    • m0_prog.m0_PSR_T
    • m0_prog.m0_PSR_V
    • m0_prog.m0_PSR_Z
    • m0_prog.m0_PSR_psr'rst
    • m0_prog.m0_REG
    • m0_prog.m0_REGISTERS
    • m0_prog.m0_SHPR2
    • m0_prog.m0_SHPR3
    • m0_prog.m0_VTOR
    • m0_prog.m0_WORD
    • m0_prog.m0_c_AIRCR_ENDIANNESS
    • m0_prog.m0_c_AIRCR_SYSRESETREQ
    • m0_prog.m0_c_AIRCR_VECTCLRACTIVE
    • m0_prog.m0_c_AIRCR_VECTKEY
    • m0_prog.m0_c_AIRCR_aircr'rst
    • m0_prog.m0_c_CCR
    • m0_prog.m0_c_CONTROL_SPSEL
    • m0_prog.m0_c_CONTROL_control'rst
    • m0_prog.m0_c_CONTROL_nPRIV
    • m0_prog.m0_c_CurrentMode
    • m0_prog.m0_c_ExceptionActive
    • m0_prog.m0_c_MEM
    • m0_prog.m0_c_NVIC_IPR
    • m0_prog.m0_c_PRIMASK
    • m0_prog.m0_c_PSR_C
    • m0_prog.m0_c_PSR_ExceptionNumber
    • m0_prog.m0_c_PSR_N
    • m0_prog.m0_c_PSR_T
    • m0_prog.m0_c_PSR_V
    • m0_prog.m0_c_PSR_Z
    • m0_prog.m0_c_PSR_psr'rst
    • m0_prog.m0_c_REG
    • m0_prog.m0_c_SHPR2
    • m0_prog.m0_c_SHPR3
    • m0_prog.m0_c_VTOR
    • m0_prog.m0_c_count
    • m0_prog.m0_c_exception
    • m0_prog.m0_c_pending
    • m0_prog.m0_component_CASE
    • m0_prog.m0_component_size
    • m0_prog.m0_count
    • m0_prog.m0_d_ARM_Exception_option
    • m0_prog.m0_d_CCR
    • m0_prog.m0_d_IPR
    • m0_prog.m0_d_Mode
    • m0_prog.m0_d_PRIMASK
    • m0_prog.m0_d_SHPR2
    • m0_prog.m0_d_SHPR3
    • m0_prog.m0_d_bool
    • m0_prog.m0_d_exception
    • m0_prog.m0_d_num
    • m0_prog.m0_d_word13
    • m0_prog.m0_d_word16
    • m0_prog.m0_d_word21
    • m0_prog.m0_d_word32
    • m0_prog.m0_d_word6
    • m0_prog.m0_d_word8
    • m0_prog.m0_data_CASE
    • m0_prog.m0_data_size
    • m0_prog.m0_exception
    • m0_prog.m0_instr
    • m0_prog.m0_pending
    • m0_prog.m0_proj
    • m0_prog.M0_MODEL

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 opc₁₆. P (a, Data.Sum.left opc₁₆)) ∧
    (∀a opc₃₂. P (a, Data.Sum.right opc₃₂)) ⇒ ∀v v₁. P (v, v₁)

⊦ prog.SPEC m (set_sep.STAR p₁ (m0_prog.m0_PC pc)) code
    (set_sep.STAR p₂ (m0_prog.m0_REG m0.RName_PC pc')) ⇒
  (alignment.aligned 1 pc ⇒ alignment.aligned 1 pc') ⇒
  prog.SPEC m (set_sep.STAR p₁ (m0_prog.m0_PC pc)) code
    (set_sep.STAR p₂ (m0_prog.m0_PC pc'))

⊦ temporal_state.TEMPORAL_NEXT m (set_sep.STAR p₁ (m0_prog.m0_PC pc)) code
    (set_sep.STAR p₂ (m0_prog.m0_REG m0.RName_PC pc')) ⇒
  (alignment.aligned 1 pc ⇒ alignment.aligned 1 pc') ⇒
  temporal_state.TEMPORAL_NEXT m (set_sep.STAR p₁ (m0_prog.m0_PC pc)) code
    (set_sep.STAR p₂ (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) ∨ (∃P₀. x = m0_prog.m0_d_PRIMASK P₀) ∨
    (∃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))
        (λv₀. m0_prog.m0_d_word32 (m0.m0_state_REG s v₀))
        (m0_prog.m0_d_PRIMASK (m0.m0_state_PRIMASK s))
        (λv₁. m0_prog.m0_d_IPR (m0.m0_state_NVIC_IPR s v₁))
        (λv₂. m0_prog.m0_d_word8 (m0.m0_state_MEM s v₂))
        (λv₃. m0_prog.m0_d_bool (m0.m0_state_ExceptionActive s v₃))
        (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 opc₁₆) =
  pred_set.INSERT
    (m0_prog.m0_c_MEM a, m0_prog.m0_d_word8 (words.word_extract 7 0 opc₁₆))
    (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) opc₁₆))
       pred_set.EMPTY) ∧
  m0_prog.m0_instr (a, Data.Sum.right opc₃₂) =
  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) opc₃₂))
    (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)))) opc₃₂))
       (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 opc₃₂))
          (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) opc₃₂))
             pred_set.EMPTY)))

⊦ m0_prog.m0_instr =
  relation.WFREC (select R'. Relation.wellFounded R')
    (λm0_instr a'.
       pair.pair_CASE a'
         (λa v₁.
            sum.sum_CASE v₁
              (λopc₁₆.
                 id
                   (pred_set.INSERT
                      (m0_prog.m0_c_MEM a,
                       m0_prog.m0_d_word8 (words.word_extract 7 0 opc₁₆))
                      (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)
                               opc₁₆)) pred_set.EMPTY)))
              (λopc₃₂.
                 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) opc₃₂))
                      (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))))
                               opc₃₂))
                         (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 opc₃₂))
                            (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) opc₃₂))
                               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

⊦ ∀f₀ f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
    ∃fn.
      (∀a. fn (m0_prog.m0_d_ARM_Exception_option a) = f₀ a) ∧
      (∀a. fn (m0_prog.m0_d_exception a) = f₁ a) ∧
      (∀a. fn (m0_prog.m0_d_num a) = f₂ a) ∧
      (∀a. fn (m0_prog.m0_d_SHPR3 a) = f₃ a) ∧
      (∀a. fn (m0_prog.m0_d_SHPR2 a) = f₄ a) ∧
      (∀a. fn (m0_prog.m0_d_word32 a) = f₅ a) ∧
      (∀a. fn (m0_prog.m0_d_PRIMASK a) = f₆ a) ∧
      (∀a. fn (m0_prog.m0_d_IPR a) = f₇ a) ∧
      (∀a. fn (m0_prog.m0_d_word8 a) = f₈ a) ∧
      (∀a. fn (m0_prog.m0_d_Mode a) = f₉ a) ∧
      (∀a. fn (m0_prog.m0_d_CCR a) = f₁₀ a) ∧
      (∀a. fn (m0_prog.m0_d_word21 a) = f₁₁ a) ∧
      (∀a. fn (m0_prog.m0_d_word6 a) = f₁₂ a) ∧
      (∀a. fn (m0_prog.m0_d_word13 a) = f₁₃ a) ∧
      (∀a. fn (m0_prog.m0_d_word16 a) = f₁₄ a) ∧
      ∀a. fn (m0_prog.m0_d_bool a) = f₁₅ 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

⊦ ∀f₀ f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ f₁₆ f₁₇ f₁₈ f₁₉
    f₂₀ f₂₁ f₂₂ f₂₃ f₂₄ f₂₅ f₂₆ f₂₇.
    ∃fn.
      fn m0_prog.m0_c_pending = f₀ ∧ fn m0_prog.m0_c_exception = f₁ ∧
      fn m0_prog.m0_c_count = f₂ ∧ fn m0_prog.m0_c_VTOR = f₃ ∧
      fn m0_prog.m0_c_SHPR3 = f₄ ∧ fn m0_prog.m0_c_SHPR2 = f₅ ∧
      (∀a. fn (m0_prog.m0_c_REG a) = f₆ a) ∧ fn m0_prog.m0_c_PRIMASK = f₇ ∧
      (∀a. fn (m0_prog.m0_c_NVIC_IPR a) = f₈ a) ∧
      (∀a. fn (m0_prog.m0_c_MEM a) = f₉ a) ∧
      (∀a. fn (m0_prog.m0_c_ExceptionActive a) = f₁₀ a) ∧
      fn m0_prog.m0_c_CurrentMode = f₁₁ ∧ fn m0_prog.m0_c_CCR = f₁₂ ∧
      fn m0_prog.m0_c_PSR_psr'rst = f₁₃ ∧ fn m0_prog.m0_c_PSR_Z = f₁₄ ∧
      fn m0_prog.m0_c_PSR_V = f₁₅ ∧ fn m0_prog.m0_c_PSR_T = f₁₆ ∧
      fn m0_prog.m0_c_PSR_N = f₁₇ ∧
      fn m0_prog.m0_c_PSR_ExceptionNumber = f₁₈ ∧
      fn m0_prog.m0_c_PSR_C = f₁₉ ∧ fn m0_prog.m0_c_CONTROL_nPRIV = f₂₀ ∧
      fn m0_prog.m0_c_CONTROL_control'rst = f₂₁ ∧
      fn m0_prog.m0_c_CONTROL_SPSEL = f₂₂ ∧
      fn m0_prog.m0_c_AIRCR_aircr'rst = f₂₃ ∧
      fn m0_prog.m0_c_AIRCR_VECTKEY = f₂₄ ∧
      fn m0_prog.m0_c_AIRCR_VECTCLRACTIVE = f₂₅ ∧
      fn m0_prog.m0_c_AIRCR_SYSRESETREQ = f₂₆ ∧
      fn m0_prog.m0_c_AIRCR_ENDIANNESS = f₂₇

⊦ (∀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 f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
    M = M' ∧ (∀a. M' = m0_prog.m0_d_ARM_Exception_option a ⇒ f a = f' a) ∧
    (∀a. M' = m0_prog.m0_d_exception a ⇒ f₁ a = f1' a) ∧
    (∀a. M' = m0_prog.m0_d_num a ⇒ f₂ a = f2' a) ∧
    (∀a. M' = m0_prog.m0_d_SHPR3 a ⇒ f₃ a = f3' a) ∧
    (∀a. M' = m0_prog.m0_d_SHPR2 a ⇒ f₄ a = f4' a) ∧
    (∀a. M' = m0_prog.m0_d_word32 a ⇒ f₅ a = f5' a) ∧
    (∀a. M' = m0_prog.m0_d_PRIMASK a ⇒ f₆ a = f6' a) ∧
    (∀a. M' = m0_prog.m0_d_IPR a ⇒ f₇ a = f7' a) ∧
    (∀a. M' = m0_prog.m0_d_word8 a ⇒ f₈ a = f8' a) ∧
    (∀a. M' = m0_prog.m0_d_Mode a ⇒ f₉ a = f9' a) ∧
    (∀a. M' = m0_prog.m0_d_CCR a ⇒ f₁₀ a = f10' a) ∧
    (∀a. M' = m0_prog.m0_d_word21 a ⇒ f₁₁ a = f11' a) ∧
    (∀a. M' = m0_prog.m0_d_word6 a ⇒ f₁₂ a = f12' a) ∧
    (∀a. M' = m0_prog.m0_d_word13 a ⇒ f₁₃ a = f13' a) ∧
    (∀a. M' = m0_prog.m0_d_word16 a ⇒ f₁₄ a = f14' a) ∧
    (∀a. M' = m0_prog.m0_d_bool a ⇒ f₁₅ a = f15' a) ⇒
    m0_prog.m0_data_CASE M f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄
      f₁₅ =
    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 v₁ v₂ v₃ v₄ v₅ f v₆ f₁ f₂ f₃ v₇ v₈ v₉ v₁₀ v₁₁ v₁₂ v₁₃ v₁₄ v₁₅ v₁₆
    v₁₇ v₁₈ v₁₉ v₂₀ v₂₁ v₂₂ v₂₃.
    M = M' ∧ (M' = m0_prog.m0_c_pending ⇒ v = v') ∧
    (M' = m0_prog.m0_c_exception ⇒ v₁ = v1') ∧
    (M' = m0_prog.m0_c_count ⇒ v₂ = v2') ∧
    (M' = m0_prog.m0_c_VTOR ⇒ v₃ = v3') ∧
    (M' = m0_prog.m0_c_SHPR3 ⇒ v₄ = v4') ∧
    (M' = m0_prog.m0_c_SHPR2 ⇒ v₅ = v5') ∧
    (∀a. M' = m0_prog.m0_c_REG a ⇒ f a = f' a) ∧
    (M' = m0_prog.m0_c_PRIMASK ⇒ v₆ = v6') ∧
    (∀a. M' = m0_prog.m0_c_NVIC_IPR a ⇒ f₁ a = f1' a) ∧
    (∀a. M' = m0_prog.m0_c_MEM a ⇒ f₂ a = f2' a) ∧
    (∀a. M' = m0_prog.m0_c_ExceptionActive a ⇒ f₃ a = f3' a) ∧
    (M' = m0_prog.m0_c_CurrentMode ⇒ v₇ = v7') ∧
    (M' = m0_prog.m0_c_CCR ⇒ v₈ = v8') ∧
    (M' = m0_prog.m0_c_PSR_psr'rst ⇒ v₉ = v9') ∧
    (M' = m0_prog.m0_c_PSR_Z ⇒ v₁₀ = v10') ∧
    (M' = m0_prog.m0_c_PSR_V ⇒ v₁₁ = v11') ∧
    (M' = m0_prog.m0_c_PSR_T ⇒ v₁₂ = v12') ∧
    (M' = m0_prog.m0_c_PSR_N ⇒ v₁₃ = v13') ∧
    (M' = m0_prog.m0_c_PSR_ExceptionNumber ⇒ v₁₄ = v14') ∧
    (M' = m0_prog.m0_c_PSR_C ⇒ v₁₅ = v15') ∧
    (M' = m0_prog.m0_c_CONTROL_nPRIV ⇒ v₁₆ = v16') ∧
    (M' = m0_prog.m0_c_CONTROL_control'rst ⇒ v₁₇ = v17') ∧
    (M' = m0_prog.m0_c_CONTROL_SPSEL ⇒ v₁₈ = v18') ∧
    (M' = m0_prog.m0_c_AIRCR_aircr'rst ⇒ v₁₉ = v19') ∧
    (M' = m0_prog.m0_c_AIRCR_VECTKEY ⇒ v₂₀ = v20') ∧
    (M' = m0_prog.m0_c_AIRCR_VECTCLRACTIVE ⇒ v₂₁ = v21') ∧
    (M' = m0_prog.m0_c_AIRCR_SYSRESETREQ ⇒ v₂₂ = v22') ∧
    (M' = m0_prog.m0_c_AIRCR_ENDIANNESS ⇒ v₂₃ = v23') ⇒
    m0_prog.m0_component_CASE M v v₁ v₂ v₃ v₄ v₅ f v₆ f₁ f₂ f₃ v₇ v₈ v₉ v₁₀
      v₁₁ v₁₂ v₁₃ v₁₄ v₁₅ v₁₆ v₁₇ v₁₈ v₁₉ v₂₀ v₂₁ v₂₂ v₂₃ =
    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 f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_ARM_Exception_option a) f f₁ f₂ f₃
       f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_exception a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇
       f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_num a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉
       f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₂ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_SHPR3 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₃ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_SHPR2 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₄ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word32 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₅ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_PRIMASK a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇
       f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₆ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_IPR a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉
       f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₇ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word8 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₈ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_Mode a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₉ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_CCR a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉
       f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₀ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word21 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₁ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word6 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₂ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word13 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₃ a) ∧
  (∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
     m0_prog.m0_data_CASE (m0_prog.m0_d_word16 a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈
       f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₄ a) ∧
  ∀a f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅.
    m0_prog.m0_data_CASE (m0_prog.m0_d_bool a) f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉
      f₁₀ f₁₁ f₁₂ f₁₃ f₁₄ f₁₅ = f₁₅ a