source: src/common/StatusSimulation.ma @ 2539

Last change on this file since 2539 was 2539, checked in by tranquil, 8 years ago

added cl_jump case to trace_any_any_free

File size: 34.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/StructuredTraces.ma".
16
17(* We work with two relations on states in parallel, as well as two derived ones.
18   sem_rel is the classic semantic relation between states, keeping track of
19   memory and how program counters are mapped between languages.
20   call_rel keeps track of what pcs corresponding calls have and just that:
21   this is different than corresponance between program counters in sem_rel when
22   CALL f ↦ instr* CALL f instr* *)
23
24record status_rel
25  (S1 : abstract_status)
26  (S2 : abstract_status)
27  : Type[1] ≝
28  { sem_rel :2> S1 → S2 → Prop
29  (* this is kept separate, as not necessarily carrier will
30     synchronise on calls. It should state the minimal properties
31     necessary for as_after_return (typically just the program counter)
32     maybe what function is called too? *)
33  ; call_rel : (Σs.as_classifier S1 s cl_call) →
34               (Σs.as_classifier S2 s cl_call) → Prop
35  ; sim_final :
36    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
37  }.
38
39(* The two derived relations are
40   label_rel which tells that the two states are colabelled
41   ret_rel which tells that two return states are in relation: the idea is that
42   it happens when "going back" through as_after_return on one side we get
43   a pair of call_rel related states, then we enjoy as_after_return also on the
44   other. Roughly call_rel will store just enough information so that we can
45   advance locally on a return step and build structured traces any way *)
46
47(* if we later generalise, we should move this inside status_rel *)
48definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
49
50definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
51  λs1_ret,s2_ret.
52  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
53                 call_rel ?? R s1_pre s2_pre →
54                 as_after_return S2 s2_pre s2_ret.
55
56(* the equivalent of a collapsable trace_any_label where we do not force
57   costedness of the lookahead status *)
58inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
59| taaf_base : ∀s.trace_any_any_free S s s
60| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
61  as_classifier S s2 cl_other →
62  trace_any_any_free S s1 s3
63| taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
64  as_classifier S s2 cl_jump →
65  as_costed S s3 →
66  trace_any_any_free S s1 s3.
67
68definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
69match taaf with
70[ taaf_base _ ⇒ false
71| _ ⇒ true
72].
73
74(* the base property we ask for simulation to work depends on the status_class
75   S will mark semantic relation, C call relation, L label relation, R return relation *)
76
77definition status_simulation ≝
78  λS1 : abstract_status.
79  λS2 : abstract_status.
80  λsim_status_rel : status_rel S1 S2.
81    ∀st1,st1',st2.as_execute S1 st1 st1' →
82    sim_status_rel st1 st2 →
83    match as_classify … st1 with
84    [ cl_call ⇒ ∀prf.
85      (*
86           st1' ------------S----------\
87            ↑ \                         \
88           st1 \--L--\                   \
89            | \       \                   \
90            S  \-C-\  st2_after_call →taa→ st2'
91            |       \     ↑
92           st2 →taa→ st2_pre_call
93      *)
94      ∃st2_pre_call.
95      as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
96      call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
97      ∃st2_after_call,st2'.
98      ∃taa2 : trace_any_any … st2 st2_pre_call.
99      ∃taa2' : trace_any_any … st2_after_call st2'.
100      as_execute … st2_pre_call st2_after_call ∧
101      sim_status_rel st1' st2' ∧
102      label_rel … st1' st2_after_call
103    | cl_return ⇒
104      (*
105           st1
106          / ↓
107         | st1'----------S,L------------\
108         S   \                           \
109          \   \-----R-------\            |     
110           \                 |           |
111           st2 →taa→ st2_ret |           |
112                        ↓   /            |
113                   st2_after_ret →taaf→ st2'
114
115         we also ask that st2_after_ret be not labelled if the taaf tail is
116         not empty
117      *)
118      ∃st2_ret,st2_after_ret,st2'.
119      ∃taa2 : trace_any_any … st2 st2_ret.
120      ∃taa2' : trace_any_any_free … st2_after_ret st2'.
121      (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
122      as_classifier … st2_ret cl_return ∧
123      as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
124      ret_rel … sim_status_rel st1' st2_after_ret ∧
125      label_rel … st1' st2'
126    | _ ⇒
127        (*         
128        st1 → st1'
129          |      \
130          S      S,L
131          |        \
132         st2 →taaf→ st2'
133         
134         the taaf can be empty (e.g. tunneling) but we ask it must not be the
135         case when both st1 and st1' are labelled (we would be able to collapse
136         labels otherwise)
137       *)
138      ∃st2'.
139      ∃taa2 : trace_any_any_free … st2 st2'.
140      (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
141      sim_status_rel st1' st2' ∧
142      label_rel … st1' st2'
143(*    | cl_jump ⇒
144      (*
145          st1 → st1'           st1 → st1'--------\
146          |    /               |                  \
147          S  S,L       or      S                  S,L
148          |  /                 |                    \
149          st2                 st2 →collapsable tal→ st2'
150      *)
151      (¬as_costed … st1 (* st1' will necessarily be costed *) ∧
152       sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨
153      (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'.
154        tal_collapsable … tal ∧
155        sim_status_rel st1' st2' ∧ label_rel … st1' st2')*)
156    ].
157
158
159(* some useful lemmas *)
160
161let rec taa_append_taa S st1 st2 st3
162  (taa : trace_any_any S st1 st2) on taa :
163  trace_any_any S st2 st3 →
164  trace_any_any S st1 st3 ≝
165  match taa
166  with
167  [ taa_base st1' ⇒ λst3,taa2.taa2
168  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
169    taa_step ???? H I J (taa_append_taa … tl taa2)
170  ] st3.
171
172lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
173  ∀taa1 : trace_any_any S s1 s2.
174  ∀taa2 : trace_any_any S s2 s3.
175  ∀tal : trace_any_label S fl s3 s4.
176  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
177#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
178[ #s1 #taa2 #tal %
179| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
180  normalize >IH %
181]
182qed.
183
184lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
185  ∀taa1 : trace_any_any S s1 s2.
186  ∀taa2 : trace_any_any S s2 s3.
187  ∀taa3 : trace_any_any S s3 s4.
188  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
189  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
190#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
191[ #s1 #taa2 #tal %
192| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
193  normalize >IH %
194]
195qed.
196
197let rec taa_append_tal_rel S1 fl1 st1 st1'
198  (tal1 : trace_any_label S1 fl1 st1 st1')
199  S2 st2 st2mid fl2 st2'
200  (taa2 : trace_any_any S2 st2 st2mid)
201  (tal2 : trace_any_label S2 fl2 st2mid st2')
202  on tal1 :
203  tal_rel … tal1 tal2 →
204  tal_rel … tal1 (taa2 @ tal2) ≝
205match tal1 return λfl1,st1,st1',tal1.? with
206  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
207  | tal_base_return st1 st1' _ _ ⇒ ?
208  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
209  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
210  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
211  ].
212[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
213| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
214| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
215  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
216  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
217  ]
218| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
219  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
220  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
221  ]
222| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
223]
224destruct
225<associative_taa_append_tal
226  [1,2,3,4:%{(refl …)}] %{st2mid}
227  [1,2:|*: %{G2} %{EQcall} ]
228  %{(taa_append_taa … taa2 taa2')}
229  [1,2: %{H2} %{G2} [%{K2}] %
230  |*: %{st2mid'} %{H2}
231    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
232    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
233  ]
234qed.
235
236let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
237  on tal : as_costed … st2 ≝
238  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
239  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
240  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
241  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
242  | tal_base_return _ _ _ _ ⇒ λprf.⊥
243  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
244  ] (refl …).
245[ destruct
246|*: >prf %
247]
248qed.
249
250lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
251  if taa_non_empty … taa then ¬as_costed … s2 else True.
252#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
253[ #s1 %
254| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
255  [ #s2 #H #K #_ assumption
256  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
257  ]
258]
259qed.
260
261let rec tal_collapsable_to_rel S fl st1 st2
262  (tal : trace_any_label S fl st1 st2) on tal :
263  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
264  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
265  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
266  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
267  with
268  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
269  | tal_base_not_return _ st2' _ _ K ⇒ ?
270  | _ ⇒ Ⓧ
271  ].
272* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
273qed.
274
275let rec tal_collapsable_eq_flag S fl st1 st2
276  (tal : trace_any_label S fl st1 st2) on tal :
277  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
278  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
279  with
280  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
281  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
282  | _ ⇒ Ⓧ
283  ].
284
285let rec tal_collapsable_split S fl st1 st2
286  (tal : trace_any_label S fl st1 st2) on tal :
287  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
288  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
289  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
290  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
291  with
292  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
293  | tal_base_not_return st1' st2' H I J ⇒ ?
294  | _ ⇒ Ⓧ
295  ].
296[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
297| #coll
298  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
299  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
300  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
301  #EQ >EQ %
302]
303qed.
304
305lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
306tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
307  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
308#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
309elim (tal_collapsable_split … coll) lapply tal
310 >(tal_collapsable_eq_flag … coll) -tal #tal
311#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
312%[|%[|%[|%[|%[| % ]]]]]
313qed.
314
315definition taaf_append_tal : ∀S,st1,fl,st2,st3.
316  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
317  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
318  match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
319  trace_any_label S fl st1 st3 with
320  [ taaf_base s ⇒ λ_.λtal.tal
321  | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
322  | taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J)
323  ]. 
324
325lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
326  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
327  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
328#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
329[ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
330#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
331change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
332<associative_taa_append_tal /2 by taa_append_tal_rel/
333qed.
334
335(* little helpers *)
336lemma if_else_True : ∀b,P.P → if b then P else True.
337* // qed-.
338lemma if_then_True : ∀b,P.P → if b then True else P.
339* // qed-.
340
341include alias "basics/logic.ma".
342
343let rec status_simulation_produce_tlr S1 S2 R
344(* we start from this situation
345     st1 →→→→tlr→→→→ st1'
346      | \
347      L  \---S--\
348      |          \
349   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
350                        by the preceding call)
351   
352   and we produce
353     st1 →→→→tlr→→→→ st1'
354             \\      /  \
355             //     R    \-L,S-\
356             \\     |           \
357   st2_lab →tlr→ st2_mid →taaf→ st2'
358*)
359  st1 st1' st2_lab st2
360  (tlr1 : trace_label_return S1 st1 st1')
361  (taa2_pre : trace_any_any S2 st2_lab st2)
362  (sim_execute : status_simulation S1 S2 R)
363  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
364  ∃st2_mid.∃st2'.
365  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
366  ∃taa2 : trace_any_any_free … st2_mid st2'.
367  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
368  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
369  tlr_rel … tlr1 tlr2 ≝
370 match tlr1 with
371 [ tlr_base st1 st1' tll1 ⇒ ?
372 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
373 ]
374and status_simulation_produce_tll S1 S2 R
375(* we start from this situation
376     st1 →→→→tll→→→ st1'
377      | \
378      L  \---S--\
379      |          \
380   st2_lab →taa→ st2
381   
382   and if the tll is a returning one we produce a diagram like the one for tlr,
383   otherwise a simpler:
384     st1 →→→→tll→→→→ st1'
385             \\       |
386             //      L,S
387             \\       |
388   st2_lab →→→tll→→→ st2'
389*)
390  fl st1 st1' st2_lab st2
391  (tll1 : trace_label_label S1 fl st1 st1')
392  (taa2_pre : trace_any_any S2 st2_lab st2)
393  (sim_execute : status_simulation S1 S2 R)
394   on tll1 : R st1 st2 → label_rel … st1 st2_lab →
395    match fl with
396    [ ends_with_ret ⇒
397      ∃st2_mid.∃st2'.
398      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
399      ∃taa2 : trace_any_any_free … st2_mid st2'.
400      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
401      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
402      tll_rel … tll1 tll2
403    | doesnt_end_with_ret ⇒
404      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
405      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
406    ] ≝
407  match tll1 with
408  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
409  ]
410and status_simulation_produce_tal S1 S2 R
411(* we start from this situation
412     st1 →→tal→→ st1'
413      |
414      S
415      |
416     st2
417   
418   and if the tal is a returning one we produce a diagram like the one for tlr,
419   otherwise we allow for two possibilities:
420   either
421
422     st1 →→tal→→ st1'
423            \\    |
424            //   L,S
425            \\    |
426     st2 →→tal→→ st2'
427
428   or we do not advance from st2:
429
430     st1 →→tal→→ st1'  collapsable, and st1 uncosted
431                /
432         /-L,S-/
433        /
434     st2
435*)
436  fl st1 st1' st2
437  (tal1 : trace_any_label S1 fl st1 st1')
438  (sim_execute : status_simulation S1 S2 R)
439   on tal1 : R st1 st2 →
440    match fl with
441    [ ends_with_ret ⇒
442      ∃st2_mid.∃st2'.
443      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
444      ∃taa2 : trace_any_any_free … st2_mid st2'.
445      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
446      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
447      tal_rel … tal1 tal2
448    | doesnt_end_with_ret ⇒
449      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
450       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
451      (* empty *)
452      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
453    ] ≝
454  match tal1 with
455  [ tal_base_not_return st1' st1'' H G K ⇒ ?
456  | tal_base_return st1' st1'' H G ⇒ ?
457  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
458  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
459  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
460  ].
461#st1_R_st2
462[1,2,3: #st1_L_st2_lab ]
463[ (* tlr_base *)
464  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
465  #st2_mid * #st2' * #tll2 #H
466  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
467| (* tlr_step *)
468  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
469  #st2_mid * #tll2 ** #H1 #H2 #H3
470  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
471  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
472  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
473  %{H4} %{H3 H5}
474| (* tll_base *)
475  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
476  cases fl1' in tal1; normalize nodelta #tal1 *
477  [3: * #_ #ABS elim (absurd … H ABS) ]
478  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
479  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
480  [1,3: whd <st1_L_st2_lab assumption
481  |*: [%{taa2} ] %{H1} %
482    [1,3: change with (opt_safe ??? = opt_safe ???)
483      @opt_safe_elim #a #EQ1
484      @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
485    |*: @taa_append_tal_rel assumption
486    ]
487  ]
488| (* tal_base_non_return *) whd
489  cases G -G #G
490  lapply (sim_execute … H st1_R_st2)
491  (* without try it fails... why? *)
492  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
493  #st2' ** -st2 -st2'
494  [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *)
495    ** whd in ⊢ (%→?); *
496    [1,3: #ncost #R' #L' %2 /4 by conj/
497    |*: * #ABS elim (ABS K)
498    ]
499  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ]
500    *** #st1_R_st2' #st1_L_st2' %1
501    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
502    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
503    % /2 by conj/
504    % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
505  ]
506| (* tal_base_return *) whd
507  lapply (sim_execute … H st1_R_st2)
508  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
509  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
510  ***** #ncost #J2 #K2
511  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
512  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
513  % [ /4 by conj/ ]
514  %[ % | %[|%[|%[|%[| % ]]]]]]]
515| (* tal_base_call *) whd
516  lapply (sim_execute … H st1_R_st2)
517  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
518  #H elim (H G) -H
519  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
520  #st1_R_st2_mid #st1_L_st2_after_call
521  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
522  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
523  [ #st2' #tlr2 *****
524  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
525    #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
526  ]
527  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
528  %{st2'}
529  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
530    [3: % [ % assumption ]
531      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
532    ]
533  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
534    [2: %1{J2} |6: %2{J2}
535    |4,8: % try (% assumption)
536      % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
537        % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
538      ]]]]]]]]]]
539    ]
540  ]
541  [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption
542  |*: whd <st1_L_st2' assumption
543  ]
544| (* tal_step_call *)
545  lapply (sim_execute … H st1_R_st2)
546  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
547  #H elim (H G) -H
548  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
549  #st1_R_st2_mid #st1_L_st2_after_call
550  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
551  #st2_after_ret * #st2' * #tlr2 * #taa2''
552  ****
553  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
554  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
555  cases fl1' in tl1; #tl1 *
556  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
557    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
558    [4: %{taa2'''} % [ /4 by conj/ ]
559      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
560    ]]]
561  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
562    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
563    [4: % [ /2 by conj/ ]
564      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
565    ]]
566  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
567    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
568    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
569      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
570      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
571      [3: % [ /2 by conj/ ]
572      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
573    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
574      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
575      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
576      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
577      [2: %1{J2'} |6: %2{J2'}
578      |4,8: % [1,3: /2 by conj/]
579        %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
580          %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
581        ]]]]]]]]]]
582      ]]
583    ]
584  ]
585  [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption
586  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
587    [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
588    |*: normalize nodelta //
589    ]
590  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
591  |*: whd <st1_L_st2'' @(tal_end_costed … tl1)
592  ]
593| (* step_default *)
594  lapply (sim_execute … H st1_R_st2)
595  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
596  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
597  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
598  cases fl1' in tl1; #tl1 *
599  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
600    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
601      [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
602    ]]
603  | *#st2' *#tal2 *#H #G %1
604    %[| %{(taaf_append_tal … taa2 ? tal2)}
605      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
606    ]
607  | (* can't happen *)
608    *** #_ #L' elim (absurd ?? K)
609    whd >st1_L_st2_mid <L' @(tal_end_costed … tl1)
610  ]
611  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
612]
613qed.
614
615(* finite flat traces, with recursive structure right to left. The list of
616   identifiers represents the call stack *)
617
618inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
619| ft_start : flat_trace S start start [ ]
620| ft_advance_flat :
621  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
622  (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) →
623  flat_trace S start st2 stack
624| ft_advance_call :
625  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
626  ∀prf : as_classifier ? st1 cl_call.
627  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
628| ft_advance_ret :
629  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
630  as_classifier ? st1 cl_return →
631  flat_trace S start st2 stack.
632
633let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
634  (taa : trace_any_any S st2 st3)
635on taa : flat_trace S st1 st3 stack ≝
636match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
637[ taa_base s ⇒ λacc.acc
638| taa_step st1 st2 st3 H G _ tl ⇒
639  λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
640] ft.
641
642lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
643  ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
644  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
645#S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
646/2/
647qed.
648
649definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
650  λtaaf : trace_any_any_free S st2 st3.
651  match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
652  [ taaf_base s ⇒ λft.ft
653  | taaf_step s1 s2 s3 pre H G ⇒
654    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
655  | taaf_step_jump s1 s2 s3 pre H G K ⇒
656    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … G)
657  ] ft.
658
659definition option_to_list : ∀A.option A → list A ≝ λA,x.
660  match x with
661  [ Some x ⇒ [x]
662  | None ⇒ [ ]
663  ].
664
665(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
666
667inductive intensional_event : Type[0] ≝
668| IEVcost : costlabel → intensional_event
669| IEVcall : ident → intensional_event
670| IEVret : ident → intensional_event.
671
672let rec ft_observables_aux acc S st st' stack
673  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
674match ft with
675[ ft_start ⇒ acc
676| ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
677  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
678  ft_observables_aux (add @ acc) … pre1
679| ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
680  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
681  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
682  ft_observables_aux (add @ acc) … pre1
683| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
684  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
685  let add ≝ add @ [IEVret f] in
686  ft_observables_aux (add @ acc) … pre1
687].
688
689definition ft_observables ≝ ft_observables_aux [ ].
690
691lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
692  ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
693#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
694[ // ]
695#st2 #st3 #stack [3: #f ] #pre #H #G #IH #acc
696whd in ⊢ (??%(??%?));
697>IH >IH >append_nil //
698qed.
699
700lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
701  ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
702    ft_observables … ft @
703    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
704#S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
705[ #st2 #ft >append_nil % ]
706#st2 #st3 #st4 #H #K #G #taa #IH #ft
707normalize in ⊢ (??(?????%)?); >IH
708-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
709[ #st3 #H #G
710| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
711  >(not_costed_no_label … G)
712] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
713qed.
714
715lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
716  ∀ft : flat_trace S st1 st2 stack.
717  ∀taa : trace_any_any S st2 st3.
718  ∀H : as_execute S st3 st4.∀G.
719  ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
720  ft_observables … ft @
721  option_to_list … (!l←as_label … st2;return IEVcost l) @
722  [IEVcall (as_call_ident … «st3, G»)].
723#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
724whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
725>ft_extend_taa_obs
726lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
727[ #st2 * #ft #H #G >append_nil %
728| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
729  >(not_costed_no_label … K)
730  normalize nodelta //
731]
732qed.
733
734lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
735  ∀ft : flat_trace S st1 st2 (f :: stack).
736  ∀taa : trace_any_any S st2 st3.
737  ∀H : as_execute S st3 st4.∀G.
738  ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
739    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
740#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
741whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
742>ft_extend_taa_obs
743lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
744[ #st2 * #ft #H >append_nil %
745| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
746  >(not_costed_no_label … K)
747  normalize nodelta //
748]
749qed.
750
751lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
752  ∀ft : flat_trace S st1 st2 stack.
753  ∀taa : trace_any_any S st2 st3.
754  ∀H : as_execute S st3 st4.∀G.
755  ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
756    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
757#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
758whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
759>ft_extend_taa_obs
760lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
761[ #st2 * #ft #H >append_nil %
762| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
763  >(not_costed_no_label … K)
764  normalize nodelta >append_nil //
765]
766qed.
767
768lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
769  ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
770    ft_observables … ft @
771    if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
772#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
773[ #st2 #ft >append_nil % ]
774#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
775@ft_extend_taa_advance_flat_obs
776qed.
777
778(* little helper to avoid splitting equal cases *)
779lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
780
781theorem status_simulation_produce_ft :
782(* from
783
784  st1 →→→ft→→→ st1'
785   |
786  R,L
787   |
788  st2
789
790  we produce
791 
792  st1 →→→ft→→→ st1'-------\
793         //      \         \
794         \\       L         S
795         //       |          \
796  st2 →→→ft→→→ st2_lab →taa→ st2'
797 
798  so that from any tlr or tll following st1' we can produce the corresponding
799  structured trace from st2_lab using the previous result
800*)
801  ∀S1,S2.
802  ∀R.
803  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
804  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
805  ∃st2_lab,st2'.
806  ∃ft2 : flat_trace S2 st2 st2_lab stack.
807  ∃taa : trace_any_any S2 st2_lab st2'.
808  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
809#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
810[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
811|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
812  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
813  [1,2: (* other/jump *)
814    lapply (sim_execute … ex G')
815    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
816    #st2' *#taaf ** #ncost #G'' #H''
817    %{st2'} %{st2'}
818    %[1,3:
819      @(ft_extend_taaf … taaf)
820      @(ft_extend_taa … taa)
821      assumption]
822    %{(taa_base …)}
823    % [1,3: %{H'' G''} ]
824    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
825    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
826    [1,4: #st2' #H'' #taa * #ncost
827      >ft_extend_taa_obs <L'
828      [1,3: >(not_costed_no_label … ncost) >if_eq >S %
829      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
830        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
831          >not_costed_no_label
832          [1,3: >append_nil @S ]
833          whd in ⊢ (?%); >L' <H'' assumption
834        |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
835          >S %
836        ]
837      ]
838    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
839      whd in ⊢ (???(?????%));
840      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
841      >S >L' %
842    ]
843  |3: (* ret *)
844    lapply (sim_execute … ex G')
845    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
846    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
847    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
848    %[@(ft_extend_taaf … taa2')
849      @(ft_advance_ret … f … ex' cl')
850      @(ft_extend_taa … (taa_append_taa … taa taa2))
851      assumption]
852    %{(taa_base …)}
853    % [ %{H'' G''} ]
854    >ft_extend_taaf_obs
855    >ft_extend_taa_advance_ret_obs
856    whd in ⊢ (??%?);
857    >ft_observables_aux_def >append_nil
858    lapply ncost cases taa2' -st2_after_ret -st2'
859    [ #st2' * >append_nil
860    |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
861      >(not_costed_no_label … ncost)
862      >if_eq >append_nil
863    ]
864    >S >L' %
865  |4: (* call *)
866    lapply (sim_execute … ex G')
867    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
868    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
869    * #taa2 * #taa2' ** #ex' #G'' #H''
870    %{st2_after_call} %{st2'}
871    lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
872    generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
873    <EQcall in ⊢ (%→???%%→%);
874    #ft1' #EQft1'
875    %[@(ft_advance_call … ex' cl')
876      @(ft_extend_taa … (taa_append_taa … taa taa2))
877      assumption]
878    %{taa2'}
879    % [ %{H'' G''} ]
880    >ft_extend_taa_advance_call_obs
881    lapply EQft1' lapply ft1' -ft1'
882    >EQcall in ⊢ (%→???%%→%);
883    #ft1' #EQft1' destruct (EQft1')
884    whd in ⊢ (??%?);
885    >ft_observables_aux_def >append_nil
886    >S >L' %
887  ]
888]
889qed.
Note: See TracBrowser for help on using the repository browser.