- Timestamp:
- Mar 23, 2013, 2:31:23 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/ERTLptrToLTLProof.ma
r2942 r2944 649 649 #EQst1st2 #_ #_ 650 650 (* CSC: END *) 651 lapply (sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable) 652 XXXX 653 <EQst1st2 654 655 lapply Heval_seq_no_pc; whd in match eval_seq_no_pc; normalize nodelta 656 657 whd in Heval_seq_no_pc:(??%%); whd in match (st_no_pc ??); 658 659 660 661 662 663 <(injective_OK ??? EQst1_no_pc) 664 change with (set_regs ???) in match (st_no_pc ??); 651 letin before ≝ (livebefore ???) 652 whd in match succ_pc; normalize nodelta >point_of_pc_of_point 653 whd in match (point_of_succ ???); 654 cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1))) 655 [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt 656 (* Ha funzionato solo a dx, non a sinistra...*) 657 normalize nodelta whd in match statement_semantics; normalize nodelta 658 >Heliminable 659 cases daemon (*CSC: Genuine proof obligation! *) 660 | #Hext ] 661 >(to_be_cleared_fb_respects_equal_valuations … Hext) 662 >(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable) 663 >EQst1st2 664 >(to_be_cleared_sb_respects_equal_valuations … Hext) % 665 | 666 | 665 667 668 XXXX 666 669 667 670 *
Note: See TracChangeset
for help on using the changeset viewer.