include "ASM/Assembly.ma".
include "ASM/Interpret.ma".
include "ASM/StatusProofs.ma".

definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
  λP.
    P true ∧ P false.
 
let rec bitvector_elim_prop_internal
  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
  match m return λm. m ≤ n → BitVector (n - m) → Prop with
  [ O    ⇒ λprf1. λprefix. P ?
  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
  ].
  [ applyS prefix
  | letin res ≝ (bit ::: prefix)
    < (minus_S_S ? ?)
    > (minus_Sn_m ? ?)
  [ @ res
  | @ prf2
  ]
  | /2/
  ].
qed.

definition bitvector_elim_prop ≝
  λn: nat.
  λP: BitVector n → Prop.
    bitvector_elim_prop_internal n P n ? ?.
  [ @ (le_n ?)
  | < (minus_n_n ?)
    @ [[ ]]
  ]
qed.

lemma bool_eq_internal_eq:
  ∀b, c.
    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
  #b #c
  cases b
  [ normalize //
  | normalize
    cases c
    [ normalize //
    | normalize //
    ]
  ]
qed.

definition bit_elim: ∀P: bool → bool. bool ≝
  λP.
    P true ∧ P false.

let rec bitvector_elim_internal
  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
  match m return λm. m ≤ n → BitVector (n - m) → bool with
  [ O    ⇒ λprf1. λprefix. P ?
  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
  ].
  [ applyS prefix
  | letin res ≝ (bit ::: prefix)
    < (minus_S_S ? ?)
    > (minus_Sn_m ? ?)
    [ @ res
    | @ prf2
    ]
  | /2/
  ].
qed.

definition bitvector_elim ≝
  λn: nat.
  λP: BitVector n → bool.
    bitvector_elim_internal n P n ? ?.
  [ @ (le_n ?)
  | < (minus_n_n ?)
    @ [[ ]]
  ]
qed.

lemma super_rewrite2:
 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
  ∀P: ∀m. Vector A m → Prop.
   n=m → v1 ≃ v2 → P n v1 → P m v2.
 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
qed.

lemma vector_cons_append:
  ∀A: Type[0].
  ∀n: nat.
  ∀e: A.
  ∀v: Vector A n.
    e ::: v = [[ e ]] @@ v.
  # A # N # E # V
  elim V
  [ normalize %
  | # NN # AA # VV # IH
    normalize
    %
qed. 

lemma vector_cons_append2:
  ∀A: Type[0].
  ∀n, m: nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀hd: A.
    hd:::(v@@q) = (hd:::v)@@q.
  #A #n #m #v #q
  elim v
  [ #hd %
  | #n' #hd' #tl' #ih #hd' <ih %
  ]
qed.

lemma jmeq_cons_vector_monotone:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v: Vector A m.
  ∀q: Vector A n.
  ∀prf: m = n.
  ∀hd: A.
    v ≃ q → hd:::v ≃ hd:::q.
  #A #m #n #v #q #prf #hd #E
  @(super_rewrite2 A … E)
  [ assumption | @jmrefl ]
qed.

lemma vector_associative_append:
  ∀A: Type[0].
  ∀n, m, o:  nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀r: Vector A o.
    ((v @@ q) @@ r)
    ≃
    (v @@ (q @@ r)).
  #A #n #m #o #v #q #r
  elim v
  [ %
  | #n' #hd #tl #ih
    <(vector_cons_append2 A … hd)
    @jmeq_cons_vector_monotone
    //
  ]
qed.

lemma mem_middle_vector:
  ∀A: Type[0].
  ∀m, o: nat.
  ∀eq: A → A → bool.
  ∀reflex: ∀a. eq a a = true.
  ∀p: Vector A m.
  ∀a: A.
  ∀r: Vector A o.
    mem A eq ? (p@@(a:::r)) a = true.
  # A # M # O # EQ # REFLEX # P # A
  elim P
  [ normalize
    > (REFLEX A)
    normalize
    # H
    %
  | # NN # AA # PP # IH
    normalize
    cases (EQ A AA) //
     @ IH
  ]
qed.

lemma mem_monotonic_wrt_append:
  ∀A: Type[0].
  ∀m, o: nat.
  ∀eq: A → A → bool.
  ∀reflex: ∀a. eq a a = true.
  ∀p: Vector A m.
  ∀a: A.
  ∀r: Vector A o.
    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
  # A # M # O # EQ # REFLEX # P # A
  elim P
  [ #R #H @H
  | #NN #AA # PP # IH #R #H
    normalize
    cases (EQ A AA)
    [ normalize %
    | @ IH @ H
    ]
  ]
qed.

lemma subvector_multiple_append:
  ∀A: Type[0].
  ∀o, n: nat.
  ∀eq: A → A → bool.
  ∀refl: ∀a. eq a a = true.
  ∀h: Vector A o.
  ∀v: Vector A n.
  ∀m: nat.
  ∀q: Vector A m.
    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
  # A # O # N # EQ # REFLEX # H # V
  elim V
  [ normalize
    # M # V %
  | # NN # AA # VV # IH # MM # QQ
    change with (bool_to_Prop (andb ??))
    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
    [ 
    | # HH > HH
      > (vector_cons_append ? ? AA VV)
      change with (bool_to_Prop (subvector_with ??????))
      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
        ?
        (vector_associative_append A ? ? ? QQ [[AA]] VV))
      [ >associative_plus //
      | @IH ]
    ]
    @(mem_monotonic_wrt_append)
    [ @ REFLEX
    | @(mem_monotonic_wrt_append)
      [ @ REFLEX
      | normalize
        > REFLEX
        normalize
        %
      ]
    ]
qed.

lemma vector_cons_empty:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
    [[ ]] @@ v = v.
  # A # N # V
  elim V
  [ normalize %
  | # NN # HH # VV #H %
  ]
qed.

corollary subvector_hd_tl:
  ∀A: Type[0].
  ∀o: nat.
  ∀eq: A → A → bool.
  ∀refl: ∀a. eq a a = true.
  ∀h: A.
  ∀v: Vector A o.
    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
  # A # O # EQ # REFLEX # H # V
  > (vector_cons_append A ? H V)
  < (vector_cons_empty A ? ([[H]] @@ V))
  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
qed.

lemma eq_a_reflexive:
  ∀a. eq_a a a = true.
  # A
  cases A
  %
qed.

lemma is_in_monotonic_wrt_append:
  ∀m, n: nat.
  ∀p: Vector addressing_mode_tag m.
  ∀q: Vector addressing_mode_tag n.
  ∀to_search: addressing_mode.
    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
  # M # N # P # Q # TO_SEARCH
  # H
  elim Q
  [ normalize
    @ H
  | # NN # PP # QQ # IH
    normalize
    cases (is_a PP TO_SEARCH)
    [ normalize
      %
    | normalize
      normalize in IH
      @ IH
    ]
  ]
qed.

corollary is_in_hd_tl:
  ∀to_search: addressing_mode.
  ∀hd: addressing_mode_tag.
  ∀n: nat.
  ∀v: Vector addressing_mode_tag n.
    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
  # TO_SEARCH # HD # N # V
  elim V
  [ # H
    normalize in H;
    cases H
  | # NN # HHD # VV # IH # HH
    > vector_cons_append
    > (vector_cons_append ? ? HHD VV)
    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
    @ HH
  ]
qed.
  
let rec list_addressing_mode_tags_elim
  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
   (l → bool) → bool ] with
  [ VEmpty      ⇒  true  
  | VCons len hd tl ⇒ λP.
    let process_hd ≝
      match hd return λhd. ∀P: hd:::tl → bool. bool with
      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
      | acc_a ⇒ λP.P ACC_A
      | acc_b ⇒ λP.P ACC_B
      | dptr ⇒ λP.P DPTR
      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
      | acc_dptr ⇒ λP.P ACC_DPTR
      | acc_pc ⇒ λP.P ACC_PC
      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
      | carry ⇒ λP.P CARRY
      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
      ]
    in
      andb (process_hd P)
       (match len return λx. x = len → bool with
         [ O ⇒ λprf. true
         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
  ].
  try %
  [ 2: cases (sym_eq ??? prf); @tl
  | generalize in match H; generalize in match tl; cases prf;
    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    #tl
    normalize in ⊢ (∀_: %. ?)
    # H
    whd
    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
qed.

definition product_elim ≝
  λm, n: nat.
  λv: Vector addressing_mode_tag (S m).
  λq: Vector addressing_mode_tag (S n).
  λP: (v × q) → bool.
    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).

definition union_elim ≝ 
  λA, B: Type[0].
  λelimA: (A → bool) → bool.
  λelimB: (B → bool) → bool.
  λelimU: A ⊎ B → bool.
    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).

