source: Deliverables/D4.1/Matita/DoTest.ma @ 369

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

Proof of missing lemma seems to be done, but won't Qed. My version of autotac seems to be behaving very strangely.

File size: 1.1 KB
Line 
1include "Test.ma".
2include "Interpret.ma".
3include "Assembly.ma".
4
5ndefinition testmem ≝ assembly test.
6ndefinition teststatus ≝ load testmem initialise_status.
7ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.
8
9notation "'STATUS'" with precedence 90 for @{ 'status }.
10interpretation "status" 'status = (mk_Status ??????????).
11
12(*
13nlemma xoo: testfinal = testfinal.
14 nnormalize in ⊢ (??%?); @;
15nqed.
16*)
17
18(*
19nlemma test:
20 (let status ≝
21 load
22  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
23   initialise_status
24  in
25   fetch (code_memory status) (program_counter status)
26  ) = ?.
27##[ nnormalize in ⊢ (??%?);
28*)
29
30nlemma xoo:
31 (let testfinal ≝ testfinal in
32 first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) =
33 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
34 nnormalize in ⊢ (??%?);
35nqed.
36
37nlemma xoo: program_counter testfinal = program_counter testfinal.
38 nnormalize in ⊢ (??%?);
39nqed.
Note: See TracBrowser for help on using the repository browser.