source: LTS/Simulation.ma @ 3388

Last change on this file since 3388 was 3388, checked in by piccolo, 6 years ago

partial commit

File size: 17.4 KB
Line 
1include "Common.ma".
2include "Traces.ma".
3
4record relations (S : abstract_status) : Type[0] ≝
5 { Srel: S → S → Prop
6 ; Crel: S → S → Prop
7 }.
8
9definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S.
10 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
11
12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
13 { simulate_tau:
14     ∀s1,s2,s1' : S.
15      as_execute … (cost_act (None ?))  s1 s1'→
16      Srel … rel s1 s2 →
17      ∃s2'. ∃t: raw_trace S s2 s2'.
18        Srel … rel s1' s2' ∧ silent_trace … t
19 ; simulate_label:
20     ∀s1,s2,l,s1'.
21      as_execute S (cost_act (Some ? l)) s1 s1' →
22      as_classify … s1' ≠ cl_io →
23      Srel … rel s1 s2 →
24      ∃s2',s2'',s2'''.
25       ∃t1: raw_trace S s2 s2'.
26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
27       ∃t3: raw_trace S s2'' s2'''.
28        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
29 ; simulate_call_pl:
30     ∀s1,s2,s1' : S.∀f,l.
31      is_call_post_label … s1 →
32      as_execute … (call_act f l) s1 s1' →
33      as_classify … s1' ≠ cl_io →
34      Srel … rel s1 s2 →
35      ∃s2',s2'',s2'''.
36       ∃t1: raw_trace S s2 s2'.
37       as_classify … s2' ≠ cl_jump ∧
38       as_execute … (call_act f l) s2' s2'' ∧
39       bool_to_Prop(is_call_post_label … s2') ∧
40       as_classify … s2'' ≠ cl_io ∧
41       ∃t3: raw_trace S s2'' s2'''.
42        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
43 ; simulate_ret_l:
44     ∀s1,s2,s1' : S.∀l.
45      as_execute S (ret_act (Some ? l)) s1 s1' →
46      as_classify … s1' ≠ cl_io →
47      Srel  … rel s1 s2 →
48      ∃s2',s2'',s2'''.
49       ∃t1: raw_trace S s2 s2'.
50       as_classify … s2' ≠ cl_jump ∧
51       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
52       as_classify … s2'' ≠ cl_io ∧
53       ∃t3: raw_trace S s2'' s2'''.
54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
55 ; simulate_call_n:
56     ∀s1,s2,s1' : S.∀f,l.
57      as_execute … (call_act f l) s1 s1' →
58      ¬ is_call_post_label … s1 →
59      Srel … rel s1 s2 →
60      ∃s2',s2'',s2'''.
61       ∃t1: raw_trace S s2 s2'.
62       as_execute … (call_act f l) s2' s2'' ∧
63       ∃t3: raw_trace S s2'' s2'''.
64        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
65        ∧ Crel … rel s1 s2'
66 ; simulate_ret_n:
67     ∀s1,s2,s1' : S.
68      as_execute … (ret_act (None ?)) s1 s1' →
69      Srel … rel s1 s2 →
70      ∃s2',s2'',s2'''.
71       ∃t1: raw_trace S s2 s2'.
72       as_execute … (ret_act (None ?)) s2' s2''  ∧
73       ∃t3: raw_trace S s2'' s2'''.
74        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
75        ∧ Rrel … rel s2 s2''
76 }.
77
78let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
79(t : raw_trace S st1 st2) on t : list CostLabel ≝
80match t with
81[ t_base st ⇒ [ ]
82| t_ind st1' st2' st3' l prf t' ⇒
83    let tl ≝ get_costlabels_of_trace … t' in
84    match l with
85    [ call_act f c ⇒ c :: tl
86    | ret_act x ⇒ match x with
87                  [ Some c ⇒ ret_act_label_to_cost_label c :: tl
88                  | None ⇒ tl
89                  ]
90    | cost_act x ⇒ match x with
91                  [ Some c ⇒ a_non_functional_label c :: tl
92                  | None ⇒ tl
93                  ]
94    | init_act ⇒ tl
95    ]
96].
97
98
99lemma append_premeasurable_silent : ∀S : abstract_status.
100∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
101pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io →
102pre_measurable_trace … (t' @ t).
103#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
104[ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
105#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
106[ #s #EQ1 #EQ2 destruct #EQ destruct]
107#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
108destruct #_ #Hs1' whd in ⊢ (????%); %2
109[ assumption
110| %{(None ?)} %
111| @IH try assumption >Hclass % #EQ destruct
112]
113qed.
114
115definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
116raw_trace S st1 st2 → bool ≝
117λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
118
119lemma append_well_formed_silent : ∀S : abstract_status.
120∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
121well_formed_trace … t → pre_silent_trace … t' →
122(is_trace_non_empty … t' → as_classify … st1' = cl_other) →
123well_formed_trace … (t' @ t).
124#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
125[ #st #t #H #_ #_ assumption ]
126#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
127inversion H in ⊢ ?;
128[ #st #EQ1 #EQ2 #EQ3 destruct]
129#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
130#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
131[2: >(Hclass1 I) % #EQ destruct]
132@IH try assumption #_ assumption
133qed.
134
135lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
136∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
137pre_silent_trace … t1 →
138get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
139#S #st1 #st2 #st3 #t1 elim t1
140[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
141inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
142#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
143#_ whd in ⊢ (??%?); >IH [%] assumption
144qed.
145
146(*
147lemma raw_trace_ind_r : ∀S : abstract_status.
148∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
149(∀st : S.P … (t_base … st)) →
150(∀st1,st2,st3,l.
151 ∀prf : as_execute S l st2 st3.
152 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
153∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
154#S #P #base #ind #st1 #st2 #t elim t [ assumption]
155#st1 #st2 #st3 #l #prf #raw #IH
156*)
157
158
159theorem simulates_pre_mesurable:
160 ∀S : abstract_status.∀rel : relations S.
161 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
162  simulation_conditions S rel →
163  pre_measurable_trace … t1 →
164  well_formed_trace … t1 → ∀s2 : S.
165  as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
166  ∃s2'. ∃t2: raw_trace … s2 s2'.
167    pre_measurable_trace … t2 ∧
168    well_formed_trace … t2 ∧
169    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
170    Srel … rel s1' s2'.
171#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
172[ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
173  /8 by refl, pm_empty, wf_empty, conj/
174| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
175  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
176  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
177    * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'')
178    [2: cases(well_formed_trace_inv … well_formed)
179         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
180             #EQ destruct(EQ) assumption
181         | *
182            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
183                assumption
184            | * #EQ1 #EQ2 destruct
185            ]
186         ]
187    |3: @(silent_io … silent_ts2'')  assumption   
188    ]
189    #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
190    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] %
191    [ %
192      [ @append_premeasurable_silent assumption
193      | @append_well_formed_silent assumption
194      ]
195    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
196      [% | assumption]
197    ]
198  | cases(simulate_label … good … execute … REL)
199    [2: cases pre_measurable_tl
200        [ #st #H @H
201        | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
202        | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
203        | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
204        | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
205        ]
206    ]
207    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
208    * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')
209    [2: cases(well_formed_trace_inv … well_formed)
210         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
211             #EQ destruct(EQ) assumption
212         | *
213            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
214                assumption
215            | * #EQ1 #EQ2 destruct
216            ]
217         ]
218    |3: @(silent_io … sil_t_s2'''') assumption
219    ]
220    #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
221    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
222    %
223    [ %
224      [ @append_premeasurable_silent try assumption %2
225        [ @(silent_io … t_s2'') assumption
226        | %{(Some ? c)} %
227        ]
228        @append_premeasurable_silent assumption
229      | @append_well_formed_silent try assumption inversion(as_classify … s2'')
230        #Hclass
231        [ %3 [2: %{c} %]
232        |*: %2 [2,4: >Hclass % #EQ destruct]
233        ]
234        @append_well_formed_silent assumption
235      ]
236    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
237      [2: assumption] whd in ⊢ (???%);
238      >get_cost_label_invariant_for_append_silent_trace_l
239      [ % | assumption]
240    ]
241  ]
242| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
243  #pre_meas_tl #IH #H inversion H
244  [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
245  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
246  [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
247  #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
248  cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
249  [2: inversion pre_meas_tl
250      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
251      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
252      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
253      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
254      destruct assumption ]
255  #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2'''
256  #sil_t1 #sil_t2
257  cases(IH … wf_tl' … rel_s2_s2''')
258  [2: @(silent_io … (proj1 … sil_t2)) assumption]
259  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
260  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
261  % [2: whd in ⊢ (??%?);
262        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
263        whd in ⊢ (???%);
264        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
265        @eq_f assumption ]
266  %
267  [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
268    %3
269    [ @(silent_io … (proj1 … sil_t1)) assumption
270    | whd %{ret_lab} %
271    | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
272    ]
273  | @append_well_formed_silent
274    [ %2 try assumption @append_well_formed_silent try assumption
275      [ @(proj1 … sil_t2)
276      | @(proj2 … sil_t2)
277      ]
278    | @(proj1 … sil_t1)
279    | @(proj2 … sil_t1)
280    ]
281  ]
282| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
283  #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
284  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
285  [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
286   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
287   cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
288   [2: inversion pre_tl
289      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
290      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
291      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
292      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
293      destruct assumption ]
294   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
295   cases(IH … wf_tl' … REL)
296   [2: @(silent_io … (proj1 … sil_t2)) assumption ]
297   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
298   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
299   [2: whd in ⊢ (??%?);
300        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
301        whd in ⊢ (???%);
302        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
303        @eq_f assumption ]
304   %
305   [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
306     %4 try assumption
307     [ @(silent_io … (proj1 … sil_t1)) assumption
308     | whd %{f} %{lab} %
309     | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
310     ]
311   | @append_well_formed_silent
312     [ %2 try assumption @append_well_formed_silent try assumption
313        [ @(proj1 … sil_t2)
314        | @(proj2 … sil_t2)
315        ]
316     | @(proj1 …  sil_t1)
317     | @(proj2 … sil_t1)
318     ]
319   ]
320| cases daemon (*TODO*)
321]
322qed.
323
324 
325 
326   #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH
327  #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL)
328  #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil
329  xxxxxxxxx
330
331
332 #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?);   
333      @append_premeasurable_silent
334   
335    xxxxxxxxxxxxxx
336  ]
337|*: cases daemon (*TODO*)
338]
339qed.*)
340
341(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
342   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
343   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
344
345(* measurable fattorizzata sotto come measurable'
346definition measurable ≝
347 λL,s1,s2.λt: raw_trace … s1 s2.
348  ∃L',s0,so. as_execute … s0 s1 L ∧
349  pre_measurable_trace … t ∧
350  well_formed_trace … t ∧
351  as_execute … s2 so L'. *)
352
353record LR_raw_trace (S : abstract_status) : Type[0] ≝
354 { L_label: ActionLabel
355 ; R_label : ActionLabel
356 ; LR_s1: S
357 ; LR_s2: S
358 ; LR_t : raw_trace S LR_s1 LR_s2
359 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act
360 ; L_noinit_ok :
361      bool_to_Prop (¬ as_initial … LR_s1) →
362        ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label
363        ∧ ¬ bool_to_Prop (is_act_io_entering S L_label)
364 ; R_nonfin_ok :
365    bool_to_Prop (¬ as_final … (LR_s2)) →
366      ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label
367          ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label)
368 }.
369 
370definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
371pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
372
373
374(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
375  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
376  il teorema sotto sembra suggerire il merge *)
377
378definition unmovable_entry_label ≝
379λS : abstract_status.λl.
380match l with
381[ call_act _ _ ⇒ false
382| ret_act _ ⇒ false
383| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
384                            | None ⇒ false
385                            ]
386| init_act ⇒ true
387].
388 
389definition unmovable_exit_label ≝
390λS : abstract_status.λl.
391match l with
392[ call_act _ _ ⇒ false
393| ret_act _ ⇒ false
394| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
395                            | None ⇒ false
396                            ]
397| init_act ⇒ false
398].
399
400theorem simulates_LR_raw_trace :
401∀S : abstract_status.
402∀t : LR_raw_trace S.
403∀rel : relations S.
404measurable S t →
405∀s1'.Srel … rel (LR_s1 … t) s1' →
406∃ t' : LR_raw_trace S.
407measurable S t' ∧
408if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
409   LR_s1 … t' = s1'
410else
411   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
412∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
413if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
414   LR_s2 … t' = s1''
415else
416  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
417
418get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
419cases daemon (*TODO*)
420qed.
421
422xxxx
423
424theorem simulates_L_raw_trace:
425 ∀t: L_raw_trace.
426  pre_measurable_trace … (L_t t1) →
427  well_formed_trace … (L_t t1) →
428 ∀s1'.
429   S (L_s1 t) s1' →
430   s1' -flat-→ (L_s1 t2) →
431   ∃s2',t2: L_raw_trace.
432    pre_mesurable_trace … (L_t t2) ∧
433    well_formed_trace … (L_t t2) ∧
434    |t1| = |t2| ∧
435    S (L_s2 t1) s2' ∧
436    (L_s2 t2) -flat-→ s2'.
437 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
438       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
439
440
441(*********************************************************************)
442
443(* quello che segue tentava di permettere di evitare l'emissione di label
444   associate a codice morto *)
445
446replace_last x : weak_trace → weak_trace
447   [] ⇒ [], Some x
448 | l::t ⇒
449     let 〈t',x'〉 ≝ replace_last x t in
450     match x' with
451     [ None ⇒ l::t', None
452     | Some x'' ⇒ [], Some x''
453
454theorem simulates:
455 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
456  pre_measurable_trace … t1 →
457  well_formed_trace … t1.
458 ∀l1: option NonFunctionalLabel.
459 ∀s1'.
460   S s1 s1' →
461   ∃dead_labels.
462   ∃s2'. ∃t2: raw_trace … s1' s2'.
463    pre_mesurable_trace … t2 ∧
464    well_formed_trace … t2.
465   ∃l2: option NonFunctionalLabel.
466    match l1 with
467    [ None ⇒
468       match l2 with
469       [ None ⇒ |t1| = |t2|
470       | Some l2' ⇒ |t1| = l2'::|t2| ]
471    | Some l1' ⇒
472       match l2 with
473       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
474       | Some l2' ⇒
475          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
476          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
477       ]
478    ]
Note: See TracBrowser for help on using the repository browser.