source: LTS/Simulation.ma @ 3524

Last change on this file since 3524 was 3524, checked in by piccolo, 5 years ago

rearrangments of lemmas, final statement in place

File size: 17.0 KB
Line 
1include "Traces.ma".
2include "basics/jmeq.ma".
3
4discriminator option.
5
6record relations (S1,S2 : abstract_status) : Type[0] ≝
7 { Srel: S1 → S2 → Prop
8 ; Crel: S1 → S2 → Prop
9 }.
10
11definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'.
12 ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'.
13
14record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝
15 { initial_is_initial :
16   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
17 ; final_is_final :
18   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
19 ; simulate_tau:
20     ∀s1:S1.∀s2:S2.∀s1':S1.
21      as_execute … (cost_act (None ?))  s1 s1'→
22      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
23      ∃s2'. ∃t: raw_trace S2 s2 s2'.
24        Srel … rel s1' s2' ∧ silent_trace … t
25 ; simulate_label:
26     ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
27      as_execute S1 (cost_act (Some ? l)) s1 s1' →
28      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
29      Srel … rel s1 s2 →
30      ∃s2',s2'',s2'''.
31       ∃t1: raw_trace S2 s2 s2'.
32       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
33       ∃t3: raw_trace … s2'' s2'''.
34        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
35 ; simulate_call_pl:
36     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
37      is_call_post_label … s1 →
38      as_execute … (call_act f l) s1 s1' →
39      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
40      Srel … rel s1 s2 →
41      ∃s2',s2'',s2'''.
42       ∃t1: raw_trace S2 s2 s2'.
43       as_execute … (call_act f l) s2' s2'' ∧
44       bool_to_Prop(is_call_post_label … s2') ∧
45       ∃t3: raw_trace S2 s2'' s2'''.
46        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
47 ; simulate_ret_l:
48     ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
49      as_execute S1 (ret_act (Some ? l)) s1 s1' →
50      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
51      Srel  … rel s1 s2 →
52      ∃s2',s2'',s2'''.
53       ∃t1: raw_trace S2 s2 s2'.
54       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
55       ∃t3: raw_trace S2 s2'' s2'''.
56        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
57 ; simulate_call_n:
58     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
59      as_execute … (call_act f l) s1 s1' →
60      ¬ is_call_post_label … s1 →
61      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
62      Srel … rel s1 s2 →
63      ∃s2',s2'',s2'''.
64       ∃t1: raw_trace S2 s2 s2'.
65       bool_to_Prop (¬ is_call_post_label … s2') ∧
66       as_execute … (call_act f l) s2' s2'' ∧
67       ∃t3: raw_trace S2 s2'' s2'''.
68        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
69        ∧ Crel … rel s1 s2'
70 ; simulate_ret_n:
71     ∀s1:S1.∀s2:S2.∀s1':S1.
72      as_execute … (ret_act (None ?)) s1 s1' →
73      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
74      Srel … rel s1 s2 →
75      ∃s2',s2'',s2''': S2.
76       ∃t1: raw_trace S2 s2 s2'.
77       as_execute … (ret_act (None ?)) s2' s2''  ∧
78       ∃t3: raw_trace S2 s2'' s2'''.
79        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
80        ∧ Rrel … rel s1' s2''
81 ; simulate_io_in :
82   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
83   as_execute … (cost_act … (Some ? l)) s1 s1' →
84   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
85   Srel … rel s1 s2 →
86   ∃s2',s2''.∃t: raw_trace … s2 s2'.
87   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
88   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
89; simulate_io_out :
90   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
91   as_execute … (cost_act … (Some ? l)) s1 s1' →
92   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
93   Srel … rel s1 s2 →
94   ∃s2',s2''.∃t : raw_trace … s2' s2''.
95   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
96   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
97 }.
98
99
100theorem simulates_pre_mesurable:
101 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
102 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
103  simulation_conditions … rel →
104  pre_measurable_trace … t1 →
105  ∀s2 : S2.
106 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
107  ∃s2'. ∃t2: raw_trace … s2 s2'.
108    pre_measurable_trace … t2 ∧
109    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
110    Srel … rel s1' s2' ∧
111    (measurable_suffix … t1 → measurable_suffix … t2) ∧
112    (silent_trace … t1 → silent_trace … t2).
113#S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
114[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
115 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
116  * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
117 | #_ %2 % *
118 ]
119| #st1 #st2 #st3 #l #prf #tl #Hclass **
120  [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
121    cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
122    #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
123    [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
124        #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
125    #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
126    cut(? : Prop)
127      [3: #Hpre %
128         [ %
129             [ %
130                 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
131                 | assumption
132                 ]
133             |  #meas_suff cases(Hm ?)
134                [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
135                  destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
136                  %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
137                | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
138                  [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
139                    ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
140                  | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
141                    * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
142                    %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
143                  ]
144                ]
145             ]
146        | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
147          #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
148          /4 by append_silent,or_introl/
149        ]
150     |
151     ]
152    @append_premeasurable_silent //
153  | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
154    cases(simulate_label … sim … prf … REL)
155    [2,3: /2/]
156    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
157    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
158    #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
159    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
160    [2: * [ #H inversion H
161            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
162            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
163            ]
164          | * #H cases(H I)
165          ]
166     ]
167    %
168    [ % [2: assumption] %
169      [ @append_premeasurable_silent // %2 /2 by ex_intro/
170       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
171         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
172         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
173         cases H47 #ABS @⊥ @ABS % ]
174       @append_premeasurable_silent // % //
175    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
176      [2: assumption] whd in ⊢ (???%);
177      >get_cost_label_invariant_for_append_silent_trace_l //
178    ] % assumption
179    | #Hsuff cases(measurable_suffix_tind … Hsuff)
180      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
181      % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
182      | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
183        @measurable_suffix_append /2/
184      ]
185  ]
186  ]
187| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
188  #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
189  cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
190  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
191  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
192  [2: @(pre_silent_io … sil_t2) assumption]
193  #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
194  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
195  [2: * [ #H inversion H
196            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
197            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
198            ]
199          | * #H cases(H I)
200          ]
201  ]
202  %
203    [ % [2: assumption]
204      % [2: whd in ⊢ (??%?);
205        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
206        whd in ⊢ (???%);
207        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
208        @eq_f assumption ]
209  @append_premeasurable_silent [2: //] %3
210  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
211  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
212  [ #H49 #H50 #H51 #H52 #H53 destruct //]
213  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
214  #ABS @⊥ @ABS %
215 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
216      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
217      % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
218      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
219        @measurable_suffix_append /2/
220      ]
221  ]
222| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
223  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
224   cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
225   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
226   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
227   cases(IH  … REL)
228   [2: /2 by pre_silent_io/ ]
229   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
230   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
231   [2: * [ #H inversion H
232            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
233            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
234            ]
235          | * #H cases(H I)
236          ]
237  ]
238  %
239   [ % [2: assumption] %
240   [2: whd in ⊢ (??%?);
241        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
242        whd in ⊢ (???%);
243        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
244        @eq_f assumption ]
245   @append_premeasurable_silent try assumption
246     %4 try assumption
247     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
248       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
249       #ABS @⊥ @ABS %
250     | whd %{f} %{lab} %
251     | @append_premeasurable_silent // % assumption
252     ]
253   | #Hsuff cases(measurable_suffix_tind … Hsuff)
254      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
255      % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
256      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
257        @measurable_suffix_append /2/
258      ]
259  ]
260|  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
261  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
262  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
263  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
264  #sil_tr2 #call_rel cases(IH1 … REL1)
265  [2: /2 by pre_silent_io/ ]
266  #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
267  cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
268  #st3'' * #st4' * #st4'' *
269  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
270  #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
271  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
272  %
273  [2: * [ #H inversion H
274            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
275            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
276            ]
277          | * #H cases(H I)
278          ]
279  ]
280  %
281  [ % [2: assumption] %
282  [ @append_premeasurable_silent try assumption %5
283       [1,2: /2 by pre_silent_io/
284             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
285             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
286             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
287             cases H107 #ABS @⊥ @ABS %
288       | whd %{f} %{l} %
289       | assumption
290       | @append_premeasurable_silent try assumption [2: % //]
291         @append_silent_premeasurable // % //
292       | @append_premeasurable_silent try assumption
293       | @(RET_REL … call_rel) assumption
294       | %
295       ]
296  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
297    whd in ⊢ (??%%); @eq_f >append_associative
298    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
299    [2: % // ] >append_associative
300    >get_cost_label_append in ⊢ (???%);
301    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
302    [2: % //] normalize
303    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
304    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
305    assumption
306  ]
307  % //
308 | #Hsuff cases(measurable_suffix_tind … Hsuff)
309   [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
310     * #ex_em ** inversion t_pre in ⊢ ?;
311     [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
312         #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
313         -Hsuff -e0 -EQ #H inversion H
314         [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
315         #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
316     ]
317     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
318     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
319   | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
320     change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
321     cases(measurable_suffix_append_case … Hsuff)
322     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
323       [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
324         -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
325         #st2 #_ #EQ destruct(EQ)
326       | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
327       ]
328     | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
329       [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
330         lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
331       | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
332         * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
333         %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
334       ]
335     ]
336   ]
337 ]
338]
339qed.
340
341theorem simulates_measurable:
342 ∀S1,S2: abstract_status.
343 
344 ∀rel: relations S1 S2. simulation_conditions … rel →
345 
346 ∀si,sn: S1. ∀t: raw_trace … si sn.
347 
348 ∀s1,s2. measurable … s1 s2 … t →
349 
350 ∀si': S2. as_classify … si' ≠ cl_io →
351 
352 Srel … rel si si' →
353 
354 ∃sn'. ∃t': raw_trace … si' sn'.
355
356 Srel … rel sn sn' ∧
357
358 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
359 
360 ∃s1',s2'. measurable … s1' s2' … t'.
361#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
362cases(simulates_pre_mesurable … rel … t … Rsi_si') //
363[2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
364#Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
365<EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
366#H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
367 >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
368qed.
Note: See TracBrowser for help on using the repository browser.