Changeset 3523 for LTS/Final.ma


Ignore:
Timestamp:
Mar 11, 2015, 12:59:28 PM (5 years ago)
Author:
piccolo
Message:

closed all daemon with the final statement

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3511 r3523  
    1616include "Vm.ma".
    1717
    18 axiom simulates_measurable:
     18inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
     19  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
     20| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
     21                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
     22
     23lemma no_io_append : ∀S : abstract_status.
     24∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     25∀t2 : raw_trace … st2 st3.
     26no_io_trace … t1 → no_io_trace … t2 →
     27no_io_trace … (t1 @ t2).
     28#S #st1 #st2 #st3 #t1 lapply st3 elim t1
     29[ #st #st3 #t2 #_ //]
     30#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
     31[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
     32#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
     33#H3 %2 // @IH //
     34qed.
     35
     36lemma pre_measurable_no_io : ∀S : abstract_status.
     37∀st1,st2 : S. ∀t : raw_trace … st1 st2.
     38pre_measurable_trace … t →
     39no_io_trace … t.
     40#S #st1 #st2 #t #H elim H /2/ -st1-st2
     41#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
     42#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
     43qed.
     44
     45lemma head_of_no_io_is_no_io : ∀S : abstract_status.
     46∀st1,st2 : S. ∀t : raw_trace … st1 st2.
     47no_io_trace … t → as_classify … st1 ≠ cl_io.
     48#S #st1 #st2 #t #H elim H //
     49qed.
     50
     51
     52lemma no_io_append_l1 : ∀S : abstract_status.
     53∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     54∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
     55no_io_trace … t1.
     56#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
     57#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
     58[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     59#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
     60%2 // @IH //
     61qed.
     62
     63lemma no_io_append_l2 : ∀S : abstract_status.
     64∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     65∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
     66no_io_trace … t2.
     67#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
     68#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
     69[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     70#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
     71qed.
     72
     73lemma is_costlabelled_act_elim :
     74∀P : ActionLabel → Prop.
     75(∀l. is_costlabelled_act l → P l) →
     76(∀l. ¬is_costlabelled_act l → P l) →
     77∀l.P l.
     78#P #H1 #H2 * /2/
     79[ * /2/ @H2 % *] * /2/ @H2 %*
     80qed.
     81
     82(*
     83lemma append_silent_premeasurable_l : ∀S : abstract_status.
     84∀st1,st2,st3,st4 : S.∀t1 : raw_trace … st1 st2.∀l,prf.
     85∀t2 : raw_trace … st3 st4.
     86pre_measurable_trace … (t1 @ (t_ind … l prf t2)) →
     87as_classify … st2 ≠ cl_io.
     88#S #st1 #st2 #st3 #st4 #t1 lapply st4 lapply st3 -st3 -st4 elim t1
     89[ #st #st3 #st4 #l #prf #t2 #H @(head_of_premeasurable_is_not_io … H)
     90| #st' #st'' #st''' #l1 #prf #tl #IH
     91*)
     92
     93definition measurable_prefix ≝ 
     94λS : abstract_status.
     95λs1,s4 :S.
     96λt : raw_trace … s1 s4.
     97∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
     98∃l.∃prf : as_execute … l s2 s3.
     99∃t34 : raw_trace … s3 s4.
     100silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
     101
     102lemma measurable_prefix_of_premeasurable :
     103∀S : abstract_status.
     104∀s1,s4 : S.
     105∀t : raw_trace … s1 s4.
     106pre_measurable_trace … t →
     107get_costlabels_of_trace … t ≠ nil ? →
     108measurable_prefix … t.
     109#S #s1 #s4 #t elim t
     110[ #st #_ * #H @⊥ @H %]
     111#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
     112[ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
     113  % // % // %2 normalize % *]
     114#l #Hl #prf #t' #IH #H inversion H
     115[ #st #H1 #H2 #H3 #H4 #H5 destruct
     116| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     117  cases l2 in Hl Hl2 prf2;
     118  [ #f #c #_ * #z #EQ destruct
     119  | * [|#lbl] #_ * #z #EQ destruct
     120  | * [|#lbl * #H cases(H I)]
     121  ]
     122| #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     123  cases l2 in Hl Hl2 prf2;
     124  [ #f #c #_ * #z #EQ destruct
     125  | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
     126  | #lbl #_ * #z #EQ destruct
     127  ]
     128| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     129  cases l2 in Hl Hl2 prf2;
     130  [ #f #c * #H @⊥ @H %
     131  | #lbl1 #_ * #z * #z1 #EQ destruct
     132  | #lbl #_ * #z * #z1 #EQ destruct
     133  ]
     134| #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
     135  #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     136  cases l2 in Hl Hl2 prf2;
     137  [ #f #c * #H @⊥ @H %
     138  | #lbl1 #_ * #z * #z1 #EQ destruct
     139  | #lbl #_ * #z * #z1 #EQ destruct
     140  ]
     141]
     142#_ #_ #prf #H1 cases(IH pre_tl ?)
     143[2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
     144#s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
     145%{l1} %{prf1} %{t34} % // %
     146[ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
     147  #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
     148| >H3 //
     149]
     150qed.
     151
     152(*
     153definition measurable_suffix ≝
     154 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
     155∃s1_em1 : S.
     156∃t_pre_em : raw_trace … s1 s1_em1.
     157∃s1_postem1 : S.
     158     ∃t_post_em : raw_trace … s1_postem s1'.
     159     silent_trace S ?? t_post_em ∧
     160     ∃l_em : ActionLabel.
     161     ∃ex_em : as_execute … l_em s1_em s1_postem.
     162     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
     163     (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)).
     164*)     
     165
     166lemma append_nil_is_nil : ∀S : abstract_status.
     167∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
     168t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
     169#S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
     170[ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
     171#s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     172qed.
     173
     174lemma append_silent : ∀S : abstract_status.
     175∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
     176∀t2 : raw_trace … s2 s3.silent_trace … t1 →
     177silent_trace … t2 →
     178silent_trace … (t1 @ t2).
     179#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     180[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
     181#st1 #st2 #st3 #l #prf #tl #IH #t2 *
     182[2: * #H cases(H I) ] #H inversion H in ⊢ ?;
     183[ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
     184#st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     185#Ht2 % %2 // cases(IH … Ht2) /2/
     186inversion(tl' @ t2)
     187[2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
     188#st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
     189qed.
     190
     191
     192definition measurable_suffix ≝
     193 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
     194∃s1_em : S.
     195∃t_pre_em : raw_trace … s1 s1_em.
     196∃s1_postem : S.
     197     ∃t_post_em : raw_trace … s1_postem s1'.
     198     silent_trace S ?? t_post_em ∧
     199     ∃l_em : ActionLabel.
     200     ∃ex_em : as_execute … l_em s1_em s1_postem.
     201     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
     202     (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
     203     is_costlabelled_act l_em.
     204     
     205
     206lemma measurable_suffix_tind : ∀S : abstract_status.
     207∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
     208measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t.
     209#S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
     210[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
     211 inversion t_pre in ⊢ ?;
     212 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     213  #_ /4 by or_introl, conj/
     214 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
     215   lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
     216   [ #H38 #H39 #H40 #H41 destruct
     217   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
     218   ]
     219 normalize in e0; destruct
     220]
     221]
     222#s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
     223[ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
     224  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
     225| #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
     226  #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
     227  >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
     228]
     229qed.
     230
     231lemma measurable_suffix_append : ∀S : abstract_status.
     232∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     233measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
     234#S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
     235* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
     236%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
     237qed.
     238
     239lemma silent_append_l2 : ∀S : abstract_status.
     240∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     241silent_trace … (t1 @ t2) → silent_trace … t2.
     242#S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
     243#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
     244#H @IH % inversion H in ⊢ ?;
     245[ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
     246| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
     247]
     248qed.
     249
     250lemma silent_append_l1 : ∀S : abstract_status.
     251∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     252silent_trace … (t1 @ t2) → silent_trace … t1.
     253#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     254[ #st #t2 #_ %2 % *]
     255#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
     256% inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
     257#z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
     258%2 // cases(IH t2 …) /2/ inversion tl
     259[2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
     260#st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
     261[ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
     262| #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
     263]
     264qed.
     265
     266lemma measurable_suffix_append_l1 : ∀S : abstract_status.
     267∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     268measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
     269#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     270[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
     271 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
     272 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
     273 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
     274]
     275#st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
     276[ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
     277  * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     278  #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
     279  %{l_em} %{ex_em} /4 by refl, conj/
     280| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
     281  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
     282  change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) //
     283  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
     284]
     285qed.
     286
     287lemma measurable_suffix_append_case : ∀S : abstract_status.
     288∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     289measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
     290#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     291[ #st #t2 #H %2 assumption]
     292#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
     293cases(measurable_suffix_tind … Hsuff)
     294[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%);
     295 @(measurable_suffix_append_l1 … Hsuff) /2/
     296| #H cases(IH … H)
     297  [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append //
     298  | /2/
     299  ]
     300]
     301qed.
     302
     303
     304
     305theorem simulates_pre_mesurable:
     306 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     307 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     308  simulation_conditions … rel →
     309  pre_measurable_trace … t1 →
     310  ∀s2 : S2.
     311 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
     312  ∃s2'. ∃t2: raw_trace … s2 s2'.
     313    pre_measurable_trace … t2 ∧
     314    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
     315    Srel … rel s1' s2' ∧
     316    (measurable_suffix … t1 → measurable_suffix … t2) ∧
     317    (silent_trace … t1 → silent_trace … t2).
     318#S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
     319[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
     320 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
     321  * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     322 | #_ %2 % *
     323 ]
     324| #st1 #st2 #st3 #l #prf #tl #Hclass **
     325  [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
     326    cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
     327    #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
     328    [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
     329        #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
     330    #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
     331    cut(? : Prop)
     332      [3: #Hpre %
     333         [ %
     334             [ %
     335                 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
     336                 | assumption
     337                 ]
     338             |  #meas_suff cases(Hm ?)
     339                [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
     340                  destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
     341                  %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
     342                | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
     343                  [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
     344                    ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     345                  | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
     346                    * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
     347                    %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
     348                  ]
     349                ]
     350             ]
     351        | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
     352          #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     353          /4 by append_silent,or_introl/
     354        ]
     355     |
     356     ]
     357    @append_premeasurable_silent //
     358  | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
     359    cases(simulate_label … sim … prf … REL)
     360    [2,3: /2/]
     361    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
     362    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
     363    #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
     364    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
     365    [2: * [ #H inversion H
     366            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     367            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     368            ]
     369          | * #H cases(H I)
     370          ]
     371     ]
     372    %
     373    [ % [2: assumption] %
     374      [ @append_premeasurable_silent // %2 /2 by ex_intro/
     375       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
     376         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
     377         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     378         cases H47 #ABS @⊥ @ABS % ]
     379       @append_premeasurable_silent // % //
     380    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     381      [2: assumption] whd in ⊢ (???%);
     382      >get_cost_label_invariant_for_append_silent_trace_l //
     383    ] % assumption
     384    | #Hsuff cases(measurable_suffix_tind … Hsuff)
     385      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
     386      % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
     387      | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
     388        @measurable_suffix_append /2/
     389      ]
     390  ]
     391  ]
     392| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
     393  #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
     394  cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
     395  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
     396  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
     397  [2: @(pre_silent_io … sil_t2) assumption]
     398  #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
     399  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     400  [2: * [ #H inversion H
     401            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     402            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     403            ]
     404          | * #H cases(H I)
     405          ]
     406  ]
     407  %
     408    [ % [2: assumption]
     409      % [2: whd in ⊢ (??%?);
     410        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
     411        whd in ⊢ (???%);
     412        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
     413        @eq_f assumption ]
     414  @append_premeasurable_silent [2: //] %3
     415  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
     416  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
     417  [ #H49 #H50 #H51 #H52 #H53 destruct //]
     418  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
     419  #ABS @⊥ @ABS %
     420 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
     421      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
     422      % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
     423      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     424        @measurable_suffix_append /2/
     425      ]
     426  ]
     427| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
     428  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
     429   cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
     430   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     431   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
     432   cases(IH  … REL)
     433   [2: /2 by pre_silent_io/ ]
     434   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
     435   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     436   [2: * [ #H inversion H
     437            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     438            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     439            ]
     440          | * #H cases(H I)
     441          ]
     442  ]
     443  %
     444   [ % [2: assumption] %
     445   [2: whd in ⊢ (??%?);
     446        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
     447        whd in ⊢ (???%);
     448        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
     449        @eq_f assumption ]
     450   @append_premeasurable_silent try assumption
     451     %4 try assumption
     452     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
     453       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
     454       #ABS @⊥ @ABS %
     455     | whd %{f} %{lab} %
     456     | @append_premeasurable_silent // % assumption
     457     ]
     458   | #Hsuff cases(measurable_suffix_tind … Hsuff)
     459      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
     460      % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
     461      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     462        @measurable_suffix_append /2/
     463      ]
     464  ]
     465|  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     466  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
     467  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
     468  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
     469  #sil_tr2 #call_rel cases(IH1 … REL1)
     470  [2: /2 by pre_silent_io/ ]
     471  #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
     472  cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     473  #st3'' * #st4' * #st4'' *
     474  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
     475  #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
     476  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
     477  %
     478  [2: * [ #H inversion H
     479            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     480            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     481            ]
     482          | * #H cases(H I)
     483          ]
     484  ]
     485  %
     486  [ % [2: assumption] %
     487  [ @append_premeasurable_silent try assumption %5
     488       [1,2: /2 by pre_silent_io/
     489             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
     490             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
     491             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
     492             cases H107 #ABS @⊥ @ABS %
     493       | whd %{f} %{l} %
     494       | assumption
     495       | @append_premeasurable_silent try assumption [2: % //]
     496         @append_silent_premeasurable // % //
     497       | @append_premeasurable_silent try assumption
     498       | @(RET_REL … call_rel) assumption
     499       | %
     500       ]
     501  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
     502    whd in ⊢ (??%%); @eq_f >append_associative
     503    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     504    [2: % // ] >append_associative
     505    >get_cost_label_append in ⊢ (???%);
     506    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     507    [2: % //] normalize
     508    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     509    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     510    assumption
     511  ]
     512  % //
     513 | #Hsuff cases(measurable_suffix_tind … Hsuff)
     514   [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
     515     * #ex_em ** inversion t_pre in ⊢ ?;
     516     [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
     517         #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
     518         -Hsuff -e0 -EQ #H inversion H
     519         [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
     520         #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
     521     ]
     522     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     523     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
     524   | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
     525     change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
     526     cases(measurable_suffix_append_case … Hsuff)
     527     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     528       [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
     529         -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
     530         #st2 #_ #EQ destruct(EQ)
     531       | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
     532       ]
     533     | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
     534       [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
     535         lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     536       | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
     537         * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
     538         %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
     539       ]
     540     ]
     541   ]
     542 ]
     543]
     544qed.
     545         
     546       
     547lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
     548get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
     549#S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
     550[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     551| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     552| #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     553| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     554| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
     555  #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
     556  destruct
     557]
     558whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
     559#prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl;
     560[2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
     561#st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
     562qed.
     563
     564lemma measurable_is_measurable_suffix : ∀S : abstract_status.
     565∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
     566#S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *****
     567#EQ destruct /11 width=20 by conj,ex_intro/
     568qed.
     569
     570lemma get_costlabelled_is_costlabelled :
     571∀S : abstract_status.∀s1,s2,s3 : S. ∀l.
     572∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
     573is_costlabelled_act l →
     574|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
     575#S #s1 #s2 #s3 * normalize
     576  [ /2 by monotonic_pred/
     577  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
     578  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
     579  ]
     580qed.
     581
     582lemma silent_suffix_cancellable : ∀S : abstract_status.
     583∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
     584∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
     585∀t2 : raw_trace … s3 s4.
     586∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
     587∀t2' : raw_trace … s3' s4.
     588is_costlabelled_act l → is_costlabelled_act l' →
     589silent_trace … t2 → silent_trace … t2' →
     590t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
     591s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
     592#S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
     593lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
     594[ normalize #st * normalize
     595  [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
     596  | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     597    @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
     598    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     599    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
     600    ]
     601  ]
     602]
     603#st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
     604[ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     605  @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
     606    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     607    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
     608    ]
     609| #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
     610  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
     611]
     612qed.
     613
     614
     615lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status.
     616∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
     617∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
     618pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
     619silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
     620pre_measurable_trace … t1.
     621#S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
     622lapply s3 -s3 elim H -t -s1 -s4
     623[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
     624  [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
     625  | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
     626    normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
     627  ]
     628| #st1 #st2 #st3 #lbl #prf #tl #Hclass **
     629  [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
     630    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     631      destruct *
     632    | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?);
     633      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
     634    ]
     635  | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
     636    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     637      destruct #_ #_ #_ % //
     638    | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     639      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
     640   ]
     641 ]
     642| #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
     643  #t1 #t2 inversion t2 in ⊢ ?;
     644  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     645    destruct #_ #_ #_ % //
     646  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     647      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
     648  ]
     649| #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
     650  #t1 #t2 inversion t2 in ⊢ ?;
     651  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     652    destruct #_ #_ #_ % //
     653  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     654      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
     655  ]
     656| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
     657  #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
     658  #t3 #t4 inversion t4 in ⊢ ?;
     659  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     660    destruct #_ #_ #_ % //
     661  | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     662    lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
     663    cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
     664    [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
     665    #Hmeas cases(measurable_suffix_append_case … Hmeas)
     666    [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     667      [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
     668      | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
     669      ]
     670    | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
     671      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
     672      * #l_em * #ex_em ** #EQ destruct #H1 #H2
     673      change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0;
     674      <append_associative in e0; <append_associative #e0
     675      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
     676      >append_associative %5 /2/ [ %{f} %{c} //] normalize
     677      @(IH2 … (refl …)) /2/
     678     ]
     679   ]
     680 ]
     681qed.
     682 
     683
     684lemma measurable_suffix_is_measurable:
     685∀S : abstract_status.
     686∀s1,s4 : S.
     687∀t : raw_trace … s1 s4.
     688pre_measurable_trace … t →
     6892 ≤ |get_costlabels_of_trace … t | →
     690measurable_suffix … t → ∃s1,s3.
     691measurable … s1 … s3 … t.
     692#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
     693* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
     694>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
     695>(get_cost_label_silent_is_empty … sil_tpost) #CARD
     696cases(measurable_prefix_of_premeasurable … t_pre)
     697[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
     698|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
     699| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
     700  /20 width=20 by conj,ex_intro/
     701]
     702qed.
     703
     704
     705
     706theorem simulates_measurable:
    19707 ∀S1,S2: abstract_status.
    20708 
     
    36724 
    37725 ∃s1',s2'. measurable … s1' s2' … t'.
     726#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
     727cases(simulates_pre_mesurable … rel … t … Rsi_si') //
     728[2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
     729#Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
     730<EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
     731#H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
     732 >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
     733qed.
     734   
     735
     736
    38737
    39738theorem cerco:
Note: See TracChangeset for help on using the changeset viewer.