Changeset 368
 Timestamp:
 Dec 2, 2010, 6:27:52 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r367 r368 5 5 λb. 6 6 zero eight @@ b. 7 8 naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.9 7 10 8 naxiom execute_1_technical: … … 495 493 in 496 494 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 ); 516 509 nqed. 517 510 
Deliverables/D4.1/Matita/Vector.ma
r364 r368 422 422 λv: Vector A n. 423 423 λ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. 428 425 429 426 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.