include "Universes.ma". include "Equality.ma". include "Connectives.ma". include "Nat.ma". include "Exponential.ma". include "Bool.ma". include "BitVector.ma". include "List.ma". ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))). ndefinition sixteen ≝ eight + eight. ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. ndefinition two_hundred_and_fifty_six ≝ one_hundred_and_twenty_eight + one_hundred_and_twenty_eight. ndefinition nat_of_bool ≝ λb: Bool. match b with [ False ⇒ Z | True ⇒ S Z ]. ndefinition add_n_with_carry: ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝ λn: Nat. λb: BitVector n. λc: BitVector n. λcarry: Bool. let b_as_nat ≝ nat_of_bitvector n b in let c_as_nat ≝ nat_of_bitvector n c in let carry_as_nat ≝ nat_of_bool carry in let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) + (modulus c_as_nat ((S (S Z)) * n)) + c_as_nat) ≥ ((S (S Z)) * n) in let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) + (modulus c_as_nat ((S (S Z))^(n - (S Z)))) + c_as_nat) ≥ ((S (S Z))^(n - (S Z)))) in let result ≝ modulus result_old ((S (S Z))^n) in let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result)) (cy_flag :: ac_flag :: ov_flag :: Empty Bool)). //. nqed. (* ndefinition sub_8_with_carry ≝ λb: BitVector eight. λc: BitVector eight. λcarry: Bool. let b_as_nat ≝ nat_of_bitvector eight b in let c_as_nat ≝ nat_of_bitvector eight c in let carry_as_nat ≝ nat_of_bool carry in let result_old_1 ≝ subtraction_underflow b_as_nat c_as_nat in match result_old_1 with [ Nothing ⇒ let ac_flag ≝ True in | Just result_old_1' ⇒ ] *) ndefinition add_8_with_carry ≝ add_n_with_carry eight. ndefinition add_16_with_carry ≝ add_n_with_carry sixteen. (* ndefinition increment ≝ λn: Nat. λb: BitVector n. let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in let overflow ≝ b_as_nat ≥ (S (S Z))^n in match overflow with [ False ⇒ bitvector_of_nat n b_as_nat | True ⇒ bitvector_of_nat n Z ]. ndefinition decrement ≝ λn: Nat. λb: BitVector n. let b_as_nat ≝ nat_of_bitvector n b in match b_as_nat with [ Z ⇒ max n | S o ⇒ bitvector_of_nat n o ]. alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop". ndefinition bitvector_of_bool: ∀n: Nat. ∀b: Bool. BitVector n ≝ λn: Nat. λb: Bool. ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). //. nqed. *)