Ignore:
Timestamp:
Mar 10, 2011, 11:48:33 AM (9 years ago)
Author:
mulligan
Message:

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Demo-March-2011/matita/Search.ma

    r646 r664  
    22
    33ndefinition test1: List instruction ≝
    4  [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
    5   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;false;false;true;false;false;false]]);
    6   SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
    7   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;true;false;false;false;true]])〉))));
    8   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;true;false;true;false;true;true;true;false]]);
    9   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    10   Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
     4 [LCALL … (ADDR16 [[false;false;false;false;false;false;true;false;true;true;false;false;true;true;true;false]]);
    115  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    12   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    13   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
    14   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    15   Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
    16   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    17   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;true;true;false;true;true;false;false;true;false]])〉)));
    18   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    19   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    20   CLR … (ACC_A);
    21   MOVC … (ACC_A) (ACC_DPTR);
    22   MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
    23   INC … (DPTR);
    24   INC … (REGISTER [[false;false;false]]);
    25   Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
    26   INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
    27   Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
    28   Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
    29   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
    30   CLR … (ACC_A);
    31   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
    32   MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
    33   Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
    34   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    35   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    36   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉))].
    37   @.
    38 nqed.
    39  
     6  NOP … ;
     7  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;false]])〉)))));
     8  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;true;false;false]])〉))));
     9  CLR … (CARRY);
     10  SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;false]]);
     11  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;false]]),(ACC_A)〉))));
     12  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;true]])〉)))));
     13  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     14  SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;true]]);
     15  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;true]]),(ACC_A)〉))));
     16  POP … (DIRECT [[true;true;true;false;false;false;false;false]]);
     17  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(ACC_A)〉))));
     18  POP … (DIRECT [[true;true;true;false;false;false;false;false]]);
     19  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;false]]),(ACC_A)〉))));
     20  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     21  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     22  CLR … (CARRY);
     23  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     24  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     25  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;false;true]])〉)))));
     26  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     27  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;false]]),(ACC_A)〉))));
     28  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     29  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     30  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     31  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     32  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
     33  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     34  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(ACC_A)〉))));
     35  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     36  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     37  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;false]])〉)))));
     38  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     39  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     40  CLR … (CARRY);
     41  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     42  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     43  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     44  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     45  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     46  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     47  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     48  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     49  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     50  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     51  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     52  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     53  CLR … (CARRY)
     54  ].
     55  @.
     56nqed.
     57
    4058ndefinition test2: List instruction ≝
    41   [Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
    42   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    43   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    44   CLR … (ACC_A);
    45   MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
    46   INC … (REGISTER [[false;false;true]]);
    47   Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    48   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    49   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    50   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    51   Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
    52   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    53   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    54   CLR … (ACC_A);
     59  [MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     60  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     61  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     62  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     63  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     64  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     65  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     66  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     67  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     68  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     69  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     70  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     71  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     72  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     73  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     74  XRL … (Left … 〈(ACC_A),(DIRECT [[true;true;true;true;false;false;false;false]])〉);
     75  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     76  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     77  CLR … (CARRY);
     78  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     79  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     80  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     81  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     82  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     83  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     84  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     85  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     86  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     87  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     88  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     89  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     90  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     91  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     92  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     93  XRL … (Left … 〈(ACC_A),(DIRECT [[true;true;true;true;false;false;false;false]])〉);
     94  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     95  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     96  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;false]]));
     97  SJMP … (RELATIVE [[false;false;false;false;false;false;true;true]]);
     98  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;true;true;false;false;false;false;true;false]]);
     99  NOP … ;
     100  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;true;false;true;true;true;true;true;false]]);
     101  NOP … ;
     102  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;false]])〉)))));
     103  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     104  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
     105  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     106  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     107  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;false;false;false;true;false]])〉))));
     108  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     109  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     110  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     111  DIV … (ACC_A) (ACC_B)
     112  ].
     113  @.
     114nqed.
     115
     116ndefinition test3: List instruction ≝
     117  [MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(ACC_A)〉))));
     118  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     119  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     120  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     121  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     122  MUL … (ACC_A) (ACC_B);
     123  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     124  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     125  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     126  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;false]])〉)))));
     127  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     128  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     129  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     130  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;true]])〉)))));
     131  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     132  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     133  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     134  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     135  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     136  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     137  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     138  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     139  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     140  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     141  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     142  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     143  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     144  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     145  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     146  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     147  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     148  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;false]]),(ACC_A)〉))));
     149  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     150  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     151  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;false;false]])〉)))));
     152  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     153  MOVX … (Left … 〈(ACC_A),(EXT_INDIRECT_DPTR)〉);
     154  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     155  CLR … (CARRY)
     156  ].
     157  @.
     158nqed.
     159
     160ndefinition test4: List instruction ≝
     161  [MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;false;false]])〉)))));
     162  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     163  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     164  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     165  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     166  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     167  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;false]]));
     168  SJMP … (RELATIVE [[false;false;false;false;false;false;true;true]]);
     169  LJMP … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;true;true;true;true;false;true]]);
     170  NOP … ;
     171  LJMP … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;true;false;true;false;false;false]]);
     172  NOP … ;
     173  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     174  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     175  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(ACC_A)〉))));
     176  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     177  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;false]]),(ACC_A)〉))));
     178  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;false;false]])〉)))));
     179  PUSH … (DIRECT [[true;true;true;false;false;false;false;false]]);
     180  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;false;true]])〉)))));
     181  PUSH … (DIRECT [[true;true;true;false;false;false;false;false]]);
     182  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;true;false;false]])〉))));
     183  ADD … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;false]]);
     184  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;false]]),(ACC_A)〉))));
     185  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     186  ADDC … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;true]]);
     187  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;true]]),(ACC_A)〉))));
     188  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;false;true]])〉)))));
     189  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     190  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;false;false]])〉)))));
     191  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     192  RET …
     193  ].
     194  @.
     195nqed.
     196
     197ndefinition test5: List instruction ≝
     198  [MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     199  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     200  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     201  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     202  MUL … (ACC_A) (ACC_B);
     203  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     204  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     205  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     206  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;false]])〉)))));
     207  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     208  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     209  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     210  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;true]])〉)))));
     211  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     212  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     213  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     214  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     215  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     216  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     217  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     218  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     219  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     220  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     221  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     222  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     223  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     224  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     225  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     226  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     227  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     228  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;false]]),(ACC_A)〉))));
     229  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     230  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     231  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;false;false]])〉)))));
     232  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     233  MOVX … (Left … 〈(ACC_A),(EXT_INDIRECT_DPTR)〉)
     234  ].
     235  @.
     236nqed.
     237
     238ndefinition test6: List instruction ≝
     239  [MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     240  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;true]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     241  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     242  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;true]])〉)))));
     243  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     244  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     245  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     246  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;true]]),(ACC_A)〉))));
     247  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     248  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     249  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;false;false]])〉)))));
     250  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     251  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(ACC_A)〉))));
     252  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     253  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     254  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     255  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     256  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     257  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     258  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     259  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     260  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     261  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;true]])〉)))));
     262  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     263  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     264  CLR … (CARRY);
     265  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     266  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     267  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     268  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     269  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     270  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     271  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     272  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     273  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     274  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     275  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     276  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     277  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;false]]));
     278  SJMP … (RELATIVE [[false;false;false;false;false;false;true;true]]);
     279  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;false;false;false;false;true;true;false;true]]);
     280  NOP … ;
     281  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;true;false;true;false;true;true;false;true]]);
     282  NOP …
     283  ].
     284  @.
     285nqed.
     286
     287ndefinition test7: List instruction ≝
     288  [MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     289  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     290  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     291  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     292  MUL … (ACC_A) (ACC_B);
     293  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     294  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     295  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     296  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;false]])〉)))));
     297  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     298  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     299  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     300  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;true;true]])〉)))));
     301  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     302  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     303  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     304  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     305  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     306  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     307  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     308  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     309  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     310  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     311  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     312  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     313  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     314  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     315  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     316  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     317  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     318  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;false]]),(ACC_A)〉))));
     319  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     320  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     321  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;false;false]])〉)))));
     322  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     323  MOVX … (Left … 〈(ACC_A),(EXT_INDIRECT_DPTR)〉);
     324  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(ACC_A)〉))));
     325  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     326  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉))));
     327  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     328  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     329  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;true;false;false]])〉)))));
     330  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     331  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(ACC_A)〉))));
     332  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     333  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     334  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;true;true;false;false]])〉)))));
     335  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     336  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     337  CLR … (CARRY)
     338  ].
     339  @.
     340nqed.
     341
     342ndefinition test8: List instruction ≝
     343  [MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     344  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     345  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;true]])〉)))));
     346  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     347  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     348  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     349  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     350  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     351  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     352  ADDC … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     353  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     354  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     355  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;false]]));
     356  SJMP … (RELATIVE [[false;false;false;false;false;false;true;true]]);
     357  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;true;false;false;true;true;false;false;true]]);
     358  NOP … ;
     359  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;true;false;false;true;true;true;false;true]]);
     360  NOP … ;
     361  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;true;true;false;false;true;true]]);
     362  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     363  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     364  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     365  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     366  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     367  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;false]]),(ACC_A)〉))));
     368  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;true;true;false;false;true;true]]);
     369  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     370  CLR … (CARRY);
     371  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     372  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     373  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     374  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     375  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;false]]),(ACC_A)〉))));
     376  LJMP … (ADDR16 [[false;false;false;false;false;false;true;false;false;false;false;false;true;true;true;false]]);
     377  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉))));
     378  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;false]])〉)))));
     379  CPL … (ACC_A);
     380  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(ACC_A)〉))));
     381  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
     382  INC … (ACC_A);
     383  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(ACC_A)〉))));
     384  LJMP … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;true;true;true;true;true;false]]);
     385  NOP …
     386  ].
     387  @.
     388nqed.
     389
     390ndefinition test9: List instruction ≝
     391  [MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;false]])〉)))));
     392  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
     393  CLR … (CARRY);
     394  SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;false]]);
     395  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;false]]),(ACC_A)〉))));
     396  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;true]])〉)))));
     397  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     398  SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;true]]);
     399  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;true;true]]),(ACC_A)〉))));
     400  POP … (DIRECT [[true;true;true;false;false;false;false;false]]);
     401  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     402  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉))));
     403  ADD … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;false]]);
     404  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     405  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     406  ADDC … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;true]]);
     407  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     408  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;true]])〉)))));
    55409  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
    56   INC … (DPTR);
    57   Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    58   Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
    59   LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    60   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    61   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;true]]),(DIRECT [[true;false;false;false;false;false;true;true]])〉)))));
    62   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;false]]),(DIRECT [[true;true;true;true;false;false;false;false]])〉)))));
    63   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    64   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;false]])〉)))));
    65   DEC … (ACC_A);
    66   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;false]]),(ACC_A)〉))));
    67   CLR … (CARRY);
    68   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
    69   XRL … (Left … 〈(ACC_A),(DATA [[true;false;false;false;false;false;false;false]])〉);
    70   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[true;false;true]])〉))));
    71   XRL … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉);
    72   SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
    73   Jump … (JNC … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    74   LJMP … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;false;false;false;true;false;false]]);
    75   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
    76   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
    77   RLC … (ACC_A);
    78   SUBB … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
    79   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(ACC_A)〉)))));
    80   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;false;true]])〉)))));
    81   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(ACC_A)〉)))));
    82   RLC … (ACC_A)].
    83   @.
    84 nqed.
    85  
    86 ndefinition test3: List instruction ≝
    87   [SUBB … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
    88   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;false]]),(ACC_A)〉)))));
    89   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
    90   ADD … (ACC_A) (REGISTER [[true;true;true]]);
    91   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
    92   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
    93   ADDC … (ACC_A) (REGISTER [[false;false;false]]);
    94   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
    95   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;false]]),(DATA [[false;false;false;false;false;false;true;false]])〉))));
    96   CLR … (ACC_A);
    97   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;true]]),(ACC_A)〉))));
    98   PUSH … (DIRECT [[false;false;false;false;false;false;true;false]]);
    99   PUSH … (DIRECT [[false;false;false;false;false;false;true;true]]);
    100   PUSH … (DIRECT [[false;false;false;false;false;true;false;false]]);
    101   PUSH … (DIRECT [[false;false;false;false;false;true;false;true]]);
    102   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;true;true;false;true;true;false]]);
    103   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;false]]),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    104   POP … (DIRECT [[false;false;false;false;false;true;false;true]]);
    105   POP … (DIRECT [[false;false;false;false;false;true;false;false]]);
    106   POP … (DIRECT [[false;false;false;false;false;false;true;true]]);
    107   POP … (DIRECT [[false;false;false;false;false;false;true;false]]);
    108   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
    109   ADD … (ACC_A) (REGISTER [[false;true;false]]);
    110   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
    111   CLR … (ACC_A);
    112   ADDC … (ACC_A) (REGISTER [[false;true;true]]);
    113   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(ACC_A)〉)))));
    114   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(REGISTER [[true;false;false]])〉))));
    115   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[true;true;true]])〉))));
    116   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(REGISTER [[false;false;false]])〉))));
    117   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[false;false;true]])〉))));
    118   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;false;true;true;false;true;false]]);
    119   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
    120   Jump … (CJNE … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉) (RELATIVE [[false;false;false;false;false;false;true;true]]));
    121   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[true;true;false]])〉))));
    122   RET … ;
    123   CLR … (CARRY);
    124   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉)))));
    125   XRL … (Left … 〈(ACC_A),(DATA [[true;false;false;false;false;false;false;false]])〉);
    126   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[true;true;true]])〉))));
    127   XRL … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉);
    128   SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
    129   Jump … (JNC … (RELATIVE [[false;false;false;false;false;true;false;false]]));
    130   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
    131   DEC … (ACC_A);
    132   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;false]]),(ACC_A)〉))));
    133   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
    134   ADD … (ACC_A) (REGISTER [[false;true;false]]);
    135   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
    136   CLR … (ACC_A);
    137   ADDC … (ACC_A) (REGISTER [[false;true;true]]);
    138   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(ACC_A)〉)))));
    139   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(REGISTER [[true;false;false]])〉))));
    140   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[true;true;true]])〉))));
    141   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(REGISTER [[false;false;false]])〉))));
    142   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[false;false;true]])〉))));
    143   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;false;true;true;false;true;false]]);
    144   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
    145   CLR … (CARRY);
    146   XRL … (Left … 〈(ACC_A),(DATA [[true;false;false;false;false;false;false;false]])〉);
    147   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DIRECT [[true;true;true;true;false;false;false;false]])〉))));
    148   XRL … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉);
    149   SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
    150   Jump … (JC … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    151   LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;false;true]]);
    152   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
    153   INC … (ACC_A)].
    154   @.
    155 nqed.
    156 
    157 ndefinition test4: List instruction ≝
    158  [MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;true]]),(ACC_A)〉)))));
    159   LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;false;true]]);
    160   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
    161   RET … ;
    162   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    163   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;false]]),(DATA [[false;false;false;true;false;false;true;false]])〉))));
    164   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;false;true]]),(DATA [[false;false;false;true;false;true;true;true]])〉))));
    165   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;true;false]]),(DATA [[false;false;true;true;true;false;false;true]])〉))));
    166   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;true;true;true]]),(DATA [[false;true;true;true;true;false;false;false]])〉))));
    167   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉))));
    168   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;false;true]]),(DATA [[false;false;false;true;true;false;true;false]])〉))));
    169   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;true;true]])〉)));
    170   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(DATA [[false;true;false;false;false;false;false;false]])〉))));
    171   LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
    172   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    173   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(ACC_A)〉)))));
    174   RLC … (ACC_A);
    175   SUBB … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
    176   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[false;true;false]])〉))));
    177   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
    178   RET … ;
    179   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;true;false;false;false;false]])〉)))));
    180   CLR … (ACC_A);
    181   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;true]]),(ACC_A)〉)))));
    182   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;false]]),(ACC_A)〉)))));
    183   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    184   ADD … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
    185   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
    186   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;true]])〉)))));
    187   RLC … (ACC_A);
    188   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
    189   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;true;true]])〉)))));
    190   RLC … (ACC_A);
    191   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;true]]),(ACC_A)〉)))));
    192   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;false;false]])〉)))));
    193   RLC … (ACC_A);
    194   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;false]]),(ACC_A)〉)))));
    195   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;true;true]])〉)))));
    196   SUBB … (ACC_A) (DIRECT [[false;false;false;true;false;false;false;false]]);
    197   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
    198   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;false;false]])〉)))));
    199   SUBB … (ACC_A) (DIRECT [[false;false;false;true;false;false;false;true]]);
    200   Jump … (JC … (RELATIVE [[false;false;false;false;false;true;true;false]]));
    201   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;false]]),(ACC_A)〉)))));
    202   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;true]]),(DIRECT [[true;true;true;true;false;false;false;false]])〉)))));
    203   ORL … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;true]])〉));
    204   Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;false;true;true;true;false;true]]));
    205   RET … ;
    206   Jump … (JB … (BIT_ADDR [[true;true;true;true;false;true;true;true]]) (RELATIVE [[false;false;false;true;false;true;false;false]]));
    207   Jump … (JNB … (BIT_ADDR [[true;true;true;true;false;true;true;false]]) (RELATIVE [[false;false;false;true;false;true;false;false]]));
    208   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(REGISTER [[false;false;false]])〉))));
    209   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    210   Jump … (JB … (BIT_ADDR [[true;true;true;true;false;true;false;true]]) (RELATIVE [[false;false;false;false;false;true;true;true]]));
    211   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(INDIRECT false)〉)))));
    212   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DIRECT [[true;false;false;false;false;false;true;true]])〉)))));
    213   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    214   RET … ;
    215   MOVX … (Left … 〈(ACC_A),(EXT_INDIRECT false)〉);
    216   SJMP … (RELATIVE [[true;true;true;true;false;true;true;true]]);
    217   CLR … (ACC_A);
    218   MOVC … (ACC_A) (ACC_DPTR);
    219   RET … ;
    220   MOVX … (Left … 〈(ACC_A),(EXT_INDIRECT_DPTR)〉);
    221   RET … ;
    222   CLR … (BIT_ADDR [[true;true;false;true;false;true;false;true]]);
    223   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;true]])〉)))));
    224   Jump … (JNB … (BIT_ADDR [[true;true;true;false;false;true;true;true]]) (RELATIVE [[false;false;false;false;true;true;false;true]]));
    225   SETB … (BIT_ADDR [[true;true;false;true;false;true;false;true]]);
    226   CLR … (ACC_A);
    227   CLR … (CARRY);
    228   SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;false]]);
    229   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
    230   CLR … (ACC_A);
    231   SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;true]]);
    232   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
    233   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;true;false;false;false;true]])〉)))));
    234   Jump … (JNB … (BIT_ADDR [[true;true;true;false;false;true;true;true]]) (RELATIVE [[false;false;false;false;true;true;false;true]]));
    235   CPL … (BIT_ADDR [[true;true;false;true;false;true;false;true]]);
    236   CLR … (ACC_A);
    237   CLR … (CARRY);
    238   SUBB … (ACC_A) (DIRECT [[false;false;false;true;false;false;false;false]]);
    239   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;false]]),(ACC_A)〉))));
    240   CLR … (ACC_A);
    241   SUBB … (ACC_A) (DIRECT [[false;false;false;true;false;false;false;true]]);
    242   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;true]]),(ACC_A)〉))));
    243   LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;true;true;false;false;false;true]]);
    244   Jump … (JNB … (BIT_ADDR [[true;true;false;true;false;true;false;true]]) (RELATIVE [[false;false;false;false;true;false;true;true]]));
    245   CLR … (ACC_A);
    246   CLR … (CARRY);
    247   SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;false]]);
    248   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
    249   CLR … (ACC_A);
    250   SUBB … (ACC_A) (DIRECT [[true;false;false;false;false;false;true;true]]);
    251   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
    252   RET … ;
    253   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    254   RET … ].
    255   @.
    256 nqed.
    257 
    258 ndefinition test ≝ test1 @ test2 @ test3 @ test4.
     410  POP … (DIRECT [[true;true;true;false;false;false;false;false]]);
     411  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     412  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;true;true;false]])〉))));
     413  ADD … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;false]]);
     414  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     415  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     416  ADDC … (ACC_A) (DIRECT [[false;false;false;false;false;true;true;true]]);
     417  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
     418  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;true;true]])〉)))));
     419  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
     420  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;true]])〉)))));
     421  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;true;false]]),(ACC_A)〉))));
     422  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;true;true;false]])〉)))));
     423  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(ACC_A)〉))));
     424  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     425  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;false;false]])〉)))));
     426  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(ACC_A)〉))));
     427  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;false;false;false;true]])〉)))));
     428  ADD … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
     429  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(ACC_A)〉))))
     430  ].
     431  @.
     432nqed.
     433
     434ndefinition test ≝ test1 @ test2 @ test3 @ test4 @ test5 @ test6 @ test7
     435                         @ test8 @ test9.
Note: See TracChangeset for help on using the changeset viewer.