Changeset 361


Ignore:
Timestamp:
Dec 2, 2010, 10:52:55 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r360 r361  
    55ndefinition testmem ≝ assembly test.
    66ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute one teststatus.
     7ndefinition testfinal ≝ execute six teststatus.
    88
    99notation "'STATUS'" with precedence 90 for @{ 'status }.
     
    2828*)
    2929
    30 
    3130nlemma xoo:
    32  fetch (code_memory testfinal) (program_counter testfinal) =
    33  fetch (code_memory testfinal) (program_counter testfinal).
    34  nnormalize in ⊢ (??%?); @;
     31 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))) =
     32 first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
     33 nnormalize in ⊢ (??%?);
    3534nqed.
    36 *)
    3735
    3836nlemma xoo: program_counter testfinal = program_counter testfinal.
    39  nnormalize in ⊢ (??%?); @;
     37 nnormalize in ⊢ (??%?);
    4038nqed.
Note: See TracChangeset for help on using the changeset viewer.