Changeset 286 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 25, 2010, 11:18:27 AM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r281 r286 27 27 ndefinition eighteen ≝ nine + nine. 28 28 ndefinition nineteen ≝ ten + nine. 29 ndefinition twenty_four ≝ sixteen + eight. 29 30 ndefinition one_hundred ≝ ten * ten. 30 31 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. 
Deliverables/D4.1/Matita/Status.ma
r285 r286 567 567 ncases not_implemented. 568 568 nqed. 569 570 ndefinition bit_address_of_register ≝ 571 λs: Status. 572 λb, c, d: Bit. 573 let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 574 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in 575 let offset ≝ 576 if conjunction (negation r1) (negation r0) then 577 Z 578 else if conjunction (negation r1) r0 then 579 eight 580 else if conjunction r1 r0 then 581 twenty_four 582 else 583 sixteen 584 in 585 bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). 586 nnormalize. 587 nrepeat (napply less_than_or_equal_monotone). 588 napply less_than_or_equal_zero. 589 nrepeat (napply less_than_or_equal_monotone). 590 napply less_than_or_equal_zero. 591 nqed.
Note: See TracChangeset
for help on using the changeset viewer.