Changeset 3388 for LTS


Ignore:
Timestamp:
Aug 27, 2013, 6:11:57 PM (6 years ago)
Author:
piccolo
Message:

partial commit

Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3387 r3388  
    1010 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
    1111
    12 record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0]
     12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop
    1313 { simulate_tau:
    1414     ∀s1,s2,s1' : S.
     
    1616      Srel … rel s1 s2 →
    1717      ∃s2'. ∃t: raw_trace S s2 s2'.
    18         Srel … rel s2 s2' ∧ silent_trace … t
     18        Srel … rel s1' s2' ∧ silent_trace … t
    1919 ; simulate_label:
    2020     ∀s1,s2,l,s1'.
    2121      as_execute S (cost_act (Some ? l)) s1 s1' →
     22      as_classify … s1' ≠ cl_io →
    2223      Srel … rel s1 s2 →
    2324      ∃s2',s2'',s2'''.
    2425       ∃t1: raw_trace S s2 s2'.
    25        as_execute … (cost_act (Some ? l)) s2' s2'' ∧
     26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
    2627       ∃t3: raw_trace S s2'' s2'''.
    2728        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    3031      is_call_post_label … s1 →
    3132      as_execute … (call_act f l) s1 s1' →
     33      as_classify … s1' ≠ cl_io →
    3234      Srel … rel s1 s2 →
    3335      ∃s2',s2'',s2'''.
    3436       ∃t1: raw_trace S s2 s2'.
     37       as_classify … s2' ≠ cl_jump ∧
    3538       as_execute … (call_act f l) s2' s2'' ∧
     39       bool_to_Prop(is_call_post_label … s2') ∧
     40       as_classify … s2'' ≠ cl_io ∧
    3641       ∃t3: raw_trace S s2'' s2'''.
    3742        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    3944     ∀s1,s2,s1' : S.∀l.
    4045      as_execute S (ret_act (Some ? l)) s1 s1' →
     46      as_classify … s1' ≠ cl_io →
    4147      Srel  … rel s1 s2 →
    4248      ∃s2',s2'',s2'''.
    4349       ∃t1: raw_trace S s2 s2'.
     50       as_classify … s2' ≠ cl_jump ∧
    4451       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
     52       as_classify … s2'' ≠ cl_io ∧
    4553       ∃t3: raw_trace S s2'' s2'''.
    46         Srel … rel s2 s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    4755 ; simulate_call_n:
    4856     ∀s1,s2,s1' : S.∀f,l.
     
    8997
    9098
     99lemma append_premeasurable_silent : ∀S : abstract_status.
     100∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     101pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io →
     102pre_measurable_trace … (t' @ t).
     103#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     104[ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
     105#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
     106[ #s #EQ1 #EQ2 destruct #EQ destruct]
     107#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
     108destruct #_ #Hs1' whd in ⊢ (????%); %2
     109[ assumption
     110| %{(None ?)} %
     111| @IH try assumption >Hclass % #EQ destruct
     112]
     113qed.
     114
     115definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     116raw_trace S st1 st2 → bool ≝
     117λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     118
     119lemma append_well_formed_silent : ∀S : abstract_status.
     120∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     121well_formed_trace … t → pre_silent_trace … t' →
     122(is_trace_non_empty … t' → as_classify … st1' = cl_other) →
     123well_formed_trace … (t' @ t).
     124#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     125[ #st #t #H #_ #_ assumption ]
     126#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
     127inversion H in ⊢ ?;
     128[ #st #EQ1 #EQ2 #EQ3 destruct]
     129#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
     130#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
     131[2: >(Hclass1 I) % #EQ destruct]
     132@IH try assumption #_ assumption
     133qed.
     134
     135lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
     136∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     137pre_silent_trace … t1 →
     138get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
     139#S #st1 #st2 #st3 #t1 elim t1
     140[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
     141inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     142#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
     143#_ whd in ⊢ (??%?); >IH [%] assumption
     144qed.
     145
     146(*
     147lemma raw_trace_ind_r : ∀S : abstract_status.
     148∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
     149(∀st : S.P … (t_base … st)) →
     150(∀st1,st2,st3,l.
     151 ∀prf : as_execute S l st2 st3.
     152 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
     153∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
     154#S #P #base #ind #st1 #st2 #t elim t [ assumption]
     155#st1 #st2 #st3 #l #prf #raw #IH
     156*)
     157
     158
    91159theorem simulates_pre_mesurable:
    92160 ∀S : abstract_status.∀rel : relations S.
    93161 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
     162  simulation_conditions S rel →
    94163  pre_measurable_trace … t1 →
    95   well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 →
    96   ∃s2'. ∃t2: raw_trace … s1' s2'.
     164  well_formed_trace … t1 → ∀s2 : S.
     165  as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
     166  ∃s2'. ∃t2: raw_trace … s2 s2'.
    97167    pre_measurable_trace … t2 ∧
    98168    well_formed_trace … t2 ∧
    99169    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    100     Srel … rel s2 s2'.
    101 cases daemon (*TODO*)
    102 qed.
     170    Srel … rel s1' s2'.
     171#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     172[ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
     173  /8 by refl, pm_empty, wf_empty, conj/
     174| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
     175  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
     176  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
     177    * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'')
     178    [2: cases(well_formed_trace_inv … well_formed)
     179         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     180             #EQ destruct(EQ) assumption
     181         | *
     182            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
     183                assumption
     184            | * #EQ1 #EQ2 destruct
     185            ]
     186         ]
     187    |3: @(silent_io … silent_ts2'')  assumption   
     188    ]
     189    #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
     190    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] %
     191    [ %
     192      [ @append_premeasurable_silent assumption
     193      | @append_well_formed_silent assumption
     194      ]
     195    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     196      [% | assumption]
     197    ]
     198  | cases(simulate_label … good … execute … REL)
     199    [2: cases pre_measurable_tl
     200        [ #st #H @H
     201        | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
     202        | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
     203        | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
     204        | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
     205        ]
     206    ]
     207    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
     208    * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')
     209    [2: cases(well_formed_trace_inv … well_formed)
     210         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     211             #EQ destruct(EQ) assumption
     212         | *
     213            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
     214                assumption
     215            | * #EQ1 #EQ2 destruct
     216            ]
     217         ]
     218    |3: @(silent_io … sil_t_s2'''') assumption
     219    ]
     220    #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
     221    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
     222    %
     223    [ %
     224      [ @append_premeasurable_silent try assumption %2
     225        [ @(silent_io … t_s2'') assumption
     226        | %{(Some ? c)} %
     227        ]
     228        @append_premeasurable_silent assumption
     229      | @append_well_formed_silent try assumption inversion(as_classify … s2'')
     230        #Hclass
     231        [ %3 [2: %{c} %]
     232        |*: %2 [2,4: >Hclass % #EQ destruct]
     233        ]
     234        @append_well_formed_silent assumption
     235      ]
     236    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     237      [2: assumption] whd in ⊢ (???%);
     238      >get_cost_label_invariant_for_append_silent_trace_l
     239      [ % | assumption]
     240    ]
     241  ]
     242| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
     243  #pre_meas_tl #IH #H inversion H
     244  [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
     245  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
     246  [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
     247  #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
     248  cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
     249  [2: inversion pre_meas_tl
     250      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
     251      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
     252      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
     253      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
     254      destruct assumption ]
     255  #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2'''
     256  #sil_t1 #sil_t2
     257  cases(IH … wf_tl' … rel_s2_s2''')
     258  [2: @(silent_io … (proj1 … sil_t2)) assumption]
     259  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
     260  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
     261  % [2: whd in ⊢ (??%?);
     262        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     263        whd in ⊢ (???%);
     264        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     265        @eq_f assumption ]
     266  %
     267  [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     268    %3
     269    [ @(silent_io … (proj1 … sil_t1)) assumption
     270    | whd %{ret_lab} %
     271    | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     272    ]
     273  | @append_well_formed_silent
     274    [ %2 try assumption @append_well_formed_silent try assumption
     275      [ @(proj1 … sil_t2)
     276      | @(proj2 … sil_t2)
     277      ]
     278    | @(proj1 … sil_t1)
     279    | @(proj2 … sil_t1)
     280    ]
     281  ]
     282| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
     283  #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
     284  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
     285  [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
     286   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
     287   cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
     288   [2: inversion pre_tl
     289      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
     290      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
     291      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
     292      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
     293      destruct assumption ]
     294   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
     295   cases(IH … wf_tl' … REL)
     296   [2: @(silent_io … (proj1 … sil_t2)) assumption ]
     297   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
     298   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
     299   [2: whd in ⊢ (??%?);
     300        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     301        whd in ⊢ (???%);
     302        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     303        @eq_f assumption ]
     304   %
     305   [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     306     %4 try assumption
     307     [ @(silent_io … (proj1 … sil_t1)) assumption
     308     | whd %{f} %{lab} %
     309     | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     310     ]
     311   | @append_well_formed_silent
     312     [ %2 try assumption @append_well_formed_silent try assumption
     313        [ @(proj1 … sil_t2)
     314        | @(proj2 … sil_t2)
     315        ]
     316     | @(proj1 …  sil_t1)
     317     | @(proj2 … sil_t1)
     318     ]
     319   ]
     320| cases daemon (*TODO*)
     321]
     322qed.
     323
     324 
     325 
     326   #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH
     327  #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL)
     328  #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil
     329  xxxxxxxxx
     330
     331
     332 #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?);   
     333      @append_premeasurable_silent
     334   
     335    xxxxxxxxxxxxxx
     336  ]
     337|*: cases daemon (*TODO*)
     338]
     339qed.*)
    103340
    104341(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
  • LTS/Traces.ma

    r3387 r3388  
    139139                  well_formed_trace … tl → is_non_silent_cost_act l →
    140140                  well_formed_trace … (t_ind … prf … tl).
     141(*  | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel.
     142                 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     143                 well_formed_trace … tl → as_classify … st1 = cl_io →
     144                 is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*)
     145
     146lemma well_formed_trace_inv :
     147∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
     148well_formed_trace … t →
     149(st1 = st2 ∧ t ≃ t_base S st1) ∨
     150(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     151well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
     152t ≃ t_ind … prf … tl) ∨
     153(∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
     154 well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
     155(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     156 well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
     157 is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
     158#S #st1 #st2 #t #H inversion H
     159[ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
     160| #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
     161  %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
     162| #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
     163  %{l} %{prf} %{tl} % // % //
     164(*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
     165  destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
     166]
     167qed.
     168
    141169
    142170let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     
    166194λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    167195
    168 inductive silent_trace (S : abstract_status) :
     196inductive pre_silent_trace (S : abstract_status) :
    169197∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    170 | silent_empty : ∀st : S.silent_trace … (t_base S st)
     198| silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
    171199| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    172                 ∀tl : raw_trace S st2 st3. silent_trace … tl →
    173                 silent_trace … (t_ind … prf … tl).
     200                ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other → pre_silent_trace … tl →
     201                pre_silent_trace … (t_ind … prf … tl).
     202
     203lemma silent_io : ∀S : abstract_status.
     204∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io →
     205as_classify … s2 ≠ cl_io.
     206#S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass]
     207#st1 #st2 #st3 #l #prf #tl #IH #H inversion H
     208[ #st' #EQ1 #EQ2 destruct #EQ destruct]
     209#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
     210#EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct
     211qed.
     212
     213definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     214raw_trace S st1 st2 → bool ≝
     215λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     216
     217definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
     218raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
     219(is_trace_non_empty … t → as_classify … st1 = cl_other).
     220
     221lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
     222∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
     223#S #st1 #st2 #t elim t -t
     224[ #st #_ %]
     225#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
     226[2: >cl % #EQ destruct]
     227@IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     228#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
     229% [ assumption | #_ assumption]
     230qed.
    174231
    175232inductive pre_measurable_trace (S : abstract_status) :
     
    199256                      is_unlabelled_ret_act l2 →
    200257                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
     258                     
     259lemma pre_measurable_trace_inv : ∀S : abstract_status.
     260∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
     261(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
     262(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     263 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
     264 pre_measurable_trace … tl) ∨
     265(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     266 t = t_ind … prf … tl ∧
     267 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
     268(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
     269 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
     270 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
     271(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
     272 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
     273 ∃prf' : as_execute S l2 st1'' st1'''.
     274 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
     275 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
     276 bool_to_Prop (¬ is_call_post_label … st1) ∧
     277 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
     278 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
     279#S #st1 #st2 #t #H inversion H
     280[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
     281| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     282  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     283| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     284  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     285| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     286  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
     287| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
     288  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
     289  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
     290  %{prf'} /12 by conj/
     291]
     292qed.
     293                     
Note: See TracChangeset for help on using the changeset viewer.