- Timestamp:
- Jul 5, 2012, 2:22:08 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r2149 r2154 703 703 nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2. 704 704 705 axiom add_bitvector_of_nat: 706 ∀n,m1,m2. 707 bitvector_of_nat n (m1 + m2) = 708 add n (bitvector_of_nat n m1) (bitvector_of_nat n m2). 709 705 710 example add_SO: 706 711 ∀n: nat. -
src/ASM/Assembly.ma
r2151 r2154 712 712 nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16). 713 713 714 715 (*CSC: move elsewhere*)716 axiom add_bitvector_of_nat:717 ∀n,m1,m2.718 bitvector_of_nat n (m1 + m2) =719 add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).720 714 721 715 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
Note: See TracChangeset
for help on using the changeset viewer.