Changeset 275 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Nov 24, 2010, 3:40:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r274 r275 62 62 nqed. 63 63 64 naxiom less_than_or_equal_b: Nat → Nat → Bool.65 naxiom ior: Bool → Bool → Bool.66 naxiom neg: Bool → Bool.67 naxiom con: Bool → Bool → Bool.68 naxiom eq: Nat → Nat → Bool.69 70 64 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝ 71 65 λb: BitVector eight. … … 76 70 let carry_as_nat ≝ nat_of_bool carry in 77 71 let temporary ≝ minus (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) in 78 let ac_flag ≝ i or79 (neg (con (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat)))80 (con (con (eq b_as_nat Z) (eq c_as_nat Z)) (eqcarry_as_nat Z)) in81 let bit_six ≝ i or82 (neg (con (less_than_or_equal_b (modulus b_as_nat one_hundred_and_twenty_eight) (modulus c_as_nat one_hundred_and_twenty_eight)) (less_than_or_equal_b temporary carry_as_nat)))83 (con (con (eq b_as_nat Z) (eq c_as_nat Z)) (eqcarry_as_nat Z)) in72 let ac_flag ≝ inclusive_disjunction 73 (negation (conjunction (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat))) 74 (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in 75 let bit_six ≝ inclusive_disjunction 76 (negation (conjunction (less_than_or_equal_b (modulus b_as_nat one_hundred_and_twenty_eight) (modulus c_as_nat one_hundred_and_twenty_eight)) (less_than_or_equal_b temporary carry_as_nat))) 77 (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in 84 78 let old_result_1 ≝ b_as_nat  c_as_nat in 85 79 let old_result_2 ≝ old_result_1  carry_as_nat in
Note: See TracChangeset
for help on using the changeset viewer.