Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (8 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/ExtraMonads.ma

    r2590 r2783  
    305305#y * #y_spec #v_spec %{y} % // >y_spec %
    306306qed.
     307
     308lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
     309res_preserve1 X Y F n (Error … e).
     310#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
     311qed.
Note: See TracChangeset for help on using the changeset viewer.