Changeset 2889
- Timestamp:
- Mar 15, 2013, 7:36:04 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/ERTLptrToLTLProof.ma
r2883 r2889 274 274 ∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) → 275 275 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 276 eliminable ? (after l) stmt = None ?→276 eliminable ? (after l) stmt = false → 277 277 lives (inl ? ? r) (livebefore … fn l after). 278 278 #fix_comp #prog #fn #l * … … 429 429 letin p_out ≝ (mk_prog_params LTL_semantics ??) 430 430 letin trans_prog ≝ (b_graph_transform_program ????) 431 #st1 #st1' #st2 #f #fn * 431 #st1 #st1' #st2 #f #fn * 432 432 [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 433 433 normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H … … 444 444 change with p_in in match p_in; 445 445 change with trans_prog in match trans_prog; 446 #mid #mid1 #EQmid % [%] 447 [ cases (andb ??) whd in match (preserve_carry_bit ???); 448 whd in match ensure_step_block; normalize nodelta 449 XXX 450 451 452 whd normalize nodelta 453 change with p_out in match p_out; 454 change with p_in in match p_in; 455 change with trans_prog in match trans_prog; 456 letin coloured_dst ≝ (colouring ???) 457 letin coloured_src ≝ (colouring ???) 458 whd in match translate_op1; normalize nodelta 459 460 461 462 whd in match (translate_op1 ?????); 463 change with (bind_new_P' ? (? × ?) ? 464 (f_step ERTLptr_semantics ?????)); 465 whd in match (translate_data ????); 466 change with (bind_new_P' ??? (f_step ??????)); 467 whd in match (f_step ??????); 468 @(λH.H) 469 470 whd in match ( #mid whd # 471 472 446 % [2: % [ % | ] | skip] 473 447 qed. 474 448
Note: See TracChangeset
for help on using the changeset viewer.