Ignore:
Timestamp:
Dec 3, 2010, 10:33:48 AM (9 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/DoTest.ma

    r361 r369  
    55ndefinition testmem ≝ assembly test.
    66ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute six teststatus.
     7ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.
    88
    99notation "'STATUS'" with precedence 90 for @{ 'status }.
     
    2929
    3030nlemma xoo:
    31  first … (first … (fetch (code_memory testfinal) (program_counter testfinal))) =
     31 (let testfinal ≝ testfinal in
     32 first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) =
    3233 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
    3334 nnormalize in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.