include "ASM/Assembly.ma".
include "ASM/Interpret.ma".
include "ASM/StatusProofs.ma".
include alias "arithmetics/nat.ma".
include "ASM/AssemblyProof.ma".

lemma let_pair_in_status_of_pseudo_status:
  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    c' = c →
    (∀left, right.
      s' left right c' = status_of_pseudo_status M cm (s left right c') sigma policy) →
    (let 〈left, right〉 ≝ c' in s' left right c') =
    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
qed.

lemma let_pair_as_in_status_of_pseudo_status:
  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    c' = c →
    (∀left, right, H, H'. s' left right H' c' = status_of_pseudo_status M cm (s left right H c) sigma policy) →
    (let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
  destruct(destruct_refl) /2/
qed.

lemma if_then_else_status_of_pseudo_status:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀s, s', s'', s'''.
  ∀t, t': bool.
    t = t' →
    s' = status_of_pseudo_status M cm s sigma policy →
    s''' = status_of_pseudo_status M cm s'' sigma policy →
      if t then
        s'
      else
        s''' =
      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
qed.

lemma set_program_counter_status_of_pseudo_status:
  ∀M.
  ∀cm.
  ∀sigma.
  ∀policy.
  ∀s, s'.
  ∀new_ppc, new_ppc'.
    sigma new_ppc = new_ppc' →
    s' = status_of_pseudo_status M cm s sigma policy →
    set_program_counter (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' new_ppc' =
    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
  #new_ppc_refl #s_refl <new_ppc_refl >s_refl //
qed.

lemma set_p1_latch_status_of_pseudo_status:
  ∀M.
  ∀code_memory.
  ∀sigma.
  ∀policy.
  ∀s,s'.
  ∀v.
   s' = status_of_pseudo_status M code_memory s sigma policy →
    set_p1_latch (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
      s' v =
    status_of_pseudo_status M code_memory
      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
  #M #cm #sigma #policy #s #s' #new_ppc #s_refl >s_refl //
qed.

lemma set_p3_latch_status_of_pseudo_status:
  ∀M.
  ∀code_memory.
  ∀sigma.
  ∀policy.
  ∀s, s'.
  ∀v.
  s' = status_of_pseudo_status M code_memory s sigma policy →
    set_p3_latch (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
      s' v =
    status_of_pseudo_status M code_memory
      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
  #M #code_memory #sigma #policy #s #s' #v #s_refl >s_refl //
qed.

definition map_address_using_internal_pseudo_address_map:
    ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝
  λM, sigma, sfr, v.
  match sfr with
  [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v
  | _         ⇒ v
  ].

lemma set_index_set_index_overwrite:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
  ∀index: nat.
  ∀e, e': A.
  ∀proof.
  ∀proof'.
    set_index A n v index e proof =
      set_index A n (set_index A n v index e' proof') index e proof.
  #A #n #v elim v normalize
  [1:
    #index #e #e' #absurd cases (lt_to_not_zero … absurd)
  |2:
    #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof'
    normalize //
  ]
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.

(* XXX: move elsewhere *)
lemma get_index_v_set_index_miss:
  ∀a: Type[0].
  ∀n: nat.
  ∀v: Vector a n.
  ∀i, j: nat.
  ∀e: a.
  ∀i_proof: i < n.
  ∀j_proof: j < n.
    i ≠ j →
      get_index_v a n (set_index a n v i e i_proof) j j_proof =
        get_index_v a n v j j_proof.
  #a #n #v elim v
  [1:
    #i #j #e #i_proof
    cases (lt_to_not_zero … i_proof)
  |2:
    #n' #hd #tl #inductive_hypothesis #i #j
    cases i cases j
    [1:
      #e #i_proof #j_proof #neq_assm
      cases (absurd ? (refl … 0) neq_assm)
    |2,3:
      #i' #e #i_proof #j_proof #_ %
    |4:
      #i' #j' #e #i_proof #j_proof #neq_assm
      @inductive_hypothesis @nmk #eq_assm
      >eq_assm in neq_assm; #neq_assm
      cases (absurd ? (refl ??) neq_assm)
    ]
  ]
qed.

lemma get_index_v_set_index_hit:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
  ∀i: nat.
  ∀e: A.
  ∀i_lt_n_proof: i < n.
  ∀i_lt_n_proof': i < n.
    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
  #A #n #v elim v
  [1:
    #i #e #i_lt_n_proof
    cases (lt_to_not_zero … i_lt_n_proof)
  |2:
    #n' #hd #tl #inductive_hypothesis #i #e
    cases i
    [1:
      #i_lt_n_proof #i_lt_n_proof' %
    |2:
      #i' #i_lt_n_proof' #i_lt_n_proof''
      whd in ⊢ (??%?); @inductive_hypothesis
    ]
  ]
qed.

lemma set_index_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
(set_index Byte 19
  (special_function_registers_8051 (BitVectorTrie Byte 16)
   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
   (status_of_pseudo_status M code_memory s sigma policy))
  (sfr_8051_index sfr) v' (sfr8051_index_19 sfr)
  =sfr_8051_of_pseudo_sfr_8051 M
   (special_function_registers_8051 pseudo_assembly_program code_memory
    (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma).
  #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
  [1:
    <sfr_neq_acc_a_assm cases sfr
    [18:
      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
      >sndM_refl %
    ]
    %
  |2:
    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    @pair_elim #high #low #high_low_refl normalize nodelta
    whd in match set_8051_sfr; normalize nodelta
    <sfr_neq_acc_a_assm
    cases sfr in high_low_refl sfr_neq_acc_a_assm; 
    [18,37:
      @pair_elim #high' #low' #high_low_refl'
      #high_low_refl
      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
      >sndM_refl normalize nodelta whd in match map_value_using_opt_address_entry; normalize nodelta
      >eq_upper_lower_refl normalize nodelta
      [1:
        #relevant >relevant
        <set_index_set_index_overwrite in ⊢ (??%?);
        <set_index_set_index_overwrite in ⊢ (???%);
        >get_index_v_set_index_hit in high_low_refl'; 
        #assm >assm in relevant; normalize nodelta * %
      |2:
        #relevant >relevant
        <set_index_set_index_overwrite in ⊢ (??%?);
        <set_index_set_index_overwrite in ⊢ (???%);
        >get_index_v_set_index_hit in high_low_refl'; 
        #assm >assm in relevant; normalize nodelta * %
      ]
    ]
    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    #relevant * >get_index_v_set_index_miss
    try (% #absurd normalize in absurd; destruct(absurd))
    >relevant normalize nodelta
    @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
  ]
qed.

lemma get_index_v_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, s', sfr.
    map_address_using_internal_pseudo_address_map M sigma sfr
      (get_index_v Byte 19
        (special_function_registers_8051 pseudo_assembly_program code_memory s)
        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
    get_index_v Byte 19
      (special_function_registers_8051 (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
      (status_of_pseudo_status M code_memory s sigma policy))
      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
 [1:
    cases sfr
    [18:
      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
      >sndM_refl %
    ]
    %
  |2:
   inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    @pair_elim #high #low #high_low_refl normalize nodelta
    cases sfr
    [18,37:
      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
      whd in match map_value_using_opt_address_entry; normalize nodelta
      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
      >eq_upper_lower_refl normalize nodelta
      whd in match (set_8051_sfr ?????); //
    ]
    @get_index_v_set_index_miss whd in ⊢ (?(??%%));
    @nmk #absurd destruct(absurd)
  ]
qed.

lemma set_8051_sfr_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
    s' = status_of_pseudo_status M code_memory s sigma policy →
    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
      status_of_pseudo_status M code_memory
        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
  >s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
qed.

(*lemma get_8051_sfr_status_of_pseudo_status:
  ∀M.
  ∀cm, ps, sigma, policy.
  ∀sfr.
    (sfr = SFR_ACC_A → \snd M = None …) →
    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 #address
  cases (eq_upper_lower ??) normalize nodelta
  @pair_elim #upper #lower #upper_lower_refl
  @get_index_v_set_index_miss @nmk #relevant
  normalize in relevant; destruct(relevant)
qed.*)

lemma get_8051_sfr_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    s' = status_of_pseudo_status M code_memory s sigma policy →
    map_address_using_internal_pseudo_address_map M sigma sfr
     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
  get_8051_sfr (BitVectorTrie Byte 16)
    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     s' sfr = s''.
  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' >s_refl <s_refl'
  whd in match get_8051_sfr; normalize nodelta
  @get_index_v_status_of_pseudo_status %
qed.

lemma get_8052_sfr_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, s', sfr.
  s' = status_of_pseudo_status M code_memory s sigma policy →
  (get_8052_sfr (BitVectorTrie Byte 16)
    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    s' sfr =
   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
  #M #code_memory #sigma #policy #s #s' #sfr #s_refl >s_refl //
qed.

lemma set_8052_sfr_status_of_pseudo_status:
  ∀M, code_memory, sigma, policy, s, s', sfr, v.
  s' = status_of_pseudo_status M code_memory s sigma policy →
    (set_8052_sfr (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
    status_of_pseudo_status M code_memory
     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl >s_refl //
qed.
  
definition map_address_Byte_using_internal_pseudo_address_map ≝
 λM,sigma,d,v.
  match sfr_of_Byte d with
  [ None ⇒ v
  | Some sfr8051_8052 ⇒
    match sfr8051_8052 with
    [ inl sfr ⇒
      map_address_using_internal_pseudo_address_map M sigma sfr v
    | inr _ ⇒ v
    ]
  ].

lemma set_bit_addressable_sfr_status_of_pseudo_status':
  let M ≝ pseudo_assembly_program in
    ∀code_memory: M.
    ∀s: PreStatus M code_memory.
    ∀d: Byte.
    ∀v: Byte.
      Σp: PreStatus M code_memory.
        ∀M.
        ∀sigma.
        ∀policy.
        ∀s'.
        ∀v'.
          s' = status_of_pseudo_status M code_memory s sigma policy →
            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
                (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
              status_of_pseudo_status M code_memory
                (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
  whd in match map_address_Byte_using_internal_pseudo_address_map;
  whd in match set_bit_addressable_sfr;
  normalize nodelta
  @(let M ≝ pseudo_assembly_program in
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
  λv: Byte.
   match sfr_of_Byte b with
   [ None ⇒ match not_implemented in False with [ ]
   | Some sfr8051_8052 ⇒
      match sfr8051_8052 with
      [ inl sfr ⇒
         match sfr with
         [ SFR_P1 ⇒
           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
           set_p1_latch ?? s v
         | SFR_P3 ⇒
           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
           set_p3_latch ?? s v
         | _ ⇒ set_8051_sfr ?? s sfr v ]
      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
  normalize nodelta #M #sigma #policy #s' #v' #s_refl >s_refl
  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
  #v_refl >v_refl //
qed.

lemma set_bit_addressable_sfr_status_of_pseudo_status:
 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
  s' = status_of_pseudo_status M code_memory s sigma policy →
  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
  s' d v'
  =status_of_pseudo_status M code_memory
   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
 #H @H
qed.

lemma set_low_internal_ram_status_of_pseudo_status:
 ∀cm,sigma,policy,M,s,s',ram.
  s' = status_of_pseudo_status M cm s sigma policy →
  set_low_internal_ram (BitVectorTrie Byte 16)
  (code_memory_of_pseudo_assembly_program cm sigma policy)
  s'
  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
  = status_of_pseudo_status M cm
    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
  #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
qed.

(* Real axiom ATM *)
axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
 ∀M,sigma,cm,s,addr,v,v'.
 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
  insert Byte 7 addr v'
  (low_internal_ram_of_pseudo_low_internal_ram M sigma
   (low_internal_ram pseudo_assembly_program cm s))
  =low_internal_ram_of_pseudo_low_internal_ram M sigma
   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
               
lemma insert_low_internal_ram_status_of_pseudo_status:
 ∀M,cm,sigma,policy,s,addr,v,v'.
 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
  insert Byte 7 addr v'
   (low_internal_ram (BitVectorTrie Byte 16)
    (code_memory_of_pseudo_assembly_program cm sigma policy)
    (status_of_pseudo_status M cm s sigma policy))
  = low_internal_ram_of_pseudo_low_internal_ram M sigma
     (insert Byte 7 addr v
      (low_internal_ram pseudo_assembly_program cm s)).
 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
qed.

(* Real axiom ATM *)
axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
 ∀M,sigma,cm,s,addr,v,v'.
 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
  insert Byte 7 addr v'
  (high_internal_ram_of_pseudo_high_internal_ram M sigma
   (high_internal_ram pseudo_assembly_program cm s))
  =high_internal_ram_of_pseudo_high_internal_ram M sigma
   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).

lemma insert_high_internal_ram_status_of_pseudo_status:
 ∀M,cm,sigma,policy,s,addr,v,v'.
 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
  insert Byte 7 addr v'
   (high_internal_ram (BitVectorTrie Byte 16)
    (code_memory_of_pseudo_assembly_program cm sigma policy)
    (status_of_pseudo_status M cm s sigma policy))
  = high_internal_ram_of_pseudo_high_internal_ram M sigma
     (insert Byte 7 addr v
      (high_internal_ram pseudo_assembly_program cm s)).
 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
qed.

lemma bit_address_of_register_status_of_pseudo_status:
 ∀M,cm,s,sigma,policy,r.
  bit_address_of_register …
  (code_memory_of_pseudo_assembly_program cm sigma policy)
  (status_of_pseudo_status M cm s sigma policy) r =
  bit_address_of_register … cm s r.
 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
 @pair_elim #un #ln #_
 @pair_elim #r1 #r0 #_ %
qed.

(*CSC: provable using the axiom in AssemblyProof, but this one seems more
  primitive *)
axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
 ∀M,sigma,cm,s,s',addr.
  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
  (lookup Byte 7 addr
   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
  lookup Byte 7 addr
  (low_internal_ram_of_pseudo_low_internal_ram M sigma
   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
  = s'.

(*CSC: provable using the axiom in AssemblyProof, but this one seems more
  primitive *)
axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
 ∀M,sigma,cm,s,s',addr.
  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
  (lookup Byte 7 addr
   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
  lookup Byte 7 addr
  (high_internal_ram_of_pseudo_high_internal_ram M sigma
   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
  = s'.

lemma get_register_status_of_pseudo_status:
 ∀M,cm,sigma,policy,s,s',s'',r.
  status_of_pseudo_status M cm s sigma policy = s' →
  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
   (get_register … cm s r) = s'' →
  get_register …
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   s' r = s''.
 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
 whd in match get_register; normalize nodelta
 whd in match status_of_pseudo_status; normalize nodelta
 >bit_address_of_register_status_of_pseudo_status
 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
qed.

lemma external_ram_status_of_pseudo_status:
 ∀M,cm,s,sigma,policy.
  external_ram …
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   (status_of_pseudo_status M cm s sigma policy) =
  external_ram … cm s.
 //
qed.

lemma set_external_ram_status_of_pseudo_status:
  ∀M,cm,ps,sigma,policy,ram.
    set_external_ram …
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      (status_of_pseudo_status M cm ps sigma policy)
      ram =
    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
  //
qed.

lemma set_register_status_of_pseudo_status:
 ∀M,sigma,policy,cm,s,s',r,v,v'.
  s' = status_of_pseudo_status M cm s sigma policy →
  map_internal_ram_address_using_pseudo_address_map M sigma
   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
  set_register (BitVectorTrie Byte 16)
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   s' r v'
  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
    sigma policy.
  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl >s_refl #v_ok
 whd in match set_register; normalize nodelta
 >bit_address_of_register_status_of_pseudo_status
 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
 @set_low_internal_ram_status_of_pseudo_status %
qed.

definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
  let 〈low,high,accA〉 ≝ M in
  match addr with
  [ INDIRECT i ⇒
     lookup_opt …
      (bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None …
  | EXT_INDIRECT e ⇒
     lookup_opt …
      (bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None …
  | ACC_DPTR ⇒
    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
            in the ACC_A *)
      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
        get_8051_sfr … cm s SFR_ACC_A
  | ACC_PC ⇒
      (* XXX: as above *)
      map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) =
        get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s
  | _ ⇒ True ].

definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
  match addr with
  [ DIRECT d ⇒
     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
     match head' … bit_one with
     [ true ⇒
      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
     | false ⇒
      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
  | INDIRECT i ⇒
     let register ≝ get_register ?? s [[ false; false; i ]] in
     map_internal_ram_address_using_pseudo_address_map M sigma register v
  | REGISTER r ⇒
     map_internal_ram_address_using_pseudo_address_map M sigma
      (false:::bit_address_of_register … s r) v
  | ACC_A ⇒
     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
  | _ ⇒ v ].

(*CSC: move elsewhere*)
lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
 #A #n #v inversion v in ⊢ ?;
 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
qed.

(*CSC: move elsewhere*)
lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
 #A #v inversion v in ⊢ ?;
 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
   /2 by jmeq_to_eq/
 ]
qed.

(*CSC: move elsewhere*)
lemma eq_cons_head_append:
 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
  head' A 0 hd:::tl = hd@@tl.
 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
qed.

lemma set_arg_8_status_of_pseudo_status':
  ∀cm.
  ∀ps.
  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
   s' = status_of_pseudo_status M cm ps sigma policy →
   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
    set_arg_8 (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' addr value' =
    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
  whd in match set_arg_8; normalize nodelta
  @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ;
                                   acc_a ; acc_b ; ext_indirect ;
                                   ext_indirect_dptr ]]. λv.
    match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
                                                acc_a ; acc_b ; ext_indirect ;
                                                ext_indirect_dptr ]] addr) →
                   Σp.?
            with
      [ DIRECT d ⇒
        λdirect: True.
          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
            match head' … bit_one with
              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
              | false ⇒
                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory
              ]
              
      | INDIRECT i ⇒
        λindirect: True.
          let register ≝ get_register ?? s [[ false; false; i ]] in
          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
            match head' … bit_one with
              [ false ⇒
                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory
              | true ⇒ 
                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
                  set_high_internal_ram ?? s memory
              ]
      | REGISTER r ⇒ λregister: True. set_register ?? s r v
      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]] in
          let padded_address ≝ pad 8 8 address in
          let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
            set_external_ram ?? s memory
      | EXT_INDIRECT_DPTR ⇒
        λext_indirect_dptr: True.
          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
          let memory ≝ insert ? 16 address v (external_ram ?? s) in
            set_external_ram ?? s memory
      | _ ⇒ 
        λother: False.
          match other in False with [ ]
      ] (subaddressing_modein … a)) normalize nodelta
  #M #sigma #policy #s' #v' #s_refl >s_refl
  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
  [1,2:
    <vsplit_refl normalize nodelta >p normalize nodelta
    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
  |3,4: cases M * -M #low #high #accA normalize nodelta
      #EQ1 #EQ2 change with (get_register ????) in match register in p;
      >(get_register_status_of_pseudo_status … (refl …) (refl …))
      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
      whd in match (lookup_from_internal_ram ??);
      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
  |5: cases M * -M #low #high #accA normalize nodelta
      #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
      whd in match lookup_from_internal_ram; normalize nodelta
      >EQ1 normalize nodelta
      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
  |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/
  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
qed.

lemma set_arg_8_status_of_pseudo_status:
  ∀cm.
  ∀ps.
  ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
  ∀value.
  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
   addr = addr' →
   s' = status_of_pseudo_status M cm ps sigma policy →
   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
    set_arg_8 (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' addr value' =
    status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
  #cm #ps #addr #addr' #value
  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
  #M #sigma #policy #s' #value' #addr_refl <addr_refl
  @relevant
qed.

lemma p1_latch_status_of_pseudo_status:
    ∀M.
    ∀sigma.
    ∀policy.
    ∀code_memory: pseudo_assembly_program.
    ∀s: PreStatus … code_memory.
    ∀s'.
    s' = status_of_pseudo_status M code_memory s sigma policy →
    (p1_latch (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
      s' =
    (p1_latch pseudo_assembly_program code_memory s)).
  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
qed.

lemma p3_latch_status_of_pseudo_status:
    ∀M.
    ∀sigma.
    ∀policy.
    ∀code_memory: pseudo_assembly_program.
    ∀s: PreStatus … code_memory.
    ∀s'.
    s' = status_of_pseudo_status M code_memory s sigma policy →
    (p3_latch (BitVectorTrie Byte 16)
      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
      (status_of_pseudo_status M code_memory s sigma policy) =
    (p3_latch pseudo_assembly_program code_memory s)).
  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
qed.

lemma get_bit_addressable_sfr_status_of_pseudo_status':
  let M ≝ pseudo_assembly_program in
    ∀code_memory: M.
    ∀s: PreStatus M code_memory.
    ∀d: Byte.
    ∀l: bool.
      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
        s' = status_of_pseudo_status M code_memory s sigma policy →
        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
          s' d l =
        map_address_Byte_using_internal_pseudo_address_map M sigma
         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
  whd in match get_bit_addressable_sfr;
  whd in match map_address_Byte_using_internal_pseudo_address_map;
  normalize nodelta
  @(let M ≝ pseudo_assembly_program in
    λcode_memory:M.
    λs: PreStatus M code_memory.
    λb: Byte.
    λl: bool.
    match sfr_of_Byte b with
    [ None ⇒ match not_implemented in False with [ ]
    | Some sfr8051_8052 ⇒
    match sfr8051_8052 with
    [ inl sfr ⇒
      match sfr with
      [ SFR_P1 ⇒
        if l then
          p1_latch … s
        else
          get_8051_sfr … s SFR_P1
      | SFR_P3 ⇒
        if l then
          p3_latch … s
        else
          get_8051_sfr … s SFR_P3
      | _ ⇒ get_8051_sfr … s sfr
      ]
    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
    ]
    ])
  #M #sigma #policy #s' #s_refl >s_refl normalize nodelta
  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
qed.

lemma get_bit_addressable_sfr_status_of_pseudo_status:
  let M ≝ pseudo_assembly_program in
    ∀code_memory: M.
    ∀s: PreStatus M code_memory.
    ∀d: Byte.
    ∀l: bool.
    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
      map_address_Byte_using_internal_pseudo_address_map M sigma
         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
      s' = status_of_pseudo_status M code_memory s sigma policy →
        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
          s' d l) = s''.
 #code #s #d #v
 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl >s_refl' @relevant %
qed.

lemma program_counter_status_of_pseudo_status:
    ∀M. ∀sigma: Word → Word. ∀policy.
    ∀code_memory: pseudo_assembly_program.
    ∀s: PreStatus ? code_memory.
    ∀s'.
    ∀s''.
    sigma (program_counter … s) = s'' →
    s' = status_of_pseudo_status M code_memory s sigma policy →
      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
        s' = s''.
  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl >s_refl' //
qed.

lemma get_cy_flag_status_of_pseudo_status:
  ∀M, cm, sigma, policy, s, s'.
  s' = status_of_pseudo_status M cm s sigma policy →
  (get_cy_flag (BitVectorTrie Byte 16)
    (code_memory_of_pseudo_assembly_program cm sigma policy)
    s' =
  get_cy_flag pseudo_assembly_program cm s).
  #M #cm #sigma #policy #s #s' #s_refl >s_refl
  whd in match get_cy_flag; normalize nodelta
  >(get_index_v_status_of_pseudo_status … (refl …)) %
qed.

lemma get_arg_8_status_of_pseudo_status':
  ∀cm.
  ∀ps.
  ∀l.
  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
      s' = status_of_pseudo_status M cm ps sigma policy →
      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' l addr =
      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
  whd in match get_arg_8; normalize nodelta
  @(let m ≝ pseudo_assembly_program in
    λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]].
    match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with
      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
      | DATA d ⇒ λdata: True. d
      | REGISTER r ⇒ λregister: True. get_register ?? s r
      | EXT_INDIRECT_DPTR ⇒
        λext_indirect_dptr: True.
          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]]  in
          let padded_address ≝ pad 8 8 address in
            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
      | ACC_DPTR ⇒
        λacc_dptr: True.
          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | ACC_PC ⇒
        λacc_pc: True.
          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | DIRECT d ⇒
        λdirect: True.
          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
            match head' … hd with
            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
            ]
      | INDIRECT i ⇒
        λindirect: True.
          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
            match head' … hd with
            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
            ]
      | _ ⇒ λother: False.
        match other in False with [ ]
      ] (subaddressing_modein … a)) normalize nodelta
  #M #sigma #policy #s' #s_refl >s_refl
  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
  [1:
    #_ >p normalize nodelta >p1 normalize nodelta
    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
  |2:
    #_>p normalize nodelta >p1 normalize nodelta
    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
  |3,4: cases M -M * #low #high #accA
    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    whd in match lookup_from_internal_ram; normalize nodelta
    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
    [1:
      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma)
    |2:
      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma)
    ]
    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
  |5: cases M -M * #low #high #accA
    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    whd in match lookup_from_internal_ram; normalize nodelta
    >assoc_list_assm normalize nodelta %
  |6,7,8,9:
    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
  |10: cases M -M * #low #high #accA
    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    >acc_a_assm >p normalize nodelta //
  |11: cases M -M * #low #high #accA
    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    >sigma_assm >map_acc_a_assm >p normalize nodelta //
  |12:
    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    >external_ram_status_of_pseudo_status //
  ]
qed.

lemma get_arg_8_status_of_pseudo_status:
  ∀cm.
  ∀ps.
  ∀l.
  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
  ∀M. ∀sigma. ∀policy. ∀s', s''.
      s' = status_of_pseudo_status M cm ps sigma policy →
      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' l addr = s''.
  #cm #ps #l #addr
  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
  @relevant assumption
qed.

lemma get_arg_16_status_of_pseudo_status:
  ∀cm.
  ∀ps.
  ∀addr: [[data16]].
  ∀M. ∀sigma. ∀policy. ∀s'.
    s' = status_of_pseudo_status M cm ps sigma policy →
      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' addr =
      (get_arg_16 … cm ps addr).
  #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
qed.

lemma set_arg_16_status_of_pseudo_status:
  ∀cm.
  ∀ps.
  ∀addr,addr': [[dptr]].
  ∀v,v': Word.
  ∀M. ∀sigma. ∀policy. ∀s'.
    s' = status_of_pseudo_status M cm ps sigma policy →
    v=v' → addr=addr' →
      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' v' addr' =
      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl >s_refl #addr_refl
  <addr_refl #v_refl <v_refl 
  @(subaddressing_mode_elim … addr)
  whd in match set_arg_16; normalize nodelta
  whd in match set_arg_16'; normalize nodelta
  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
  @set_8051_sfr_status_of_pseudo_status try %
  @set_8051_sfr_status_of_pseudo_status %
qed.

definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
  match addr with
  [ BIT_ADDR b ⇒
    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
    match head' … bit_1 with
    [ true ⇒
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
      let trans ≝ true:::four_bits @@ [[false; false; false]] in
        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
    | false ⇒
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
      let address' ≝ [[true; false; false]]@@four_bits in
      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
      map_internal_ram_address_using_pseudo_address_map M sigma
          (false:::address') t = t
    ]
  | N_BIT_ADDR b ⇒
    let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
    match head' … bit_1 with
    [ true ⇒
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
      let trans ≝ true:::four_bits @@ [[false; false; false]] in
        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
    | false ⇒
      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
      let address' ≝ [[true; false; false]]@@four_bits in
      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
      map_internal_ram_address_using_pseudo_address_map M sigma
          (false:::address') t = t
    ]
  | _ ⇒ True ].

lemma get_arg_1_status_of_pseudo_status':
  ∀cm.
  ∀ps.
  ∀addr: [[bit_addr; n_bit_addr; carry]].
  ∀l.
    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
      s' = status_of_pseudo_status M cm ps sigma policy →
      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' addr l =
      (get_arg_1 … cm ps addr l).
  whd in match get_arg_1; normalize nodelta
  @(let m ≝ pseudo_assembly_program in
    λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl.
    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
                                                 n_bit_addr ;
                                                 carry ]] x) → Σb: bool. ? with
      [ BIT_ADDR b ⇒
        λbit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
        match head' … bit_1 with
        [ true ⇒
          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
            get_index_v … sfr (nat_of_bitvector … three_bits) ?
        | false ⇒
          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
            get_index_v … t (nat_of_bitvector … three_bits) ?
        ]
      | N_BIT_ADDR n ⇒
        λn_bit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
        match head' … bit_1 with
        [ true ⇒
          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
        | false ⇒
          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
        ]
      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
      | _ ⇒ λother.
        match other in False with [ ]
      ] (subaddressing_modein … a)) normalize nodelta
  [4,5,8,9: //]
  #M #sigma #policy #s' #s_refl >s_refl
  [1:
    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
  |2,4:
    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2
    normalize nodelta
    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
    >map_address_assm %
  |3,5:
    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta
    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    #map_address_assm >map_address_assm %
  ]
qed.

lemma get_arg_1_status_of_pseudo_status:
  ∀cm.
  ∀ps.
  ∀addr, addr': [[bit_addr; n_bit_addr; carry]].
  ∀l.
  ∀M. ∀sigma. ∀policy. ∀s'.
    addr = addr' →
    s' = status_of_pseudo_status M cm ps sigma policy →
      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s' addr l =
      (get_arg_1 … cm ps addr' l).
  #cm #ps #addr #addr' #l
  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
  #M #sigma #policy #s' #addr_refl <addr_refl
  @assm
qed.

(*CSC: daemon
definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
  λM: internal_pseudo_address_map.
  λcm: pseudo_assembly_program.
  λs: PreStatus ? cm.
  λsigma: Word → Word.
  λaddr: [[bit_addr; carry]].
  λv: Bit.
  match addr with
  [ BIT_ADDR b ⇒
    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    match head' … bit_1 with
    [ true ⇒
      let address ≝ nat_of_bitvector … seven_bits in
      let d ≝ address ÷ 8 in
      let m ≝ address mod 8 in
      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
      let sfr ≝ get_bit_addressable_sfr … s t true in
        map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr
    | false ⇒
      let address ≝ nat_of_bitvector … seven_bits in
      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
        map_internal_ram_address_using_pseudo_address_map M sigma
          (false:::address') t = t
    ]   
  | CARRY ⇒ True
  | _ ⇒ True
  ].

definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝
  λM: internal_pseudo_address_map.
  λcm: pseudo_assembly_program.
  λs: PreStatus ? cm.
  λsigma: Word → Word.
  λaddr: [[bit_addr; carry]].
  λv: Bit.
  match addr with
  [ BIT_ADDR b ⇒
    let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
    match head' … bit_1 with
    [ true ⇒
      let address ≝ nat_of_bitvector … seven_bits in
      let d ≝ address ÷ 8 in
      let m ≝ address mod 8 in
      let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
      let sfr ≝ get_bit_addressable_sfr … s t true in
      let new_sfr ≝ set_index … sfr m v ? in
        map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t
    | false ⇒
      let address ≝ nat_of_bitvector … seven_bits in
      let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
      let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
      let n_bit ≝ set_index … t (modulus address 8) v ? in
      let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
        map_internal_ram_address_using_pseudo_address_map M sigma
          (false:::address') n_bit = n_bit
    ]   
  | CARRY ⇒ True
  | _ ⇒ True
  ].
  @modulus_less_than
qed.

lemma set_arg_1_status_of_pseudo_status':
  ∀cm: pseudo_assembly_program.
  ∀ps: PreStatus pseudo_assembly_program cm.
  ∀addr: [[bit_addr; carry]].
  ∀b: Bit.
    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
      b = b' →
      status_of_pseudo_status M cm ps sigma policy = s' →
      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
        set_arg_1 (BitVectorTrie Byte 16)
          (code_memory_of_pseudo_assembly_program cm sigma policy)
          s' addr b =
        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
  whd in match set_arg_1; normalize nodelta
  whd in ⊢ (? → ? → ? → ? → ??(λx.? → ? → ? → ? → ? → ? → ? → %?????? → %?????? → ?));
  normalize nodelta
  @(let m ≝ pseudo_assembly_program in
    λcm.
    λs: PreStatus m cm.
    λa: [[bit_addr; carry]].
    λv: Bit.
    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with
      [ BIT_ADDR b ⇒ λbit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
        match head' … bit_1 with
        [ true ⇒
          let address ≝ nat_of_bitvector … seven_bits in
          let d ≝ address ÷ 8 in
          let m ≝ address mod 8 in
          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
          let sfr ≝ get_bit_addressable_sfr … s t true in
          let new_sfr ≝ set_index … sfr m v ? in
            set_bit_addressable_sfr … s new_sfr t
        | false ⇒
          let address ≝ nat_of_bitvector … seven_bits in
          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
          let n_bit ≝ set_index … t (modulus address 8) v ? in
          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
            set_low_internal_ram … s memory
        ]
      | CARRY ⇒
        λcarry: True.
        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
        let new_psw ≝ v:::seven_bits in
          set_8051_sfr ?? s SFR_PSW new_psw
      | _ ⇒
        λother: False.
          match other in False with
            [ ]
      ] (subaddressing_modein … a)) normalize nodelta
  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
  [1:
    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
  |2,3:
    >p normalize nodelta >p1 normalize nodelta
    #map_bit_address_assm_1 #map_bit_address_assm_2
    [1:
      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
      >map_bit_address_assm_1
      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
    |2:
      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
      >map_bit_address_assm_1
      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
      >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); %
    ]
  ]
qed.

lemma set_arg_1_status_of_pseudo_status:
  ∀cm: pseudo_assembly_program.
  ∀ps: PreStatus pseudo_assembly_program cm.
  ∀addr: [[bit_addr; carry]].
  ∀b: Bit.
  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
      b = b' →
      status_of_pseudo_status M cm ps sigma policy = s' →
      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
        set_arg_1 (BitVectorTrie Byte 16)
          (code_memory_of_pseudo_assembly_program cm sigma policy)
          s' addr b =
        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
  #cm #ps #addr #b
  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
  @relevant
qed.*)

lemma clock_status_of_pseudo_status:
 ∀M,cm,sigma,policy,s,s'.
  s' = status_of_pseudo_status M cm s sigma policy →
  clock …
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   s'
  = clock … cm s.
  #M #cm #sigma #policy #s #s' #s_refl >s_refl //
qed.

lemma set_clock_status_of_pseudo_status:
 ∀M,cm,sigma,policy,s,s',v,v'.
 s' = status_of_pseudo_status M cm s sigma policy →
 v = v' →
  set_clock …
   (code_memory_of_pseudo_assembly_program cm sigma policy)
   s' v
  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl >s_refl <v_refl //
qed.

lemma set_flags_status_of_pseudo_status:
  ∀M.
  ∀sigma.
  ∀policy.
  ∀code_memory: pseudo_assembly_program.
  ∀s: PreStatus ? code_memory.
  ∀s'.
  ∀b, b': Bit.
  ∀opt, opt': option Bit.
  ∀c, c': Bit.
    b = b' →
    opt = opt' →
    c = c' →
    s' = status_of_pseudo_status M code_memory s sigma policy →
      set_flags … s' b opt c =
        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
  ** #low #high #accA #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl >s_refl
  whd in match set_flags; normalize nodelta
  @set_8051_sfr_status_of_pseudo_status try %
  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]  
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]  
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
  %
qed.

lemma get_ac_flag_status_of_pseudo_status:
  ∀M: internal_pseudo_address_map.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀code_memory: pseudo_assembly_program.
  ∀s: PreStatus ? code_memory.
  ∀s'.
    s' = status_of_pseudo_status M code_memory s sigma policy →
      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
  whd in match get_ac_flag; normalize nodelta
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  cases (\snd M) try % normalize nodelta ** normalize nodelta
  #address
  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
  whd in match sfr_8051_index; normalize nodelta
  >get_index_v_set_index_miss [2,4: /2/] %
qed.

lemma get_ov_flag_status_of_pseudo_status:
  ∀M: internal_pseudo_address_map.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀code_memory: pseudo_assembly_program.
  ∀s: PreStatus ? code_memory.
  ∀s'.
    s' = status_of_pseudo_status M code_memory s sigma policy →
      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
  whd in match get_ov_flag; normalize nodelta
  whd in match status_of_pseudo_status; normalize nodelta
  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
  cases (\snd M) try %
  ** normalize nodelta #address
  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
  whd in match sfr_8051_index; normalize nodelta
  >get_index_v_set_index_miss [2,4: /2/] %
qed.

(*CSC: useless?
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]].
    assert_data 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 (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
        [1:
          #absurd destruct(absurd)
        |2:
          * normalize nodelta
          [1:
          |2:
            #_ #absurd destruct(absurd)
          ]
        #absurd try % @sym_eq assumption
      ]
    ]
  |2:
    #addressing_mode_ok_refl whd in ⊢ (??%?);
    @pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX 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 addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
  ∀M, cm, ps, sigma, x.
  ∀addr1: [[acc_a]].
    assert_data pseudo_assembly_program M cm ps addr1=true → 
      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
  #M #cm #ps #sigma #x #addr1
  @(subaddressing_mode_elim … addr1)
  whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//]
  * #upper_lower #address normalize nodelta #absurd destruct(absurd) 
qed.

lemma addressing_mode_ok_to_snd_M_data:
  ∀M, cm, ps.
  ∀addr: [[acc_a]].
  assert_data pseudo_assembly_program M cm ps addr = true →
    \snd M = None ….
  #M #cm #ps #addr
  @(subaddressing_mode_elim … addr)
  whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta
  [ #_ %
  | #addr #abs destruct(abs) ]
qed.

(*(*CSC: move elsewhere*)
lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
  ∀A, B: Type[0].
  ∀e: A.
  ∀the_list: list (A × B).
  ∀eq_f: A → A → bool.
    assoc_list_exists A B e eq_f the_list = true →
      ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
  #A #B #e #the_list #eq_f elim the_list
  [1:
    whd in ⊢ (??%? → ?); #absurd destruct(absurd)
  |2:
    #hd #tl #inductive_hypothesis
    whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
    cases (eq_f (\fst hd) e) normalize nodelta
    [1:
      #_ %{(\snd hd)} %
    |2:
      @inductive_hypothesis
    ]
  ]
qed.

(*CSC: move elsewhere*)
lemma assoc_list_exists_false_to_assoc_list_lookup_None:
  ∀A, B: Type[0].
  ∀e, e': A.
  ∀the_list, the_list': list (A × B).
  ∀eq_f: A → A → bool.
    e = e' →
    the_list = the_list' →
      assoc_list_exists A B e eq_f the_list = false →
        assoc_list_lookup A B e' eq_f the_list' = None ….
  #A #B #e #e' #the_list elim the_list
  [1:
    #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
  |2:
    #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
    whd in ⊢ (??%? → ??%?); <e_refl
    cases (eq_f (\fst hd) e) normalize nodelta
    [1:
      #absurd destruct(absurd)
    |2:
      >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
    ]
  ]
qed.*)

lemma sfr_psw_eq_to_bit_address_of_register_eq:
  ∀A: Type[0].
  ∀code_memory: A.
  ∀status, status', register_address.
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
      bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
  #A #code_memory #status #status' #register_address #sfr_psw_refl
  whd in match bit_address_of_register; normalize nodelta
  <sfr_psw_refl %
qed.

lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
  ∀A: Type[0].
  ∀code_memory: A.
  ∀status, status', register_address.
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
      low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
        get_register A code_memory status register_address = get_register A code_memory status' register_address.
  #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
  whd in match get_register; normalize nodelta <low_internal_ram_refl
  >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
qed.

lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
  ∀M, cm, status, status', sigma.
  ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    assert_data pseudo_assembly_program M cm status addr1 = true →
    map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1.
  * * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl
  @(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w
  whd in ⊢ (??%? → %); whd in match (data_or_address ?????);
  whd in match exists; normalize nodelta
  <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption
  cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
qed.

lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
  ∀M.
  ∀sigma.
  ∀sfr8051.
  ∀b.
    sfr8051 ≠ SFR_ACC_A →
      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
  #M #sigma * #b
  [18:
    #relevant cases (absurd … (refl ??) relevant)
  ]
  #_ %
qed.

lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
  ∀M.
  ∀sigma: Word → Word.
  ∀w: BitVector 8.
  ∀b.
    w ≠ bitvector_of_nat … 224 →
      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
  #M #sigma #w #b #w_neq_assm
  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
  [1:
    #sfr_of_Byte_refl %
  |2:
    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
    @(absurd ?? w_neq_assm)
    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
    whd in match sfr_of_Byte; normalize nodelta
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    #absurd destruct(absurd)
qed.

(*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
  ∀M, sigma, w, b.
    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
  #M #sigma #w #b #assoc_list_exists_assm
  whd in ⊢ (??%?);
  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
qed.*)
    
lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
  ∀M', cm.
  ∀sigma, status, status', b, b'.
  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
    b = b' →
    assert_data pseudo_assembly_program M' cm status addr1 = true →
      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
  @(subaddressing_mode_elim … addr1)
  [1:
    whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high *
    [1:
      normalize nodelta #_ %
    |2:
      * #upper_lower #address normalize nodelta #absurd destruct(absurd)
    ]
  |2: cases M' -M' * #low #high #accA
    #w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??);
    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
    cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
  |4: cases M' -M' * #low #high #accA
    #w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram;
    whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta
    whd in match get_register; normalize nodelta
    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl)
    cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)]
    <low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta
    cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta
    #x try % #abs destruct(abs)
  |3: cases M' -M' * #low #high #accA
    #w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta
    @vsplit_elim #hd #tl #w_refl normalize nodelta
    lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd))
    cases (head' bool ??) normalize nodelta
    [2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????);
        whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????);
        normalize nodelta // #x #abs destruct(abs) ] #EQhd
    >w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta
    [1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_
        normalize in eq_bv_refl; >eq_bv_refl %
    |2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ]
  |5,6,7,8:
    #w try #w' %
  ]
qed.

(*CSC: move elsewhere*)
lemma bv_append_eq_to_eq:
 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
 #A #n #v1 elim v1
 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
qed.

lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀s: PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀addr: [[bit_addr]]. (* XXX: expand as needed *)
  ∀f: bool.
  assert_data pseudo_assembly_program M cm s addr = true →
    map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
  ** #low #high #accA #cm #s #sigma #addr #f
  @(subaddressing_mode_elim … addr) #w
  whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta
  @vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
  @vsplit_elim #four #three #four_three_refl normalize nodelta
  cases (head' bool ??) normalize nodelta
  [1: @eq_bv_elim normalize nodelta
      [1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour %
      |2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map
          try % normalize #EQ @(absurd ?? NEQ)
          cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1
          cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ]
  |2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
      whd in match lookup_from_internal_ram; normalize nodelta
      cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ]
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.
  ** #low #high * [2: * #upper_lower #addr] #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
  whd in match (set_8051_sfr ?????);
  whd in match (special_function_registers_8051 ???);
  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta try %
  cases upper_lower normalize nodelta whd in match (set_8051_sfr ?????);
  >get_index_v_set_index_miss [2,4: @eqb_false_to_not_eq assumption]
  @vsplit_elim #h #l #h_l_refl normalize nodelta
  @set_index_set_index_commutation @eqb_false_to_not_eq assumption
qed.

(*
lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀s, s': PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
  ∀f: bool.
  s = s' →
  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
    map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
  @(subaddressing_mode_elim … addr) [1: #w ]
  whd in ⊢ (??%? → %); [2: #_ @I ]
  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
  cases (head' bool ??) normalize nodelta
  [1:
    #eq_accumulator_assm whd in ⊢ (??%?);
    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
    whd in ⊢ (??%?);
    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
  |2:
    #assoc_list_exists_assm whd in ⊢ (??%?);
    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
    whd in assoc_list_exists_assm:(???%);
    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
  ]
qed.

lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
  ∀M: internal_pseudo_address_map.
  ∀cm: pseudo_assembly_program.
  ∀s, s': PreStatus pseudo_assembly_program cm.
  ∀sigma: Word → Word.
  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
  ∀f: bool.
  s = s' →
  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
    map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
  @(subaddressing_mode_elim … addr) [1: #w ]
  whd in ⊢ (??%? → %); [2: #_ @I ]
  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
  cases (head' bool ??) normalize nodelta
  [1:
    #eq_accumulator_assm whd in ⊢ (??%?);
    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
    whd in ⊢ (??%?);
    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
  |2:
    #assoc_list_exists_assm whd in ⊢ (??%?);
    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
    whd in assoc_list_exists_assm:(???%);
    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
  ]
qed.*)

(*
axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
  ∀M, M', sigma,cm,s,addr,v,v'.
    (∀addr'.
      ((false:::addr) = addr' →
        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
      ((false:::addr) ≠ addr' →
        let 〈callM, accM〉 ≝ M in
        let 〈callM', accM'〉 ≝ M' in
          accM = accM' ∧
            assoc_list_lookup … addr' (eq_bv 8) … callM =
              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
    insert Byte 7 addr v'
      (low_internal_ram_of_pseudo_low_internal_ram M'
      (low_internal_ram pseudo_assembly_program cm s)) =
    low_internal_ram_of_pseudo_low_internal_ram M
      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
*)

(*
lemma write_at_stack_pointer_status_of_pseudo_status:
  ∀M, M'.
  ∀cm.
  ∀sigma.
  ∀policy.
  ∀s, s'.
  ∀new_b, new_b'.
    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
    status_of_pseudo_status M cm s sigma policy = s' →
    write_at_stack_pointer ?? s' new_b' =
    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
  #new_b_refl #s_refl <new_b_refl <s_refl
  whd in match write_at_stack_pointer; normalize nodelta
  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
  [1:
    @eq_f
    whd in match get_8051_sfr; normalize nodelta
    whd in match sfr_8051_index; normalize nodelta
    whd in match status_of_pseudo_status; normalize nodelta
    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    cases (\snd M) [2: * #address ] normalize nodelta
    [1,2:
      cases (vsplit bool ???) #high #low normalize nodelta
      whd in match sfr_8051_index; normalize nodelta
      >get_index_v_set_index_miss %
      #absurd destruct(absurd)
    |3:
      %
    ]
  |2:
    @if_then_else_status_of_pseudo_status try %
    [2:
      @sym_eq <set_low_internal_ram_status_of_pseudo_status
      [1:
        @eq_f2
        [2:
          @insert_low_internal_ram_of_pseudo_low_internal_ram'
    @sym_eq
    [2:
      <set_low_internal_ram_status_of_pseudo_status
      [1:
        @eq_f2
        [2:
          @sym_eq
          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
          [2:
            >new_b_refl
    ]
  ]
qed.*)