source: Deliverables/D4.1/Demo-March-2011/matita/Search.ma @ 646

Last change on this file since 646 was 646, checked in by mulligan, 10 years ago

Got Search.ma working with Matita emulator.

File size: 23.9 KB
Line 
1include "ASM.ma".
2
3ndefinition 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]]));
11  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  @.
38nqed.
39 
40ndefinition 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);
55  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  @.
84nqed.
85 
86ndefinition 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  @.
155nqed.
156
157ndefinition 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  @.
256nqed.
257
258ndefinition test ≝ test1 @ test2 @ test3 @ test4.
Note: See TracBrowser for help on using the repository browser.