Ignore:
Timestamp:
Dec 2, 2010, 6:27:52 PM (9 years ago)
Author:
mulligan
Message:

All 450 proof obligations closed.

File:
1 edited

Legend:

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

    r367 r368  
    55  λb.
    66    zero eight @@ b.
    7    
    8 naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.
    97   
    108naxiom execute_1_technical:
     
    495493    in
    496494      s.
    497     ##[ ntry
    498           nassumption;
    499     ##| ntry (
    500           nnormalize
    501           nrepeat (napply (less_than_or_equal_monotone))
    502           napply (less_than_or_equal_zero)
    503         );
    504     ##| ntry (
    505           nnormalize
    506           //
    507         );
    508     ##| ntry (
    509           nnormalize
    510           //);
    511     ##| napply (execute_1_technical ? ? [[ acc_a ]]
    512                                         [[ direct; indirect; register;
    513                                            acc_a; acc_b; data; acc_dptr;
    514                                            acc_pc; ext_indirect;
    515                                            ext_indirect_dptr ]] ACC_A).
     495    ntry nassumption;
     496    ntry (
     497      nnormalize
     498      nrepeat (napply (less_than_or_equal_monotone))
     499      napply (less_than_or_equal_zero)
     500    );
     501    ntry (
     502      nnormalize
     503      //
     504    );
     505    ntry (
     506      napply (execute_1_technical … (subaddressing_modein …))
     507      napply I
     508    );     
    516509nqed.
    517510
Note: See TracChangeset for help on using the changeset viewer.