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

Last change on this file since 352 was 352, checked in by mulligan, 10 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.