include "ASM/AssemblyProof.ma".
include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".

lemma set_arg_16_mk_Status_commutation:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀w: Word.
  ∀d: [[dptr]].
    set_arg_16 M cm s w d =
      mk_PreStatus M cm
        (low_internal_ram … s)
        (high_internal_ram … s)
        (external_ram … s)
        (program_counter … s)
        (special_function_registers_8051 … (set_arg_16 M cm s w d))
        (special_function_registers_8052 … s)
        (p1_latch … s)
        (p3_latch … s)
        (clock … s).
  #M #cm #s #w #d
  whd in match set_arg_16; normalize nodelta
  whd in match set_arg_16'; normalize nodelta
  @(subaddressing_mode_elim … d)
  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
  whd in match set_8051_sfr; normalize nodelta %
qed.

lemma set_program_counter_mk_Status_commutation:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀w: Word.
    set_program_counter M cm s w =
      mk_PreStatus M cm
        (low_internal_ram … s)
        (high_internal_ram … s)
        (external_ram … s)
        w
        (special_function_registers_8051 … s)
        (special_function_registers_8052 … s)
        (p1_latch … s)
        (p3_latch … s)
        (clock … s).
  //
qed.

lemma set_clock_mk_Status_commutation:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀c: nat.
    set_clock M cm s c =
      mk_PreStatus M cm
        (low_internal_ram … s)
        (high_internal_ram … s)
        (external_ram … s)
        (program_counter … s)
        (special_function_registers_8051 … s)
        (special_function_registers_8052 … s)
        (p1_latch … s)
        (p3_latch … s)
        c.
  //
qed.

lemma get_8051_sfr_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀t: Time.
    get_8051_sfr M cm (set_clock M cm s t) sfr =
      get_8051_sfr M cm s sfr.
  #M #cm #s #sfr #t %
qed.

lemma get_8051_sfr_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀pc: Word.
    get_8051_sfr M cm (set_program_counter M cm s pc) =
      get_8051_sfr M cm s.
  #M #cm #s #sfr #pc %
qed.

lemma special_function_registers_8051_set_arg_16:
  ∀M, M': Type[0].
  ∀cm: M.
  ∀cm': M'.
  ∀s: PreStatus M cm.
  ∀s': PreStatus M' cm'.
  ∀w, w': Word.
  ∀d, d': [[dptr]].
   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
    w = w' →
      special_function_registers_8051 ?? (set_arg_16 … s w d) =
        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
  #M #M' #cm #cm' #s #s' #w #w'
  #d @(subaddressing_mode_elim … d)
  #d' @(subaddressing_mode_elim … d')
  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
qed.

lemma program_counter_set_arg_1:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀addr: [[bit_addr; carry]].
  ∀b: Bit.
    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
  #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta
  #addr #b
  @(subaddressing_mode_elim … addr)
  [1:
    #byte cases (vsplit ????) #nu #nl normalize nodelta
    cases (vsplit ????) #ignore #three_bits normalize nodelta
    cases (get_index_v bool ????) normalize nodelta
    [1:
      @program_counter_set_bit_addressable_sfr
    |2:
      @program_counter_set_low_internal_ram
    ]
  |2:
    cases (vsplit ????) //
  ] *)
qed.

lemma get_ov_flag_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
    get_ov_flag M cm (set_program_counter M cm s pc) =
      get_ov_flag M cm s.
  #M #cm #s #pc %
qed.

lemma external_ram_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
    external_ram M cm (set_program_counter M cm s pc) =
      external_ram M cm s.
  #M #cm #s #pc %
qed.

lemma low_internal_ram_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
    low_internal_ram M cm (set_program_counter M cm s pc) =
      low_internal_ram M cm s.
  #M #cm #s #pc %
qed.

lemma high_internal_ram_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
    high_internal_ram M cm (set_program_counter M cm s pc) =
      high_internal_ram M cm s.
  #M #cm #s #pc %
qed.

