source: LTS/Lang_corr.ma @ 3553

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

added paolo's trick
File size: 59.8 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 "Language.ma".
16
17lemma correctness_lemma : ∀p,p',prog.
18no_duplicates_labels … prog →
19let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
20∀s1,s2,s1' : state p.∀abs_top,abs_tail.
21∀t : raw_trace p (operational_semantics p p' prog) s1 s2.
22pre_measurable_trace … t →
23state_rel … m keep abs_top abs_tail s1 s1' →
24∃abs_top'.∃s2'.∃t' : raw_trace p (operational_semantics … p' t_prog) s1' s2'.
25state_rel p m keep abs_top' abs_tail s2 s2' ∧
26is_permutation ? ((abs_top @ (map_labels_on_trace … m (get_costlabels_of_trace … t))) @ abs_tail) 
27                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail) ∧
28 len … t = len … t' ∧
29 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act … (None ?),i〉 →
30 cont … s1 = k @ cont … s2 →
31∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
32∧ pre_measurable_trace … t' ∧
33(pre_silent_trace … t → pre_silent_trace … t').
34#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
35#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
36-abs_tail lapply s1' -s1' elim Hpre
37[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{s1'} %{(t_base …)}
38  cut(? : Prop)
39  [3: #Hpre' %
40  [ %
41   [ %
42    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
43      @is_permutation_eq
44    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
45    ]
46  | @Hpre'
47  ]
48 | #_ %1 /2 by head_of_premeasurable_is_not_io/
49 ]
50 | skip
51 ]
52   %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
53    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
54    inversion(code ??) normalize nodelta
55    [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
56     | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_
57     | #lin #io #lout #i #_ ]
58    #EQcode_s1' normalize nodelta [|*: % #EQ destruct] <H2
59    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
60    normalize in Hst; <e1 in Hst; normalize nodelta //
61| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
62  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
63    #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #class_st11 * #opt_l #EQ destruct(EQ)
64    #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
65    whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
66    inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
67    normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????);
68    inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2
69    >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
70    * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
71    cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
72    [ #x #y #_ (*#_ #_ #_ #H*) *****
73    | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
74      normalize * /2/ ] *
75    [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
76      #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
77      [
78      | #x
79      | #seq #lbl #i #_
80      | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
81      | #cond #ltrue #i1 #lfalse #i2 #_ #_
82      | #f #act_p #ret_post #i #_
83      | #l_in #io #l_out #i #_
84      ]
85      [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
86           cases(call_post_clean ?????) normalize nodelta
87           [1,3,5,7,9: #EQ destruct(EQ)]
88        [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta]
89          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
90        | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?);
91          [2: cases(call_post_clean ?????) normalize nodelta
92          [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?);
93          #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
94        | * #z1 #z2 cases(call_post_clean ?????)
95          [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta]
96          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
97        | * #z1 #z2 cases ret_post normalize nodelta
98          [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ]
99          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
100        | * #z1 #z2 cases(?∧?) normalize nodelta
101          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
102        ]
103      ]
104      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
105      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
106      [2: whd whd in match check_continuations; normalize nodelta
107         change with (check_continuations ??????) in match (foldr2 ???????); >EQHl2
108         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
109      #abs_top' * #st3' * #t' *****
110      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' #Hsil
111      %{abs_top'} %{st3'} %{(t_ind … (cost_act … (None ?)) …  t')}
112      [ @hide_prf whd @(empty ????? 〈(cost_act … (None ?)),?〉)
113        [3: assumption |4: assumption |*:] /3 by nmk/ ]
114      % [ %
115      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
116      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
117      [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
118      destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
119      #EQk1 #EQlength %{(〈cost_act … (None ?),new_code'〉::k1)}
120      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
121      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
122      normalize in class_st11; >EQcode11 in class_st11; // ]
123      #H inversion H in ⊢ ?;
124      [ #H1 #H2 #H3 #H4 #H5 #H6 destruct ] #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
125      destruct %2
126      [ % whd in ⊢ (??%% → ?); >EQcodes1' normalize nodelta <EQio11 inversion(io_info … H8)
127        normalize nodelta [2: #_ #EQ destruct] #ABS lapply class_st11 whd in match (as_classify ??);
128        >EQcode11 normalize nodelta >ABS normalize nodelta ** whd in ⊢ (??%?); >EQcode11 normalize >ABS %
129      ]
130      @Hsil //
131    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
132      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
133      inversion(code … s1')
134      [
135      | #x
136      | #seq #lbl #i #_
137      | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
138      | #cond #ltrue #i1 #lfalse #i2 #_ #_
139      | #f #act_p #ret_post #i #_
140      | #l_in #io #l_out #i #_
141      ]
142      [|*: #_ whd in ⊢ (??%% → ?);
143           [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
144           | cases(call_post_clean ?????) normalize nodelta
145             [| * #z2 #z3 cases lbl normalize nodelta
146                [| #z4 cases(?==?) normalize nodelta] ]
147             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
148           | cases(call_post_clean ?????) normalize nodelta
149             [| * #z2 #z3 cases(call_post_clean ?????)
150               [| * #z4 #z5 >m_return_bind cases(call_post_clean ?????)
151                  [| * #z6 #z7 >m_return_bind cases(?∧?) normalize nodelta ]]]
152             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
153           |  cases(call_post_clean ?????) normalize nodelta
154             [| * #z2 #z3 cases(call_post_clean ?????)
155                [| * #z4 #z5 >m_return_bind cases(?∧?) normalize nodelta ]]
156             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
157           | cases(call_post_clean ?????) normalize nodelta
158             [| * #z1 #z2 cases ret_post normalize nodelta
159                [| #z3 cases(memb ???) normalize nodelta
160                   [ cases (?==?) normalize nodelta]]]
161             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
162           | cases(call_post_clean ?????) normalize nodelta
163             [| * #z1 #z2 cases(?∧?) normalize nodelta ]
164             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
165           ]
166      ]
167      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore1 #EQio #EQ destruct(EQ)
168      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
169      [2: whd whd in match check_continuations; normalize nodelta
170         change with (check_continuations ??????) in match (foldr2 ???????);
171         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
172         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
173      #abs_top' * #st3' * #t' ***** #Hst3st3' #EQcost #EQlen #stack_safety
174      #pre_t' #Hsil
175      %{abs_top'} %{st3'}
176      %{(t_ind … (cost_act … (Some ? lbl)) … t')}
177      [ @hide_prf whd @(empty ????? 〈(cost_act … (Some ? lbl)),?〉)
178        [3: assumption |4: assumption |*:] /3 by nmk/ ]
179     cut(? : Prop)
180     [3: #Hpre' %
181      [ %
182      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
183          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
184          whd in match (map_labels_on_trace ?? [lbl]); >append_nil >EQget_el
185          @is_permutation_cons @EQcost
186        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
187          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
188          destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
189          #EQk1 #EQlength %{(〈cost_act … (Some ? lbl),new_code'〉::k1)}
190          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
191        ]]
192      @Hpre' ]
193      #h inversion h in ⊢ ?; [ #H21 #H22 #H23 #H24 #H25 #H26 destruct]
194      #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
195      |skip |
196      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
197      normalize in class_st11; >EQcode11 in class_st11; //
198    ]]
199  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
200    #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11
201    #_ #Hpre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
202    inversion(check_continuations ??????) normalize nodelta [1,3: #_ *]
203    ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
204    #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ]
205    inversion(code ??)
206    [1,2,4,5,6,7,8,9,11,12,13,14:
207      [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
208      |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
209      |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
210            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
211            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
212                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
213                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
214            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
215      |4,10:  #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
216            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
217            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
218                [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
219            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
220      |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
221             normalize nodelta
222             [2,4: * #z1 #z2 cases lbl normalize nodelta
223               [2,4: #l1 cases(memb ???) normalize nodelta
224                 [1,3: cases(?==?) normalize nodelta ]]]
225            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
226      |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
227             normalize nodelta
228             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
229             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
230      ]
231    ]
232    #seq1 #opt_l #i' #_ #EQcode_s1'
233    change with (m_bind ?????) in ⊢ (??%? → ?);
234    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
235    * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta
236    [2,4: #lab1 ] #EQ destruct(EQ)
237    [1,2: inversion(?==?) normalize nodelta #EQget_el ]
238    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
239    #EQstore #EQinfo #EQ destruct(EQ)
240    cases(IH … (mk_state ? i' (cont … s1') (store … st12) (io_info … s1')) abs_tail_cont ?)
241    [3,6: whd
242       [ <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
243       | <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
244       ]
245       normalize nodelta % // % // % // % // assumption
246    |2,5:
247    ]
248    #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
249    #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
250    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
251    |2,5:
252    ]
253    cut(? : Prop)
254    [3,6: #Hpre'
255       %
256   
257    [1,3: % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f @EQlen ] %{Hst3_s2'} [2: @EQcosts]
258        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
259        whd in match (map_labels_on_trace ???); >(\P EQget_el) @is_permutation_cons
260        @EQcosts
261      |*: #k #i #EQcont_st3 >EQcont #EQ
262          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
263      ]]
264      @Hpre'
265      |*: #h inversion h in ⊢ ?;
266          [1,3: #H41 #H42 #H43 #H44 #H45 #H46 destruct
267          |*: #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
268              %2 [ /2 by head_of_premeasurable_is_not_io/ ] @Hsil //
269          ]
270          ] |1,4:]
271    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
272  |
273   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
274    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
275    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
276    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
277    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
278    [1,2,3,5,6,7:
279     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
280     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
281     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
282       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
283       [2: #l1 cases(?==?) normalize nodelta]]
284       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
285     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
286       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
287       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
288       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
289       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
290     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
291             normalize nodelta
292             [2,4: * #z1 #z2 cases lbl normalize nodelta
293               [2,4: #l1 cases(memb ???) normalize nodelta
294                 [1,3: cases(?==?) normalize nodelta ]]]
295            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
296     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
297             normalize nodelta
298             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
299             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
300      ]
301    ]
302    #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
303    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
304    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
305    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
306    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
307    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
308    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
309    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
310    #EQ destruct(EQ)
311    cases(IH …
312     (mk_state ? i_true1 (〈cost_act … (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
313     abs_tail_cont gen_lab_i_true')
314    [2: whd whd in match (check_continuations ??????);
315        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
316        change with (check_continuations ??????) in match (foldr2 ???????);
317        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
318        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
319    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen
320      #stack_safety #pre_t' #Hsil %{abs_top1}
321    %{s2'} %{(t_ind … t')}
322    [ @hide_prf @(cond_true … EQcode_s1') //
323    |
324    ] % [
325    % [ %
326    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
327      whd in match (get_costlabels_of_trace ?????); whd in match(map_labels_on_trace ???);
328      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ?????) in ⊢ (???%); @is_permutation_cons
329      assumption
330    |  #k #i1 #EQcont_st3 #EQcont_st11
331       cases(stack_safety … (〈cost_act … (None (NonFunctionalLabel …)),i〉::k) … EQcont_st3 …)
332       [2: >EQcont_st12 >EQcont_st11 % ]
333       * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
334       %{tl1} % // whd in EQk1 : (??%%); destruct //
335    ]]
336    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
337    ]
338    #h inversion h in ⊢ ?;
339    [#H1 #H2 #H3 #H4 #H5 #H6 destruct
340    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct
341    ]
342  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
343    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
344    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
345    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
346    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
347    [1,2,3,5,6,7:
348     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
349     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
350     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
351       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
352       [2: #l1 cases(?==?) normalize nodelta]]
353       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
354     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
355       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
356       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
357       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
358       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
359     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
360             normalize nodelta
361             [2,4: * #z1 #z2 cases lbl normalize nodelta
362               [2,4: #l1 cases(memb ???) normalize nodelta
363                 [1,3: cases(?==?) normalize nodelta ]]]
364            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
365     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
366             normalize nodelta
367             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
368             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
369      ]
370    ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
371    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
372    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
373    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
374    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
375    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
376    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
377    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
378    #EQ destruct(EQ)
379    cases(IH …
380     (mk_state ? ifalse1 (〈cost_act … (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
381     abs_tail_cont gen_lab_ifalse1)
382    [2: whd whd in match (check_continuations ??????);
383        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
384        change with (check_continuations ??????) in match (foldr2 ???????);
385        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
386        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
387    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety
388    #pre_t' #Hsil
389    %{abs_top1} %{s2'} %{(t_ind … t')}
390    [ @hide_prf @(cond_false … EQcode_s1') //
391    |
392    ] % [
393    % [ %
394    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
395      whd in match (get_costlabels_of_trace ?????); whd in match(map_labels_on_trace ???);
396      >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ?????) in ⊢ (???%); @is_permutation_cons
397      assumption
398    | #k #i1 #EQcont_st3 #EQcont_st11
399      cases(stack_safety … (〈cost_act … (None (NonFunctionalLabel …)),i〉::k) … EQcont_st3 …)
400      [2: >EQcont_st12 >EQcont_st11 % ]
401      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
402      %{tl1} % // whd in EQk1 : (??%%); destruct //
403    ] ]
404    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
405    #h inversion h in ⊢ ?;
406    [ #H21 #H22 #H23 #H24 #H25 #H26 destruct
407    | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
408    ]
409 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
410   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
411   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
412   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
413   [1,2,3,4,6,7:
414     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
415     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
416     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
417       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
418       [2: #l1 cases(?==?) normalize nodelta]]
419       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
420     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
421            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
422            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
423                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
424                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
425            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
426     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
427             normalize nodelta
428             [2,4: * #z1 #z2 cases lbl normalize nodelta
429               [2,4: #l1 cases(memb ???) normalize nodelta
430                 [1,3: cases(?==?) normalize nodelta ]]]
431            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
432     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
433             normalize nodelta
434             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
435             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
436      ]
437   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
438   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
439   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
440   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
441   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
442   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
443   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
444   cases(IH …
445    (mk_state ? i_true1
446     (〈cost_act … (None ?),LOOP … cond ltrue i_true1 lfalse i_false1〉 ::
447        cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_itrue1)
448   [2: whd >EQcont_st12 whd in match (check_continuations ??????);
449       whd in match (foldr2 ???????);
450       change with (check_continuations ??????) in match (foldr2 ???????);
451       >EQcheck normalize nodelta whd in match (call_post_clean ??????);
452       >EQi_false2 normalize nodelta >EQi_true2 >m_return_bind >EQget_ltrue1
453       >EQget_lfalse1 normalize nodelta % // % // % // % [2: assumption] % //
454       % //
455   ]
456   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
457   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
458   [ @hide_prf @(loop_true … EQcode_s1') // |] % [
459   % [ %
460   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
461     whd in match (get_costlabels_of_trace ?????); whd in match(map_labels_on_trace ???);
462      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ?????) in ⊢ (???%);
463     @is_permutation_cons assumption
464   | #k #i1 #EQcont_st3 #EQcont_st11
465      cases(stack_safety … (〈cost_act … (None (NonFunctionalLabel …)), LOOP p … cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …)
466      [2: >EQcont_st12 >EQcont_st11 % ]
467      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
468      %{tl1} % // whd in EQk1 : (??%%); destruct //
469   ] ]
470   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
471   #h inversion h in ⊢ ?;
472   [ #H41 #H42 #H43 #H44 #H45 #H46 destruct
473   | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
474   ]
475 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
476   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
477   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
478   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
479   [1,2,3,4,6,7:
480     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
481     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
482     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
483       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
484       [2: #l1 cases(?==?) normalize nodelta]]
485       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
486     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
487            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
488            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
489                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
490                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
491            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
492     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
493             normalize nodelta
494             [2,4: * #z1 #z2 cases lbl normalize nodelta
495               [2,4: #l1 cases(memb ???) normalize nodelta
496                 [1,3: cases(?==?) normalize nodelta ]]]
497            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
498     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
499             normalize nodelta
500             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
501             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
502      ]
503   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
504   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
505   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
506   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
507   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
508   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
509   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
510   cases(IH …
511    (mk_state ? i_false1
512     (cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_ifalse1)
513   [2: whd >EQcont_st12 whd in match (check_continuations ??????);
514       whd in match (foldr2 ???????);
515       change with (check_continuations ??????) in match (foldr2 ???????);
516       >EQcheck normalize nodelta whd in match (call_post_clean ??????);
517       >EQi_false2 normalize nodelta >EQi_true2
518        % // % // % // % [2: %] //
519   ]
520   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
521   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
522   [ @hide_prf @(loop_false … EQcode_s1') // |] % [
523   % [ %
524   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
525     whd in match (get_costlabels_of_trace ?????); whd in match(map_labels_on_trace ???);
526     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ?????) in ⊢ (???%);
527     @is_permutation_cons assumption
528   | #k #i #EQcont_st3 <EQcont_st12 #EQ
529     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
530   ]]
531   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct]
532   #h inversion h in ⊢ ?;
533   [ #H61 #H62 #H63 #H64 #H65 #H66 destruct
534   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct
535   ]
536 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
537   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
538   #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????)
539   [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
540   #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
541   [1,2,3,4,5,6:
542     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
543     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
544     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
545       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
546       [2: #l1 cases(?==?) normalize nodelta]]
547       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
548     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
549            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
550            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
551                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
552                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
553            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
554     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
555       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
556       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
557       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
558       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
559     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
560             normalize nodelta
561             [2,4: * #z1 #z2 cases lbl normalize nodelta
562               [2,4: #l1 cases(memb ???) normalize nodelta
563                 [1,3: cases(?==?) normalize nodelta ]]]
564            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
565      ]
566   ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
567   whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
568   [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta
569   [2: #_ #EQ destruct] #EQget_lout1 inversion(?==?) #EQget_lin1 normalize nodelta
570   whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
571   #EQstore11 #EQinfo11 #EQ destruct
572   cases(IH …
573    (mk_state ? (EMPTY p …) (〈cost_act … (Some ? lout),i1〉::cont … s1') (store … st12) true)
574    abs_tail_cont [ ])
575   [2: whd >EQcont_st12 whd in match (check_continuations ??????);
576       whd in match (foldr2 ???????);
577       change with (check_continuations ??????) in match (foldr2 ???????);
578       >EQcheck normalize nodelta >EQ_i2 normalize nodelta % // % // % // %
579       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
580   ]
581   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
582   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
583   [ @hide_prf @(io_in … EQcode_s1') // |] % [
584   % [ %
585   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
586     whd in match (get_costlabels_of_trace ?????); whd in match(map_labels_on_trace ???);
587     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ?????) in ⊢ (???%);
588     @is_permutation_cons assumption
589   | #k #i1 #EQcont_st3 #EQcont_st11
590      cases(stack_safety … (〈cost_act … (Some ? lout),i〉::k) … EQcont_st3 …)
591      [2: >EQcont_st12 >EQcont_st11 %]
592      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
593      %{tl1} % // whd in EQk1 : (??%%); destruct //
594   ]]
595   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
596   #h inversion h in ⊢ ?;
597   [ #H81 #H82 #H83 #H84 #H85 #H86 destruct
598   | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct
599   ]
600  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
601    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
602  | #r_t #mem #con #rb #i #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12
603    destruct #t #_ * #nf #EQ destruct
604  ]
605| #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?;
606  [1,2,3,4,5,6,7,8:
607    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
608    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
609    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
610    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
611    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
612    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
613    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
614    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
615    ]
616    destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS %
617  ]
618  #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ)
619  #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6)
620  #t * #lbl #EQ destruct(EQ) #pre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
621  inversion(check_continuations …) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont
622  >EQcont_st11 in ⊢ (% → ?); inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
623  * #act_lab #i #cont_s1'' #_ #EQcont_s1' whd in ⊢ (??%% → ?);
624  change with (check_continuations ??????) in match (foldr2 ???????);
625  inversion(check_continuations ??????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
626  ** #H2 #abs_top_cont' #abs_tail_cont' #EQcheck normalize nodelta
627  inversion(call_post_clean ??????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****]
628  * #gen_labs #i' #EQi' inversion act_lab normalize nodelta
629  [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ)
630  [1,6: whd in ⊢ (??%% → ?); #EQ destruct *****
631  |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct
632  ]
633  whd in match ret_costed_abs; normalize nodelta
634  [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** #EQ destruct(EQ) ]
635  inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
636  ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?);
637  inversion(code … s1')
638  [1,3,4,5,6,7:
639     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
640     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
641       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
642       [2: #l1 cases(?==?) normalize nodelta]]
643       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
644     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
645            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
646            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
647                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
648                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
649            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
650     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
651       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
652       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
653       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
654       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
655     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
656             normalize nodelta
657             [2,4: * #z1 #z2 cases lbl normalize nodelta
658               [2,4: #l1 cases(memb ???) normalize nodelta
659                 [1,3: cases(?==?) normalize nodelta ]]]
660            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
661     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
662             normalize nodelta
663             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
664             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
665      ]
666  ]
667   #r_t' #EQcode_s1'
668  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
669  #EQstore11 #EQio_111 #EQ destruct
670  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
671  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
672  #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
673  #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
674  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
675  | ] % [
676  % [ %
677  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
678    whd in match (get_costlabels_of_trace ?????);
679    whd in match (get_costlabels_of_trace ?????) in ⊢ (???%);
680    whd in match (map_labels_on_trace ???); >EQget_el @is_permutation_cons
681    assumption
682  | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%);
683    [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
684    destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
685    #EQk1 #EQlength %{(〈ret_act … (Some ? lbl1),i〉::k1)}
686    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
687  ]]
688  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
689  #h inversion h in ⊢ ?;
690  [ #H101 #H102 #H103 #H104 #H105 #H106 destruct
691  | #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct
692  ]
693| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
694  [1,2,3,4,5,6,7,9:
695    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
696    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
697    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
698    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
699    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
700    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
701    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
702    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
703    ]
704    destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); *
705  | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
706    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
707    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?);
708    normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *]
709    #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail
710    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
711    #abs_top_cont #abs_tail_cont #EQcheck
712    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
713    [1,2,3,4,5,7:
714     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
715     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
716     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
717       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
718       [2: #l1 cases(?==?) normalize nodelta]]
719       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
720     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
721            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
722            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
723                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
724                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
725            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
726     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
727       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
728       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
729       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
730       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
731     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
732             normalize nodelta
733             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
734             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
735     ]
736    ] #f' #act_p' #opt_l' #i' #_
737    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
738    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
739    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh'
740    #EQenv_it' ***** #EQtrans
741    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
742    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
743    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
744    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
745    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
746        [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
747           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
748          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
749          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
750          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
751          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
752          #EQ destruct(EQ)
753          cases(IH (mk_state ? (f_body … env_it') (〈ret_act … opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
754          [2: whd >EQcont12
755            change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????);
756            >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
757            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
758            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
759            @(inverse_call_post_trans … is_fresh_fresh')
760            [2: % |*: [2,3: /2 by / ]
761                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
762                whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
763                #no_dup lapply(no_duplicates_append_r … no_dup) #H1
764                lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
765                change with ([?]@?) in match (?::?); #H1
766                lapply(no_duplicates_append_r … H1) >append_nil //
767            ]
768          ]
769          #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety
770          #pre_t' #Hsil %{abs_top'''}
771          %{st3'} %{(t_ind … (call_act … f (f_lab … env_it')) …  t')}
772          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [
773          % [ %
774          [ % [2: whd in ⊢ (??%%); >EQlen %]
775            %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ?????) in ⊢ (???%);
776            >EQlab_env_it >associative_append whd in match (append ???); >associative_append
777            >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
778            whd in match (map_labels_on_trace ???); >EQgen_labels @is_permutation_cons
779            >append_nil whd in match (append ???) in ⊢ (???%); //
780          | #k #i1 #EQcont_st3 #EQcont_st11
781            cases(stack_safety … (〈ret_act … (Some ? lbl),i〉::k) … EQcont_st3 …)
782            [2: >EQcont12 >EQcont_st11 % ]
783            * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
784            %{tl1} % // whd in EQk1 : (??%%); destruct //
785          ]]
786          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
787          ]
788          #h inversion h in ⊢ ?;
789          [ #H121 #H122 #H123 #H124 #H125 #H126 destruct
790          | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct
791          ]
792        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
793        ]
794    | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
795    ]
796  ]
797| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
798  [1,2,3,4,5,6,7,9:
799    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
800    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
801    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
802    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
803    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
804    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
805    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
806    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
807    ]
808    destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H %
809  ]
810  #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
811  #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
812  destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?;
813  [1,2,3,4,5,6,7,8:
814    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
815    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
816    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
817    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
818    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
819    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
820    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
821    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
822    ]
823    destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ)
824    @⊥ >EQ in x12; * #H @H %
825  ]
826   #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
827   #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio
828   #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
829   inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l)
830   #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); * #EQcont11_42 >EQcode11 in ⊢ (% → ?);
831   normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?);
832   #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail
833    whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ *] ** #H1
834    #abs_top_cont #abs_tail_cont #EQcheck
835    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
836    [1,2,3,4,5,7:
837     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
838     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
839     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
840       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
841       [2: #l1 cases(?==?) normalize nodelta]]
842       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
843     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
844            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
845            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
846                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
847                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
848            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
849     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
850       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
851       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
852       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
853       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
854     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
855             normalize nodelta
856             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
857             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
858     ]
859    ] #f' #act_p' #opt_l' #i' #_
860    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
861    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
862    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans
863    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
864    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
865    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
866    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
867    [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l')
868    inversion(memb ???) normalize nodelta #Hlbl_keep'
869    [ cases(?==?) normalize nodelta ]
870     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
871     cases(IH1
872            (mk_state ?
873              (f_body … env_it')
874              (〈ret_act … (Some ? lbl'),i'〉 :: (cont … st1'))
875              (store ? st12) false)
876            (abs_top''@abs_tail_cont)
877            (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
878     [2: whd >EQcont12
879         change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????);
880          >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
881          whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta
882          % // % // % // % [/5 by conj/] >EQcode12 <EQtrans
883          @(inverse_call_post_trans … fresh')
884          [2: % |*: [2,3: /2 by / ]
885              cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
886              whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
887              #no_dup lapply(no_duplicates_append_r … no_dup) #H1
888              lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
889              change with ([?]@?) in match (?::?); #H1
890              lapply(no_duplicates_append_r … H1) >append_nil //
891          ]
892     ]
893     #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1
894     #pre_t1' #Hsil1
895     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
896     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
897     whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta
898     [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41'
899     change with (check_continuations ??????) in match (foldr2 ???????);
900     inversion(check_continuations ??????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
901     ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind
902     normalize nodelta inversion(call_post_clean ??????) normalize nodelta
903     [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i'''
904     #EQ_clean_i'' inversion(act_lbl) normalize nodelta
905     [1,3,4:
906       [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct *****
907       | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?);
908         #EQ destruct ****** [2: *] #EQ destruct
909       ]
910     ]
911     cut(act_lbl = ret_act … (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i')
912     [ cases(stack_safety1 [ ] …)
913       [3: >EQcont41 in ⊢ (??%?); % |4: normalize // |5: % |2:] * [|#x #xs] *
914       whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct > EQcont_st41' in EQ1;
915       #EQ destruct(EQ) /3 by conj/
916     ]
917     ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta
918     >Hlbl_keep' normalize nodelta
919     whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ)
920     >EQcode41 in ⊢ (% → ?); inversion(code … st41')
921     [1,3,4,5,6,7:
922       [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
923       | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
924         normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
925         [2: #l1 cases(?==?) normalize nodelta]]
926         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
927       | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
928            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
929            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
930                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
931                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
932            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
933       | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
934         whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
935         [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
936         [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
937         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
938       | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
939             normalize nodelta
940             [2,4: * #z1 #z2 cases lbl normalize nodelta
941               [2,4: #l1 cases(memb ???) normalize nodelta
942                 [1,3: cases(?==?) normalize nodelta ]]]
943            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
944       | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
945             normalize nodelta
946             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
947             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
948       ]   
949     ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
950     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
951     #EQ1 >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
952     #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ)
953     cases(IH2
954             (mk_state ? i' (cont … st1') (store … st42) (io_info … st42))
955             abs_tail_cont abs_top'''')
956     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
957     #abs_top_1 * #st5' * #t2' ***** #Hst5_st5' #EQcosts'
958     #EQlen'  #stack_safety2 #pre_t2' #Hsil2 %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
959     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
960     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
961     |2,4: skip
962     ] % [
963     % [ %
964     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
965           whd in ⊢ (??%%); @eq_f // ]
966       %{Hst5_st5'} whd in match (map_labels_on_trace ???);
967       change with (map_labels_on_trace ???) in match (foldr ?????);
968       >map_labels_on_trace_append >get_cost_label_append
969       whd in match (get_costlabels_of_trace ???? (t_ind …));
970       whd in match (get_costlabels_of_trace ???? (t_ind …));
971       >get_cost_label_append
972       whd in match (get_costlabels_of_trace ???? (t_ind …));
973       >map_labels_on_trace_append >EQlab_env_it >EQgen_labels
974       whd in match (map_labels_on_trace ?? [ ]);
975       whd in match (append ? (nil ?) ?);
976       cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
977       >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
978     | #k #i #EQcont_st3 #EQ
979       cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
980     ]]
981     %4
982     [ normalize >EQcode_st1' normalize nodelta % #EQ destruct
983     | %{f} % //
984     | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I
985     | @append_premeasurable // %3 //
986       [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct
987       | whd %{lbl'} %
988       ]
989     ] whd in EQ : (??%?); >EQcode_st41' in EQ; normalize nodelta
990     #EQ destruct
991  ]
992   #h inversion h in ⊢ ?;
993  [ #H141 #H142 #H143 #H144 #H145 #H146 destruct
994  |#H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 destruct
995  ]
996]
997qed.
998
999
1000lemma silent_in_silent : ∀p,p',prog.
1001no_duplicates_labels … prog →
1002let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
1003∀s1,s2,s1' : state p.∀abs_top,abs_tail.
1004∀t : raw_trace p (operational_semantics … p' prog) s1 s2.
1005silent_trace … t →
1006state_rel … m keep abs_top abs_tail s1 s1' →
1007∃abs_top'.∃s2'.∃t' : raw_trace p (operational_semantics … p' t_prog) s1' s2'.
1008state_rel  … m keep abs_top' abs_tail s2 s2' ∧
1009silent_trace … t'.
1010#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
1011#s1 #s2 #s1' #abs_top #abs_tail #t *
1012[2: cases t -s1 -s2 [2: #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 cases H87 #H cases(H I)]
1013#st #_ #H %{abs_top} %{s1'} %{(t_base …)} % // %2 % * ]
1014#H #H1 lapply(correctness_lemma p p' prog no_dup) >EQt_prog normalize nodelta #H2
1015cases(H2 … (pre_silent_is_premeasurable … H) … H1)  -H2 #abs_top' * #s2' * #t' ***** #REL'
1016#_ #_ #_ #_ #H2 %{abs_top'} %{s2'} %{t'} %{REL'} % @H2 //
1017qed.
Note: See TracBrowser for help on using the repository browser.