Changeset 465 for Deliverables/D4.1/Matita/Fetch.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r332 r465 3 3 include "ASM.ma". 4 4 5 ndefinition next: BitVectorTrie Byte sixteen→ Word → Word × Byte ≝5 ndefinition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝ 6 6 λpmem,pc. 7 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in8 〈res, lookup … pc pmem (zero eight)〉.7 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in 8 〈res, lookup … pc pmem (zero 8)〉. 9 9 10 10 (* timings taken from SIEMENS *) 11 11 12 ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝12 ndefinition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝ 13 13 λpmem,pc. 14 14 let 〈pc,v〉 ≝ next pmem pc in … … 18 18 let 〈b,v〉≝ head … v in if b then 19 19 let 〈b,v〉≝ head … v in if b then 20 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,ACC_A〉))))), pc〉, one〉21 else 22 let 〈b,v〉≝ head … v in if b then 23 let 〈b,v〉≝ head … v in if b then 24 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, one〉25 else 26 let 〈b,v〉≝ head … v in if b then 27 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,ACC_A〉)))), pc〉, one〉28 else 29 〈〈CPL … ACC_A, pc〉, one〉30 else 31 let 〈b,v〉≝ head … v in if b then 32 〈〈MOVX … ( Right … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, two〉33 else 34 let 〈b,v〉≝ head … v in if b then 35 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉36 else 37 〈〈MOVX … ( Right … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, two〉38 else 39 let 〈b,v〉≝ head … v in if b then 40 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉))))), pc〉, one〉41 else 42 let 〈b,v〉≝ head … v in if b then 43 let 〈b,v〉≝ head … v in if b then 44 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, one〉45 else 46 let 〈b,v〉≝ head … v in if b then 47 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,DIRECT b1〉))))), pc〉, one〉48 else 49 〈〈CLR … ACC_A, pc〉, one〉50 else 51 let 〈b,v〉≝ head … v in if b then 52 〈〈MOVX … ( Left … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, two〉53 else 54 let 〈b,v〉≝ head … v in if b then 55 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉56 else 57 〈〈MOVX … ( Left … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, two〉20 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉 21 else 22 let 〈b,v〉≝ head … v in if b then 23 let 〈b,v〉≝ head … v in if b then 24 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉 25 else 26 let 〈b,v〉≝ head … v in if b then 27 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉 28 else 29 〈〈CPL … ACC_A, pc〉, 1〉 30 else 31 let 〈b,v〉≝ head … v in if b then 32 〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉 33 else 34 let 〈b,v〉≝ head … v in if b then 35 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 36 else 37 〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉 38 else 39 let 〈b,v〉≝ head … v in if b then 40 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉 41 else 42 let 〈b,v〉≝ head … v in if b then 43 let 〈b,v〉≝ head … v in if b then 44 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉 45 else 46 let 〈b,v〉≝ head … v in if b then 47 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉 48 else 49 〈〈CLR … ACC_A, pc〉, 1〉 50 else 51 let 〈b,v〉≝ head … v in if b then 52 〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉 53 else 54 let 〈b,v〉≝ head … v in if b then 55 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 56 else 57 〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉 58 58 else 59 59 let 〈b,v〉≝ head … v in if b then 60 60 let 〈b,v〉≝ head … v in if b then 61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉62 else 63 let 〈b,v〉≝ head … v in if b then 64 let 〈b,v〉≝ head … v in if b then 65 〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉66 else 67 let 〈b,v〉≝ head … v in if b then 68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉69 else 70 〈〈DA … ACC_A, pc〉, one〉71 else 72 let 〈b,v〉≝ head … v in if b then 73 let 〈b,v〉≝ head … v in if b then 74 〈〈SETB … CARRY, pc〉, one〉75 else 76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉77 else 78 let 〈b,v〉≝ head … v in if b then 79 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉80 else 81 let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, two〉82 else 83 let 〈b,v〉≝ head … v in if b then 84 〈〈XCH … ACC_A (REGISTER v), pc〉, one〉85 else 86 let 〈b,v〉≝ head … v in if b then 87 let 〈b,v〉≝ head … v in if b then 88 〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉89 else 90 let 〈b,v〉≝ head … v in if b then 91 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, one〉92 else 93 〈〈SWAP … ACC_A, pc〉, one〉94 else 95 let 〈b,v〉≝ head … v in if b then 96 let 〈b,v〉≝ head … v in if b then 97 〈〈CLR … CARRY, pc〉, one〉98 else 99 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉100 else 101 let 〈b,v〉≝ head … v in if b then 102 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉103 else 104 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, two〉61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 62 else 63 let 〈b,v〉≝ head … v in if b then 64 let 〈b,v〉≝ head … v in if b then 65 〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 66 else 67 let 〈b,v〉≝ head … v in if b then 68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 69 else 70 〈〈DA … ACC_A, pc〉, 1〉 71 else 72 let 〈b,v〉≝ head … v in if b then 73 let 〈b,v〉≝ head … v in if b then 74 〈〈SETB … CARRY, pc〉, 1〉 75 else 76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉 77 else 78 let 〈b,v〉≝ head … v in if b then 79 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 80 else 81 let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉 82 else 83 let 〈b,v〉≝ head … v in if b then 84 〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉 85 else 86 let 〈b,v〉≝ head … v in if b then 87 let 〈b,v〉≝ head … v in if b then 88 〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 89 else 90 let 〈b,v〉≝ head … v in if b then 91 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉 92 else 93 〈〈SWAP … ACC_A, pc〉, 1〉 94 else 95 let 〈b,v〉≝ head … v in if b then 96 let 〈b,v〉≝ head … v in if b then 97 〈〈CLR … CARRY, pc〉, 1〉 98 else 99 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉 100 else 101 let 〈b,v〉≝ head … v in if b then 102 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 103 else 104 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉 105 105 else 106 106 let 〈b,v〉≝ head … v in if b then 107 107 let 〈b,v〉≝ head … v in if b then 108 108 let 〈b,v〉≝ head … v in if b then 109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Right … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, two〉110 else 111 let 〈b,v〉≝ head … v in if b then 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Right … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, two〉114 else 115 let 〈b,v〉≝ head … v in if b then 116 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Left … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, two〉117 else 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Left … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, two〉119 else 120 let 〈b,v〉≝ head … v in if b then 121 let 〈b,v〉≝ head … v in if b then 122 〈〈CPL … CARRY, pc〉, one〉123 else 124 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉125 else 126 let 〈b,v〉≝ head … v in if b then 127 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉128 else 129 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉130 else 131 let 〈b,v〉≝ head … v in if b then 132 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DIRECT b1〉))))), pc〉, two〉133 else 134 let 〈b,v〉≝ head … v in if b then 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, two〉137 else 138 〈〈MUL … ACC_A ACC_B, pc〉, four〉139 else 140 let 〈b,v〉≝ head … v in if b then 141 let 〈b,v〉≝ head … v in if b then 142 〈〈INC … DPTR, pc〉, two〉143 else 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Right … 〈CARRY,BIT_ADDR b1〉)), pc〉, one〉145 else 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉148 else 149 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 110 else 111 let 〈b,v〉≝ head … v in if b then 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 114 else 115 let 〈b,v〉≝ head … v in if b then 116 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 117 else 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 119 else 120 let 〈b,v〉≝ head … v in if b then 121 let 〈b,v〉≝ head … v in if b then 122 〈〈CPL … CARRY, pc〉, 1〉 123 else 124 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉 125 else 126 let 〈b,v〉≝ head … v in if b then 127 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 128 else 129 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉 130 else 131 let 〈b,v〉≝ head … v in if b then 132 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉 133 else 134 let 〈b,v〉≝ head … v in if b then 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉 137 else 138 〈〈MUL … ACC_A ACC_B, pc〉, 4〉 139 else 140 let 〈b,v〉≝ head … v in if b then 141 let 〈b,v〉≝ head … v in if b then 142 〈〈INC … DPTR, pc〉, 2〉 143 else 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉 145 else 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 148 else 149 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉 150 150 else 151 151 let 〈b,v〉≝ head … v in if b then 152 152 let 〈b,v〉≝ head … v in if b then 153 〈〈SUBB … ACC_A (REGISTER v), pc〉, one〉154 else 155 let 〈b,v〉≝ head … v in if b then 156 let 〈b,v〉≝ head … v in if b then 157 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉158 else 159 let 〈b,v〉≝ head … v in if b then 160 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, one〉161 else 162 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉163 else 164 let 〈b,v〉≝ head … v in if b then 165 let 〈b,v〉≝ head … v in if b then 166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉167 else 168 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Right … 〈BIT_ADDR b1,CARRY〉), pc〉, two〉169 else 170 let 〈b,v〉≝ head … v in if b then 171 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉172 else 173 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Right … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, two〉174 else 175 let 〈b,v〉≝ head … v in if b then 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,REGISTER v〉)))), pc〉, two〉177 else 178 let 〈b,v〉≝ head … v in if b then 179 let 〈b,v〉≝ head … v in if b then 180 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, two〉181 else 182 let 〈b,v〉≝ head … v in if b then 183 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,DIRECT b2〉)))), pc〉, two〉184 else 185 〈〈DIV … ACC_A ACC_B, pc〉, four〉186 else 187 let 〈b,v〉≝ head … v in if b then 188 let 〈b,v〉≝ head … v in if b then 189 〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉190 else 191 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉192 else 193 let 〈b,v〉≝ head … v in if b then 194 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉195 else 196 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉153 〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉 154 else 155 let 〈b,v〉≝ head … v in if b then 156 let 〈b,v〉≝ head … v in if b then 157 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 158 else 159 let 〈b,v〉≝ head … v in if b then 160 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉 161 else 162 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉 163 else 164 let 〈b,v〉≝ head … v in if b then 165 let 〈b,v〉≝ head … v in if b then 166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 167 else 168 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉 169 else 170 let 〈b,v〉≝ head … v in if b then 171 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 172 else 173 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉 174 else 175 let 〈b,v〉≝ head … v in if b then 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉 177 else 178 let 〈b,v〉≝ head … v in if b then 179 let 〈b,v〉≝ head … v in if b then 180 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉 181 else 182 let 〈b,v〉≝ head … v in if b then 183 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉 184 else 185 〈〈DIV … ACC_A ACC_B, pc〉, 4〉 186 else 187 let 〈b,v〉≝ head … v in if b then 188 let 〈b,v〉≝ head … v in if b then 189 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 190 else 191 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉 192 else 193 let 〈b,v〉≝ head … v in if b then 194 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 195 else 196 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 197 197 else 198 198 let 〈b,v〉≝ head … v in if b then … … 200 200 let 〈b,v〉≝ head … v in if b then 201 201 let 〈b,v〉≝ head … v in if b then 202 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DATA b1〉))))), pc〉, one〉203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈b,v〉≝ head … v in if b then 206 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, one〉207 else 208 let 〈b,v〉≝ head … v in if b then 209 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,DATA b2〉)))), pc〉, three〉210 else 211 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,DATA b1〉))))), pc〉, one〉212 else 213 let 〈b,v〉≝ head … v in if b then 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP … INDIRECT_DPTR, pc〉, two〉216 else 217 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉218 else 219 let 〈b,v〉≝ head … v in if b then 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, two〉223 else 224 let 〈b,v〉≝ head … v in if b then 225 〈〈XRL … ( Left … 〈ACC_A,REGISTER v〉), pc〉, one〉226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈b,v〉≝ head … v in if b then 229 〈〈XRL … ( Left … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, one〉230 else 231 let 〈b,v〉≝ head … v in if b then 232 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Left … 〈ACC_A,DIRECT b1〉), pc〉, one〉233 else 234 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Left … 〈ACC_A,DATA b1〉), pc〉, one〉235 else 236 let 〈b,v〉≝ head … v in if b then 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … ( Right … 〈DIRECT b1,DATA b2〉), pc〉, two〉239 else 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Right … 〈DIRECT b1,ACC_A〉), pc〉, one〉241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉202 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉 203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈b,v〉≝ head … v in if b then 206 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉 207 else 208 let 〈b,v〉≝ head … v in if b then 209 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉 210 else 211 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉 212 else 213 let 〈b,v〉≝ head … v in if b then 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 216 else 217 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉 218 else 219 let 〈b,v〉≝ head … v in if b then 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉 223 else 224 let 〈b,v〉≝ head … v in if b then 225 〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉 226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈b,v〉≝ head … v in if b then 229 〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉 230 else 231 let 〈b,v〉≝ head … v in if b then 232 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉 233 else 234 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉 235 else 236 let 〈b,v〉≝ head … v in if b then 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉 239 else 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉 241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉 246 246 else 247 247 let 〈b,v〉≝ head … v in if b then 248 248 let 〈b,v〉≝ head … v in if b then 249 〈〈ANL … ( Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉250 else 251 let 〈b,v〉≝ head … v in if b then 252 let 〈b,v〉≝ head … v in if b then 253 〈〈ANL … ( Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉254 else 255 let 〈b,v〉≝ head … v in if b then 256 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉257 else 258 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉259 else 260 let 〈b,v〉≝ head … v in if b then 261 let 〈b,v〉≝ head … v in if b then 262 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … ( Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉263 else 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉265 else 266 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, two〉270 else 271 let 〈b,v〉≝ head … v in if b then 272 〈〈ORL … ( Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉273 else 274 let 〈b,v〉≝ head … v in if b then 275 let 〈b,v〉≝ head … v in if b then 276 〈〈ORL … ( Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉277 else 278 let 〈b,v〉≝ head … v in if b then 279 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉280 else 281 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉282 else 283 let 〈b,v〉≝ head … v in if b then 284 let 〈b,v〉≝ head … v in if b then 285 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … ( Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉286 else 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉288 else 289 let 〈b,v〉≝ head … v in if b then 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉249 〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 250 else 251 let 〈b,v〉≝ head … v in if b then 252 let 〈b,v〉≝ head … v in if b then 253 〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 254 else 255 let 〈b,v〉≝ head … v in if b then 256 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 257 else 258 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 259 else 260 let 〈b,v〉≝ head … v in if b then 261 let 〈b,v〉≝ head … v in if b then 262 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 263 else 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 265 else 266 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉 270 else 271 let 〈b,v〉≝ head … v in if b then 272 〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 273 else 274 let 〈b,v〉≝ head … v in if b then 275 let 〈b,v〉≝ head … v in if b then 276 〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 277 else 278 let 〈b,v〉≝ head … v in if b then 279 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 280 else 281 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 282 else 283 let 〈b,v〉≝ head … v in if b then 284 let 〈b,v〉≝ head … v in if b then 285 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 286 else 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 288 else 289 let 〈b,v〉≝ head … v in if b then 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉 293 293 else 294 294 let 〈b,v〉≝ head … v in if b then 295 295 let 〈b,v〉≝ head … v in if b then 296 296 let 〈b,v〉≝ head … v in if b then 297 〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉302 else 303 let 〈b,v〉≝ head … v in if b then 304 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, one〉305 else 306 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉307 else 308 let 〈b,v〉≝ head … v in if b then 309 let 〈b,v〉≝ head … v in if b then 310 〈〈RLC … ACC_A, pc〉, one〉311 else 312 〈〈RETI …, pc〉, two〉313 else 314 let 〈b,v〉≝ head … v in if b then 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉318 else 319 let 〈b,v〉≝ head … v in if b then 320 〈〈ADD … ACC_A (REGISTER v), pc〉, one〉321 else 322 let 〈b,v〉≝ head … v in if b then 323 let 〈b,v〉≝ head … v in if b then 324 〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉325 else 326 let 〈b,v〉≝ head … v in if b then 327 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, one〉328 else 329 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉330 else 331 let 〈b,v〉≝ head … v in if b then 332 let 〈b,v〉≝ head … v in if b then 333 〈〈RL … ACC_A, pc〉, one〉334 else 335 〈〈RET …, pc〉, two〉336 else 337 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉297 〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉 298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 302 else 303 let 〈b,v〉≝ head … v in if b then 304 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉 305 else 306 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉 307 else 308 let 〈b,v〉≝ head … v in if b then 309 let 〈b,v〉≝ head … v in if b then 310 〈〈RLC … ACC_A, pc〉, 1〉 311 else 312 〈〈RETI …, pc〉, 2〉 313 else 314 let 〈b,v〉≝ head … v in if b then 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 318 else 319 let 〈b,v〉≝ head … v in if b then 320 〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉 321 else 322 let 〈b,v〉≝ head … v in if b then 323 let 〈b,v〉≝ head … v in if b then 324 〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 325 else 326 let 〈b,v〉≝ head … v in if b then 327 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉 328 else 329 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉 330 else 331 let 〈b,v〉≝ head … v in if b then 332 let 〈b,v〉≝ head … v in if b then 333 〈〈RL … ACC_A, pc〉, 1〉 334 else 335 〈〈RET …, pc〉, 2〉 336 else 337 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 341 341 else 342 342 let 〈b,v〉≝ head … v in if b then 343 343 let 〈b,v〉≝ head … v in if b then 344 〈〈DEC … (REGISTER v), pc〉, one〉345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉349 else 350 let 〈b,v〉≝ head … v in if b then 351 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, one〉352 else 353 〈〈DEC … ACC_A, pc〉, one〉354 else 355 let 〈b,v〉≝ head … v in if b then 356 let 〈b,v〉≝ head … v in if b then 357 〈〈RRC … ACC_A, pc〉, one〉358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉360 else 361 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉365 else 366 let 〈b,v〉≝ head … v in if b then 367 〈〈INC … (REGISTER v), pc〉, one〉368 else 369 let 〈b,v〉≝ head … v in if b then 370 let 〈b,v〉≝ head … v in if b then 371 〈〈INC … (INDIRECT (from_singl … v)), pc〉, one〉372 else 373 let 〈b,v〉≝ head … v in if b then 374 let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, one〉375 else 376 〈〈INC … ACC_A, pc〉, one〉377 else 378 let 〈b,v〉≝ head … v in if b then 379 let 〈b,v〉≝ head … v in if b then 380 〈〈RR … ACC_A, pc〉, one〉381 else 382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉383 else 384 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉386 else 387 〈〈NOP …, pc〉, one〉.344 〈〈DEC … (REGISTER v), pc〉, 1〉 345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉 349 else 350 let 〈b,v〉≝ head … v in if b then 351 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉 352 else 353 〈〈DEC … ACC_A, pc〉, 1〉 354 else 355 let 〈b,v〉≝ head … v in if b then 356 let 〈b,v〉≝ head … v in if b then 357 〈〈RRC … ACC_A, pc〉, 1〉 358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 360 else 361 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 365 else 366 let 〈b,v〉≝ head … v in if b then 367 〈〈INC … (REGISTER v), pc〉, 1〉 368 else 369 let 〈b,v〉≝ head … v in if b then 370 let 〈b,v〉≝ head … v in if b then 371 〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉 372 else 373 let 〈b,v〉≝ head … v in if b then 374 let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉 375 else 376 〈〈INC … ACC_A, pc〉, 1〉 377 else 378 let 〈b,v〉≝ head … v in if b then 379 let 〈b,v〉≝ head … v in if b then 380 〈〈RR … ACC_A, pc〉, 1〉 381 else 382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 383 else 384 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 386 else 387 〈〈NOP …, pc〉, 1〉. 388 388 @. 389 389 nqed.
Note: See TracChangeset
for help on using the changeset viewer.