Changeset 368


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

All 450 proof obligations closed.

Location:
Deliverables/D4.1/Matita
Files:
2 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
  • Deliverables/D4.1/Matita/Vector.ma

    r364 r368  
    422422  λv: Vector A n.
    423423  λq: Vector A m.
    424     let list_q ≝ list_of_vector A m q in
    425     let list_v ≝ list_of_vector A n v in
    426     let power ≝ power_list A list_q in
    427       member_with ? list_v (λx, y. eq_l ? f x y) power.
     424    fold_right ? ? ? (λx, v. conjunction v (fold_right ? ? ? (λy, z. inclusive_disjunction z (f x y)) false q)) true v.
    428425   
    429426(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.