Package arm-prog: ARM evaluator

Information

Files

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

Defined Type Operators

• HOL4
  • arm_prog
    • arm_prog.arm_component
    • arm_prog.arm_data

Defined Constants

• HOL4
  • arm_prog
    • arm_prog.aS
    • arm_prog.arm_Architecture
    • arm_prog.arm_BE_WORD
    • arm_prog.arm_BE_WORD_MEMORY
    • arm_prog.arm_CONFIG
    • arm_prog.arm_CP14
    • arm_prog.arm_CP15
    • arm_prog.arm_CPSR_A
    • arm_prog.arm_CPSR_C
    • arm_prog.arm_CPSR_E
    • arm_prog.arm_CPSR_F
    • arm_prog.arm_CPSR_GE
    • arm_prog.arm_CPSR_I
    • arm_prog.arm_CPSR_IT
    • arm_prog.arm_CPSR_J
    • arm_prog.arm_CPSR_M
    • arm_prog.arm_CPSR_N
    • arm_prog.arm_CPSR_Q
    • arm_prog.arm_CPSR_T
    • arm_prog.arm_CPSR_V
    • arm_prog.arm_CPSR_Z
    • arm_prog.arm_CPSR_psr'rst
    • arm_prog.arm_ELR_hyp
    • arm_prog.arm_Extensions
    • arm_prog.arm_FP_FPSCR_AHP
    • arm_prog.arm_FP_FPSCR_C
    • arm_prog.arm_FP_FPSCR_DN
    • arm_prog.arm_FP_FPSCR_DZC
    • arm_prog.arm_FP_FPSCR_DZE
    • arm_prog.arm_FP_FPSCR_FZ
    • arm_prog.arm_FP_FPSCR_IDC
    • arm_prog.arm_FP_FPSCR_IDE
    • arm_prog.arm_FP_FPSCR_IOC
    • arm_prog.arm_FP_FPSCR_IOE
    • arm_prog.arm_FP_FPSCR_IXC
    • arm_prog.arm_FP_FPSCR_IXE
    • arm_prog.arm_FP_FPSCR_N
    • arm_prog.arm_FP_FPSCR_OFC
    • arm_prog.arm_FP_FPSCR_OFE
    • arm_prog.arm_FP_FPSCR_QC
    • arm_prog.arm_FP_FPSCR_RMode
    • arm_prog.arm_FP_FPSCR_UFC
    • arm_prog.arm_FP_FPSCR_UFE
    • arm_prog.arm_FP_FPSCR_V
    • arm_prog.arm_FP_FPSCR_Z
    • arm_prog.arm_FP_FPSCR_fpscr'rst
    • arm_prog.arm_FP_REG
    • arm_prog.arm_FP_REGISTERS
    • arm_prog.arm_MEM
    • arm_prog.arm_MEMORY
    • arm_prog.arm_PC
    • arm_prog.arm_REG
    • arm_prog.arm_REGISTERS
    • arm_prog.arm_SPSR_abt
    • arm_prog.arm_SPSR_fiq
    • arm_prog.arm_SPSR_hyp
    • arm_prog.arm_SPSR_irq
    • arm_prog.arm_SPSR_mon
    • arm_prog.arm_SPSR_svc
    • arm_prog.arm_SPSR_und
    • arm_prog.arm_VFPExtension
    • arm_prog.arm_WORD
    • arm_prog.arm_WORD_MEMORY
    • arm_prog.arm_c_Architecture
    • arm_prog.arm_c_CP14
    • arm_prog.arm_c_CP15
    • arm_prog.arm_c_CPSR_A
    • arm_prog.arm_c_CPSR_C
    • arm_prog.arm_c_CPSR_E
    • arm_prog.arm_c_CPSR_F
    • arm_prog.arm_c_CPSR_GE
    • arm_prog.arm_c_CPSR_I
    • arm_prog.arm_c_CPSR_IT
    • arm_prog.arm_c_CPSR_J
    • arm_prog.arm_c_CPSR_M
    • arm_prog.arm_c_CPSR_N
    • arm_prog.arm_c_CPSR_Q
    • arm_prog.arm_c_CPSR_T
    • arm_prog.arm_c_CPSR_V
    • arm_prog.arm_c_CPSR_Z
    • arm_prog.arm_c_CPSR_psr'rst
    • arm_prog.arm_c_ELR_hyp
    • arm_prog.arm_c_Extensions
    • arm_prog.arm_c_FP_FPSCR_AHP
    • arm_prog.arm_c_FP_FPSCR_C
    • arm_prog.arm_c_FP_FPSCR_DN
    • arm_prog.arm_c_FP_FPSCR_DZC
    • arm_prog.arm_c_FP_FPSCR_DZE
    • arm_prog.arm_c_FP_FPSCR_FZ
    • arm_prog.arm_c_FP_FPSCR_IDC
    • arm_prog.arm_c_FP_FPSCR_IDE
    • arm_prog.arm_c_FP_FPSCR_IOC
    • arm_prog.arm_c_FP_FPSCR_IOE
    • arm_prog.arm_c_FP_FPSCR_IXC
    • arm_prog.arm_c_FP_FPSCR_IXE
    • arm_prog.arm_c_FP_FPSCR_N
    • arm_prog.arm_c_FP_FPSCR_OFC
    • arm_prog.arm_c_FP_FPSCR_OFE
    • arm_prog.arm_c_FP_FPSCR_QC
    • arm_prog.arm_c_FP_FPSCR_RMode
    • arm_prog.arm_c_FP_FPSCR_UFC
    • arm_prog.arm_c_FP_FPSCR_UFE
    • arm_prog.arm_c_FP_FPSCR_V
    • arm_prog.arm_c_FP_FPSCR_Z
    • arm_prog.arm_c_FP_FPSCR_fpscr'rst
    • arm_prog.arm_c_FP_REG
    • arm_prog.arm_c_MEM
    • arm_prog.arm_c_REG
    • arm_prog.arm_c_SPSR_abt
    • arm_prog.arm_c_SPSR_fiq
    • arm_prog.arm_c_SPSR_hyp
    • arm_prog.arm_c_SPSR_irq
    • arm_prog.arm_c_SPSR_mon
    • arm_prog.arm_c_SPSR_svc
    • arm_prog.arm_c_SPSR_und
    • arm_prog.arm_c_VFPExtension
    • arm_prog.arm_c_exception
    • arm_prog.arm_component_CASE
    • arm_prog.arm_component_size
    • arm_prog.arm_d_Architecture
    • arm_prog.arm_d_CP14
    • arm_prog.arm_d_CP15
    • arm_prog.arm_d_PSR
    • arm_prog.arm_d_VFPExtension
    • arm_prog.arm_d_bool
    • arm_prog.arm_d_exception
    • arm_prog.arm_d_word10
    • arm_prog.arm_d_word2
    • arm_prog.arm_d_word32
    • arm_prog.arm_d_word4
    • arm_prog.arm_d_word5
    • arm_prog.arm_d_word64
    • arm_prog.arm_d_word8
    • arm_prog.arm_data_CASE
    • arm_prog.arm_data_size
    • arm_prog.arm_exception
    • arm_prog.arm_instr
    • arm_prog.arm_proj
    • arm_prog.ARM_MODEL

