Changeset 3391

Timestamp:

Oct 10, 2013, 5:28:33 PM (6 years ago)

Author:

piccolo

Message:

Definition of well formed trace is in the operational semantics

Location:

LTS

Files:

• Simulation.ma (modified) (13 diffs)
• Traces.ma (modified) (8 diffs)

LTS/Simulation.ma

@@ -14 +14 @@
      ∀s1,s2,s1' : S.
       as_execute … (cost_act (None ?))  s1 s1'→
-      Srel … rel s1 s2 →
+      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
       ∃s2'. ∃t: raw_trace S s2 s2'.
         Srel … rel s1' s2' ∧ silent_trace … t
@@ -20 +20 @@
      ∀s1,s2,l,s1'.
       as_execute S (cost_act (Some ? l)) s1 s1' →
-      as_classify … s1' ≠ cl_io → 
+      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
       Srel … rel s1 s2 →
       ∃s2',s2'',s2'''.
        ∃t1: raw_trace S s2 s2'.
-       as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
+       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
        ∃t3: raw_trace S s2'' s2'''.
         Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
@@ -31 +31 @@
       is_call_post_label … s1 →
       as_execute … (call_act f l) s1 s1' →
-      as_classify … s1' ≠ cl_io → 
+      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
       Srel … rel s1 s2 →
       ∃s2',s2'',s2'''.
        ∃t1: raw_trace S s2 s2'.
