source: src/common/StructuredTraces.ma @ 1939

Last change on this file since 1939 was 1939, checked in by mulligan, 8 years ago

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

File size: 20.9 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4include "common/CostLabel.ma".
5include "utilities/option.ma".
6include "basics/lists/listb.ma".
7include "ASM/Util.ma".
8include "ASM/AbstractStatus.ma".
9
10(* temporary alias for backward compatibility *)
11definition final_abstract_status ≝ abstract_status.
12
13definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
14  λa_s,st.as_label ? st ≠ None ?.
15
16definition as_label_safe : ∀a_s : abstract_status.
17  (Σs : a_s.as_costed ? s) → costlabel ≝
18  λa_s,st_sig.opt_safe … (pi2 … st_sig).
19
20inductive trace_ends_with_ret: Type[0] ≝
21  | ends_with_ret: trace_ends_with_ret
22  | doesnt_end_with_ret: trace_ends_with_ret.
23
24inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
25  | tlr_base:
26      ∀status_before: S.
27      ∀status_after: S.
28        trace_label_label S ends_with_ret status_before status_after →
29        trace_label_return S status_before status_after
30  | tlr_step:
31      ∀status_initial: S.
32      ∀status_labelled: S.
33      ∀status_final: S.
34        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
35        trace_label_return S status_labelled status_final →
36          trace_label_return S status_initial status_final
37with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
38  | tll_base:
39      ∀ends_flag: trace_ends_with_ret.
40      ∀start_status: S.
41      ∀end_status: S.
42        trace_any_label S ends_flag start_status end_status →
43        as_costed S start_status →
44          trace_label_label S ends_flag start_status end_status
45with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
46  (* Single steps within a function which reach a label.
47     Note that this is the only case applicable for a jump. *)
48  | tal_base_not_return:
49      ∀start_status: S.
50      ∀final_status: S.
51        as_execute S start_status final_status →
52        (as_classifier S start_status cl_jump ∨
53         as_classifier S start_status cl_other) →
54        as_costed S final_status →
55          trace_any_label S doesnt_end_with_ret start_status final_status
56  | tal_base_return:
57      ∀start_status: S.
58      ∀final_status: S.
59        as_execute S start_status final_status →
60        as_classifier S start_status cl_return →
61          trace_any_label S ends_with_ret start_status final_status
62  (* A call followed by a label on return. *)
63  | tal_base_call:
64      ∀status_pre_fun_call: S.
65      ∀status_start_fun_call: S.
66      ∀status_final: S.
67        as_execute S status_pre_fun_call status_start_fun_call →
68        ∀H:as_classifier S status_pre_fun_call cl_call.
69          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
70          trace_label_return S status_start_fun_call status_final →
71          as_costed S status_final →
72            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
73  (* A call followed by a non-empty trace. *)
74  | tal_step_call:
75      ∀end_flag: trace_ends_with_ret.
76      ∀status_pre_fun_call: S.
77      ∀status_start_fun_call: S.
78      ∀status_after_fun_call: S.
79      ∀status_final: S.
80        as_execute S status_pre_fun_call status_start_fun_call →
81        ∀H:as_classifier S status_pre_fun_call cl_call.
82          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
83          trace_label_return S status_start_fun_call status_after_fun_call →
84          ¬ as_costed S status_after_fun_call →
85          trace_any_label S end_flag status_after_fun_call status_final →
86            trace_any_label S end_flag status_pre_fun_call status_final
87  | tal_step_default:
88      ∀end_flag: trace_ends_with_ret.
89      ∀status_pre: S.
90      ∀status_init: S.
91      ∀status_end: S.
92        as_execute S status_pre status_init →
93        trace_any_label S end_flag status_init status_end →
94        as_classifier S status_pre cl_other →
95        ¬ (as_costed S status_init) →
96          trace_any_label S end_flag status_pre status_end.
97
98let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
99  on tal : list (as_pc S) ≝
100 match tal with
101 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
102 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
103 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
104 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
105 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
106 ].
107
108definition as_trace_any_label_length':
109    ∀S: abstract_status.
110    ∀trace_ends_flag: trace_ends_with_ret.
111    ∀start_status: S.
112    ∀final_status: S.
113    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
114      nat ≝
115  λS: abstract_status.
116  λtrace_ends_flag: trace_ends_with_ret.
117  λstart_status: S.
118  λfinal_status: S.
119  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
120    |tal_pc_list … the_trace|.
121
122let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
123  match tlr with
124  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
125  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
126  ]
127and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
128  match tll with
129  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
130  ]
131and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
132  match tal with
133  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
134    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
135    tal_unrepeating … tl ∧
136    tlr_unrepeating … tlr
137  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
138    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
139    tal_unrepeating … tl
140  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
141  | _ ⇒ True
142  ].
143
144definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
145  trace_label_label S fl st1 st2 → costlabel ≝
146  λS,fl,st1,st2,tr.match tr with
147  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
148
149definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
150  trace_label_return S st1 st2 → costlabel ≝
151  λS,st1,st2,tr.match tr with
152  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
153  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
154  ].
155
156let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
157  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
158cases tal //
159#fl' #st1' [#st_fun] #st2' #st3' #H
160[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
161#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
162qed.
163
164inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
165  | tac_base:
166      ∀status: S.
167        as_classifier S status cl_call →
168          trace_any_call S status status
169  | tac_step_call:
170      ∀status_pre_fun_call: S.
171      ∀status_after_fun_call: S.
172      ∀status_final: S.
173      ∀status_start_fun_call: S.
174        as_execute S status_pre_fun_call status_start_fun_call →
175        ∀H:as_classifier S status_pre_fun_call cl_call.
176          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
177          trace_label_return S status_start_fun_call status_after_fun_call →
178          ¬ as_costed S status_after_fun_call →
179          trace_any_call S status_after_fun_call status_final →
180            trace_any_call S status_pre_fun_call status_final
181  | tac_step_default:
182      ∀status_pre: S.
183      ∀status_end: S.
184      ∀status_init: S.
185        as_execute S status_pre status_init →
186        trace_any_call S status_init status_end →
187        as_classifier S status_pre cl_other →
188        ¬ (as_costed S status_init) →
189          trace_any_call S status_pre status_end.
190
191             
192inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
193  | tlc_base:
194      ∀start_status: S.
195      ∀end_status: S.
196        trace_any_call S start_status end_status →
197        as_costed S start_status →
198        trace_label_call S start_status end_status
199.
200
201definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
202  trace_label_call S st1 st2 → costlabel ≝
203  λS,st1,st2,tr.match tr with
204  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
205  ].
206   
207coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
208  | tld_step:
209      ∀status_initial: S.
210      ∀status_labelled: S.
211          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
212          trace_label_diverges S status_labelled →
213            trace_label_diverges S status_initial
214  | tld_base:
215      ∀status_initial: S.
216      ∀status_pre_fun_call: S.
217      ∀status_start_fun_call: S.
218        trace_label_call S status_initial status_pre_fun_call →
219        as_execute S status_pre_fun_call status_start_fun_call →
220        ∀H:as_classifier S status_pre_fun_call cl_call.
221          trace_label_diverges S status_start_fun_call →
222            trace_label_diverges S status_initial.
223
224definition tld_hd_label : ∀S : abstract_status.∀st.
225  trace_label_diverges S st → costlabel ≝
226  λS,st,tr.match tr with
227  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
228  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
229  ].       
230
231(* Version in Prop for showing existence. *)
232coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
233  | tld_step:
234      ∀status_initial: S.
235      ∀status_labelled: S.
236          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
237          trace_label_diverges_exists S status_labelled →
238            trace_label_diverges_exists S status_initial
239  | tld_base:
240      ∀status_initial: S.
241      ∀status_pre_fun_call: S.
242      ∀status_start_fun_call: S.
243        trace_label_call S status_initial status_pre_fun_call →
244        as_execute S status_pre_fun_call status_start_fun_call →
245        ∀H:as_classifier S status_pre_fun_call cl_call.
246          trace_label_diverges_exists S status_start_fun_call →
247            trace_label_diverges_exists S status_initial.
248
249inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
250  | twp_terminating:
251      ∀status_initial: S.
252      ∀status_start_fun: S.
253      ∀status_final: S.
254        as_classifier S status_initial cl_call →
255        as_execute S status_initial status_start_fun →
256        trace_label_return S status_start_fun status_final →
257        as_final S status_final →
258        trace_whole_program S status_initial
259  | twp_diverges:
260      ∀status_initial: S.
261      ∀status_start_fun: S.
262        as_classifier S status_initial cl_call →
263        as_execute S status_initial status_start_fun →
264        trace_label_diverges S status_start_fun →
265        trace_whole_program S status_initial.
266
267(* Again, an identical version in Prop for existence proofs. *)
268inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
269  | twp_terminating:
270      ∀status_initial: S.
271      ∀status_start_fun: S.
272      ∀status_final: S.
273        as_classifier S status_initial cl_call →
274        as_execute S status_initial status_start_fun →
275        trace_label_return S status_start_fun status_final →
276        as_final S status_final →
277        trace_whole_program_exists S status_initial
278  | twp_diverges:
279      ∀status_initial: S.
280      ∀status_start_fun: S.
281        as_classifier S status_initial cl_call →
282        as_execute S status_initial status_start_fun →
283        trace_label_diverges_exists S status_start_fun →
284        trace_whole_program_exists S status_initial.
285
286
287let rec trace_any_label_label S s s' f
288  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
289match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
290[ tal_base_not_return start final _ _ C ⇒ C
291| tal_base_return _ _  _ _ ⇒ I
292| tal_base_call _ _ _ _ _ _ _ C ⇒ C
293| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
294| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
295].
296
297definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
298  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
299  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
300
301lemma trace_label_label_label : ∀S,s,s',f.
302  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
303#S #s #s' #f #tr
304cases tr
305#f #start #end #tr' #C @(trace_any_label_label … tr')
306qed.
307
308definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
309  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
310  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
311
312lemma trace_any_call_call : ∀S,s,s'.
313  trace_any_call S s s' → as_classifier S s' cl_call.
314#S #s #s' #T elim T //
315qed.
316
317(* an uncalling, unreturning and *unjumping*,
318  as well as unlabelled (but possibly for the first and last statuses)
319  possibly empty trace segment *)
320inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
321  | taa_base :
322      ∀start_status: S.
323        trace_any_any S start_status start_status
324  | taa_step :
325      ∀status_pre: S.
326      ∀status_init: S.
327      ∀status_end: S.
328        as_execute S status_pre status_init →
329        trace_any_any S status_init status_end →
330        as_classifier S status_pre cl_other →
331        ¬as_costed … status_init →
332          trace_any_any S status_pre status_end.
333
334let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
335  match taa with
336  [ taa_base st1' ⇒ [st1']
337  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
338  ].
339
340let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
341  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
342  match taa1
343  return λst1,st2.λx : trace_any_any S st1 st2.
344    trace_any_any S st2 st3 → trace_any_any S st1 st3
345  with
346  [ taa_base _ ⇒ λtaa2.taa2
347  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
348      taa_step … H (taa_append_taa … tl taa2) G K
349  ].
350
351let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
352  on taa :
353  trace_any_label S fl st2 st3 →
354  trace_any_label S fl st1 st3 ≝
355  match taa
356  return λst1,st2.λx : trace_any_any S st1 st2.
357    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
358  with
359  [ taa_base _ ⇒ λtaa2.taa2
360  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
361      tal_step_default … H (taa_append_tal … tl taa2) G K
362  ].
363
364let rec tlr_rel S1 st1 st1' S2 st2 st2'
365  (tlr1 : trace_label_return S1 st1 st1')
366  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
367match tlr1 with
368  [ tlr_base st1 st1' tll1 ⇒
369    match tlr2 with
370    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
371    | _ ⇒ False
372    ]
373  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
374    match tlr2 with
375    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
376      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
377    | _ ⇒ False
378    ]
379  ]
380and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
381 (tll1 : trace_label_label S1 fl1 st1 st1')
382 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
383  match tll1 with
384  [ tll_base fl1 st1 st1' tal1 H ⇒
385    match tll2 with
386    [ tll_base fl2 st2 st2 tal2 G ⇒
387      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
388      tal_rel … tal1 tal2
389    ]
390  ]
391and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
392 (tal1 : trace_any_label S1 fl1 st1 st1')
393 (tal2 : trace_any_label S2 fl2 st2 st2')
394   on tal1 : Prop ≝
395  match tal1 with
396  [ tal_base_not_return st1 st1' _ _ _ ⇒
397    ∃st2mid,taa,H,G,K.
398    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
399      (tal_base_not_return ? st2mid st2' H G K)
400  | tal_base_return st1 st1' _ _ ⇒
401    ∃st2mid,taa,H,G.
402    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
403      (tal_base_return ? st2mid st2' H G)
404  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
405    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
406    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
407      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
408      tlr_rel … tlr1 tlr2
409  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
410    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
411    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
412      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
413      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
414  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
415    tal_rel … tl1 tal2 (* <- this makes it many to many *)
416  ].
417
418let rec as_compute_cost_trace_label_label
419  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
420    (start_status: S) (final_status: S)
421     
422      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
423        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
424  match the_trace with
425  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
426      let label ≝
427        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
428        [ None ⇒ λabs. ⊥
429        | Some l ⇒ λ_. l
430        ] labelled_proof
431      in
432        (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
433  ]
434and as_compute_cost_trace_any_label
435  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
436    (start_status: S) (final_status: S)
437      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
438        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
439  match the_trace with
440  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
441  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
442      as_compute_cost_trace_label_return … call_trace
443  | tal_base_return the_status _ _ _ ⇒ [ ]
444  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
445    _ _ _ call_trace _ final_trace ⇒
446    let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
447    let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
448        call_cost_trace @ final_cost_trace
449  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
450      as_compute_cost_trace_any_label … tail_trace
451  ]
452and as_compute_cost_trace_label_return
453  (S: abstract_status)
454    (start_status: S) (final_status: S)
455      (the_trace: trace_label_return S start_status final_status)
456        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
457  match the_trace with
458  [ tlr_base before after trace_to_lift ⇒
459      as_compute_cost_trace_label_label … trace_to_lift
460  | tlr_step initial labelled final labelled_trace ret_trace ⇒
461    let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
462    let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
463        labelled_cost @ return_cost
464  ].
465  [2:
466    cases abs -abs #abs @abs %
467  |1:
468    %{initial} whd in match label;
469    generalize in match labelled_proof; whd in ⊢ (% → ?);
470    cases (as_label S initial)
471    [1:
472      #absurd @⊥ cases absurd -absurd #absurd @absurd %
473    |2:
474      #costlabel normalize nodelta #_ %
475    ]
476  ]
477qed.
478
479(* XXX: dependent type madness *)
480
481let rec tll_rel_to_traces_same_cost
482  (S: abstract_status) (S': abstract_status)
483    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
484    (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
485      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
486        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
487          on the_trace_l:
488            tll_rel … the_trace_l the_trace_r →
489              as_compute_cost_trace_label_label … the_trace_l =
490                as_compute_cost_trace_label_label S' trace_ends_flag_r ? ? the_trace_r ≝ ?.
491and tal_rel_to_traces_same_cost
492  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
493    (trace_ends_flag_r: trace_ends_with_ret)
494      (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
495        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
496          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
497          on the_trace_l:
498            tal_rel … the_trace_l the_trace_r →
499              as_compute_cost_trace_any_label … the_trace_l =
500                as_compute_cost_trace_any_label … the_trace_r ≝ ?
501and tlr_rel_to_traces_same_cost
502  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
503    (start_status_r: S') (final_status_r: S')
504      (the_trace_l: trace_label_return S start_status_l final_status_l)
505        (the_trace_r: trace_label_return S' start_status_r final_status_r)
506        on the_trace_l:
507          tlr_rel … the_trace_l the_trace_r →
508            as_compute_cost_trace_label_return … the_trace_l =
509              as_compute_cost_trace_label_return … the_trace_r ≝ ?.
510  cases daemon
511qed.
Note: See TracBrowser for help on using the repository browser.