Theorems

⊦ ∀d.
    arm_prog.arm_CPSR_A d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_A, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_C d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_C, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_E d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_E, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_F d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_F, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_I d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_I, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_J d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_J, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_N d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_N, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_Q d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_Q, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_T d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_T, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_V d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_V, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_Z d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_Z, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_AHP d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_AHP, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_C d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_C, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_DN d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_DN, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_DZC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_DZC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_DZE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_DZE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_FZ d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_FZ, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IDC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IDC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IDE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IDE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IOC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IOC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IOE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IOE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IXC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IXC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_IXE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_IXE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_N d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_N, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_OFC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_OFC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_OFE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_OFE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_QC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_QC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_UFC d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_UFC, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_UFE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_UFE, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_V d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_V, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_Z d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_FPSCR_Z, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_exception d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_exception, arm_prog.arm_d_exception d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_Architecture d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_Architecture, arm_prog.arm_d_Architecture d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CP14 d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CP14, arm_prog.arm_d_CP14 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CP15 d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CP15, arm_prog.arm_d_CP15 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_abt d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_abt, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_fiq d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_fiq, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_hyp d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_hyp, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_irq d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_irq, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_mon d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_mon, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_svc d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_svc, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_SPSR_und d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_SPSR_und, arm_prog.arm_d_PSR d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_VFPExtension d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_VFPExtension, arm_prog.arm_d_VFPExtension d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_RMode d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_FP_FPSCR_RMode, arm_prog.arm_d_word2 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_GE d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_GE, arm_prog.arm_d_word4 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_psr'rst d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_CPSR_psr'rst, arm_prog.arm_d_word4 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_M d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_M, arm_prog.arm_d_word5 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_CPSR_IT d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_CPSR_IT, arm_prog.arm_d_word8 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_FP_FPSCR_fpscr'rst d =
    pred_set.INSERT
      (pred_set.INSERT
         (arm_prog.arm_c_FP_FPSCR_fpscr'rst, arm_prog.arm_d_word10 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀d.
    arm_prog.arm_ELR_hyp d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_ELR_hyp, arm_prog.arm_d_word32 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀pc.
    arm_prog.arm_PC pc =
    set_sep.STAR (arm_prog.arm_REG arm.RName_PC pc)
      (set_sep.cond (alignment.aligned (arithmetic.BIT2 0) pc))

⊦ set_sep.SEP_HIDE arm_prog.aS =
  set_sep.STAR
    (set_sep.STAR
       (set_sep.STAR (set_sep.SEP_HIDE arm_prog.arm_CPSR_N)
          (set_sep.SEP_HIDE arm_prog.arm_CPSR_Z))
       (set_sep.SEP_HIDE arm_prog.arm_CPSR_C))
    (set_sep.SEP_HIDE arm_prog.arm_CPSR_V)

⊦ arm_prog.ARM_MODEL =
  (state.STATE arm_prog.arm_proj, state.NEXT_REL (=) arm_step.NextStateARM,
   arm_prog.arm_instr, (=), const ⊥)

⊦ ∀c d.
    arm_prog.arm_Extensions c d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_Extensions c, arm_prog.arm_d_bool d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀c d.
    arm_prog.arm_REG c d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_REG c, arm_prog.arm_d_word32 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀c d.
    arm_prog.arm_FP_REG c d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_FP_REG c, arm_prog.arm_d_word64 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀c d.
    arm_prog.arm_MEM c d =
    pred_set.INSERT
      (pred_set.INSERT (arm_prog.arm_c_MEM c, arm_prog.arm_d_word8 d)
         pred_set.EMPTY) pred_set.EMPTY

⊦ ∀dreg reg.
    arm_prog.arm_REGISTERS dreg reg =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λc.
               (pred_set.BIGUNION (arm_prog.arm_REG c (reg c)),
                bool.IN c dreg)))) pred_set.EMPTY

⊦ ∀dfpr fpr.
    arm_prog.arm_FP_REGISTERS dfpr fpr =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λc.
               (pred_set.BIGUNION (arm_prog.arm_FP_REG c (fpr c)),
                bool.IN c dfpr)))) pred_set.EMPTY

