source: Deliverables/D4.1/Matita/Test.ma @ 352

Last change on this file since 352 was 352, checked in by mulligan, 9 years ago

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File size: 7.3 KB
Line 
1include "Interpret.ma".
2include "Assembly.ma".
3
4ndefinition test: List instruction ≝
5 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
6  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
7  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
8  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
9  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
10  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
11  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
12  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
13  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
14  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
15  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
16  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
17  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
18  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
19  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
20  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
21  CLR … (ACC_A);
22  MOVC … (ACC_A) (ACC_DPTR);
23  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
24  INC … (DPTR);
25  INC … (REGISTER [[false;false;false]]);
26  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]]));
27  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
28  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
29  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
30  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
31  CLR … (ACC_A);
32  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
33  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
34  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
35  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
36  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
37  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
38  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
39  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
40  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
41  CLR … (ACC_A);
42  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
43  INC … (REGISTER [[false;false;true]]);
44  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
45  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
46  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
47  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
48  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
49  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
50  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
51  CLR … (ACC_A);
52  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
53  INC … (DPTR);
54  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
55  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
56  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
57  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
58  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
59  XCHD … (ACC_A) (INDIRECT false);
60  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
61  RET … ;
62  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
63  RET … ;
64  NOP … ;
65  NOP … ;
66  NOP … ;
67  NOP … ;
68  NOP … ;
69  NOP … ;
70  NOP … ;
71  NOP … ;
72  NOP … ;
73  NOP … ;
74  NOP … ;
75  NOP … ;
76  NOP … ;
77  NOP … ;
78  NOP … ;
79  NOP … ;
80  NOP … ;
81  NOP … ;
82  NOP … ;
83  NOP … ;
84  NOP … ;
85  NOP … ;
86  NOP … ;
87  NOP … ;
88  NOP … ;
89  NOP … ;
90  NOP … ;
91  NOP … ;
92  NOP … ;
93  NOP … ;
94  NOP … ;
95  NOP … ;
96  NOP … ;
97  NOP … ;
98  NOP … ;
99  NOP … ;
100  NOP … ;
101  NOP … ;
102  NOP … ;
103  NOP … ;
104  NOP … ;
105  NOP … ;
106  NOP … ;
107  NOP … ;
108  NOP … ;
109  NOP … ;
110  NOP … ;
111  NOP … ;
112  NOP … ;
113  NOP … ;
114  NOP … ;
115  NOP … ;
116  NOP … ;
117  NOP … ;
118  NOP … ;
119  NOP … ;
120  NOP … ;
121  NOP … ;
122  NOP … ;
123  NOP … ;
124  NOP … ;
125  NOP … ;
126  NOP … ;
127  NOP … ;
128  NOP … ;
129  NOP … ;
130  NOP … ;
131  NOP … ;
132  NOP … ;
133  NOP … ;
134  NOP … ;
135  NOP … ;
136  NOP … ;
137  NOP … ;
138  NOP … ;
139  NOP … ;
140  NOP … ;
141  NOP … ;
142  NOP … ;
143  NOP … ;
144  NOP … ;
145  NOP … ;
146  NOP … ;
147  NOP … ;
148  NOP … ;
149  NOP … ;
150  NOP … ].
151 @.
152nqed.
Note: See TracBrowser for help on using the repository browser.