include "ASM/BitVectorTrie.ma". include "ASM/Arithmetic.ma". include "ASM/ASM.ma". definition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝ λpmem: BitVectorTrie Byte 16. λpc: Word. 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉. (* timings taken from SIEMENS *) definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝ λpmem: BitVectorTrie Byte 16. λpc_v. let 〈pc,v〉 ≝ pc_v in 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〉≝ 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〉≝ 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〉≝ 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〉≝ 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〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ 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〉≝ 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〉≝ 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〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ 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〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ 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〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ 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〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ 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〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 else let 〈pc,b1〉≝ 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〉≝ 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〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 else let 〈pc,b1〉≝ 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〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ 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〉≝ 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〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 else 〈〈RealInstruction (NOP …), pc〉, 1〉. %. qed. definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝ λpmem: BitVectorTrie Byte 16. λpc: Word. fetch0 pmem (next pmem pc).