⊦ ∀dmem mem.
    arm_prog.arm_MEMORY dmem mem =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λc.
               (pred_set.BIGUNION (arm_prog.arm_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 (arm_prog.arm_REG c d)
      (arm_prog.arm_REGISTERS (pred_set.DELETE dreg c) reg) =
    arm_prog.arm_REGISTERS dreg (combin.UPDATE c d reg)

⊦ ∀c d.
    bool.IN c dfpr ⇒
    set_sep.STAR (arm_prog.arm_FP_REG c d)
      (arm_prog.arm_FP_REGISTERS (pred_set.DELETE dfpr c) fpr) =
    arm_prog.arm_FP_REGISTERS dfpr (combin.UPDATE c d fpr)

⊦ ∀c d.
    bool.IN c dmem ⇒
    set_sep.STAR (arm_prog.arm_MEM c d)
      (arm_prog.arm_MEMORY (pred_set.DELETE dmem c) mem) =
    arm_prog.arm_MEMORY dmem (combin.UPDATE c d mem)

⊦ ∀dmem mem.
    arm_prog.arm_BE_WORD_MEMORY dmem mem =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λa.
               (pred_set.BIGUNION (arm_prog.arm_BE_WORD a (mem a)),
                bool.IN a dmem ∧
                alignment.aligned (arithmetic.BIT2 0) a)))) pred_set.EMPTY

⊦ ∀dmem mem.
    arm_prog.arm_WORD_MEMORY dmem mem =
    pred_set.INSERT
      (pred_set.BIGUNION
         (pred_set.GSPEC
            (λa.
               (pred_set.BIGUNION (arm_prog.arm_WORD a (mem a)),
                bool.IN a dmem ∧
                alignment.aligned (arithmetic.BIT2 0) a)))) pred_set.EMPTY

⊦ ∀n z c v.
    arm_prog.aS (n, z, c, v) =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR (arm_prog.arm_CPSR_N n) (arm_prog.arm_CPSR_Z z))
         (arm_prog.arm_CPSR_C c)) (arm_prog.arm_CPSR_V v)

⊦ ∀f df c d.
    bool.IN c df ∧ (let a ← c in alignment.aligned (arithmetic.BIT2 0) a) ⇒
    set_sep.STAR (arm_prog.arm_BE_WORD c d)
      (arm_prog.arm_BE_WORD_MEMORY (pred_set.DELETE df c) f) =
    arm_prog.arm_BE_WORD_MEMORY df (combin.UPDATE c d f)

⊦ ∀f df c d.
    bool.IN c df ∧ (let a ← c in alignment.aligned (arithmetic.BIT2 0) a) ⇒
    set_sep.STAR (arm_prog.arm_WORD c d)
      (arm_prog.arm_WORD_MEMORY (pred_set.DELETE df c) f) =
    arm_prog.arm_WORD_MEMORY df (combin.UPDATE c d f)

