Ignore:
Timestamp:
Jan 11, 2013, 9:36:21 PM (7 years ago)
Author:
garnier
Message:

Progress on CL to CM, fixed some stuff in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2572 r2578  
    648648qed.
    649649
     650(* --------------------------------------------------------------------------- *)
     651(* Some more stuff on bitvectors. *)
     652(* --------------------------------------------------------------------------- *)
     653
    650654axiom commutative_multiplication :
    651655  ∀n. ∀v1,v2:BitVector n.
    652656  multiplication ? v1 v2 = multiplication ? v2 v1.
    653  
     657
    654658lemma commutative_short_multiplication :
    655659  ∀n. ∀v1,v2:BitVector n.
     
    670674axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
    671675
     676(* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *)
    672677
    673678
Note: See TracChangeset for help on using the changeset viewer.