source: LTS/Lang_meas.ma @ 3542

Last change on this file since 3542 was 3542, checked in by piccolo, 5 years ago
File size: 20.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 "Language.ma".
16
17
18lemma top_move_source_is_empty : ∀p,p',prog.
19let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
20∀l.
21∀s1,s2,s1' : state p.∀abs_top,abs_tail.
22execute_l … p' (env … prog) l s1 s2 →
23is_costlabelled_act l →
24(is_call_act l → is_call_post_label (operational_semantics p p' prog) … s1) →
25state_rel … m keep abs_top abs_tail s1 s1' → abs_top = nil ? ∧
26(is_call_act l → is_call_post_label (operational_semantics p p' t_prog) … s1').
27#p #p' #prog @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
28#l #s1 #s2 #s1' #abs_top #abs_tail #H elim H -s1 -s2 -l
29[ #s1 #s2 * #lab #code_cont #stack #EQcode #EQcont #EQ1 #EQ2 destruct #EQstore
30  #Hio1 #Hio2 #no_ret_lab #cost_lab whd in match state_rel; normalize nodelta
31  inversion(check_continuations ?????) [ #_ #_ *] ** #Hcont #a_top #a_tail #EQcheck #_
32  normalize nodelta **** #HHcont #EQcall_post #EQstore #EQio #EQ destruct
33  >EQcont in EQcheck; whd in ⊢ (??%? → ?); inversion(cont … s1') normalize nodelta
34  [ #_ #EQ destruct] * #lab' #code_cont' #stack' #_ #EQcont'
35    change with (check_continuations ?????) in match (foldr2 ???????);
36    inversion(check_continuations ?????) [ #_ normalize #EQ destruct]
37    ** #H2 #a_top1 #a_tail1 #EQcheck >m_return_bind normalize nodelta
38    inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct cases HHcont]
39    * #labels #code_cleaned #EQclean normalize nodelta
40    >EQcode in EQcall_post; inversion(code ? s1')
41        [2,3,4,5,6,7:
42          [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
43            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
44          #_ whd in ⊢ (??%% → ?);
45          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
46          | cases(call_post_clean ?????); normalize nodelta
47            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
48               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
49                 [| #z cases(?∧?) normalize nodelta
50                 ]
51               ]
52            ]
53          | cases(call_post_clean ?????) normalize nodelta
54            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
55               [| #y cases(?∧?) normalize nodelta
56               ]
57            ]
58          | cases(call_post_clean ?????) normalize nodelta
59             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
60                [ cases (?==?) normalize nodelta ]
61             ]]
62          | cases(call_post_clean ?????) normalize nodelta
63             [| #x cases(? ∧ ?) normalize nodelta ]
64          ]
65          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
66        | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta
67          [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont
68          | * normalize nodelta [| #Lab cases(ret_costed_abs ??) normalize nodelta [| #xxx]] whd in ⊢ (??%% → ?);
69            #EQ destruct %{(refl …)} cases HHcont * [3: *] #EQ destruct #_ #_ [ #_] * #f * #c #EQ destruct
70          | * [|#LAB] normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // cases HHcont * #EQ destruct
71            try cases cost_lab #_ #_ cases EQ -EQ #EQ destruct #_ * #f * #c #EQ destruct
72          ]
73        ]
74| #s1 #s2 #i #instr #st * [|#lbl] #EQcode_s1 #EQst #EQ destruct #EQcont #EQ destruct #Hios1 #Hios2 *
75  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
76  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode_s1 inversion(code ? s1')
77  [1,2,4,5,6,7:
78    [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
79            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
80          #_ whd in ⊢ (??%% → ?);
81          [ |
82          | cases(call_post_clean ?????); normalize nodelta
83            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
84               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
85                 [| #z cases(?∧?) normalize nodelta
86                 ]
87               ]
88            ]
89          | cases(call_post_clean ?????) normalize nodelta
90            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
91               [| #y cases(?∧?) normalize nodelta
92               ]
93            ]
94          | cases(call_post_clean ?????) normalize nodelta
95             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
96                [ cases (?==?) normalize nodelta ]
97             ]]
98          | cases(call_post_clean ?????) normalize nodelta
99             [| #x cases(? ∧ ?) normalize nodelta ]
100          ]
101          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
102  | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
103    [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
104    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?==?) normalize nodelta
105    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct
106 ]
107| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ destruct #EQ destruct
108  #Hio1 #Hio2 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
109  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
110  [1,2,3,5,6,7:
111    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
112       | #lin #io #lout #instr #_ ]
113          #_ whd in ⊢ (??%% → ?);
114          [ |
115          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
116          | cases(call_post_clean ?????) normalize nodelta
117            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
118               [| #y cases(?∧?) normalize nodelta
119               ]
120            ]
121          | cases(call_post_clean ?????) normalize nodelta
122             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
123                [ cases (?==?) normalize nodelta ]
124             ]]
125          | cases(call_post_clean ?????) normalize nodelta
126             [| #x cases(? ∧ ?) normalize nodelta ]
127          ]
128          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
129  ]
130  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs'  #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
131  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
132  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
133  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
134  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
135  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
136| cases daemon
137| cases daemon
138| cases daemon
139| #s1 #s2 #lin #io #lout #instr #men #EQcode  #EQeval #EQcodes2 #EQcont_s2 #EQ destruct #Hio * whd in match state_rel;
140  normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
141  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode inversion(code ? s1')
142  [1,2,3,4,5,6: cases daemon (* ASSURDI*)
143  | #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
144    [ #EQ destruct] #x
145    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?∧?) normalize nodelta
146    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
147 ]
148| #s1 #s2 #f #act_p #lbl #instr #men #env_it #EQcode #EQenv_it  #EQeval #EQ destruct #EQcodes2 #EQ destruct #_ #_ *
149  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
150  #H1 #a_top #a_tail normalize nodelta #Hcall **** #HH1 >EQcode inversion(code ? s1')
151  [1,2,3,4,5,7: cases daemon (* ASSURDI*)
152  |*: #f' #act_p' #lbl' #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
153    [ #EQ destruct] #x cases lbl' in EQcode_s1'; normalize nodelta [ #_ #EQ destruct] #lbl'' #EQcode_s1'
154    inversion(?∈?) normalize nodelta
155    [#_ cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta
156      cases(?==?) normalize nodelta
157    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct #_#_ #EQ1 destruct % //
158    #_ whd in match (is_call_post_label ??); >EQcode_s1' %
159    ]
160    #ABS whd in ⊢ (??%% → ?);  #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct lapply(Hcall ?) [ %{f} %{(f_lab … env_it)} %]
161    whd in ⊢ (% → ?); whd in match (is_call_post_label ??); normalize nodelta >EQcode *
162 ]
163| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode #EQcont #EQ destruct #_ #_ #EQeval #EQ1 #EQ2 destruct * #_
164  whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta [ #_ *]
165  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode inversion(code … s1')
166  [1,3,4,5,6,7: cases daemon (*ASSURDI*)
167  | #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct
168    >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
169    * #LAB #instrs #stack' #_ #EQcont_s1' whd in match check_continuations; normalize nodelta
170    whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????);
171    cases(check_continuations ?????) normalize nodelta [#EQ destruct] ** #H2 #a_top1 #a_tail1
172    normalize nodelta   whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta [ #EQ destruct cases HH1]
173    * #ret_top #cleaned cases LAB in EQcont_s1';
174    [ #f #c #_ normalize nodelta #EQ destruct cases HH1
175    | *
176      [ #EQcont_s1' normalize nodelta #EQ destruct cases HH1 * #EQ destruct
177      | #lbl1 #EQcont_s1' whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) normalize nodelta
178        [ #EQkeep #EQ destruct cases HH1 ** #EQ destruct #HH2 #EQ destruct #_ #_ #_ #_ % // * #f * #c #EQ destruct
179        | #EQkeep #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
180        ]
181      ]
182    | * [|#lbl] #EQcont_s1' normalize nodelta  #EQ destruct cases HH1 *  #EQ destruct cases EQ -EQ #EQ destruct
183    ]
184  ]
185]
186qed.
187
188lemma bool_true : ∀b : bool.b=true → b. * // #EQ destruct qed.
189(*
190axiom actionlabel_of_cost_is_not_empty : ∀l : ActionLabel.
191is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c].
192*)
193lemma labelled_action_is_correct :
194∀p,p',prog.
195no_duplicates_labels … prog →
196let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
197∀s1,s2,s1' : state p.∀abs_top,abs_tail.
198∀l.is_costlabelled_act l →
199∀prf :execute_l p p' (env … prog) l s1 s2.
200state_rel … m keep abs_top abs_tail s1 s1' →
201∃abs_top'.∃s2'.
202execute_l p p' (env … t_prog) l s1' s2' ∧
203state_rel  … m keep abs_top' abs_tail s2 s2' ∧
204map_labels_on_trace … m … (actionlabel_to_costlabel l) =
205actionlabel_to_costlabel l @ abs_top'.
206#p #p' #prog  #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
207#s1 #s2 #s1' #abs_top #abs_tail #l #Hl #H lapply Hl -Hl elim H -s1 -s2 -l
208[ #s1 #s2 * #lbl #i #stack #EQcode_s1 #EQcont_s1 #EQ destruct #EQ destruct #EQstore #Hio1 #Hio2
209  #Hlbl #cost_lbl whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????)
210  normalize nodelta [ #_ *] ** #H1 #a_top #a_tail >EQcont_s1 inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
211  * #lbl' #i' #stack' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ?????) in match (foldr2 ???????);
212  inversion(check_continuations ?????) normalize nodelta [ #_ #EQ destruct] ** #H2 #a_top1 #a_tail1 #EQcheck
213  normalize nodelta inversion(call_post_clean ?????) normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct ***** ]
214  * #gen_labels #cleaned_i' #EQclean cases lbl' in EQcont_s1'; -lbl' normalize nodelta
215  [ #f #c #_ whd in ⊢ (??%% → ?); #EQ destruct *****
216  | * [|#lbl'] normalize nodelta #_ whd in ⊢ (??%% → ?); [2: cases(ret_costed_abs ??) normalize nodelta [|#lbl'']]
217    #EQ destruct ****** [2: *] #EQ destruct @⊥ cases Hlbl #H @H %
218  | * [|#lbl'] #EQcont_s1' normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct ****** [2: *] #EQ destruct
219    cases cost_lbl #HH2 #EQ destruct #EQget #EQ_cleaned #EQstore #EQio #EQ destruct
220    >EQcode_s1 in EQ_cleaned; inversion(code ? s1')
221    [2,3,4,5,6,7: cases daemon (*ASSURDI*)] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
222    %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
223    [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %]
224       whd >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // >EQclean %]
225   whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >EQget >append_nil %
226 ]
227| #s1 #s2 #seq #i #store * [|#lbl] #EQcode_s1 #EQeval #EQ destruct #EQcont #EQ destruct #Hio1 #Hio2 *
228  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta
229  [#_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
230  [1,2,4,5,6,7: cases daemon (*ASSURDI*)] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?);
231  inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned
232  cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget]
233  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct
234  %{genlab} %{(mk_state … i' (cont … s1') (store … s2) false)} % [ %
235  [ @(seq_sil … EQcode_s1') // ]
236  whd <EQcont >EQcheck normalize nodelta % // % // % // % // >EQcleaned %]
237  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >(\P EQget) >append_nil %
238| cases daemon
239| cases daemon
240| cases daemon
241| cases daemon
242| #s1 #s2 #lin #io #lout #i #store #EQcode_s1 #EQeval #EQcode_s2 #EQcont_s2. #EQ destruct #EQio_s2 *
243  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *]
244  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
245  [1,2,3,4,5,6: cases daemon (*ASSURDI*) ]
246  #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct]
247  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
248  #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct %{[]}
249  %{(mk_state … (EMPTY …) (〈cost_act (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
250  [ @(io_in … EQcode_s1') // ]
251  whd >EQcont_s2 whd in match (check_continuations ?????); change with (check_continuations ?????) in match (foldr2 ???????);
252  >EQcheck normalize nodelta >EQcleaned normalize nodelta % // % // % // % [2: >EQcode_s2 %] %
253  [2: cases(andb_Prop_true … (bool_true … EQget)) #H #_ >(\P (bool_true … H)) % ] % // % //]
254  cases(andb_Prop_true … (bool_true … EQget)) #_ #EQget'
255  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >append_nil >append_nil inversion(? == ?) in EQget';
256  [2: #_ *] #EQget' #_ >(\P EQget') %
257|*: cases daemon
258]
259qed.
260
261include "Vm.ma".
262
263theorem correctness_theorem : ∀p,p',prog.
264no_duplicates_labels … prog →
265let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
266∀si,s1,s2,sn,si' : state p.∀abs_top,abs_tail.
267∀t : raw_trace (operational_semantics … p' prog) si sn.
268measurable (operational_semantics … p' prog) … s1 s2 … t →
269state_rel … m keep abs_top abs_tail si si' →
270∃abs_top',abs_tail'.∃sn'.∃t' : raw_trace (operational_semantics … p' t_prog) si' sn'.
271state_rel  … m keep abs_top' abs_tail' sn sn' ∧
272is_permutation ? (map_labels_on_trace m (chop … (get_costlabels_of_trace … t))) 
273                  (chop … (get_costlabels_of_trace … t')) ∧
274                  ∃s1',s2'.
275measurable (operational_semantics … p' t_prog)  … s1' s2' … t'.
276#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
277#si #s1 #s3 #sn #si' #abs_top #abs_tail #t *  #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2
278* #prf1 * #prf2 ******* #pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init #Rsi_si'
279lapply(silent_in_silent … p' prog no_dup) >EQt_prog normalize nodelta #Hsilent
280cases(Hsilent … sil_ti0 … Rsi_si')
281#abs_top1 * #s0' * #t_i0' * #Rs0_s0' #sil_ti0'
282lapply(labelled_action_is_correct … p' prog no_dup) >EQt_prog normalize nodelta #Hmove
283cases(Hmove … prf1 … Rs0_s0') //
284#abs_top2 * #s1' ** #prf1' #Rs1_s1' #EQmap_l1
285lapply(correctness_lemma … p' prog no_dup) >EQt_prog normalize nodelta #H
286cases(H … pre_t12 … Rs1_s1') -H
287#abs_top3 * #s2' * #t12' ***** #Rs2_s2' #Hperm #_ #_ #pre_t12' #_
288cases(Hmove … prf2 … Rs2_s2') -Hmove //
289#abs_top4 * #s3' ** #prf2' #Rs3_s3' #EQmap_l2
290cases(Hsilent … sil_t3n … Rs3_s3')
291#abs_top5 * #sn' * #t3n' * #Rsn_sn' #sil_t3n'
292%{abs_top5} %{abs_tail} %{sn'}
293%{(t_i0' @ (t_ind … prf1' (t12' @ (t_ind … prf2' t3n'))))} %
294[ %{Rsn_sn'} >get_cost_label_append >get_cost_label_append >(get_cost_label_silent_is_empty … sil_ti0)
295  >(get_cost_label_silent_is_empty … sil_ti0') >(get_cost_label_append … (t_ind … (t_base …)))
296  >(get_cost_label_append … (t_ind … (t_base …))) in ⊢ (???%); >get_cost_label_append
297  >get_cost_label_append whd in match (get_costlabels_of_trace … (t_ind … t3n));
298  whd in match (get_costlabels_of_trace … (t_ind … t3n'));
299  >(get_cost_label_silent_is_empty … sil_t3n) >(get_cost_label_silent_is_empty … sil_t3n')
300  >append_nil cases(actionlabel_ok … Hl2) #c2 #EQc2 >EQc2 <associative_append <associative_append
301  <associative_append >chop_append_singleton <associative_append <associative_append >chop_append_singleton
302  >append_nil whd in match (get_costlabels_of_trace ??? (t_ind (operational_semantics p p' t_prog) … prf1' (t_base …)));
303  >append_nil >map_labels_on_trace_append >EQmap_l1 >associative_append @is_permutation_append_left_cancellable
304  lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
305  >(proj1 … (H … prf2 Hl2 … Rs2_s2')) in Hperm; [2: assumption] >append_nil @permute_equal_right
306| %{s1'} %{s3'} whd %{s0'} %{s2'} %{t_i0'} %{t12'} %{t3n'} %{l1} %{l2} %{prf1'} %{prf2'}
307  % [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
308  @(proj2 … (H … prf1 Hl1 … Rs0_s0')) assumption ] % // % // %
309  [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
310  @(proj2 … (H … prf2 Hl2 … Rs2_s2')) assumption ] % // % // % //
311]
312qed.
Note: See TracBrowser for help on using the repository browser.