⊦ prog.SPEC m (set_sep.STAR p₁ (arm_prog.arm_PC pc)) code
    (set_sep.STAR p₂ (arm_prog.arm_REG arm.RName_PC pc')) ⇒
  (alignment.aligned (arithmetic.BIT2 0) pc ⇒
   alignment.aligned (arithmetic.BIT2 0) pc') ⇒
  prog.SPEC m (set_sep.STAR p₁ (arm_prog.arm_PC pc)) code
    (set_sep.STAR p₂ (arm_prog.arm_PC pc'))

⊦ temporal_state.TEMPORAL_NEXT m (set_sep.STAR p₁ (arm_prog.arm_PC pc))
    code (set_sep.STAR p₂ (arm_prog.arm_REG arm.RName_PC pc')) ⇒
  (alignment.aligned (arithmetic.BIT2 0) pc ⇒
   alignment.aligned (arithmetic.BIT2 0) pc') ⇒
  temporal_state.TEMPORAL_NEXT m (set_sep.STAR p₁ (arm_prog.arm_PC pc))
    code (set_sep.STAR p₂ (arm_prog.arm_PC pc'))

⊦ ∀vfp arch bigend thumb mode.
    arm_prog.arm_CONFIG (vfp, arch, bigend, thumb, mode) =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR
                  (set_sep.STAR
                     (set_sep.STAR
                        (set_sep.STAR (arm_prog.arm_VFPExtension vfp)
                           (arm_prog.arm_Extensions arm.Extension_Security
                              ⊥)) (arm_prog.arm_Architecture arch))
                     (arm_prog.arm_exception arm.NoException))
                  (arm_prog.arm_CPSR_J ⊥)) (arm_prog.arm_CPSR_E bigend))
            (arm_prog.arm_CPSR_T thumb)) (arm_prog.arm_CPSR_M mode))
      (set_sep.cond (arm_step.GoodMode mode))

⊦ ∀c p q.
    (∀y s.
       set_sep.STAR p (prog.CODE_POOL arm_prog.arm_instr c)
         (state.SELECT_STATE arm_prog.arm_proj y s) ⇒
       ∃v.
         arm_step.NextStateARM s = some v ∧
         set_sep.STAR q (prog.CODE_POOL arm_prog.arm_instr c)
           (state.SELECT_STATE arm_prog.arm_proj y v) ∧
         state.FRAME_STATE arm_prog.arm_proj y s =
         state.FRAME_STATE arm_prog.arm_proj y v) ⇒
    prog.SPEC arm_prog.ARM_MODEL p c q

⊦ ∀c p q.
    (∀y s.
       set_sep.STAR p (prog.CODE_POOL arm_prog.arm_instr c)
         (state.SELECT_STATE arm_prog.arm_proj y s) ⇒
       ∃v.
         arm_step.NextStateARM s = some v ∧
         set_sep.STAR q (prog.CODE_POOL arm_prog.arm_instr c)
           (state.SELECT_STATE arm_prog.arm_proj y v) ∧
         state.FRAME_STATE arm_prog.arm_proj y s =
         state.FRAME_STATE arm_prog.arm_proj y v) ⇒
    temporal_state.TEMPORAL_NEXT arm_prog.ARM_MODEL p c q

⊦ (∀a a'. arm_prog.arm_c_REG a = arm_prog.arm_c_REG a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_c_MEM a = arm_prog.arm_c_MEM a' ⇔ a = a') ∧
  (∀a a'.
     arm_prog.arm_c_Extensions a = arm_prog.arm_c_Extensions a' ⇔ a = a') ∧
  ∀a a'. arm_prog.arm_c_FP_REG a = arm_prog.arm_c_FP_REG a' ⇔ a = a'

⊦ ∀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 (arm_prog.arm_instr (words.word_add pc a, x))
      (arm_prog.arm_instr (pc, y))

⊦ (n ⇒ arm_prog.arm_CPSR_N ⊤ = arm_prog.arm_CPSR_N n) ∧
  (¬n ⇒ arm_prog.arm_CPSR_N ⊥ = arm_prog.arm_CPSR_N n) ∧
  (z ⇒ arm_prog.arm_CPSR_Z ⊤ = arm_prog.arm_CPSR_Z z) ∧
  (¬z ⇒ arm_prog.arm_CPSR_Z ⊥ = arm_prog.arm_CPSR_Z z) ∧
  (c ⇒ arm_prog.arm_CPSR_C ⊤ = arm_prog.arm_CPSR_C c) ∧
  (¬c ⇒ arm_prog.arm_CPSR_C ⊥ = arm_prog.arm_CPSR_C c) ∧
  (v ⇒ arm_prog.arm_CPSR_V ⊤ = arm_prog.arm_CPSR_V v) ∧
  (¬v ⇒ arm_prog.arm_CPSR_V ⊥ = arm_prog.arm_CPSR_V v)

⊦ ∀a i.
    arm_prog.arm_BE_WORD a i =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR
            (arm_prog.arm_MEM a
               (words.word_extract 31
                  (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) i))
            (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) i)))
         (arm_prog.arm_MEM
            (words.word_add a (words.n2w (arithmetic.BIT2 0)))
            (words.word_extract 15 (arithmetic.BIT2 3) i)))
      (arm_prog.arm_MEM (words.word_add a (words.n2w 3))
         (words.word_extract 7 0 i))

⊦ ∀a i.
    arm_prog.arm_WORD a i =
    set_sep.STAR
      (set_sep.STAR
         (set_sep.STAR (arm_prog.arm_MEM a (words.word_extract 7 0 i))
            (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
               (words.word_extract 15 (arithmetic.BIT2 3) i)))
         (arm_prog.arm_MEM
            (words.word_add a (words.n2w (arithmetic.BIT2 0)))
            (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
               (arithmetic.BIT2 7) i)))
      (arm_prog.arm_MEM (words.word_add a (words.n2w 3))
         (words.word_extract 31
            (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) i))

⊦ ∀P.
    (∀a. P (arm_prog.arm_d_exception a)) ∧
    (∀a. P (arm_prog.arm_d_VFPExtension a)) ∧
    (∀a. P (arm_prog.arm_d_PSR a)) ∧ (∀a. P (arm_prog.arm_d_word32 a)) ∧
    (∀a. P (arm_prog.arm_d_CP15 a)) ∧ (∀a. P (arm_prog.arm_d_CP14 a)) ∧
    (∀a. P (arm_prog.arm_d_Architecture a)) ∧
    (∀a. P (arm_prog.arm_d_word64 a)) ∧ (∀a. P (arm_prog.arm_d_word10 a)) ∧
    (∀a. P (arm_prog.arm_d_word2 a)) ∧ (∀a. P (arm_prog.arm_d_word5 a)) ∧
    (∀a. P (arm_prog.arm_d_word8 a)) ∧ (∀a. P (arm_prog.arm_d_word4 a)) ∧
    (∀a. P (arm_prog.arm_d_bool a)) ⇒ ∀x. P x

⊦ ∀a i.
    arm_prog.arm_instr (a, i) =
    pred_set.INSERT
      (arm_prog.arm_c_MEM a,
       arm_prog.arm_d_word8 (words.word_extract 7 0 i))
      (pred_set.INSERT
         (arm_prog.arm_c_MEM (words.word_add a (words.n2w 1)),
          arm_prog.arm_d_word8
            (words.word_extract 15 (arithmetic.BIT2 3) i))
         (pred_set.INSERT
            (arm_prog.arm_c_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0))),
             arm_prog.arm_d_word8
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) i))
            (pred_set.INSERT
               (arm_prog.arm_c_MEM (words.word_add a (words.n2w 3)),
                arm_prog.arm_d_word8
                  (words.word_extract 31
                     (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))
                     i)) pred_set.EMPTY)))

⊦ ∀x.
    (∃e. x = arm_prog.arm_d_exception e) ∨
    (∃V. x = arm_prog.arm_d_VFPExtension V) ∨
    (∃P₀. x = arm_prog.arm_d_PSR P₀) ∨ (∃c. x = arm_prog.arm_d_word32 c) ∨
    (∃C'. x = arm_prog.arm_d_CP15 C') ∨ (∃C'. x = arm_prog.arm_d_CP14 C') ∨
    (∃A. x = arm_prog.arm_d_Architecture A) ∨
    (∃c. x = arm_prog.arm_d_word64 c) ∨ (∃c. x = arm_prog.arm_d_word10 c) ∨
    (∃c. x = arm_prog.arm_d_word2 c) ∨ (∃c. x = arm_prog.arm_d_word5 c) ∨
    (∃c. x = arm_prog.arm_d_word8 c) ∨ (∃c. x = arm_prog.arm_d_word4 c) ∨
    ∃b. x = arm_prog.arm_d_bool b

