Changeset 1946 for src/ASM/UtilBranch.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/UtilBranch.ma

    r1928 r1946  
    7373  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    7474    S (nat_of_bitvector_aux n buffer bv) =
    75       nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
     75      nat_of_bitvector … (add n (bitvector_of_nat … 1) bv).
    7676  #n #bv elim bv
    7777  [1:
     
    8989  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    9090    S (nat_of_bitvector … bv) = nat_of_bitvector …
    91       (\snd (half_add n (bitvector_of_nat … 1) bv)).
     91      (add n (bitvector_of_nat … 1) bv).
    9292  #n #bv elim bv
    9393  [1:
Note: See TracChangeset for help on using the changeset viewer.