Changeset 2783 for src/common/GenMem.ma


Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r2608 r2783  
    207207    let blocks ≝ update_block … b content (blocks … m) in
    208208     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
     209     
     210(* Axiom of extensional equality for the memory *)     
     211axiom mem_ext_eq :
     212  ∀m1,m2 : mem.
     213  (∀b.let bc1 ≝ blocks m1 b in
     214      let bc2 ≝ blocks m2 b in
     215      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
     216      ∀z.contents bc1 z = contents bc2 z) →
     217  nextblock m1 = nextblock m2 → m1 = m2.     
     218
Note: See TracChangeset for help on using the changeset viewer.