⊦ alignment.aligned (arithmetic.BIT2 0) pc ⇒
  alignment.aligned (arithmetic.BIT2 0)
    (if b then
       words.word_sub pc
         (words.word_add
            (bitstring.v2w
               (x₂₄ :: x₂₃ :: x₂₂ :: x₂₁ :: x₂₀ :: x₁₉ :: x₁₈ :: x₁₇ ::
                x₁₆ :: x₁₅ :: x₁₄ :: x₁₃ :: x₁₂ :: x₁₁ :: x₁₀ :: x₉ ::
                x₈ :: x₇ :: x₆ :: x₅ :: x₄ :: x₃ :: x₂ :: ⊤ :: ⊤ :: []))
            (words.n2w 1))
     else
       words.word_add pc
         (bitstring.v2w
            (y₂₄ :: y₂₃ :: y₂₂ :: y₂₁ :: y₂₀ :: y₁₉ :: y₁₈ :: y₁₇ :: y₁₆ ::
             y₁₅ :: y₁₄ :: y₁₃ :: y₁₂ :: y₁₁ :: y₁₀ :: y₉ :: y₈ :: y₇ ::
             y₆ :: y₅ :: y₄ :: y₃ :: y₂ :: ⊥ :: ⊥ :: []))) ⇔ ⊤

⊦ (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_exception a) =
     1 + arm.exception_size a) ∧
  (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_VFPExtension a) =
     1 + arm.VFPExtension_size a) ∧
  (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_PSR a) = 1 + arm.PSR_size a) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word32 a) = 1) ∧
  (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_CP15 a) =
     1 + arm.CP15_size a) ∧
  (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_CP14 a) =
     1 + arm.CP14_size a) ∧
  (∀a.
     arm_prog.arm_data_size (arm_prog.arm_d_Architecture a) =
     1 + arm.Architecture_size a) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word64 a) = 1) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word10 a) = 1) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word2 a) = 1) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word5 a) = 1) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word8 a) = 1) ∧
  (∀a. arm_prog.arm_data_size (arm_prog.arm_d_word4 a) = 1) ∧
  ∀a.
    arm_prog.arm_data_size (arm_prog.arm_d_bool a) =
    1 + basicSize.bool_size a

⊦ ∀f₀ f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃.
    ∃fn.
      (∀a. fn (arm_prog.arm_d_exception a) = f₀ a) ∧
      (∀a. fn (arm_prog.arm_d_VFPExtension a) = f₁ a) ∧
      (∀a. fn (arm_prog.arm_d_PSR a) = f₂ a) ∧
      (∀a. fn (arm_prog.arm_d_word32 a) = f₃ a) ∧
      (∀a. fn (arm_prog.arm_d_CP15 a) = f₄ a) ∧
      (∀a. fn (arm_prog.arm_d_CP14 a) = f₅ a) ∧
      (∀a. fn (arm_prog.arm_d_Architecture a) = f₆ a) ∧
      (∀a. fn (arm_prog.arm_d_word64 a) = f₇ a) ∧
      (∀a. fn (arm_prog.arm_d_word10 a) = f₈ a) ∧
      (∀a. fn (arm_prog.arm_d_word2 a) = f₉ a) ∧
      (∀a. fn (arm_prog.arm_d_word5 a) = f₁₀ a) ∧
      (∀a. fn (arm_prog.arm_d_word8 a) = f₁₁ a) ∧
      (∀a. fn (arm_prog.arm_d_word4 a) = f₁₂ a) ∧
      ∀a. fn (arm_prog.arm_d_bool a) = f₁₃ a

