Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (10 years ago)
Author:
mulligan
Message:

less axioms

File:
1 edited

Legend:

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

    r347 r350  
    164164nqed.
    165165
    166 ndefinition testfinal ≝ execute five teststatus.
     166ndefinition testfinal ≝ execute one teststatus.
     167
     168nlemma hoo: (*half_add ? (program_counter teststatus)*)
     169  (bitvector_of_nat sixteen (S Z)) = (bitvector_of_nat sixteen (S Z)).
     170 (*half_add (code_memory teststatus) (program_counter teststatus). *)
     171 nwhd in ⊢ (??%?);
    167172
    168173nlemma hoo: testfinal = testfinal.
    169  nwhd in ⊢ (???%);
     174 nwhd in ⊢ (??%?);
    170175 nnormalize; @.
    171176nqed.
Note: See TracChangeset for help on using the changeset viewer.