lemma get_arg_8_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀flag: bool.
  ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
  ∀pc: Word.
    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
      get_arg_8 M cm s flag addr.
  [2,3:
    cases addr #subaddressing_mode
    cases subaddressing_mode
    try (#addr1 whd in ⊢ (% → %);)
    whd in ⊢ (% → %); //
  ]
  #M #cm #s #flag #addr #pc
  whd in match get_arg_8; normalize nodelta
  cases addr *
  try (#addr1 #absurd normalize in absurd; cases absurd @I)
  try (#absurd normalize in absurd; cases absurd @I)
  try (#addr1 #addr2) try #addr1
  normalize nodelta %
qed.

lemma external_ram_set_flags:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀opt: option Bit.
  ∀bit1, bit2: Bit.
    external_ram M cm (set_flags M cm s bit1 opt bit2) =
      external_ram M cm s.
  #M #cm #s #opt #bit1 #bit2 %
qed.

lemma low_internal_ram_set_flags:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀opt: option Bit.
  ∀bit1, bit2: Bit.
    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
      low_internal_ram M cm s.
  #M #cm #s #opt #bit1 #bit2 %
qed.

lemma high_internal_ram_set_flags:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀opt: option Bit.
  ∀bit1, bit2: Bit.
    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
      high_internal_ram M cm s.
  #M #cm #s #opt #bit1 #bit2 %
qed.

lemma low_internal_ram_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀t: Time.
    low_internal_ram M cm (set_clock M cm s t) =
      low_internal_ram M cm s.
  #M #cm #s #t %
qed.

lemma high_internal_ram_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀t: Time.
    high_internal_ram M cm (set_clock M cm s t) =
      high_internal_ram M cm s.
  #M #cm #s #t %
qed.

lemma external_ram_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀t: Time.
    external_ram M cm (set_clock M cm s t) =
      external_ram M cm s.
  #M #cm #s #t %
qed.

lemma set_8051_sfr_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
  ∀sfr: SFR8051.
  ∀v: Byte.
    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
  #M #cm #s #pc #sfr #v %
qed.

lemma low_internal_ram_set_8051_sfr:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀v: Byte.
    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
      low_internal_ram M cm s.
  #M #cm #s #sfr #v %
qed.

lemma high_internal_ram_set_8051_sfr:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀v: Byte.
    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
      high_internal_ram M cm s.
  #M #cm #s #sfr #v %
qed.

lemma external_ram_set_8051_sfr:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀v: Byte.
    external_ram M cm (set_8051_sfr M cm s sfr v) =
      external_ram M cm s.
  #M #cm #s #sfr #v %
qed.

lemma get_arg_8_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀addr.
  ∀t: Time.
    get_arg_8 M cm (set_clock M cm s t) addr =
      get_arg_8 M cm s addr.
  #M #cm #s #addr #t %
qed.

lemma set_program_counter_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀pc: Word.
  ∀pc': Word.
    set_program_counter M cm (set_program_counter M cm s pc) pc' =
      set_program_counter M cm s pc'.
  #M #cm #s #pc #pc' %
qed.

(* XXX: move elsewhere *)
lemma bitvector_8_cases:
  ∀w: BitVector 8.
    ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
 #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
 >(BitVector_O … w) %
qed.

(* XXX: not true
lemma p3_latch_set_arg_8:
  ∀M: Type[0].
  ∀cm: M.
  ∀s: PreStatus M cm.
  ∀args.
  ∀v: Byte.
    p3_latch M cm (set_arg_8 M cm s args v) =
      p3_latch M cm s.
  #M #cm #s #args #v
  @(subaddressing_mode_elim … args)
  try #w try %
  whd in match set_arg_8; normalize nodelta
  whd in match set_arg_8'; normalize nodelta
  inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
  inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
  inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
  whd in match set_bit_addressable_sfr; normalize nodelta
  @(bitvector_8_elim_prop … w)
*)

lemma status_of_pseudo_status_does_not_change_8051_sfrs:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀s: PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
    \snd M = data →
      special_function_registers_8051 pseudo_assembly_program cm s =
        special_function_registers_8051 (BitVectorTrie Byte 16)
          (code_memory_of_pseudo_assembly_program cm sigma policy)
          (status_of_pseudo_status M cm s sigma policy).
  #M #cm #s #sigma #policy #None_proof cases s
  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  >None_proof %
qed.

lemma n_lt_19_elim_prop:
  ∀P: nat → Prop.
    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
      (∀n. n < 19 → P n).
  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
  #H15 #H16 #H17 #H18 #H19 #n
  cases n [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
  #n' normalize in ⊢ (% → ?);
  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
  cases (lt_to_not_zero … absurd)
qed.

lemma get_index_v_set_index_miss:
  ∀T: Type[0].
  ∀n, i, j: nat.
  ∀v: Vector T n.
  ∀b: T.
  ∀i_proof: i < n.
  ∀j_proof: j < n.
  i ≠ j →
    get_index_v T n (set_index T n v i b i_proof) j j_proof =
      get_index_v T n v j j_proof.
  #T #n #i #j #v lapply i lapply j elim v #i #j
  [1:
    #b #i_proof
    cases (lt_to_not_zero … i_proof)
  |2:
    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
    lapply i_proof lapply i_neq_j cases i'
    [1:
      -i_neq_j #i_neq_j -i_proof #i_proof
      whd in match (set_index ??????);
      lapply j_proof lapply i_neq_j cases j'
      [1:
        #relevant @⊥ cases relevant -relevant #absurd @absurd %
      |2:
        #j' #_ -j_proof #j_proof %
      ]
    |2:
      #i' -i_neq_j #i_neq_j -i_proof #i_proof
      lapply j_proof lapply i_neq_j cases j'
      [1:
        #_ #j_proof %
      |2:
        #j' #i_neq_j #j_proof
        @inductive_hypothesis @nmk #relevant
        cases i_neq_j #absurd @absurd >relevant %
      ]
    ]
  ]
qed.

lemma get_index_v_special_function_registers_8051_not_acc_a:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀s: PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀n: nat.
  ∀proof: n < 19.
    n ≠ 17 →
   (get_index_v Byte 19
    (special_function_registers_8051 pseudo_assembly_program cm s) n
    proof =
   get_index_v Byte 19
     (special_function_registers_8051 (BitVectorTrie Byte 16)
       (code_memory_of_pseudo_assembly_program cm sigma policy)
       (status_of_pseudo_status M cm s sigma policy)) n
       proof).
  #M #cm #s #sigma #policy #n #proof lapply proof
  @(n_lt_19_elim_prop … proof) -proof #proof
  [18:
    #absurd @⊥ cases absurd -absurd #absurd @absurd %
  ]
  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  cases M #left #right cases right normalize nodelta try %
  -right * #address
  @pair_elim #high #low #high_low_refl normalize nodelta
  whd in match sfr_8051_index; normalize nodelta
  >get_index_v_set_index_miss try %
  #absurd destruct(absurd)
qed.

(*
include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".
include alias "ASM/BitVectorTrie.ma".
*)

lemma get_8051_sfr_status_of_pseudo_status:
  ∀M.
  ∀cm, ps, sigma, policy.
  ∀sfr.
    (sfr = SFR_ACC_A → \snd M = data) →
    get_8051_sfr (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      (status_of_pseudo_status M cm ps sigma policy) sfr =
    get_8051_sfr pseudo_assembly_program cm ps sfr.
  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
  [18:
     >relevant %
  ]
  cases sndM try % * #address
  whd in match get_8051_sfr;
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  @pair_elim #upper #lower #upper_lower_refl
  @get_index_v_set_index_miss @nmk #relevant
  normalize in relevant; destruct(relevant)
qed.

lemma bitvector_cases_hd_tl:
  ∀n: nat.
  ∀w: BitVector (S n).
   ∃hd: bool. ∃tl: BitVector n.
    w ≃ hd:::tl.
  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
qed.

lemma external_ram_set_bit_addressable_sfr:
  ∀M: Type[0].
  ∀cm: M.
  ∀ps.
  ∀w.
  ∀result: Byte.
    external_ram M cm
      (set_bit_addressable_sfr M cm ps w result) =
    external_ram M cm ps.
  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
  whd in match set_bit_addressable_sfr; normalize nodelta
  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases not_implemented *)
qed.

lemma external_ram_set_arg_8:
  ∀M: Type[0].
  ∀cm: M.
  ∀ps.
  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
  ∀result.
    external_ram M cm (set_arg_8 M cm ps addr1 result) =
      external_ram M cm ps.
  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
  #M #cm #ps #addr1 #result
  @(subaddressing_mode_elim … addr1) try #w try %
  whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
  [1:
    cases (vsplit bool ???) #nu #nl normalize nodelta
    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
    cases (get_index_v bool ????) normalize nodelta try %
    @external_ram_set_bit_addressable_sfr
  |2:
    cases (vsplit bool ???) #nu #nl normalize nodelta
    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
    cases (get_index_v bool ????) normalize nodelta %
  ] *)
qed.

lemma special_function_registers_8051_set_clock:
  ∀M: Type[0].
  ∀cm: M.
  ∀ps.
  ∀t.
    special_function_registers_8051 M cm (set_clock M cm ps t) =
      special_function_registers_8051 M cm ps.
  //
qed.

lemma get_arg_8_pseudo_addressing_mode_ok:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀ps: PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀addr1: [[registr; direct]].
    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
      get_arg_8 (BitVectorTrie Byte 16)
        (code_memory_of_pseudo_assembly_program cm sigma policy)
        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
      get_arg_8 pseudo_assembly_program cm ps true addr1.
  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
  #M #cm #ps #sigma #policy #addr1
  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
  [1:
    whd in ⊢ (??%? → ??%?);
    whd in match bit_address_of_register; normalize nodelta
    @pair_elim #un #ln #un_ln_refl
    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
    @(pair_replace ?????????? un_ln_refl)
    [1:
      whd in match get_8051_sfr; normalize nodelta
      whd in match sfr_8051_index; normalize nodelta
      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
      try % #absurd destruct(absurd)
    |2:
      #assembly_mode_ok_refl
      >low_internal_ram_of_pseudo_internal_ram_miss
      [1:
        %
      |2:
        cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
        #absurd try % @sym_eq assumption
      ]
    ]
  |2:
    #addressing_mode_ok_refl whd in ⊢ (??%?);
    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    [1:
      whd in ⊢ (??%%); normalize nodelta
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1: % ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ]
      inversion (eqb ??) #eqb_refl normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
      ]
      cases (eqb ??) normalize nodelta [1:
        @get_8051_sfr_status_of_pseudo_status
        #absurd destruct(absurd)
      ] %
    |2:
      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
      whd in match status_of_pseudo_status; normalize nodelta
      >low_internal_ram_of_pseudo_internal_ram_miss try %
      cut(arg = false:::(three_bits@@nl))
      [1:
        <get_index_v_refl
        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
        [1:
          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
          [1:
            @le_S_S @le_O_n
          |2:
            cut(ignore = \fst (vsplit bool 1 3 nu))
            [1:
              >ignore_three_bits_refl %
            |2:
              #ignore_refl >ignore_refl
              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
              >nu_refl %
            ]
          |3:
            #ignore_refl >ignore_refl in ignore_three_bits_refl;
            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
            #nu_refl <nu_refl %
          ]
        |2:
          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
          @sym_eq @vsplit_ok >nu_nl_refl %
        ]
      |2:
        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
        normalize nodelta
        [1:
          cases (eq_bv ???) normalize #absurd destruct(absurd)
        |2:
          #_ %
        ]
      ]
    ]
  ] *)
qed.

lemma special_function_registers_8051_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀ps.
  ∀pc: Word.
    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
      special_function_registers_8051 M cm ps.
  //
qed.

lemma special_function_registers_8052_set_program_counter:
  ∀M: Type[0].
  ∀cm: M.
  ∀ps.
  ∀pc: Word.
    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
      special_function_registers_8052 M cm ps.
  //
qed.

lemma set_index_set_index_commutation:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
  ∀m, o: nat.
  ∀m_lt_proof: m < n.
  ∀o_lt_proof: o < n.
  ∀e, f: A.
    m ≠ o →
      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
  #A #n #v elim v
  [1:
    #m #o #m_lt_proof
    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
  |2:
    #n' #hd #tl #inductive_hypothesis
    #m #o
    cases m cases o
    [1:
      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
      @relevant %
    |2,3:
      #o' normalize //
    |4:
      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
      normalize @eq_f @inductive_hypothesis @nmk #relevant
      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
    ]
  ]
qed.

lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀ps.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀sfr.
  ∀result: Byte.
    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
      special_function_registers_8051 (BitVectorTrie Byte 16)
        (code_memory_of_pseudo_assembly_program cm sigma policy)
        (set_8051_sfr (BitVectorTrie Byte 16)
        (code_memory_of_pseudo_assembly_program cm sigma policy)
        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
      sfr_8051_of_pseudo_sfr_8051 M
        (special_function_registers_8051 pseudo_assembly_program cm
        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
  whd in match (set_8051_sfr ?????);
  cases M #callM * try % #upper_lower #address
  whd in match (special_function_registers_8051 ???);
  whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
  @pair_elim #high #low #high_low_refl normalize nodelta
  cases (eq_upper_lower ??) normalize nodelta
  whd in match (set_8051_sfr ?????);
  @set_index_set_index_commutation @nmk #relevant
  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
qed.

lemma special_function_registers_8051_set_arg_8:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀ps.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀addr1: [[ registr; direct ]].
  ∀result.
    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
    special_function_registers_8051 (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      (set_arg_8 (BitVectorTrie Byte 16)
        (code_memory_of_pseudo_assembly_program cm sigma policy)
        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
   sfr_8051_of_pseudo_sfr_8051 M
     (special_function_registers_8051 pseudo_assembly_program cm
     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
  cases daemon
(*
  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
  #M #cm #ps #sigma #policy #addr1 #result
  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?); 
  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
  cases (vsplit bool ???) #nu #nl normalize nodelta
  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
  cases (get_index_v bool ????) normalize nodelta try %
  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: % ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  inversion (eqb ??) #eqb_refl normalize nodelta [1:
    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
    whd in match (status_of_pseudo_status ?????);
    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
  ]
  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
  cases not_implemented *)
qed.