Changeset 2863 for src/ERTLptr


Ignore:
Timestamp:
Mar 13, 2013, 2:22:29 PM (7 years ago)
Author:
piccolo
Message:

Added new invariant to good_if
Generalized version of cond case for the correctness proof of each translate step

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2855 r2863  
    184184include "joint/semantics_blocks.ma".
    185185include "ASM/Util.ma".
    186 include "joint/StatusSimulationHelper.ma".
    187186
    188187lemma eval_cond_ok :
     
    210209bool_to_Prop (taaf_non_empty … taf).
    211210#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
    212 #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
    213 @(general_eval_cond_ok … good … Rst1st2 … EQfetch EQeval)
    214 whd #lbl whd #mid1 normalize nodelta
    215 letin LTL_prog_params ≝ (mk_prog_params LTL_semantics ??)
    216 
    217 
    218  whd in match eval_state; normalize nodelta
     211#ltrue #lfalse #Rst1st2 #EQfetch
     212whd in match eval_state; normalize nodelta
    219213>EQfetch >m_return_bind
    220214whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
Note: See TracChangeset for help on using the changeset viewer.