(*                           
definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
  λP.
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
    P (DA ? ACC_A) ∧
    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    P (RL ? ACC_A) ∧
    P (RLC ? ACC_A) ∧
    P (RR ? ACC_A) ∧
    P (RRC ? ACC_A) ∧
    P (SWAP ? ACC_A) ∧
    P (RET ?) ∧
    P (RETI ?) ∧
    P (NOP ?) ∧
    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
                   (λd. P (XRL ? d)) ∧
    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) 
                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
                   (λd. P (ANL ? d)) ∧
    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) 
                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
                   (λd. P (ORL ? d)) ∧
    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
                   (λd. P (MOVX ? d)) ∧
    union_elim ? ? (
      union_elim ? ? (
        union_elim ? ? (
          union_elim ? ? (
            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
                            (product_elim ? ? [[dptr]] [[data16]]))
                            (product_elim ? ? [[carry]] [[bit_addr]]))
                            (product_elim ? ? [[bit_addr]] [[carry]])
                            (λd. P (MOV ? d)).
  %
qed.
  
definition instruction_elim: ∀P: instruction → bool. bool ≝
  λP. (*
    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
    P (JMP INDIRECT_DPTR) ∧
    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
    preinstruction_elim (λp. P (RealInstruction p)). *)
  %
qed.


axiom instruction_elim_complete:
 ∀P. instruction_elim P = true → ∀i. P i = true.
*)
(*definition eq_instruction ≝
  λi, j: instruction.
    true.*)

definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
  λa, b: addressing_mode.
  match a with
  [ DIRECT d ⇒
    match b with
    [ DIRECT e ⇒ eq_bv ? d e
    | _ ⇒ false
    ]
  | INDIRECT b' ⇒
    match b with
    [ INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | EXT_INDIRECT b' ⇒
    match b with
    [ EXT_INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | REGISTER bv ⇒
    match b with
    [ REGISTER bv' ⇒ eq_bv ? bv bv'
    | _ ⇒ false
    ]
  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
  | DATA b' ⇒
    match b with
    [ DATA e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | DATA16 w ⇒ 
    match b with
    [ DATA16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
  | BIT_ADDR b' ⇒
    match b with
    [ BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | N_BIT_ADDR b' ⇒ 
    match b with
    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | RELATIVE n ⇒
    match b with
    [ RELATIVE e ⇒ eq_bv ? n e
    | _ ⇒ false
    ]
  | ADDR11 w ⇒
    match b with
    [ ADDR11 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ADDR16 w ⇒
    match b with
    [ ADDR16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  ].

lemma eq_bv_refl:
  ∀n, b.
    eq_bv n b b = true.
  #n #b cases b //
qed.

lemma eq_b_refl:
  ∀b.
    eq_b b b = true.
  #b cases b //
qed.

lemma eq_addressing_mode_refl:
  ∀a. eq_addressing_mode a a = true.
  #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl
  try normalize %
qed.
  
definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
  λlt, rt, leq, req, left, right.
    match left with
    [ inl l ⇒
      match right with
      [ inl l' ⇒ leq l l'
      | _ ⇒ false
      ]
    | inr r ⇒
      match right with
      [ inr r' ⇒ req r r'
      | _ ⇒ false
      ]
    ].

definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
  λlt, rt, leq, req, left, right.
    let 〈l, r〉 ≝ left in
    let 〈l', r'〉 ≝ right in
      leq l l' ∧ req r r'.

definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
  λi, j.
  match i with
  [ ADD arg1 arg2 ⇒
    match j with
    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | ADDC arg1 arg2 ⇒
    match j with
    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | SUBB arg1 arg2 ⇒
    match j with
    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | INC arg ⇒
    match j with
    [ INC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | DEC arg ⇒
    match j with
    [ DEC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MUL arg1 arg2 ⇒
    match j with
    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DIV arg1 arg2 ⇒
    match j with
    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DA arg ⇒
    match j with
    [ DA arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JC arg ⇒
    match j with
    [ JC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNC arg ⇒
    match j with
    [ JNC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JB arg1 arg2 ⇒
    match j with
    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JNB arg1 arg2 ⇒
    match j with
    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JBC arg1 arg2 ⇒
    match j with
    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JZ arg ⇒
    match j with
    [ JZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNZ arg ⇒
    match j with
    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CJNE arg1 arg2 ⇒
    match j with
    [ CJNE arg1' arg2' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DJNZ arg1 arg2 ⇒
    match j with
    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | CLR arg ⇒
    match j with
    [ CLR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CPL arg ⇒
    match j with
    [ CPL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RL arg ⇒
    match j with
    [ RL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RLC arg ⇒
    match j with
    [ RLC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RR arg ⇒
    match j with
    [ RR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RRC arg ⇒
    match j with
    [ RRC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SWAP arg ⇒
    match j with
    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SETB arg ⇒
    match j with
    [ SETB arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | PUSH arg ⇒
    match j with
    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | POP arg ⇒
    match j with
    [ POP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | XCH arg1 arg2 ⇒
    match j with
    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | XCHD arg1 arg2 ⇒
    match j with
    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
  | MOVX arg ⇒
    match j with
    [ MOVX arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | XRL arg ⇒
    match j with
    [ XRL arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ORL arg ⇒
    match j with
    [ ORL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ANL arg ⇒
    match j with
    [ ANL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | MOV arg ⇒
    match j with
    [ MOV arg' ⇒
      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
        sum_eq_5 arg arg'
    | _ ⇒ false
    ]
  ].

lemma eq_sum_refl:
  ∀A, B: Type[0].
  ∀leq, req.
  ∀s.
  ∀leq_refl: (∀t. leq t t = true).
  ∀req_refl: (∀u. req u u = true).
    eq_sum A B leq req s s = true.
  #A #B #leq #req #s #leq_refl #req_refl
  cases s whd in ⊢ (? → ??%?) //
qed.

lemma eq_prod_refl:
  ∀A, B: Type[0].
  ∀leq, req.
  ∀s.
  ∀leq_refl: (∀t. leq t t = true).
  ∀req_refl: (∀u. req u u = true).
    eq_prod A B leq req s s = true.
  #A #B #leq #req #s #leq_refl #req_refl
  cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl
qed.

lemma eq_preinstruction_refl:
  ∀i.
    eq_preinstruction i i = true.
  #i cases i try #arg1 try #arg2
  try @eq_addressing_mode_refl
  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    whd in ⊢ (??%?)
    try %
    >eq_addressing_mode_refl
    >eq_addressing_mode_refl %
  |13,15:
    whd in ⊢ (??%?)
    cases arg1
    [*:
      #arg1_left normalize nodelta
      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
    ]
  |11,12:
    whd in ⊢ (??%?)
    cases arg1
    [1:
      #arg1_left normalize nodelta 
      >(eq_sum_refl …)
      [1: % | 2,3: #arg @eq_prod_refl ]
      @eq_addressing_mode_refl
    |2:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: @eq_addressing_mode_refl ]
    |3:
      #arg1_left normalize nodelta
      >(eq_sum_refl …) [1: %
      |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
    |4:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    ]
  |14:
    whd in ⊢ (??%?)
    cases arg1
    [ #arg1_left normalize nodelta
      @eq_sum_refl
      [1: #arg @eq_sum_refl
        [1: #arg @eq_sum_refl
          [1: #arg @eq_sum_refl
            [1: #arg @eq_prod_refl
              [*: @eq_addressing_mode_refl ]
            |2: #arg @eq_prod_refl
              [*: #arg @eq_addressing_mode_refl ]
            ]
          |2: #arg @eq_prod_refl
            [*: #arg @eq_addressing_mode_refl ]
          ]
        |2: #arg @eq_prod_refl
          [*: #arg @eq_addressing_mode_refl ]
        ]
      |2: #arg @eq_prod_refl
        [*: #arg @eq_addressing_mode_refl ]
      ]
    |2: #arg1_right normalize nodelta
        @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    ]
  |*:
    whd in ⊢ (??%?)
    cases arg1
    [*: #arg1 >eq_sum_refl
      [1,4: normalize @eq_addressing_mode_refl
      |2,3,5,6: #arg @eq_prod_refl
        [*: #arg @eq_addressing_mode_refl ]
      ]
    ]
  ]
qed.

definition eq_instruction: instruction → instruction → bool ≝
  λi, j.
  match i with
  [ ACALL arg ⇒
    match j with
    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LCALL arg ⇒
    match j with
    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | AJMP arg ⇒ 
    match j with
    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LJMP arg ⇒
    match j with
    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SJMP arg ⇒ 
    match j with
    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JMP arg ⇒
    match j with
    [ JMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MOVC arg1 arg2 ⇒
    match j with
    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RealInstruction instr ⇒
    match j with
    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
    | _ ⇒ false
    ]
  ].
  
lemma eq_instruction_refl:
  ∀i. eq_instruction i i = true.
  #i cases i
  [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
  |7: #arg1 #arg2
      whd in ⊢ (??%?)
      >eq_addressing_mode_refl
      >eq_addressing_mode_refl
      %
  |8: #arg @eq_preinstruction_refl
  ]
qed.

let rec vect_member
  (A: Type[0]) (n: nat) (eq: A → A → bool)
  (v: Vector A n) (a: A) on v: bool ≝
  match v with
  [ VEmpty          ⇒ false
  | VCons len hd tl ⇒
    eq hd a ∨ (vect_member A ? eq tl a)
  ].

let rec list_addressing_mode_tags_elim_prop
  (n: nat)
  (l: Vector addressing_mode_tag (S n))
  on l:
  ∀P: l → Prop.
  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
  ∀x: l. P x ≝
  match l return
    λy.
      match y with
      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
               ∀x:l. P x
      ] with
  [ VEmpty          ⇒ λAbsurd. ⊥
  | VCons len hd tl ⇒ λProof. ?
  ] (refl ? (S n)). cases daemon. qed. (*
  [ destruct(Absurd)
  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
    # A8 # A9 # A10 # A11 # A12 # A13 # A14
    # A15 # A16 # A17 # A18 # A19 # X
    cases X
    # SUB cases daemon ] qed.
    cases SUB
    [ # BYTE
    normalize
  ].
  
  
(*    let prepare_hd ≝
      match hd with
      [ direct ⇒ λdirect_prf. ?
      | indirect ⇒ λindirect_prf. ?
      | ext_indirect ⇒ λext_indirect_prf. ?
      | registr ⇒ λregistr_prf. ?
      | acc_a ⇒ λacc_a_prf. ?
      | acc_b ⇒ λacc_b_prf. ?
      | dptr ⇒ λdptr_prf. ?
      | data ⇒ λdata_prf. ?
      | data16 ⇒ λdata16_prf. ?
      | acc_dptr ⇒ λacc_dptr_prf. ?
      | acc_pc ⇒ λacc_pc_prf. ?
      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
      | indirect_dptr ⇒ λindirect_prf. ?
      | carry ⇒ λcarry_prf. ?
      | bit_addr ⇒ λbit_addr_prf. ?
      | n_bit_addr ⇒ λn_bit_addr_prf. ?
      | relative ⇒ λrelative_prf. ?
      | addr11 ⇒ λaddr11_prf. ?
      | addr16 ⇒ λaddr16_prf. ?
      ]
    in ? *)
  ].
  [ 1: destruct(absd)
  | 2: # A1 # A2 # A3 # A4 # A5 # A6
       # A7 # A8 # A9 # A10 # A11 # A12
       # A13 # A14 # A15 # A16 # A17 # A18
       # A19 * 
  ].


  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
   (l → bool) → bool ] with
  [ VEmpty      ⇒  true  
  | VCons len hd tl ⇒ λP.
    let process_hd ≝
      match hd return λhd. ∀P: hd:::tl → bool. bool with
      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
      | acc_a ⇒ λP.P ACC_A
      | acc_b ⇒ λP.P ACC_B
      | dptr ⇒ λP.P DPTR
      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
      | acc_dptr ⇒ λP.P ACC_DPTR
      | acc_pc ⇒ λP.P ACC_PC
      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
      | carry ⇒ λP.P CARRY
      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
      ]
    in
      andb (process_hd P)
       (match len return λx. x = len → bool with
         [ O ⇒ λprf. true
         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
  ].
  try %
  [ 2: cases (sym_eq ??? prf); @tl
  | generalize in match H; generalize in match tl; cases prf;
    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    #tl
    normalize in ⊢ (∀_: %. ?)
    # H
    whd
    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
qed.
*)

definition load_code_memory_aux ≝
 fold_left_i_aux … (
   λi, mem, v.
     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).

lemma split_zero:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = split A 0 m v.
  #A #m #v
  elim v
  [ %
  | #n #hd #tl #ih
    normalize in ⊢ (???%) %
  ]
qed.

lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
 #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
 #n #hd #tl #abs @⊥ destruct (abs)
qed.

lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
 ∃hd.∃tl.v ≃ VCons A n hd tl.
 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
 [ #abs @⊥ destruct (abs)
 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
qed.

lemma vector_append_zero:
  ∀A,m.
  ∀v: Vector A m.
  ∀q: Vector A 0.
    v = q@@v.
  #A #m #v #q
  >(Vector_O A q) %
qed.

lemma prod_eq_left:
  ∀A: Type[0].
  ∀p, q, r: A.
    p = q → 〈p, r〉 = 〈q, r〉.
  #A #p #q #r #hyp
  >hyp %
qed.

lemma prod_eq_right:
  ∀A: Type[0].
  ∀p, q, r: A.
    p = q → 〈r, p〉 = 〈r, q〉.
  #A #p #q #r #hyp
  >hyp %
qed.

corollary prod_vector_zero_eq_left:
  ∀A, n.
  ∀q: Vector A O.
  ∀r: Vector A n.
    〈q, r〉 = 〈[[ ]], r〉.
  #A #n #q #r
  generalize in match (Vector_O A q …)
  #hyp
  >hyp in ⊢ (??%?)
  %
qed.

axiom split_succ:
  ∀A, m, n.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd: A.
    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
(*
  #A #m
  elim m
  [ #n #l #r #v #hd #equal #hyp
    normalize >(Vector_O A l) >equal
    >(Vector_O A l) %
  | #n' #ih #n #l #r #v #hd
    #equal #hyp
    cases(Vector_Sn A n' l)
    #hd' #exists
    cases exists #tl #jmeq
    >jmeq *)

lemma split_prod:
  ∀A,m,n.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = split A m n p.
  #A #m
  elim m
  [ #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @split_zero
  | #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v)
    #hd #exists
    cases exists
    #tl #jmeq >jmeq
    @split_succ [1: % |2: @ih % ] 
  ]
qed.

lemma split_prod_exists:
  ∀A, m, n.
  ∀p: Vector A (m + n).
  ∃v: Vector A m.
  ∃q: Vector A n.
    〈v, q〉 = split A m n p.
  #A #m #n #p
  elim m
  @ex_intro
  [1:
  |2: @ex_intro
      [1: 
      |2:
      ]
  ]

lemma split_elim:
 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
  #A #l #m #v #P #hyp
  normalize
  <(split_prod A l m v ? ? ?)

example half_add_SO:
 ∀pc.
 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
 cases daemon.
qed.

(*
axiom not_eqvb_S:
 ∀pc.
 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).

axiom not_eqvb_SS:
 ∀pc.
 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
 
axiom bitvector_elim_complete:
 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.

lemma bitvector_elim_complete':
 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
qed.
*)

(*
lemma andb_elim':
 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
qed.
*)

let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
                       (encoding: list Byte) on encoding: Prop ≝
  match encoding with
  [ nil ⇒ final_pc = pc
  | cons hd tl ⇒
    let 〈new_pc, byte〉 ≝ next code_memory pc in
      hd = byte ∧ encoding_check code_memory new_c final_pc tl
  ].

lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
  let intermediate_pc ≝ pc + length … l1 in
   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
 #code_memory #final_pc #l1 elim l1
  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
qed.

axiom bitvector_3_elim_prop:
 ∀P: BitVector 3 → Prop.
  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.

definition ticks_of_instruction ≝
 λi.
  let trivial_code_memory ≝ assembly1 i in
  let trivial_status ≝ load_code_memory trivial_code_memory in
   \snd (fetch trivial_status (zero ?)).

lemma fetch_assembly:
  ∀pc,i,code_memory,assembled.
    assembled = assembly1 i →
      let len ≝ length … assembled in
      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
      let 〈instr_pc, ticks〉 ≝ fetched in
      let 〈instr,pc'〉 ≝ instr_pc in
       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
 #pc #i #code_memory #assembled cases i [8: *]
 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
 [47,48,49:
 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
   59,60,63,64,65,66,67: #ARG]]
 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
   68,69,70,71: #ARG2]]
 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
 normalize in ⊢ (???% → ?)
 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
  normalize in ⊢ (???% → ?)]
 #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
 try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
 whd >eq_instruction_refl >H4 @eq_bv_refl
qed.

let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
 match expected with
  [ nil ⇒ eq_bv … pc final_pc = true
  | cons i tl ⇒
     let fetched ≝ fetch code_memory pc in
     let 〈instr_pc, ticks〉 ≝ fetched in
     let 〈instr,pc'〉 ≝ instr_pc in
      eq_instruction instr i = true ∧
      ticks = (ticks_of_instruction i) ∧
      fetch_many code_memory final_pc pc' tl].

lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
 #A #a #b #EQ destruct //
qed.

axiom eq_instruction_to_eq:
  ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
               

notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
interpretation "dp" 'dp x y = (dp x y). 

lemma fetch_assembly_pseudo':
 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
  ∀pi,code_memory,len,assembled,instructions,pc.
   let expansion ≝ pol ppc in
   Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction_safe program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
 >EQ2a >EQ2b -EQ2a EQ2b;
  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
  generalize in match pc elim instructions
  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
qed.

axiom bitvector_of_nat_nat_of_bitvector:
  ∀n,v.
    bitvector_of_nat n (nat_of_bitvector n v) = v.

(* CSC: soo long next one; can we merge with previous one now? *)
lemma fetch_assembly_pseudo:
 ∀program.∀pol:policy program.∀ppc.
  ∀code_memory.
   let lookup_labels ≝ ? in
   let lookup_datalabels ≝ ? in
   let pc ≝ ? in
   let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in
   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
      fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
 #program #pol #ppc #code_memory
 letin lookup_labels ≝ (λx:Identifier
    .sigma program pol (address_of_word_labels_code_mem (\snd  program) x))
 letin lookup_datalabels ≝
  (λx:BitVector 16
    .lookup Identifier 16 x (construct_datalabels (\fst  program)) (zero 16))
 letin pc ≝ (sigma program pol ppc)
 letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …))
 @pair_elim' #len #assembled #EQ1 #H
 generalize in match
  (fetch_assembly_pseudo' program pol ppc lookup_labels lookup_datalabels pi
  code_memory len assembled instructions (nat_of_bitvector ? pc) ???) in ⊢ ?;
 [ >bitvector_of_nat_nat_of_bitvector //
 | >bitvector_of_nat_nat_of_bitvector normalize nodelta >(sig2 ?? (expand_pseudo_instruction …)) %
 | >bitvector_of_nat_nat_of_bitvector <EQ1 @assembly_1_pseudoinstruction_ok1
 | //]
qed.

(* This is a trivial consequence of fetch_assembly + the proof that the
   function that load the code in memory is correct. The latter is based
   on missing properties from the standard library on the BitVectorTrie
   data structrure. *)
axiom assembly_ok:
 ∀program,pol,assembled,costs'.
  let 〈labels,costs〉 ≝ build_maps program pol in
  〈assembled,costs'〉 = assembly program pol →
  costs = costs' ∧
  let code_memory ≝ load_code_memory assembled in
  let preamble ≝ \fst program in
  let datalabels ≝ construct_datalabels preamble in
  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
  ∀ppc.
  let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
   ∀len,assembledi.
     〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) →
      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).

lemma fetch_assembly_pseudo2:
 ∀program,pol,ppc.
(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
  let assembled ≝ \fst (assembly program pol) in
  let code_memory ≝ load_code_memory assembled in
  let data_labels ≝ construct_datalabels (\fst program) in
  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
  let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
  let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
 * #preamble #instr_list #pol #ppc
 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
 letin code_memory ≝ (load_code_memory assembled)
 letin data_labels ≝ (construct_datalabels preamble)
 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
 @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
 @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
 #H cases (H (refl \ldots)) -H; #EQ3
 generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
 cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
 #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
 generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
 >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
 >H2 #K @K
qed.

(* OLD?
definition assembly_specification:
  ∀assembly_program: pseudo_assembly_program.
  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
  λpseudo_assembly_program.
  λcode_mem.
    ∀pc: Word.
      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
      match pre_assembled with
       [ None ⇒ True
       | Some pc_code ⇒
          let 〈new_pc,code〉 ≝ pc_code in
           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].

axiom assembly_meets_specification:
  ∀pseudo_assembly_program.
    match assembly pseudo_assembly_program with
    [ None ⇒ True
    | Some code_mem_cost ⇒
      let 〈code_mem, cost〉 ≝ code_mem_cost in
        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
    ].
(*
  # PROGRAM
  [ cases PROGRAM
    # PREAMBLE
    # INSTR_LIST
    elim INSTR_LIST
    [ whd
      whd in ⊢ (∀_. %)
      # PC
      whd
    | # INSTR
      # INSTR_LIST_TL
      # H
      whd
      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    ]
  | cases not_implemented
  ] *)
*)

definition internal_pseudo_address_map ≝ list (BitVector 8).

axiom low_internal_ram_of_pseudo_low_internal_ram:
 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.

axiom high_internal_ram_of_pseudo_high_internal_ram:
 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.

axiom low_internal_ram_of_pseudo_internal_ram_hit:
 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
  member ? (eq_bv 8) (false:::addr) M = true →
   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
   let bl ≝ lookup ? 7 addr ram (zero 8) in
   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).

(* changed from add to sub *)
axiom low_internal_ram_of_pseudo_internal_ram_miss:
 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
  let carr ≝ get_index_v ? ? flags 1 ? in
  carr = false →
  member ? (eq_bv 8) (false:::Saddr) M = false →
   member ? (eq_bv 8) (false:::addr) M = false →
    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
  //
qed.

definition addressing_mode_ok ≝
 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
  λaddr:addressing_mode.
   match addr with
    [ DIRECT d ⇒
       ¬(member ? (eq_bv 8) d M) ∧
       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
    | INDIRECT i ⇒
       let d ≝ get_register ? s [[false;false;i]] in
       ¬(member ? (eq_bv 8) d M) ∧
       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
    | EXT_INDIRECT _ ⇒ true
    | REGISTER _ ⇒ true
    | ACC_A ⇒ true
    | ACC_B ⇒ true
    | DPTR ⇒ true
    | DATA _ ⇒ true
    | DATA16 _ ⇒ true
    | ACC_DPTR ⇒ true
    | ACC_PC ⇒ true
    | EXT_INDIRECT_DPTR ⇒ true
    | INDIRECT_DPTR ⇒ true
    | CARRY ⇒ true
    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    | RELATIVE _ ⇒ true
    | ADDR11 _ ⇒ true
    | ADDR16 _ ⇒ true ].
    
definition next_internal_pseudo_address_map0 ≝
  λT.
  λfetched.
  λM: internal_pseudo_address_map.
  λs: PreStatus T.
   match fetched with
    [ Comment _ ⇒ Some ? M
    | Cost _ ⇒ Some … M
    | Jmp _ ⇒ Some … M
    | Call _ ⇒
       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
    | Mov _ _ ⇒ Some … M
    | Instruction instr ⇒
       match instr with
        [ ADD addr1 addr2 ⇒
           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
            Some ? M
           else
            None ?
        | ADDC addr1 addr2 ⇒ 
           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
            Some ? M
           else
            None ?
        | SUBB addr1 addr2 ⇒
           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
            Some ? M
           else
            None ?        
        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
  

definition next_internal_pseudo_address_map ≝
 λM:internal_pseudo_address_map.
  λs:PseudoStatus.
    next_internal_pseudo_address_map0 ?
     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
    
definition status_of_pseudo_status:
 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝
 λM,ps,pol.
  let pap ≝ code_memory … ps in
  let p ≝ assembly pap pol in
  let cm ≝ load_code_memory (\fst p) in
  let pc ≝ sigma pap pol (program_counter ? ps) in
  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     mk_PreStatus (BitVectorTrie Byte 16)
      cm
      lir
      hir
      (external_ram … ps)
      pc
      (special_function_registers_8051 … ps)
      (special_function_registers_8052 … ps)
      (p1_latch … ps)
      (p3_latch … ps)
      (clock … ps).

(*
definition write_at_stack_pointer':
 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
  λM: Type[0].
  λs: PreStatus M.
  λv: Byte.
    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
    let bit_zero ≝ get_index_v… nu O ? in
    let bit_1 ≝ get_index_v… nu 1 ? in
    let bit_2 ≝ get_index_v… nu 2 ? in
    let bit_3 ≝ get_index_v… nu 3 ? in
      if bit_zero then
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (low_internal_ram ? s) in
          set_low_internal_ram ? s memory
      else
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (high_internal_ram ? s) in
          set_high_internal_ram ? s memory.
  [ cases l0 %
  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
qed.

definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
≝
  λticks_of.
  λs.
  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
  let ticks ≝ ticks_of (program_counter ? s) in
  let s ≝ set_clock ? s (clock ? s + ticks) in
  let s ≝ set_program_counter ? s pc in
    match instr with
    [ Instruction instr ⇒
       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    | Comment cmt ⇒ s
    | Cost cst ⇒ s
    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    | Call call ⇒
      let a ≝ address_of_word_labels s call in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
      let s ≝ write_at_stack_pointer' ? s pc_bl in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let s ≝ write_at_stack_pointer' ? s pc_bu in
        set_program_counter ? s a
    | Mov dptr ident ⇒
       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    ].
 [
 |2,3,4: %
 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
 |
 | %
 ]
 cases not_implemented
qed.
*)

axiom execute_1_pseudo_instruction_preserves_code_memory:
 ∀ticks_of,ps.
  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.

(*
lemma execute_code_memory_unchanged:
 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
 #ticks #ps whd in ⊢ (??? (??%))
 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
  (program_counter pseudo_assembly_program ps)) #instr #pc
 whd in ⊢ (??? (??%)) cases instr
  [ #pre cases pre
     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
       [ #x1 whd in ⊢ (??? (??%)) 
     | *: cases not_implemented
     ]
  | #comment %
  | #cost %
  | #label %
  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    (* CSC: ??? *)
  | #dptr #label (* CSC: ??? *)
  ]
  cases not_implemented
qed.
*)

(* DEAD CODE?
lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
 ∀M:internal_pseudo_address_map.
 ∀ps,ps': PseudoStatus.
 ∀pol.
  ∀prf:code_memory … ps = code_memory … ps'.
   let pol' ≝ ? in
   match status_of_pseudo_status M ps pol with
    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
    ].
 [2: <prf @pol]
 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 generalize in match (refl … (assembly (code_memory … ps) pol))
 cases (assembly ??) in ⊢ (???% → %)
  [ #K whd whd in ⊢ (??%?) <H >K %
  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
qed.
*)

definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
  λprogram: pseudo_assembly_program.λpol.
  λppc: Word.
  λfetched.
    match fetched with
    [ Instruction instr ⇒
      match instr with
      [ JC lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNC lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JB bit lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNB bit lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JBC bit lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JZ lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNZ lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | CJNE arg lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | DJNZ arg lbl ⇒
        match pol ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | ADD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
         〈ticks, ticks〉
      | ADDC arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
         〈ticks, ticks〉
      | SUBB arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
         〈ticks, ticks〉
      | INC arg ⇒ 
        let ticks ≝ ticks_of_instruction (INC ? arg) in
         〈ticks, ticks〉
      | DEC arg ⇒ 
        let ticks ≝ ticks_of_instruction (DEC ? arg) in
         〈ticks, ticks〉
      | MUL arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
         〈ticks, ticks〉
      | DIV arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
         〈ticks, ticks〉
      | DA arg ⇒ 
        let ticks ≝ ticks_of_instruction (DA ? arg) in
         〈ticks, ticks〉
      | ANL arg ⇒
        let ticks ≝ ticks_of_instruction (ANL ? arg) in
         〈ticks, ticks〉
      | ORL arg ⇒
        let ticks ≝ ticks_of_instruction (ORL ? arg) in
         〈ticks, ticks〉
      | XRL arg ⇒
        let ticks ≝ ticks_of_instruction (XRL ? arg) in
         〈ticks, ticks〉
      | CLR arg ⇒
        let ticks ≝ ticks_of_instruction (CLR ? arg) in
         〈ticks, ticks〉
      | CPL arg ⇒
        let ticks ≝ ticks_of_instruction (CPL ? arg) in
         〈ticks, ticks〉
      | RL arg ⇒
        let ticks ≝ ticks_of_instruction (RL ? arg) in
         〈ticks, ticks〉
      | RLC arg ⇒
        let ticks ≝ ticks_of_instruction (RLC ? arg) in
         〈ticks, ticks〉
      | RR arg ⇒
        let ticks ≝ ticks_of_instruction (RR ? arg) in
         〈ticks, ticks〉
      | RRC arg ⇒
        let ticks ≝ ticks_of_instruction (RRC ? arg) in
         〈ticks, ticks〉
      | SWAP arg ⇒
        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
         〈ticks, ticks〉
      | MOV arg ⇒
        let ticks ≝ ticks_of_instruction (MOV ? arg) in
         〈ticks, ticks〉
      | MOVX arg ⇒
        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
         〈ticks, ticks〉
      | SETB arg ⇒
        let ticks ≝ ticks_of_instruction (SETB ? arg) in
         〈ticks, ticks〉
      | PUSH arg ⇒
        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
         〈ticks, ticks〉
      | POP arg ⇒
        let ticks ≝ ticks_of_instruction (POP ? arg) in
         〈ticks, ticks〉
      | XCH arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
         〈ticks, ticks〉
      | XCHD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
         〈ticks, ticks〉
      | RET ⇒
        let ticks ≝ ticks_of_instruction (RET ?) in
         〈ticks, ticks〉
      | RETI ⇒
        let ticks ≝ ticks_of_instruction (RETI ?) in
         〈ticks, ticks〉
      | NOP ⇒
        let ticks ≝ ticks_of_instruction (NOP ?) in
         〈ticks, ticks〉
      ]
    | Comment comment ⇒ 〈0, 0〉
    | Cost cost ⇒ 〈0, 0〉
    | Jmp jmp ⇒ 〈2, 2〉
    | Call call ⇒ 〈2, 2〉
    | Mov dptr tgt ⇒ 〈2, 2〉
    ].
  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
qed.

definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
  λprogram: pseudo_assembly_program.λpol.
  λppc: Word.
    let 〈preamble, pseudo〉 ≝ program in
    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
     ticks_of0 program pol ppc fetched.

lemma eq_rect_Type1_r:
  ∀A: Type[1].
  ∀a:A.
  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
  #A #a #P #H #x #p
  generalize in match H
  generalize in match P
  cases p
  //
qed.

axiom split_append:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v, v': Vector A m.
  ∀q, q': Vector A n.
    let 〈v', q'〉 ≝ split A m n (v@@q) in
      v = v' ∧ q = q'.

axiom split_vector_singleton:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A (S n).
  ∀rest: Vector A n.
  ∀s: Vector A 1.
  ∀prf.
    v = s @@ rest →
    ((get_index_v A ? v 0 prf) ::: rest) = v.

example sub_minus_one_seven_eight:
  ∀v: BitVector 7.
  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
 cases daemon.
qed.

(*
lemma blah:
  ∀m: internal_pseudo_address_map.
  ∀s: PseudoStatus.
  ∀arg: Byte.
  ∀b: bool.
    addressing_mode_ok m s (DIRECT arg) = true →
      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
      get_arg_8 ? s b (DIRECT arg).
  [2, 3: normalize % ]
  #m #s #arg #b #hyp
  whd in ⊢ (??%%)
  @split_elim''
  #nu' #nl' #arg_nu_nl_eq
  normalize nodelta
  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
  #get_index_v_eq
  normalize nodelta
  [2:
    normalize nodelta
    @split_elim''
    #bit_one' #three_bits' #bit_one_three_bit_eq
    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
    normalize nodelta
    generalize in match (refl ? (sub_7_with_carry ? ? ?))
    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
    #Saddr #carr' #Saddr_carr_eq
    normalize nodelta
    #carr_hyp'
    @carr_hyp'
    [1:
    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
        generalize in match (refl ? (¬(member (BitVector 8) ? arg m))) 
        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
        #member_eq
        normalize nodelta
        [2: #destr destruct(destr)
        |1: -carr_hyp';
            >arg_nu_nl_eq
            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
            [1: >get_index_v_eq in ⊢ (??%? → ?)
            |2: @le_S @le_S @le_S @le_n
            ]
            cases (member (BitVector 8) ? (\fst ?) ?)
            [1: #destr normalize in destr; destruct(destr)
            |2:
            ]
        ]
    |3: >get_index_v_eq in ⊢ (??%?)
        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
        >(split_vector_singleton … bit_one_three_bit_eq)
        <arg_nu_nl_eq
        whd in hyp:(??%?)
        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
        normalize nodelta [*: #ignore @sym_eq ]
    ]
  |
  ].
*)
(*
map_address0 ... (DIRECT arg) = Some .. →
  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
  get_arg_8 (internal_ram ...) (DIRECT arg)

((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
                     then Some internal_pseudo_address_map M 
                     else None internal_pseudo_address_map )
                    =Some internal_pseudo_address_map M')
*)

axiom low_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
  low_internal_ram ? s2 = low_internal_ram T2 s3 →
  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
   low_internal_ram T1
     (write_at_stack_pointer ?
       (set_8051_sfr ?
         (write_at_stack_pointer ?
           (set_8051_sfr ?
             (set_low_internal_ram ? s1
               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
      (low_internal_ram ?
       (write_at_stack_pointer ?
         (set_8051_sfr ?
           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).

axiom high_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
  high_internal_ram ? s2 = high_internal_ram T2 s3 →
  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
   high_internal_ram T1
     (write_at_stack_pointer ?
       (set_8051_sfr ?
         (write_at_stack_pointer ?
           (set_8051_sfr ?
             (set_high_internal_ram ? s1
               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
      (high_internal_ram ?
       (write_at_stack_pointer ?
         (set_8051_sfr ?
           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).

lemma Some_Some_elim:
 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
 #T #x #y #P #H #K @H @option_destruct_Some // 
qed.

theorem main_thm:
 ∀M,M',ps,pol.
  next_internal_pseudo_address_map M ps = Some … M' →
   ∃n.
      execute n (status_of_pseudo_status M ps pol)
    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
 #M #M' #ps #pol #SAFE
 cut
  (∀ps'.
    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
 #ps' #EQ
 whd in ⊢ (??(λ_.??(??%)?))
 change with
  (∃n.
    execute n
     (set_low_internal_ram ?
       (set_high_internal_ram ?
         (set_program_counter ?
           (set_code_memory ?? ps (load_code_memory ?))
          (sigma ? pol (program_counter ? ps)))
        (high_internal_ram_of_pseudo_high_internal_ram M ?))
      (low_internal_ram_of_pseudo_low_internal_ram M ?))
   = set_low_internal_ram ?
      (set_high_internal_ram ?
        (set_program_counter ?
          (set_code_memory ?? ? (load_code_memory ?))
         (sigma ???)) ?) ?)
 >EQ whd in match eq_rect_Type0_r normalize nodelta
 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
 generalize in match EQ -EQ;
 generalize in match (refl … (code_memory pseudo_assembly_program ps))
 generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
 (* Dependent types madness ends here *)
 letin ppc ≝ (program_counter … ps)
 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
 letin assembled ≝ (\fst (assembly ? pol))
 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
 letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
 @pair_elim' #pi #newppc #EQ2
 letin instructions ≝
  (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
    (sigma ? pol ppc) (refl …) (refl …) (refl …))
 change with (fetch_many ???? → ?) #H1
 change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
 generalize in match H1; -H1; generalize in match instructions -instructions
 * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi
 whd in match ticks_of normalize nodelta <EQ1 >EQ2
 cases pi in SAFE
  [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?)
   @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
   whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
   #H2 #EQ %[1,3:@0]
   <MAP >(eq_bv_eq … H2) >EQ %
  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
         @pair_elim' * #instr #newppc' #ticks #EQ4       
         * * #H2a #H2b whd in ⊢ (% → ?) #H2
         >H2b >(eq_instruction_to_eq … H2a)
         #EQ %[@1]
         <MAP >(eq_bv_eq … H2) >EQ
         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
         whd in ⊢ (??%?)
         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
  |6: (* Mov *) #arg1 #arg2
       #H1 #H2 #EQ %[@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
       normalize nodelta;
       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
       #result #flags
       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
  |5: (* Call *) #label #MAP
      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
       [ (* short *) #abs @⊥ destruct (abs)
       |3: (* long *) #H1 #H2 #EQ %[@1]
           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ??%?);
           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
           >(eq_bv_eq … H2c)
           change with
            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           @split_eq_status;
            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
              >code_memory_write_at_stack_pointer %
            | >set_program_counter_set_low_internal_ram
              >set_clock_set_low_internal_ram
              @low_internal_ram_write_at_stack_pointer
               [ >EQ0 @pol | % | %
               | @(pair_destruct_2 … EQ1)
               | @(pair_destruct_2 … EQ2)
               | >(pair_destruct_1 ????? EQpc)
                 >(pair_destruct_2 ????? EQpc)
                 @split_elim #x #y #H <H -x y H;
                 >(pair_destruct_1 ????? EQppc)
                 >(pair_destruct_2 ????? EQppc)
                 @split_elim #x #y #H <H -x y H;
                 >EQ0 % ]
            | >set_low_internal_ram_set_high_internal_ram
              >set_program_counter_set_high_internal_ram
              >set_clock_set_high_internal_ram
              @high_internal_ram_write_at_stack_pointer
               [ >EQ0 @pol | % | %
               | @(pair_destruct_2 … EQ1)
               | @(pair_destruct_2 … EQ2)
               | >(pair_destruct_1 ????? EQpc)
                 >(pair_destruct_2 ????? EQpc)
                 @split_elim #x #y #H <H -x y H;
                 >(pair_destruct_1 ????? EQppc)
                 >(pair_destruct_2 ????? EQppc)
                 @split_elim #x #y #H <H -x y H;
                 >EQ0 % ]            
            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
              >external_ram_write_at_stack_pointer %
            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
              >EQ0 % 
            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8051_write_at_stack_pointer %
            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8052_write_at_stack_pointer %
            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p1_latch_write_at_stack_pointer %
            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p3_latch_write_at_stack_pointer %
            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
              >clock_write_at_stack_pointer whd in ⊢ (???%)
              >clock_write_at_stack_pointer whd in ⊢ (???%)
              >clock_write_at_stack_pointer %]
       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
         @pair_elim' #fst_5_addr #rest_addr #EQ1
         @pair_elim' #fst_5_pc #rest_pc #EQ2
         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
         change in ⊢ (? →??%?) with (execute_1_0 ??)
         @pair_elim' * #instr #newppc' #ticks #EQn
          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
          >get_8051_sfr_set_8051_sfr
          
          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
           generalize in match (refl … (split bool 4 4 pc_bu))
           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
           generalize in match (refl … (split bool 3 8 rest_addr))
           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
           generalize in match
            (refl …
             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
           @split_eq_status try %
            [ change with (? = sigma ? (address_of_word_labels ps label))
              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
  |4: (* Jmp *) #label #MAP
      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
       [3: (* long *) #H1 #H2 #EQ %[@1]
           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
           generalize in match
            (refl ?
             (sub_16_with_carry
              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
              false))
           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ?);
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
         generalize in match
          (refl …
            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
         generalize in match
          (refl …
            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
         change in ⊢ (? →??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ?);
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
           generalize in match (refl … (split bool 4 4 pc_bu))
           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
           generalize in match (refl … (split bool 3 8 rest_addr))
           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
           generalize in match
            (refl …
             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7    
           @split_eq_status try %
            [ change with (? = sigma ?? (address_of_word_labels ps label))
              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
       normalize nodelta; #MAP;
       [1: change in ⊢ (? → %) with
        ((let 〈result,flags〉 ≝
          add_8_with_carry
           (get_arg_8 ? ps false ACC_A)
           (get_arg_8 ?
             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
             false (DIRECT ARG2))
           ? in ?) = ?)
        [2,3: %]
        change in ⊢ (???% → ?) with
         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
        >get_arg_8_set_clock
       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
         [2,4: #abs @⊥ normalize in abs; destruct (abs)
         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
       [ change in ⊢ (? → %) with
        ((let 〈result,flags〉 ≝
          add_8_with_carry
           (get_arg_8 ? ps false ACC_A)
           (get_arg_8 ?
             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
             false (DIRECT ARG2))
           ? in ?) = ?)
          >get_arg_8_set_low_internal_ram
       
        cases (add_8_with_carry ???)
         
        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
       #result #flags
       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
       [1,2,3,4: cases (half_add ???) #carry #result
       | cases (half_add ???) #carry #bl normalize nodelta;
         cases (full_add ????) #carry' #bu normalize nodelta ]
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
        [5: %
        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
      (set_program_counter pseudo_assembly_program ps newppc)
      (\fst  (ticks_of0 〈preamble,instr_list〉
                   (program_counter pseudo_assembly_program ps)
                   (Instruction (INC Identifier (DIRECT ARG))))
       +clock pseudo_assembly_program
        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
        [2,3: // ]
            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
            whd in ⊢ (??%%)
            cases (split bool 4 4 ARG)
            #nu' #nl'
            normalize nodelta
            cases (split bool 1 3 nu')
            #bit_1' #ignore'
            normalize nodelta
            cases (get_index_v bool 4 nu' ? ?)
            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
            |
            ]
cases daemon (* EASY CASES TO BE COMPLETED *)
qed.