Changeset 2944 for src

Timestamp:

Mar 23, 2013, 2:31:23 AM (7 years ago)

Author:

sacerdot

Message:

Some progress.

File:

• src/ERTLptr/ERTLptrToLTLProof.ma (modified) (1 diff)

src/ERTLptr/ERTLptrToLTLProof.ma

@@ -649 +649 @@
     #EQst1st2 #_ #_
     (* CSC: END *)
-    lapply (sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
-    XXXX
-    <EQst1st2
-    
-    lapply Heval_seq_no_pc; whd in match eval_seq_no_pc; normalize nodelta
-    
-     whd in Heval_seq_no_pc:(??%%); whd in match (st_no_pc ??);
-
-
-        
-        
-        
-        <(injective_OK ??? EQst1_no_pc)
-        change with (set_regs ???) in match (st_no_pc ??);
+    letin before ≝ (livebefore ???)
+    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
+    whd in match (point_of_succ ???);
+    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
+    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
+      (* Ha funzionato solo a dx, non a sinistra...*)
+      normalize nodelta whd in match statement_semantics; normalize nodelta
+      >Heliminable
+     cases daemon (*CSC: Genuine proof obligation! *)
+    | #Hext ]
+    >(to_be_cleared_fb_respects_equal_valuations … Hext)
+    >(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
+    >EQst1st2
+    >(to_be_cleared_sb_respects_equal_valuations … Hext) %
+|
+|
   
+  XXXX
   
   *