Changeset 1955 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
May 16, 2012, 3:03:52 PM (8 years ago)
Author:
mulligan
Message:

Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some small changes to the statement

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1946 r1955  
    545545
    546546example add_SO:
    547  ∀pc.
    548  add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1) = bitvector_of_nat … (S pc).
     547  ∀n: nat.
     548  ∀m: nat.
     549    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
    549550 cases daemon.
    550551qed.
Note: See TracChangeset for help on using the changeset viewer.