Changeset 3495

Timestamp:

Sep 25, 2014, 2:24:12 PM (6 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Vm.ma (modified) (1 diff)

LTS/Vm.ma

@@ -987 +987 @@
       #EQlabels >act_op @IH
   ]
+  try //
+  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
+      >neutral_l assumption
+   |3: >neutral_r lapply(instr_map_ok … good … good_a1) 
+       [ whd in ⊢ (??%?); @eqb_elim
+         [ #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
+         normalize nodelta >EQi in ⊢ (??%?); %
+       | assumption
+       |*:
+       ]
+       normalize in ⊢ (% → ?); #H @H
+    
+  
    [2: assumption | | assumption | assumption | cases daemon (*TODO*)|
       whd in ⊢ (??%%);