Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (10 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Fetch.ma

    r332 r465  
    33include "ASM.ma".
    44
    5 ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝
     5ndefinition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝
    66 λpmem,pc.
    7   let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in
    8    〈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)〉.
    99
    1010(* timings taken from SIEMENS *)
    1111
    12 ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝
     12ndefinition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
    1313 λpmem,pc.
    1414  let 〈pc,v〉 ≝ next pmem pc in
     
    1818      let 〈b,v〉≝  head … v in if b then
    1919       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
    5858     else
    5959      let 〈b,v〉≝  head … v in if b then
    6060       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
    105105    else
    106106     let 〈b,v〉≝  head … v in if b then
    107107      let 〈b,v〉≝  head … v in if b then
    108108       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
    150150     else
    151151      let 〈b,v〉≝  head … v in if b then
    152152       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
    197197   else
    198198    let 〈b,v〉≝  head … v in if b then
     
    200200      let 〈b,v〉≝  head … v in if b then
    201201       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
    246246     else
    247247      let 〈b,v〉≝  head … v in if b then
    248248       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
    293293    else
    294294     let 〈b,v〉≝  head … v in if b then
    295295      let 〈b,v〉≝  head … v in if b then
    296296       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
    341341     else
    342342      let 〈b,v〉≝  head … v in if b then
    343343       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〉.
    388388 @.
    389389nqed.
Note: See TracChangeset for help on using the changeset viewer.