Changeset 359 for Deliverables
 Timestamp:
 Dec 2, 2010, 10:25:32 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r357 r359 10 10 11 11 ndefinition add_n_with_carry: 12 ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) ( List Bool) ≝12 ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝ 13 13 λn: Nat. 14 14 λb: BitVector n. … … 28 28 let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in 29 29 let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in 30 ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result)) 31 (cy_flag :: ac_flag :: ov_flag :: Empty Bool)). 32 #H; nassumption; 33 nqed. 30 mk_Cartesian ? ? (bitvector_of_nat n result) 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 34 32 35 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) ( List Bool) ≝33 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝ 36 34 λb: BitVector eight. 37 35 λc: BitVector eight. … … 49 47 [ false ⇒ 50 48 let cy_flag ≝ false in 51 〈 bitvector_of_nat eight old_result_2, [ cy_flag ; ac_flag ; ov_flag ]〉49 〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉 52 50  true ⇒ 53 51 let cy_flag ≝ true in 54 52 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 55 〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ]〉53 〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉 56 54 ]. 57 55
Note: See TracChangeset
for help on using the changeset viewer.