source: LTS/Traces.ma @ 3499

Last change on this file since 3499 was 3487, checked in by sacerdot, 5 years ago

No more i_act.

Note: we do not ask anywhere that no transitions to an initial
state are allowed, nor that no transitions from the final state
are allowed. Are those conditions really vacuous? Do they make
the final statement on measurable traces more accurate?

File size: 18.1 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 "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20inductive FunctionName : Type[0] ≝
21 | a_function_id : ℕ → FunctionName.
22 
23inductive CallCostLabel : Type[0] ≝
24 | a_call_label : ℕ → CallCostLabel.
25 
26inductive ReturnPostCostLabel : Type[0] ≝
27 | a_return_cost_label : ℕ → ReturnPostCostLabel.
28 
29inductive NonFunctionalLabel : Type[0] ≝
30 | a_non_functional_label : ℕ → NonFunctionalLabel.
31 
32inductive CostLabel : Type[0] ≝
33 | a_call : CallCostLabel → CostLabel
34 | a_return_post : ReturnPostCostLabel → CostLabel
35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37coercion a_call.
38coercion a_return_post.
39coercion a_non_functional_label.
40
41(*
42definition ret_act_label_to_cost_label :
43(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
44λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b].
45
46coercion ret_act_label_to_cost_label.
47
48definition call_act_label_to_cost_label :
49(CallCostLabel + NonFunctionalLabel) → CostLabel ≝
50λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
51
52coercion call_act_label_to_cost_label.
53*)
54
55definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
56λx,y.match x with [ a_non_functional_label n ⇒
57                    match y with [a_non_functional_label m ⇒ eqb n m ] ].
58
59lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
60(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
61#P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
62
63definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
64#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
65assumption
66qed.
67
68unification hint  0 ≔ ;
69    X ≟ DEQNonFunctionalLabel
70(* ---------------------------------------- *) ⊢
71    NonFunctionalLabel ≡ carr X.
72
73unification hint  0 ≔ p1,p2;
74    X ≟ DEQNonFunctionalLabel
75(* ---------------------------------------- *) ⊢
76    eq_nf_label p1 p2 ≡ eqb X p1 p2.
77
78definition eq_function_name : FunctionName → FunctionName → bool ≝
79λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].
80
81lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
82(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
83#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.
84
85definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
86#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
87assumption
88qed.
89
90unification hint  0 ≔ ;
91    X ≟ DEQFunctionName
92(* ---------------------------------------- *) ⊢
93    FunctionName ≡ carr X.
94
95unification hint  0 ≔ p1,p2;
96    X ≟ DEQFunctionName
97(* ---------------------------------------- *) ⊢
98    eq_function_name p1 p2 ≡ eqb X p1 p2.
99
100definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
101λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
102
103lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
104(c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
105#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
106
107definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
108#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
109assumption
110qed.
111
112unification hint  0 ≔ ;
113    X ≟ DEQReturnPostCostLabel
114(* ---------------------------------------- *) ⊢
115    ReturnPostCostLabel ≡ carr X.
116
117unification hint  0 ≔ p1,p2;
118    X ≟ DEQReturnPostCostLabel
119(* ---------------------------------------- *) ⊢
120    eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
121
122definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
123λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
124
125lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
126(c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
127#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
128
129definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
130#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
131assumption
132qed.
133
134unification hint  0 ≔ ;
135    X ≟ DEQCallCostLabel
136(* ---------------------------------------- *) ⊢
137    CallCostLabel ≡ carr X.
138
139unification hint  0 ≔ p1,p2;
140    X ≟ DEQCallCostLabel
141(* ---------------------------------------- *) ⊢
142    eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
143
144definition eq_costlabel : CostLabel → CostLabel → bool ≝
145λc1.match c1 with
146  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
147  | a_return_post x1 ⇒
148      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
149  | a_non_functional_label x1 ⇒
150     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
151  ].
152
153lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
154(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
155#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
156try (@H2 % #EQ destruct)
157[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
158  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
159| change with (eq_return_cost_lab ??) in ⊢ (?%);
160   @eq_return_cost_lab_elim
161   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
162| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
163  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
164]
165qed.
166
167
168definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
169#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
170assumption
171qed.
172
173unification hint  0 ≔ ;
174    X ≟ DEQCostLabel
175(* ---------------------------------------- *) ⊢
176    CostLabel ≡ carr X.
177
178unification hint  0 ≔ p1,p2;
179    X ≟ DEQCostLabel
180(* ---------------------------------------- *) ⊢
181    eq_costlabel p1 p2 ≡ eqb X p1 p2.
182
183   
184
185
186inductive ActionLabel : Type[0] ≝
187 | call_act : FunctionName → CallCostLabel → ActionLabel
188 | ret_act : option(ReturnPostCostLabel) → ActionLabel
189 | cost_act : option NonFunctionalLabel → ActionLabel.
190 
191definition is_cost_label : ActionLabel → Prop ≝
192λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
193
194inductive status_class : Type[0] ≝
195 | cl_jump : status_class
196 | cl_io : status_class
197 | cl_other : status_class.
198
199definition is_non_silent_cost_act : ActionLabel → Prop ≝
200λact. ∃l. act = cost_act (Some ? l).
201
202record abstract_status : Type[2] ≝
203 { as_status :> Type[0]
204 ; as_execute : ActionLabel → relation as_status
205 ; as_syntactical_succ : relation as_status
206 ; as_classify : as_status → status_class
207 ; is_call_post_label : as_status → bool
208 ; as_initial : as_status → bool
209 ; as_final : as_status → bool
210 ; jump_emits : ∀s1,s2,l.
211      as_classify … s1 = cl_jump →
212      as_execute l s1 s2 → is_non_silent_cost_act l
213 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
214      as_execute l s1 s2 → is_non_silent_cost_act l
215 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
216     as_execute l s1 s2 → is_non_silent_cost_act l
217 }.
218 (*
219definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
220λS,l.match l with
221[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
222| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
223                                                   | inr c' ⇒ is_io_entering S c']
224                           | None ⇒ false
225                           ]
226| cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
227| init_act ⇒ false
228].
229
230definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
231λS,l.match l with
232[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
233| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
234                                                   | inr c' ⇒ is_io_exiting S c']
235                           | None ⇒ false
236                           ]
237| cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
238| init_act ⇒ false
239].
240*)
241
242inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
243  | t_base : ∀st : S.raw_trace S st st
244  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
245             as_execute S l st1 st2 → raw_trace S st2 st3 →
246             raw_trace S st1 st3.
247
248definition is_cost_act : ActionLabel → Prop ≝
249λact.∃l.act = cost_act l.
250
251definition is_call_act : ActionLabel → Prop ≝
252λact.∃f,l.act = call_act f l.
253
254definition is_labelled_ret_act : ActionLabel → Prop ≝
255λact.∃l.act = ret_act (Some ? l).
256
257definition is_unlabelled_ret_act : ActionLabel → Prop ≝
258λact.act = ret_act (None ?).
259
260definition is_costlabelled_act : ActionLabel → Prop ≝
261λact.match act with [ call_act _ _ ⇒ True
262                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
263                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
264                    ].
265(*
266lemma well_formed_trace_inv :
267∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
268well_formed_trace … t →
269(st1 = st2 ∧ t ≃ t_base S st1) ∨
270(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
271well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
272t ≃ t_ind … prf … tl) ∨
273(∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
274 well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
275(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
276 well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
277 is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
278#S #st1 #st2 #t #H inversion H
279[ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
280| #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
281  %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
282| #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
283  %{l} %{prf} %{tl} % // % //
284(*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
285  destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
286]
287qed.
288
289*)
290
291let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
292(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
293match t1
294return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
295with
296[ t_base st ⇒ λt2.t2
297| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
298].
299
300interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
301
302lemma append_associative : ∀S,st1,st2,st3,st4.
303∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
304∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
305#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
306[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
307qed.
308
309definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
310raw_trace … st1 st3 → Prop≝
311λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
312
313definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
314raw_trace … st1 st3 → Prop≝
315λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
316
317inductive pre_silent_trace (S : abstract_status) :
318∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
319| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
320| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
321                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
322                pre_silent_trace … (t_ind … prf … tl).
323               
324definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
325raw_trace S st1 st2 → bool ≝
326λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
327
328definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
329raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
330¬ (bool_to_Prop (is_trace_non_empty … t)).
331
332lemma pre_silent_io : ∀S : abstract_status.
333∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
334as_classify … s2 ≠ cl_io.
335#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
336#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
337#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
338#EQ destruct #_ @IH assumption
339qed.
340
341(*
342definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
343raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
344well_formed_trace … t.
345
346lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
347∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
348#S #st1 #st2 #t * //
349qed. *)
350(* elim t -t
351[ #st #_ %]
352#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
353[2: >cl % #EQ destruct]
354@IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
355#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
356% [ assumption | #_ assumption]
357qed.*)
358
359inductive pre_measurable_trace (S : abstract_status) :
360∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
361 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
362 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
363                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
364                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
365                      pre_measurable_trace … (t_ind … prf … tl)
366 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
367                      as_classify … st1 ≠ cl_io →
368                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
369                      is_labelled_ret_act l → pre_measurable_trace … tl →
370                      pre_measurable_trace … (t_ind … prf … tl)
371 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
372                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
373                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
374                      pre_measurable_trace … tl →
375                      pre_measurable_trace … (t_ind … prf … tl)
376 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
377                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
378                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
379                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
380                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
381                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
382                      as_syntactical_succ S st1 st4 →
383                      is_unlabelled_ret_act l2 →
384                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
385                     
386lemma pre_measurable_trace_inv : ∀S : abstract_status.
387∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
388(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
389(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
390 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
391 pre_measurable_trace … tl) ∨
392(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
393 t = t_ind … prf … tl ∧
394 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
395(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
396 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
397 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
398(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
399 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
400 ∃prf' : as_execute S l2 st1'' st1'''.
401 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
402 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
403 bool_to_Prop (¬ is_call_post_label … st1) ∧
404 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
405 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
406#S #st1 #st2 #t #H inversion H
407[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
408| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
409  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
410| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
411  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
412| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
413  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
414| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
415  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
416  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
417  %{prf'} /12 by conj/
418]
419qed.
420                     
Note: See TracBrowser for help on using the repository browser.