Changeset 2869 for src/joint/semantics_blocks.ma
 Timestamp:
 Mar 14, 2013, 3:40:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics_blocks.ma
r2817 r2869 14 14 λp : evaluation_params.λcurr_id. 15 15 m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id). 16 17 definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.18 as_execute S s1 s2 →19 as_classifier … s1 cl_other →20 ∀taaf : trace_any_any_free S s2 s3.21 (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →22 trace_any_any_free S s1 s3 ≝23 λS,s1,s2,s3,H,I,tl.24 match tl return λs2,s3,tl.25 as_execute … s1 s2 →26 if taaf_non_empty … tl then ¬as_costed … s2 else True →27 trace_any_any_free S s1 s328 with29 [ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I30  taaf_step s2 s3 s4 taa H' I' ⇒31 λH,J.taaf_step … (taa_step … H I J taa) H' I'32  taaf_step_jump s2 s3 s4 taa H' I' K' ⇒33 λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'34 ] H.35 36 lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.37 bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).38 #S #s1 #s2 #s3 #H #I #tl lapply H H cases tl39 [ #s #H * % *: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]40 qed.41 16 42 17 lemma produce_step_trace :
Note: See TracChangeset
for help on using the changeset viewer.