-       as_classify … s2' ≠ cl_jump ∧
        as_execute … (call_act f l) s2' s2'' ∧
        bool_to_Prop(is_call_post_label … s2') ∧
-       as_classify … s2'' ≠ cl_io ∧
        ∃t3: raw_trace S s2'' s2'''.
         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
@@ -44 +42 @@
      ∀s1,s2,s1' : S.∀l.
       as_execute S (ret_act (Some ? l)) s1 s1' →
-      as_classify … s1' ≠ cl_io → 
+      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
       Srel  … rel s1 s2 →
       ∃s2',s2'',s2'''.
        ∃t1: raw_trace S s2 s2'.
-       as_classify … s2' ≠ cl_jump ∧ 
        as_execute … (ret_act (Some ? l)) s2' s2'' ∧
-       as_classify … s2'' ≠ cl_io ∧
        ∃t3: raw_trace S s2'' s2'''.
         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
@@ -57 +53 @@
       as_execute … (call_act f l) s1 s1' →
       ¬ is_call_post_label … s1 →
+      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
       Srel … rel s1 s2 →
       ∃s2',s2'',s2'''.
        ∃t1: raw_trace S s2 s2'.
        bool_to_Prop (¬ is_call_post_label … s2') ∧
-       as_execute … (call_act f l) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧ 
-       as_classify … s2'' ≠ cl_io ∧
+       as_execute … (call_act f l) s2' s2'' ∧
        ∃t3: raw_trace S s2'' s2'''.
         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 
@@ -69 +65 @@
      ∀s1,s2,s1' : S.
       as_execute … (ret_act (None ?)) s1 s1' →
-      Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧
+      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 
+      Srel … rel s1 s2 →
       ∃s2',s2'',s2'''.
        ∃t1: raw_trace S s2 s2'.
-       as_execute … (ret_act (None ?)) s2' s2''  ∧ as_classify … s2' ≠ cl_jump ∧
-       as_classify … s2'' ≠ cl_io ∧
+       as_execute … (ret_act (None ?)) s2' s2''  ∧
        ∃t3: raw_trace S s2'' s2'''.
         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 
@@ -102 +98 @@
 lemma append_premeasurable_silent : ∀S : abstract_status.
 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
-pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io → 
+pre_measurable_trace … t → silent_trace … t' →  
 pre_measurable_trace … (t' @ t).
 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
-[ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
+[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
-[ #s #EQ1 #EQ2 destruct #EQ destruct]
+[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 
-destruct #_ #Hs1' whd in ⊢ (????%); %2 
+destruct #_ whd in ⊢ (????%); %2 
 [ assumption
 | %{(None ?)} %
@@ -116 +112 @@
 qed.
 
-lemma pre_silent_is_premeasurable : ∀S : abstract_status.
-∀st1,st2 : S. ∀t : raw_trace S st1 st2.as_classify … st1 ≠cl_io → pre_silent_trace … t 
+lemma silent_is_premeasurable : ∀S : abstract_status.
+∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t 
 → pre_measurable_trace … t.
 #S #st1 #st2 #t elim t 
-[ #st #Hst #H inversion H in ⊢ ?; [ #st' #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
-  #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
--t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #Hst1 #H inversion H in ⊢ ?;
-[ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
+[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
+#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
+-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
+[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
 @IH assumption
@@ -135 +131 @@
 lemma append_silent_premeasurable : ∀S : abstract_status.
 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
-pre_measurable_trace … t' → pre_silent_trace … t → as_classify … st1 ≠ cl_io → 
+pre_measurable_trace … t' → silent_trace … t →
 pre_measurable_trace … (t' @ t).
 #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
-[ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption
+[ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption
 |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct 
-  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r #Hs3 [ %2 | %3 | %4 ]
+  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
   try ( %{x} %) try @IH try assumption % ]
 #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
 #EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
-#r #pre_r #Hs5 normalize
-cut(∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
-    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
-    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2)
-[ @append_tind_commute ] #H >H >H >append_associative <H in ⊢ (????(??????%)); %5
+#r #pre_r normalize
+>append_tind_commute >append_tind_commute >append_associative 
+<append_tind_commute in ⊢ (????(??????%)); %5
 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
 qed.
-
-
-
-definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
-raw_trace S st1 st2 → bool ≝ 
-λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
 
 (*
@@ -175 +163 @@
 qed.*)
 
+(*
 lemma well_formed_append : ∀S : abstract_status.
 ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
@@ -210 +199 @@
 qed.
 *)
-
+*)
 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
-pre_silent_trace … t1 → 
+silent_trace … t1 → 
 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
 #S #st1 #st2 #st3 #t1 elim t1
 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H 
-inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
+inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
 #_ whd in ⊢ (??%?); >IH [%] assumption
@@ -242 +231 @@
 *)
 
+lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
+∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → 
+as_classify … st1 ≠ cl_io.
+#S #st1 #st2 #t #H inversion H //
+qed.
+
 
 theorem simulates_pre_mesurable:
@@ -248 +243 @@
   simulation_conditions S rel → 
   pre_measurable_trace … t1 →
-  well_formed_trace … t1 → ∀s2 : S.
-  as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
+  ∀s2 : S.
+ as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
   ∃s2'. ∃t2: raw_trace … s2 s2'.
     pre_measurable_trace … t2 ∧
-    well_formed_trace … t2 ∧
     get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
     Srel … rel s1' s2'.
 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
-[ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
-  /8 by refl, pm_empty, wf_empty, conj/
+[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
+  /8 by refl, silent_empty, conj, silent_is_premeasurable/
 | #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
-  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
-  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
-    ** #silent_ts2'' #Hclass_s2 #wf_ts2'' cases(IH … RELst2s2'') 
-    [2: cases(well_formed_trace_inv … well_formed)
-         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
-             #EQ destruct(EQ) assumption
-         | * 
-            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
-                assumption
-            | * #EQ1 #EQ2 destruct
-            ]
-         ]
-    |3: @(silent_io … silent_ts2'')  assumption    
-    ]
-    #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
-    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % 
-    [ % 
-      [ @append_premeasurable_silent assumption 
-      | @append_well_formed assumption
-      ]
-    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
-      [% | assumption]
-    ]
+  #pre_measurable_tl #IH #s2 #classify_s2 #REL
+  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
+    #silent_ts2'' cases(IH … RELst2s2'') /2 by silent_io/
+    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
+    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/ 
+    whd in ⊢ (??%?); /2/
   | cases(simulate_label … good … execute … REL) 
-    [2: cases pre_measurable_tl 
-        [ #st #H @H
-        | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
-        | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
-        | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
-        | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
-        ]
-    ] 
-    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2'''' 
-    ** #sil_ts2'' #Hclass_s2 #wf_ts2'' ** #sil_t_s2'''' #Hclass_s2''' #wf_ts2'''' cases(IH … RELst2_s2'''')
-    [2: cases(well_formed_trace_inv … well_formed)
-         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
-             #EQ destruct(EQ) assumption
-         | * 
-            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
-                assumption
-            | * #EQ1 #EQ2 destruct
-            ]
-         ]
-    |3: @(silent_io … sil_t_s2'''') assumption
-    ]
-    #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
+    [2,3: /2/] 
+    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' 
+    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by silent_io/
+    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
     %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
     % 
-    [ %
-      [ @append_premeasurable_silent try assumption %2
-        [ @(silent_io … t_s2'') assumption
-        | %{(Some ? c)} %
-        ]
-        @append_premeasurable_silent assumption
-      | @append_well_formed try assumption inversion(as_classify … s2'')
-        #Hclass
-        [ %3 [2: %{c} %] 
-        |*: %2 [2,4: >Hclass % #EQ destruct]
-        ]
-        @append_well_formed assumption
-      ]
+    [ /4 by pm_cons_cost_act, silent_io, ex_intro, append_premeasurable_silent/
     | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
-      [2: assumption] whd in ⊢ (???%);
-      >get_cost_label_invariant_for_append_silent_trace_l
-      [ % | assumption]
+      [2: assumption] whd in ⊢ (???%); 
+      >get_cost_label_invariant_for_append_silent_trace_l //
     ]
   ]
 | #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
-  #pre_meas_tl #IH #H inversion H
-  [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
-  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl' 
-  [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
-  #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
-  cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
-  [2: inversion pre_meas_tl
-      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
-      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
-      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
-      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
-      destruct assumption ] 
-  #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2''' 
-  #sil_t1 #sil_t2
-  cases(IH … wf_tl' … rel_s2_s2''')
-  [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption]
-  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
+  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
+  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
+  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2''' 
+  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
+  [2: @(silent_io … sil_t2) assumption]
+  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
   %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
   % [2: whd in ⊢ (??%?); 
-        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
+        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
         whd in ⊢ (???%);
-        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
+        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
         @eq_f assumption ]
-  %
-  [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
-    %3
-    [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
-    | whd %{ret_lab} %
-    | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
-    ]
-  | @append_well_formed
-    [ @(proj2 … sil_t1)]
-    %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
-  ]
-| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
-  #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
-  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
-  [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
-   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
-   cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
-   [2: inversion pre_tl
-      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
-      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
-      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
-      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
-      destruct assumption ] 
-   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
-   cases(IH … wf_tl' … REL)
-   [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption ]
-   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
+  /4 by pm_cons_lab_ret, silent_io, ex_intro, append_premeasurable_silent/
+| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
+  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
+   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2') 
+   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
+   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
+   cases(IH  … REL)
+   [2: /2 by silent_io/ ]
+   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
    %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
    [2: whd in ⊢ (??%?); 
-        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
+        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
         whd in ⊢ (???%);
-        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
+        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
         @eq_f assumption ]
-   %
-   [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
+   @append_premeasurable_silent try assumption
      %4 try assumption
-     [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
+     [ /2 by silent_io/
      | whd %{f} %{lab} %
-     | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
+     | /2 by append_premeasurable_silent/
      ]
-   | @append_well_formed [ @(proj2 … sil_t1) ]
-     %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
-   ]
 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
   #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
-  #IH1 #IH2 #wf_all #st1' #Hst1' #REL 
-  cases(simulate_call_n … good … exe_12 … Hst1 … REL)
-  #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1 
+  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
+  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1 
   #sil_tr2 #call_rel cases(IH1 … REL1)
-  [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct] 
-      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_
-      #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl))
-  |3: @(silent_io … (proj1 … (proj1 … sil_tr2))) assumption
-  ]
-  #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2
-  cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' *
-  #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3)
-  [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct]
-      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ)] #_
-      #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) -wf_tl -wf_all
-      #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
-      #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_
-      #EQ1 #EQ2 #EQ3 destruct #_ assumption
-  |3: @(silent_io … (proj1 … (proj1 … sil_tr5))) assumption
-  ]
-  #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'} 
+  [2: /2 by silent_io/ ] 
+  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
+  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ] 
+  #st3'' * #st4' * #st4'' *
+  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by silent_io/ ]
+  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'} 
   %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
   % [2: assumption] %
-  [ %
-     [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr1)) ]
-       %5
-       [ @(silent_io … (proj1 … (proj1 … sil_tr1))) assumption
-       | @(silent_io … (proj1 … (proj1 … sil_tr4))) assumption
+  [ @append_premeasurable_silent try assumption %5 
+       [1,2: /2 by silent_io/
        | whd %{f} %{l} %
        | assumption 
-       | @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr2))]
-         @append_silent_premeasurable try assumption @(proj1 … (proj1 … sil_tr4))
-       | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_tr5))
+       | @append_premeasurable_silent try assumption
+         @append_silent_premeasurable assumption
+       | @append_premeasurable_silent try assumption
        | @(RET_REL … call_rel) assumption
        | %
        ]
-     | @append_well_formed [ @(proj2 … sil_tr1) ]
-       %2 [2: assumption] >append_associative @append_well_formed
-       [ @(proj2 … sil_tr2) ]  @append_well_formed
-       [ @append_well_formed try assumption @silent_is_well_formed assumption ]
-       %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed
-       assumption
-     ]
-  | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … (proj1 … sil_tr1)) ]
+  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
     whd in ⊢ (??%%); @eq_f >append_associative 
     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
-    [2: @(proj1 … (proj1 … sil_tr2)) ] >append_associative 
+    [2: // ] >append_associative 
     >get_cost_label_append in ⊢ (???%);
     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
-    [2: @(proj1 … (proj1 … sil_tr4)) ] normalize
+    [2: //] normalize
     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
-    [2: @(proj1 … (proj1 … sil_tr5)) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
+    [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     assumption
   ]

LTS/Traces.ma

@@ -65 +65 @@
  | cl_other : status_class.
 
+definition is_non_silent_cost_act : ActionLabel → Prop ≝ 
+λact. ∃l. act = cost_act (Some ? l).
+
 record abstract_status : Type[2] ≝ 
  { as_status :> Type[0]
@@ -75 +78 @@
  ; is_io_entering : NonFunctionalLabel → bool
  ; is_io_exiting : NonFunctionalLabel → bool
+ ; jump_emits : ∀s1,s2,l.
+      as_classify … s1 = cl_jump → 
+      as_execute l s1 s2 → is_non_silent_cost_act l
  }.
  
@@ -118 +124 @@
 λact.act = ret_act (None ?).
 
-definition is_non_silent_cost_act : ActionLabel → Prop ≝ 
-λact. ∃l. act = cost_act (Some ? l).
-
 definition is_costlabelled_act : ActionLabel → Prop ≝ 
 λact.match act with [ call_act _ _ ⇒ True
@@ -127 +130 @@
                     | init_act ⇒ False
                     ].
-
-inductive well_formed_trace (S : abstract_status) :
-   ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ 
-  | wf_empty : ∀st: S.well_formed_trace … (t_base S st)
-  | wf_cons_no_jump :  ∀st1,st2,st3 : S.∀l : ActionLabel.
-                       ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3. 
-                       well_formed_trace … tl → as_classify … st1 ≠ cl_jump → 
-                       well_formed_trace … (t_ind … prf … tl)
-  | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
-                  ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
-                  well_formed_trace … tl → is_non_silent_cost_act l → 
-                  well_formed_trace … (t_ind … prf … tl).
-(*  | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel.
-                 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
-                 well_formed_trace … tl → as_classify … st1 = cl_io → 
-                 is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*)
-
+(*
 lemma well_formed_trace_inv :
 ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
@@ -167 +154 @@
 qed.
 
+*)
 
 let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
@@ -194 +182 @@
 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
 
-inductive pre_silent_trace (S : abstract_status) :
+inductive silent_trace (S : abstract_status) :
 ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ 
-| silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
+| silent_empty : ∀st : S.as_classify … st ≠ cl_io → silent_trace … (t_base S st)
 | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
-                ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl → 
-                pre_silent_trace … (t_ind … prf … tl).
+                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → silent_trace … tl → 
+                silent_trace … (t_ind … prf … tl).
 
 lemma silent_io : ∀S : abstract_status.
-∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io → 
+∀s1,s2 : S. ∀t : raw_trace … s1 s2. silent_trace … t → 
 as_classify … s2 ≠ cl_io.
-#S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass]
-#st1 #st2 #st3 #l #prf #tl #IH #H inversion H
-[ #st' #EQ1 #EQ2 destruct #EQ destruct]
+#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
+#st1 #st2 #st3 #l #prf #tl #IH #H inversion H // 
 #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
-#EQ destruct #_ #Hclass' @IH [ assumption ] assumption
+#EQ destruct #_ @IH assumption
 qed.
 
@@ -214 +201 @@
 raw_trace S st1 st2 → bool ≝ 
 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
-
+(*
 definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
 raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
-(is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
 well_formed_trace … t.
 
@@ -223 +209 @@
 ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
 #S #st1 #st2 #t * //
-qed.
+qed. *)
 (* elim t -t
 [ #st #_ %]