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 one ≝ S Z.
ndefinition two ≝ (S(S(Z))).
ndefinition three ≝ two + one.
ndefinition four ≝ two + two.
ndefinition five ≝ three + two.
ndefinition six ≝ three + three.
ndefinition seven ≝ three + four.
ndefinition eight ≝ four + four.
ndefinition nine ≝ five + four.
ndefinition ten ≝ five + five.
ndefinition eleven ≝ six + five.
ndefinition twelve ≝ six + six.
ndefinition thirteen ≝ seven + six.
ndefinition fourteen ≝ seven + seven.
ndefinition fifteen ≝ eight + seven.
ndefinition sixteen ≝ eight + eight.
ndefinition seventeen ≝ nine + eight.
ndefinition eighteen ≝ nine + nine.
ndefinition nineteen ≝ ten + nine.
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.

*)