include "ASM/BitVectorTrie.ma".
include "ASM/Arithmetic.ma".
include "ASM/ASM.ma".
include "basics/russell.ma".

definition bitvector_max_nat ≝
  λlength: nat.
    2^length.

definition code_memory_size ≝ bitvector_max_nat 16.

include alias "ASM/BitVectorTrie.ma".
include alias "ASM/Arithmetic.ma".

definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
  λpmem: BitVectorTrie Byte 16.
  λpc: Word.
    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.

definition load_code_memory0:
 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
  let program_size ≝ |program| in
   program_size ≤ 2^16 →
    ∀pc. ∀pc_ok: pc < program_size.
     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
≝
 λprogram. \snd
  (foldl_strong ?
   (λprefix.
     Σres: nat × (BitVectorTrie Byte 16).
      let 〈i,mem〉 ≝ res in
      i = |prefix| ∧
      (i ≤ 2^16 →
        ∀pc. ∀pc_ok: pc < |prefix|.
         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
   program 
   (λprefix,v,tl,prf,i_mem.
     let 〈i,mem〉 ≝ i_mem in
      〈S i,insert … (bitvector_of_nat … i) v mem〉)
  〈0,Stub Byte 16〉).
[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
  [ >length_append >H1 normalize //
  | #LE #pc #pc_ok
    cases (le_to_or_lt_eq … pc_ok)
    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
      <H1 <plus_n_O whd in ⊢ (???%); //
    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
      >H2 [2: @(transitive_le … LE) //]
      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
qed.

definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
 λprogram.load_code_memory0 program.

lemma load_code_memory_ok:
 ∀program: list Byte.
  let program_size ≝ |program| in
   program_size ≤ 2^16 →
    ∀pc. ∀pc_ok: pc < program_size.
     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
whd in match load_code_memory; normalize nodelta #program @pi2
qed.

lemma Prod_inv_rect_Type0:
 ∀A,B. ∀P: A × B → Type[0].∀ab.
  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
 #A #B #P * /2/
qed.

notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
 with precedence 10
for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.

notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
 with precedence 10
for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.

lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
[2: // ]
#A #B #C *; normalize /2/
qed.

(* timings taken from SIEMENS *)

definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
    ∀program_counter: Word. Byte → instruction × Word × nat ≝
  λpmem.
  λpc.
  λv.
   let 〈b,v〉 ≝ head … v in if b then
    let 〈b,v〉 ≝ head … v in if b then
     let 〈b,v〉 ≝ head … v in if b then
      let 〈b,v〉 ≝ head … v in if b then
       let 〈b,v〉 ≝ head … v in if b then
        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
          else
           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
          else
           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
          else
           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    else
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
         else
          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
          else
           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
   else
    let 〈b,v〉≝  head … v in if b then
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    else
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
          else
           〈〈RealInstruction (RETI …), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
          else
           〈〈RealInstruction (RET …), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (NOP …), pc〉, 1〉.
  %
qed.

definition fetch: ∀code_memory: BitVectorTrie Byte 16.
    ∀program_counter: Word. instruction × Word × nat ≝
  λpmem: BitVectorTrie Byte 16.
  λpc: Word.
  let 〈word, byte〉 ≝ next pmem pc in
    fetch0 pmem word byte.