Ignore:
Timestamp:
Mar 12, 2013, 6:51:15 PM (9 years ago)
Author:
piccolo
Message:

little bug fixed in TranslateUtils?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

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