⊦ ∀a w c p q.
    prog.SPEC arm_prog.ARM_MODEL
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR p
                  (arm_prog.arm_MEM a (words.word_extract 7 0 w)))
               (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (arm_prog.arm_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (arm_prog.arm_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
                  (arm_prog.arm_MEM a (words.word_extract 7 0 w)))
               (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (arm_prog.arm_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (arm_prog.arm_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w))) ⇔
    prog.SPEC arm_prog.ARM_MODEL
      (set_sep.STAR
         (set_sep.cond
            (pred_set.DISJOINT (arm_prog.arm_instr (a, w))
               (pred_set.BIGUNION (pred_set.IMAGE arm_prog.arm_instr c))))
         p) (pred_set.INSERT (a, w) c) q

⊦ ∀a w c p q.
    temporal_state.TEMPORAL_NEXT arm_prog.ARM_MODEL
      (set_sep.STAR
         (set_sep.STAR
            (set_sep.STAR
               (set_sep.STAR p
                  (arm_prog.arm_MEM a (words.word_extract 7 0 w)))
               (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (arm_prog.arm_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (arm_prog.arm_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
                  (arm_prog.arm_MEM a (words.word_extract 7 0 w)))
               (arm_prog.arm_MEM (words.word_add a (words.n2w 1))
                  (words.word_extract 15 (arithmetic.BIT2 3) w)))
            (arm_prog.arm_MEM
               (words.word_add a (words.n2w (arithmetic.BIT2 0)))
               (words.word_extract (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
                  (arithmetic.BIT2 7) w)))
         (arm_prog.arm_MEM (words.word_add a (words.n2w 3))
            (words.word_extract 31
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))) w))) ⇔
    temporal_state.TEMPORAL_NEXT arm_prog.ARM_MODEL
      (set_sep.STAR
         (set_sep.cond
            (pred_set.DISJOINT (arm_prog.arm_instr (a, w))
               (pred_set.BIGUNION (pred_set.IMAGE arm_prog.arm_instr c))))
         p) (pred_set.INSERT (a, w) c) q

⊦ ∀P.
    P arm_prog.arm_c_exception ∧ P arm_prog.arm_c_VFPExtension ∧
    P arm_prog.arm_c_SPSR_und ∧ P arm_prog.arm_c_SPSR_svc ∧
    P arm_prog.arm_c_SPSR_mon ∧ P arm_prog.arm_c_SPSR_irq ∧
    P arm_prog.arm_c_SPSR_hyp ∧ P arm_prog.arm_c_SPSR_fiq ∧
    P arm_prog.arm_c_SPSR_abt ∧ (∀a. P (arm_prog.arm_c_REG a)) ∧
    (∀a. P (arm_prog.arm_c_MEM a)) ∧
    (∀a. P (arm_prog.arm_c_Extensions a)) ∧ P arm_prog.arm_c_ELR_hyp ∧
    P arm_prog.arm_c_CP15 ∧ P arm_prog.arm_c_CP14 ∧
    P arm_prog.arm_c_Architecture ∧ (∀a. P (arm_prog.arm_c_FP_REG a)) ∧
    P arm_prog.arm_c_FP_FPSCR_fpscr'rst ∧ P arm_prog.arm_c_FP_FPSCR_Z ∧
    P arm_prog.arm_c_FP_FPSCR_V ∧ P arm_prog.arm_c_FP_FPSCR_UFE ∧
    P arm_prog.arm_c_FP_FPSCR_UFC ∧ P arm_prog.arm_c_FP_FPSCR_RMode ∧
    P arm_prog.arm_c_FP_FPSCR_QC ∧ P arm_prog.arm_c_FP_FPSCR_OFE ∧
    P arm_prog.arm_c_FP_FPSCR_OFC ∧ P arm_prog.arm_c_FP_FPSCR_N ∧
    P arm_prog.arm_c_FP_FPSCR_IXE ∧ P arm_prog.arm_c_FP_FPSCR_IXC ∧
    P arm_prog.arm_c_FP_FPSCR_IOE ∧ P arm_prog.arm_c_FP_FPSCR_IOC ∧
    P arm_prog.arm_c_FP_FPSCR_IDE ∧ P arm_prog.arm_c_FP_FPSCR_IDC ∧
    P arm_prog.arm_c_FP_FPSCR_FZ ∧ P arm_prog.arm_c_FP_FPSCR_DZE ∧
    P arm_prog.arm_c_FP_FPSCR_DZC ∧ P arm_prog.arm_c_FP_FPSCR_DN ∧
    P arm_prog.arm_c_FP_FPSCR_C ∧ P arm_prog.arm_c_FP_FPSCR_AHP ∧
    P arm_prog.arm_c_CPSR_psr'rst ∧ P arm_prog.arm_c_CPSR_Z ∧
    P arm_prog.arm_c_CPSR_V ∧ P arm_prog.arm_c_CPSR_T ∧
    P arm_prog.arm_c_CPSR_Q ∧ P arm_prog.arm_c_CPSR_N ∧
    P arm_prog.arm_c_CPSR_M ∧ P arm_prog.arm_c_CPSR_J ∧
    P arm_prog.arm_c_CPSR_IT ∧ P arm_prog.arm_c_CPSR_I ∧
    P arm_prog.arm_c_CPSR_GE ∧ P arm_prog.arm_c_CPSR_F ∧
    P arm_prog.arm_c_CPSR_E ∧ P arm_prog.arm_c_CPSR_C ∧
    P arm_prog.arm_c_CPSR_A ⇒ ∀x. P x

⊦ (∀a a'.
     arm_prog.arm_d_exception a = arm_prog.arm_d_exception a' ⇔ a = a') ∧
  (∀a a'.
     arm_prog.arm_d_VFPExtension a = arm_prog.arm_d_VFPExtension a' ⇔
     a = a') ∧
  (∀a a'. arm_prog.arm_d_PSR a = arm_prog.arm_d_PSR a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word32 a = arm_prog.arm_d_word32 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_CP15 a = arm_prog.arm_d_CP15 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_CP14 a = arm_prog.arm_d_CP14 a' ⇔ a = a') ∧
  (∀a a'.
     arm_prog.arm_d_Architecture a = arm_prog.arm_d_Architecture a' ⇔
     a = a') ∧
  (∀a a'. arm_prog.arm_d_word64 a = arm_prog.arm_d_word64 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word10 a = arm_prog.arm_d_word10 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word2 a = arm_prog.arm_d_word2 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word5 a = arm_prog.arm_d_word5 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word8 a = arm_prog.arm_d_word8 a' ⇔ a = a') ∧
  (∀a a'. arm_prog.arm_d_word4 a = arm_prog.arm_d_word4 a' ⇔ a = a') ∧
  ∀a a'. arm_prog.arm_d_bool a = arm_prog.arm_d_bool a' ⇔ a ⇔ a'

⊦ ∀x.
    x = arm_prog.arm_c_exception ∨ x = arm_prog.arm_c_VFPExtension ∨
    x = arm_prog.arm_c_SPSR_und ∨ x = arm_prog.arm_c_SPSR_svc ∨
    x = arm_prog.arm_c_SPSR_mon ∨ x = arm_prog.arm_c_SPSR_irq ∨
    x = arm_prog.arm_c_SPSR_hyp ∨ x = arm_prog.arm_c_SPSR_fiq ∨
    x = arm_prog.arm_c_SPSR_abt ∨ (∃R'. x = arm_prog.arm_c_REG R') ∨
    (∃c. x = arm_prog.arm_c_MEM c) ∨
    (∃E. x = arm_prog.arm_c_Extensions E) ∨ x = arm_prog.arm_c_ELR_hyp ∨
    x = arm_prog.arm_c_CP15 ∨ x = arm_prog.arm_c_CP14 ∨
    x = arm_prog.arm_c_Architecture ∨ (∃c. x = arm_prog.arm_c_FP_REG c) ∨
    x = arm_prog.arm_c_FP_FPSCR_fpscr'rst ∨ x = arm_prog.arm_c_FP_FPSCR_Z ∨
    x = arm_prog.arm_c_FP_FPSCR_V ∨ x = arm_prog.arm_c_FP_FPSCR_UFE ∨
    x = arm_prog.arm_c_FP_FPSCR_UFC ∨ x = arm_prog.arm_c_FP_FPSCR_RMode ∨
    x = arm_prog.arm_c_FP_FPSCR_QC ∨ x = arm_prog.arm_c_FP_FPSCR_OFE ∨
    x = arm_prog.arm_c_FP_FPSCR_OFC ∨ x = arm_prog.arm_c_FP_FPSCR_N ∨
    x = arm_prog.arm_c_FP_FPSCR_IXE ∨ x = arm_prog.arm_c_FP_FPSCR_IXC ∨
    x = arm_prog.arm_c_FP_FPSCR_IOE ∨ x = arm_prog.arm_c_FP_FPSCR_IOC ∨
    x = arm_prog.arm_c_FP_FPSCR_IDE ∨ x = arm_prog.arm_c_FP_FPSCR_IDC ∨
    x = arm_prog.arm_c_FP_FPSCR_FZ ∨ x = arm_prog.arm_c_FP_FPSCR_DZE ∨
    x = arm_prog.arm_c_FP_FPSCR_DZC ∨ x = arm_prog.arm_c_FP_FPSCR_DN ∨
    x = arm_prog.arm_c_FP_FPSCR_C ∨ x = arm_prog.arm_c_FP_FPSCR_AHP ∨
    x = arm_prog.arm_c_CPSR_psr'rst ∨ x = arm_prog.arm_c_CPSR_Z ∨
    x = arm_prog.arm_c_CPSR_V ∨ x = arm_prog.arm_c_CPSR_T ∨
    x = arm_prog.arm_c_CPSR_Q ∨ x = arm_prog.arm_c_CPSR_N ∨
    x = arm_prog.arm_c_CPSR_M ∨ x = arm_prog.arm_c_CPSR_J ∨
    x = arm_prog.arm_c_CPSR_IT ∨ x = arm_prog.arm_c_CPSR_I ∨
    x = arm_prog.arm_c_CPSR_GE ∨ x = arm_prog.arm_c_CPSR_F ∨
    x = arm_prog.arm_c_CPSR_E ∨ x = arm_prog.arm_c_CPSR_C ∨
    x = arm_prog.arm_c_CPSR_A

⊦ ∀s.
    arm_prog.arm_proj s =
    λa.
      arm_prog.arm_component_CASE a
        (arm_prog.arm_d_exception (arm.arm_state_exception s))
        (arm_prog.arm_d_VFPExtension (arm.arm_state_VFPExtension s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_und s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_svc s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_mon s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_irq s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_hyp s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_fiq s))
        (arm_prog.arm_d_PSR (arm.arm_state_SPSR_abt s))
        (λv₀. arm_prog.arm_d_word32 (arm.arm_state_REG s v₀))
        (λv₁. arm_prog.arm_d_word8 (arm.arm_state_MEM s v₁))
        (λv₂. arm_prog.arm_d_bool (arm.arm_state_Extensions s v₂))
        (arm_prog.arm_d_word32 (arm.arm_state_ELR_hyp s))
        (arm_prog.arm_d_CP15 (arm.arm_state_CP15 s))
        (arm_prog.arm_d_CP14 (arm.arm_state_CP14 s))
        (arm_prog.arm_d_Architecture (arm.arm_state_Architecture s))
        (λv₃. arm_prog.arm_d_word64 (arm.FP_REG (arm.arm_state_FP s) v₃))
        (arm_prog.arm_d_word10
           (arm.FPSCR_fpscr'rst (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_Z (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_V (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_UFE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_UFC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_word2
           (arm.FPSCR_RMode (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_QC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_OFE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_OFC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_N (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IXE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IXC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IOE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IOC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IDE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_IDC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_FZ (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_DZE (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_DZC (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_DN (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_C (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_bool
           (arm.FPSCR_AHP (arm.FP_FPSCR (arm.arm_state_FP s))))
        (arm_prog.arm_d_word4 (arm.PSR_psr'rst (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_Z (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_V (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_T (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_Q (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_N (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_word5 (arm.PSR_M (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_J (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_word8 (arm.PSR_IT (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_I (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_word4 (arm.PSR_GE (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_F (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_E (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_C (arm.arm_state_CPSR s)))
        (arm_prog.arm_d_bool (arm.PSR_A (arm.arm_state_CPSR s)))

⊦ ∀M M' f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃.
    M = M' ∧ (∀a. M' = arm_prog.arm_d_exception a ⇒ f a = f' a) ∧
    (∀a. M' = arm_prog.arm_d_VFPExtension a ⇒ f₁ a = f1' a) ∧
    (∀a. M' = arm_prog.arm_d_PSR a ⇒ f₂ a = f2' a) ∧
    (∀a. M' = arm_prog.arm_d_word32 a ⇒ f₃ a = f3' a) ∧
    (∀a. M' = arm_prog.arm_d_CP15 a ⇒ f₄ a = f4' a) ∧
    (∀a. M' = arm_prog.arm_d_CP14 a ⇒ f₅ a = f5' a) ∧
    (∀a. M' = arm_prog.arm_d_Architecture a ⇒ f₆ a = f6' a) ∧
    (∀a. M' = arm_prog.arm_d_word64 a ⇒ f₇ a = f7' a) ∧
    (∀a. M' = arm_prog.arm_d_word10 a ⇒ f₈ a = f8' a) ∧
    (∀a. M' = arm_prog.arm_d_word2 a ⇒ f₉ a = f9' a) ∧
    (∀a. M' = arm_prog.arm_d_word5 a ⇒ f₁₀ a = f10' a) ∧
    (∀a. M' = arm_prog.arm_d_word8 a ⇒ f₁₁ a = f11' a) ∧
    (∀a. M' = arm_prog.arm_d_word4 a ⇒ f₁₂ a = f12' a) ∧
    (∀a. M' = arm_prog.arm_d_bool a ⇒ f₁₃ a = f13' a) ⇒
    arm_prog.arm_data_CASE M f f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₈ f₉ f₁₀ f₁₁ f₁₂ f₁₃ =
    arm_prog.arm_data_CASE M' f' f1' f2' f3' f4' f5' f6' f7' f8' f9' f10'
      f11' f12' f13'

⊦ arm_prog.arm_component_size arm_prog.arm_c_exception = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_VFPExtension = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_und = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_svc = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_mon = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_irq = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_hyp = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_fiq = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_SPSR_abt = 0 ∧
  (∀a.
     arm_prog.arm_component_size (arm_prog.arm_c_REG a) =
     1 + arm.RName_size a) ∧
  (∀a. arm_prog.arm_component_size (arm_prog.arm_c_MEM a) = 1) ∧
  (∀a.
     arm_prog.arm_component_size (arm_prog.arm_c_Extensions a) =
     1 + arm.Extensions_size a) ∧
  arm_prog.arm_component_size arm_prog.arm_c_ELR_hyp = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CP15 = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CP14 = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_Architecture = 0 ∧
  (∀a. arm_prog.arm_component_size (arm_prog.arm_c_FP_REG a) = 1) ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_fpscr'rst = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_Z = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_V = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_UFE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_UFC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_RMode = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_QC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_OFE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_OFC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_N = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IXE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IXC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IOE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IOC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IDE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_IDC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_FZ = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_DZE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_DZC = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_DN = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_C = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_FP_FPSCR_AHP = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_psr'rst = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_Z = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_V = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_T = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_Q = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_N = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_M = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_J = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_IT = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_I = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_GE = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_F = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_E = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_C = 0 ∧
  arm_prog.arm_component_size arm_prog.arm_c_CPSR_A = 0

⊦ ∀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₂₇ 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 arm_prog.arm_c_exception = f₀ ∧
      fn arm_prog.arm_c_VFPExtension = f₁ ∧
      fn arm_prog.arm_c_SPSR_und = f₂ ∧ fn arm_prog.arm_c_SPSR_svc = f₃ ∧
      fn arm_prog.arm_c_SPSR_mon = f₄ ∧ fn arm_prog.arm_c_SPSR_irq = f₅ ∧
      fn arm_prog.arm_c_SPSR_hyp = f₆ ∧ fn arm_prog.arm_c_SPSR_fiq = f₇ ∧
      fn arm_prog.arm_c_SPSR_abt = f₈ ∧
      (∀a. fn (arm_prog.arm_c_REG a) = f₉ a) ∧
      (∀a. fn (arm_prog.arm_c_MEM a) = f₁₀ a) ∧
      (∀a. fn (arm_prog.arm_c_Extensions a) = f₁₁ a) ∧
      fn arm_prog.arm_c_ELR_hyp = f₁₂ ∧ fn arm_prog.arm_c_CP15 = f₁₃ ∧
      fn arm_prog.arm_c_CP14 = f₁₄ ∧ fn arm_prog.arm_c_Architecture = f₁₅ ∧
      (∀a. fn (arm_prog.arm_c_FP_REG a) = f₁₆ a) ∧
      fn arm_prog.arm_c_FP_FPSCR_fpscr'rst = f₁₇ ∧
      fn arm_prog.arm_c_FP_FPSCR_Z = f₁₈ ∧
      fn arm_prog.arm_c_FP_FPSCR_V = f₁₉ ∧
      fn arm_prog.arm_c_FP_FPSCR_UFE = f₂₀ ∧
      fn arm_prog.arm_c_FP_FPSCR_UFC = f₂₁ ∧
      fn arm_prog.arm_c_FP_FPSCR_RMode = f₂₂ ∧
      fn arm_prog.arm_c_FP_FPSCR_QC = f₂₃ ∧
      fn arm_prog.arm_c_FP_FPSCR_OFE = f₂₄ ∧
      fn arm_prog.arm_c_FP_FPSCR_OFC = f₂₅ ∧
      fn arm_prog.arm_c_FP_FPSCR_N = f₂₆ ∧
      fn arm_prog.arm_c_FP_FPSCR_IXE = f₂₇ ∧
      fn arm_prog.arm_c_FP_FPSCR_IXC = f₂₈ ∧
      fn arm_prog.arm_c_FP_FPSCR_IOE = f₂₉ ∧
      fn arm_prog.arm_c_FP_FPSCR_IOC = f₃₀ ∧
      fn arm_prog.arm_c_FP_FPSCR_IDE = f₃₁ ∧
      fn arm_prog.arm_c_FP_FPSCR_IDC = f₃₂ ∧
      fn arm_prog.arm_c_FP_FPSCR_FZ = f₃₃ ∧
      fn arm_prog.arm_c_FP_FPSCR_DZE = f₃₄ ∧
      fn arm_prog.arm_c_FP_FPSCR_DZC = f₃₅ ∧
      fn arm_prog.arm_c_FP_FPSCR_DN = f₃₆ ∧
      fn arm_prog.arm_c_FP_FPSCR_C = f₃₇ ∧
      fn arm_prog.arm_c_FP_FPSCR_AHP = f₃₈ ∧
      fn arm_prog.arm_c_CPSR_psr'rst = f₃₉ ∧
      fn arm_prog.arm_c_CPSR_Z = f₄₀ ∧ fn arm_prog.arm_c_CPSR_V = f₄₁ ∧
      fn arm_prog.arm_c_CPSR_T = f₄₂ ∧ fn arm_prog.arm_c_CPSR_Q = f₄₃ ∧
      fn arm_prog.arm_c_CPSR_N = f₄₄ ∧ fn arm_prog.arm_c_CPSR_M = f₄₅ ∧
      fn arm_prog.arm_c_CPSR_J = f₄₆ ∧ fn arm_prog.arm_c_CPSR_IT = f₄₇ ∧
      fn arm_prog.arm_c_CPSR_I = f₄₈ ∧ fn arm_prog.arm_c_CPSR_GE = f₄₉ ∧
      fn arm_prog.arm_c_CPSR_F = f₅₀ ∧ fn arm_prog.arm_c_CPSR_E = f₅₁ ∧
      fn arm_prog.arm_c_CPSR_C = f₅₂ ∧ fn arm_prog.arm_c_CPSR_A = f₅₃