Ignore:
Timestamp:
Mar 16, 2013, 9:08:20 PM (7 years ago)
Author:
campbell
Message:

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2895 r2896  
    458458| % #E destruct
    459459] qed.
     460
     461(* For *functions* the mapping between identifiers and blocks is a bijection,
     462   but to show that we have to keep more invariants about the environment. *)
     463axiom symbol_for_block_fn : ∀F,genv,b,f,id.
     464  find_symbol F genv id = Some ? b →
     465  find_funct_ptr F genv b = Some ? f →
     466  symbol_for_block F genv b = Some ? id.
    460467
    461468(* The mapping of blocks to symbols is total for functions. *)
Note: See TracChangeset for help on using the changeset viewer.