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

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