(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "Lang_corr.ma".


lemma top_move_source_is_empty : ∀p,p',prog.
let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
∀l.
∀s1,s2,s1' : state p.∀abs_top,abs_tail.
execute_l … p' (env … prog) l s1 s2 → 
is_costlabelled_act p l → 
(is_call_act p l → is_call_post_label p (operational_semantics p p' prog) … s1) → 
state_rel … m keep abs_top abs_tail s1 s1' → abs_top = nil ? ∧
(is_call_act p l → is_call_post_label p (operational_semantics p p' t_prog) … s1').
#p #p' #prog @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
#l #s1 #s2 #s1' #abs_top #abs_tail #H elim H -s1 -s2 -l
[ #s1 #s2 * #lab #code_cont #stack #EQcode #EQcont #EQ1 #EQ2 destruct #EQstore
  #Hio1 #Hio2 #no_ret_lab #cost_lab whd in match state_rel; normalize nodelta
  inversion(check_continuations ?????) [ #_ #_ *] ** #Hcont #a_top #a_tail #EQcheck #_
  normalize nodelta **** #HHcont #EQcall_post #EQstore #EQio #EQ destruct
  >EQcont in EQcheck; whd in ⊢ (??%? → ?); inversion(cont … s1') normalize nodelta
  [ #_ #EQ destruct] * #lab' #code_cont' #stack' #_ #EQcont'
    change with (check_continuations ??????) in match (foldr2 ???????);
    inversion(check_continuations ?????) [ #_ normalize #EQ destruct]
    ** #H2 #a_top1 #a_tail1 #EQcheck >m_return_bind normalize nodelta
    inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct cases HHcont]
    * #labels #code_cleaned #EQclean normalize nodelta
    >EQcode in EQcall_post; inversion(code ? s1')
        [2,3,4,5,6,7:
          [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
        | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta
          [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont
          | * normalize nodelta [| #Lab cases(ret_costed_abs ??) normalize nodelta [| #xxx]] whd in ⊢ (??%% → ?); 
            #EQ destruct %{(refl …)} cases HHcont * [3: *] #EQ destruct #_ #_ [ #_] * #f * #c #EQ destruct
          | * [|#LAB] normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // cases HHcont * #EQ destruct 
            try cases cost_lab #_ #_ cases EQ -EQ #EQ destruct #_ * #f * #c #EQ destruct
          ]
        ]
| #s1 #s2 #i #instr #st * [|#lbl] #EQcode_s1 #EQst #EQ destruct #EQcont #EQ destruct #Hios1 #Hios2 *
  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode_s1 inversion(code ? s1')
  [1,2,4,5,6,7: 
    [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?==?) normalize nodelta
    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct
 ]
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ destruct #EQ destruct
  #Hio1 #Hio2 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
  [1,2,3,5,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  ]
  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs'  #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct
  #Hio1 #Hio2 * #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1  inversion(code ? s1')
  [1,2,3,5,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  ]
  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,4,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   ]
   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,4,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   ]
   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
| #s1 #s2 #lin #io #lout #instr #men #EQcode  #EQeval #EQcodes2 #EQcont_s2 #EQ destruct #Hio * whd in match state_rel;
  normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode inversion(code ? s1')
  [1,2,3,4,5,6: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  | #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    [ #EQ destruct] #x
    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?∧?) normalize nodelta
    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
 ]
| #s1 #s2 #f #act_p #lbl #instr #men #env_it #EQcode #EQenv_it  #EQeval #EQ destruct #EQcodes2 #EQ destruct #_ #_ *
  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
  #H1 #a_top #a_tail normalize nodelta #Hcall **** #HH1 >EQcode inversion(code ? s1')
  [1,2,3,4,5,7:
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
         ]
         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 
  |*: #f' #act_p' #lbl' #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    [ #EQ destruct] #x cases lbl' in EQcode_s1'; normalize nodelta [ #_ #EQ destruct] #lbl'' #EQcode_s1'
    inversion(?∈?) normalize nodelta 
    [#_ cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta 
      cases(?==?) normalize nodelta
    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct #_#_ #EQ1 destruct % // 
    #_ whd in match (is_call_post_label ???); >EQcode_s1' %
    ]
    #ABS whd in ⊢ (??%% → ?);  #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct lapply(Hcall ?) [ %{f} %{(f_lab … env_it)} %] 
    whd in ⊢ (% → ?); whd in match (is_call_post_label ???); normalize nodelta >EQcode *
 ]
| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode #EQcont #EQ destruct #_ #_ #EQeval #EQ1 #EQ2 destruct * #_
  whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta [ #_ *]
  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode inversion(code … s1')
  [1,3,4,5,6,7:
       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
          #_ whd in ⊢ (??%% → ?);
          [ 
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
         ]
         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 
  | #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct
    >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    * #LAB #instrs #stack' #_ #EQcont_s1' whd in match check_continuations; normalize nodelta
    whd in match (foldr2 ???????); change with (check_continuations ??????) in match (foldr2 ???????);
    cases(check_continuations ?????) normalize nodelta [#EQ destruct] ** #H2 #a_top1 #a_tail1
    normalize nodelta   whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta [ #EQ destruct cases HH1]
    * #ret_top #cleaned cases LAB in EQcont_s1';
    [ #f #c #_ normalize nodelta #EQ destruct cases HH1
    | * 
      [ #EQcont_s1' normalize nodelta #EQ destruct cases HH1 * #EQ destruct
      | #lbl1 #EQcont_s1' whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) normalize nodelta
        [ #EQkeep #EQ destruct cases HH1 ** #EQ destruct #HH2 #EQ destruct #_ #_ #_ #_ % // * #f * #c #EQ destruct
        | #EQkeep #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
        ]
      ]
    | * [|#lbl] #EQcont_s1' normalize nodelta  #EQ destruct cases HH1 *  #EQ destruct cases EQ -EQ #EQ destruct
    ]
  ]
]
qed.

lemma bool_true : ∀b : bool.b=true → b. * // #EQ destruct qed.

lemma labelled_action_is_correct :
∀p,p',prog.
no_duplicates_labels … prog → 
let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
∀s1,s2,s1' : state p.∀abs_top,abs_tail.
∀l.is_costlabelled_act p l → 
∀prf :execute_l p p' (env … prog) l s1 s2.
state_rel … m keep abs_top abs_tail s1 s1' → 
(is_call_act … l → bool_to_Prop (is_call_post_label … (operational_semantics … p' prog) … s1)) → 
∃abs_top'.∃s2'.
execute_l p p' (env … t_prog) l s1' s2' ∧
state_rel  … m keep abs_top' abs_tail s2 s2' ∧
map_labels_on_trace … m … (actionlabel_to_costlabel p l) = 
actionlabel_to_costlabel p l @ abs_top'.
#p #p' #prog  #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
#s1 #s2 #s1' #abs_top #abs_tail #l #Hl #H lapply Hl -Hl elim H -s1 -s2 -l
[ #s1 #s2 * #lbl #i #stack #EQcode_s1 #EQcont_s1 #EQ destruct #EQ destruct #EQstore #Hio1 #Hio2
  #Hlbl #cost_lbl whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????)
  normalize nodelta [ #_ *] ** #H1 #a_top #a_tail >EQcont_s1 inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
  * #lbl' #i' #stack' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ??????) in match (foldr2 ???????);
  inversion(check_continuations ?????) normalize nodelta [ #_ #EQ destruct] ** #H2 #a_top1 #a_tail1 #EQcheck
  normalize nodelta inversion(call_post_clean ?????) normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct ***** ]
  * #gen_labels #cleaned_i' #EQclean cases lbl' in EQcont_s1'; -lbl' normalize nodelta
  [ #f #c #_ whd in ⊢ (??%% → ?); #EQ destruct *****
  | * [|#lbl'] normalize nodelta #_ whd in ⊢ (??%% → ?); [2: cases(ret_costed_abs ??) normalize nodelta [|#lbl'']] 
    #EQ destruct ****** [2: *] #EQ destruct @⊥ cases Hlbl #H @H %
  | * [|#lbl'] #EQcont_s1' normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct ****** [2: *] #EQ destruct
    cases cost_lbl #HH2 #EQ destruct #EQget #EQ_cleaned #EQstore #EQio #EQ destruct 
    >EQcode_s1 in EQ_cleaned; inversion(code ? s1')
    [2,3,4,5,6,7: [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
    #_ %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
    [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %]
       whd >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // >EQclean %]
   whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >EQget >append_nil %
 ]
| #s1 #s2 #seq #i #store * [|#lbl] #EQcode_s1 #EQeval #EQ destruct #EQcont #EQ destruct #Hio1 #Hio2 *
  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta
  [#_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
  [1,2,4,5,6,7: [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?);
  inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned
  cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget] 
  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct #_
  %{genlab} %{(mk_state … i' (cont … s1') (store … s2) false)} % [ %
  [ @(seq_sil … EQcode_s1') // ]
  whd <EQcont >EQcheck normalize nodelta % // % // % // % // >EQcleaned %]
  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >(\P EQget) >append_nil %
| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,5,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  ]
  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
  %{a_top3} %{(mk_state … i_true' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
  [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
  [ @(cond_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_true' %
| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,5,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  ]
  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
  %{a_top2} %{(mk_state … i_false' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
  [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
  [ @(cond_false … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_false' %
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,4,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   ]
   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 
   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   #EQstore #EQio #EQ destruct #_ %{a_top2} 
   %{(mk_state … i_true' (〈cost_act … (None ?),LOOP … exp ltrue i_true' lfalse i_false'〉::(cont … s1')) (store … s2) false)}
   % [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
    [ @(loop_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
    change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
    whd in match (call_post_clean ??????); >EQi_false' normalize nodelta >EQi_true'
    >m_return_bind >(\P EQget1) >(\P EQget2) >(\b (refl …)) >(\b (refl …)) normalize nodelta
    % // % // % // % [ % // % //] >EQi_true' %
| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
  [1,2,3,4,6,7: 
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 
       | #lin #io #lout #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   ]
   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 
   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   #EQstore #EQio #EQ destruct #_ %{a_top1} 
   %{(mk_state … i_false' (cont … s1') (store … s2) false)}
   % [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
    [ @(loop_false … EQcode_s1') // ] >EQcont_s2 >EQcheck normalize nodelta 
    % // % // % // % // >EQi_false' %
| #s1 #s2 #lin #io #lout #i #store #EQcode_s1 #EQeval #EQcode_s2 #EQcont_s2. #EQ destruct #EQio_s2 *
  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *]
  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
  [1,2,3,4,5,6:  [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ] 
          | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
          ]
          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
  #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct]
  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
  #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct #_ %{[]} 
  %{(mk_state … (EMPTY …) (〈cost_act p (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
  [ @(io_in … EQcode_s1') // ]
  whd >EQcont_s2 whd in match (check_continuations ??????); change with (check_continuations ??????) in match (foldr2 ???????);
  >EQcheck normalize nodelta >EQcleaned normalize nodelta % // % // % // % [2: >EQcode_s2 %] % 
  [2: cases(andb_Prop_true … (bool_true … EQget)) #H #_ >(\P (bool_true … H)) % ] % // % //]
  cases(andb_Prop_true … (bool_true … EQget)) #_ #EQget'
  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >append_nil >append_nil inversion(? == ?) in EQget';
  [2: #_ *] #EQget' #_ >(\P EQget') %
| #s1 #s2 #f #act_p #r_lb #i #mem #env_it #EQcode_s1 #EQlook #EQeval #EQ destruct #EQcode_s2 #EQcont_s2
  #Hio1 #Hio2 * whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
   [1,2,3,4,5,7:
    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
          #_ whd in ⊢ (??%% → ?);
          [ |
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
         ]
         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     ]
     #f' #act_p' #r_lb #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean …) normalize nodelta
     [ #_ #EQ destruct] * #a_top1 #i'' #EQi' inversion(r_lb) normalize nodelta [ #_ #EQ destruct] #lbl #EQ
     destruct inversion(? ∈ ?) normalize nodelta #EQmem [ inversion(?==?) normalize nodelta #EQget]
     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct
     lapply(trans_env_ok … no_dup) >EQt_prog normalize nodelta #H cases(H … EQlook) -H #env_it' * #n
     ** #Hfresh #EQlook' ***** #EQt_code #EQget1 #EQsig #EQlab #same_fresh #same_keep whd in match (is_call_post_label ???);
     >EQcode_s1 normalize nodelta [ #_ | * %{f} %{(f_lab … env_it)} %]
     %{(gen_labels … (call_post_trans … (f_body … env_it) n []))}
     %{(mk_state … (f_body … env_it') (〈ret_act … (Some … lbl),i'〉 :: (cont … s1')) (store … s2) false)}
     % [2,4: whd in ⊢ (??%%); >append_nil >EQlab >EQget1 % ] % [1,3: >EQlab @(call … EQcode_s1') //]
     >EQcont_s2 whd in match (check_continuations ??????); 
     change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
     >EQi' normalize nodelta whd in match ret_costed_abs; normalize nodelta >EQmem normalize nodelta
     % // % // % // % [ % [ % // % //]  >(\P EQget) % ] <EQt_code @inverse_call_post_trans //
     [ >EQcode_s2 @no_duplicates_domain_of_fun // 
     | >EQcode_s2 #H20 #H21 >same_fresh // 
     | >EQcode_s2 #H23 #H24 >same_keep // 
     ]
| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode_s1 #EQcont_s1 #EQ destruct #Hio1 #Hio2 #EQeval #EQ1 #EQ2 destruct *
  whd in match state_rel; normalize nodelta >EQcont_s1 inversion(cont … s1') [| * #lab #i' #stack' #_ ] #EQcont_s1'
  whd in match (check_continuations ??????); [*] change with (check_continuations ??????) in match (foldr2 ???????);
  inversion(check_continuations ??????) normalize nodelta [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta
  inversion(call_post_clean …) normalize nodelta [ #_ *****] * #a_top1 #i'' #EQi' inversion lab normalize nodelta
  [ #f #lb ****** |3: * [| #x] #EQ destruct normalize nodelta ****** [|*] #EQ destruct] * [|#lb] #EQ destruct
  normalize nodelta [****** #EQ destruct] whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) #EQmem
  normalize nodelta ****** [*] #EQ destruct #HH1 #EQ destruct #EQget >EQcode_s1 inversion(code … s1')
  [1,3,4,5,6,7:
       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 
        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
          #_ whd in ⊢ (??%% → ?);
          [ 
          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
          | cases(call_post_clean ?????); normalize nodelta 
            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 
               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
                 [| #z cases(?∧?) normalize nodelta
                 ]
               ]
            ]
          | cases(call_post_clean ?????) normalize nodelta 
            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
               [| #y cases(?∧?) normalize nodelta 
               ]
            ]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
                [ cases (?==?) normalize nodelta ]
             ]]
         | cases(call_post_clean ?????) normalize nodelta
             [| #x cases(? ∧ ?) normalize nodelta ]
         ]
         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
   ] #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  #EQstore #EQio #EQ destruct #_
  %{a_top1} %{(mk_state … i' stack' (store … s2) false)} % [2: whd in ⊢ (??%%); >EQget >append_nil %]
  % [ @(ret_instr … EQcode_s1' … EQcont_s1') // ] >EQcheck normalize nodelta % // % // % // % // >EQi' %
]  
qed.

include "Vm.ma".

theorem correctness_theorem : ∀p,p',prog.
no_duplicates_labels … prog → 
let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
∀si,s1,s2,sn,si' : state p.∀abs_top,abs_tail.
∀t : raw_trace p (operational_semantics … p' prog) si sn.
measurable p (operational_semantics p p' prog) … s1 s2 … t → 
state_rel … m keep abs_top abs_tail si si' → 
∃abs_top',abs_tail'.∃sn'.∃t' : raw_trace p (operational_semantics … p' t_prog) si' sn'.
state_rel  … m keep abs_top' abs_tail' sn sn' ∧
is_permutation ? (map_labels_on_trace … m (chop … (get_costlabels_of_trace … t)))  
                  (chop … (get_costlabels_of_trace … t')) ∧
                  ∃s1',s2'.
measurable p (operational_semantics … p' t_prog)  … s1' s2' … t'.
#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
#si #s1 #s3 #sn #si' #abs_top #abs_tail #t *  #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2
* #prf1 * #prf2 ******* #pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init #Rsi_si'
lapply(silent_in_silent … p' prog no_dup) >EQt_prog normalize nodelta #Hsilent
cases(Hsilent … sil_ti0 … Rsi_si')
#abs_top1 * #s0' * #t_i0' * #Rs0_s0' #sil_ti0'
lapply(labelled_action_is_correct … p' prog no_dup) >EQt_prog normalize nodelta #Hmove
cases(Hmove … prf1 … Rs0_s0') // [2: @Hcall_init]
#abs_top2 * #s1' ** #prf1' #Rs1_s1' #EQmap_l1
lapply(correctness_lemma … p' prog no_dup) >EQt_prog normalize nodelta #H
cases(H … pre_t12 … Rs1_s1') -H
#abs_top3 * #s2' * #t12' ***** #Rs2_s2' #Hperm #_ #_ #pre_t12' #_
cases(Hmove … prf2 … Rs2_s2') -Hmove // [2: @Hcall_fin]
#abs_top4 * #s3' ** #prf2' #Rs3_s3' #EQmap_l2
cases(Hsilent … sil_t3n … Rs3_s3')
#abs_top5 * #sn' * #t3n' * #Rsn_sn' #sil_t3n'
%{abs_top5} %{abs_tail} %{sn'}
%{(t_i0' @ (t_ind … prf1' (t12' @ (t_ind … prf2' t3n'))))} %
[ %{Rsn_sn'} >get_cost_label_append >get_cost_label_append >(get_cost_label_silent_is_empty … sil_ti0)
  >(get_cost_label_silent_is_empty … sil_ti0') >(get_cost_label_append … (t_ind … (t_base …)))
  >(get_cost_label_append … (t_ind … (t_base …))) in ⊢ (???%); >get_cost_label_append
  >get_cost_label_append whd in match (get_costlabels_of_trace … (t_ind … t3n));
  whd in match (get_costlabels_of_trace … (t_ind … t3n'));
  >(get_cost_label_silent_is_empty … sil_t3n) >(get_cost_label_silent_is_empty … sil_t3n')
  >append_nil cases(actionlabel_ok … Hl2) #c2 #EQc2 >EQc2 <associative_append <associative_append
  <associative_append >chop_append_singleton <associative_append <associative_append >chop_append_singleton
  >append_nil whd in match (get_costlabels_of_trace ???? (t_ind ? (operational_semantics p p' t_prog) … prf1' (t_base …)));
  >append_nil >map_labels_on_trace_append >EQmap_l1 >associative_append @is_permutation_append_left_cancellable
  lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
  >(proj1 … (H … prf2 Hl2 … Rs2_s2')) in Hperm; [2: assumption] >append_nil @permute_equal_right
| %{s1'} %{s3'} whd %{s0'} %{s2'} %{t_i0'} %{t12'} %{t3n'} %{l1} %{l2} %{prf1'} %{prf2'}
  % [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
  @(proj2 … (H … prf1 Hl1 … Rs0_s0')) assumption ] % // % // % 
  [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
  @(proj2 … (H … prf2 Hl2 … Rs2_s2')) assumption ] % // % // % //
]
qed.