source: src/joint/StatusSimulationHelper.ma @ 3096

(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "joint/semanticsUtils.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".
include "joint/semantics_blocks.ma".
include "utilities/listb_extra.ma".
include "utilities/lists.ma".

lemma set_no_pc_eta:
 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
#P * //
qed.

lemma pc_of_label_eq :
  ∀pars: sem_graph_params.
  ∀globals,ge,bl,i_fn,lbl.
  fetch_internal_function ? globals ge bl = return i_fn →
  pc_of_label pars globals ge bl lbl =
    OK ? (pc_of_point pars bl lbl). 
#p #globals #ge #bl #i_fn #lbl #EQf 
whd in match pc_of_label;
normalize nodelta >EQf >m_return_bind %
qed.


lemma bind_new_bind_new_instantiates : 
∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
bind_new_instantiates B X x m l → bind_new_P' ?? P m → 
P l x.
#B #X #m elim m normalize nodelta
[#x #y * normalize // #B #l' #P *
| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
 @Hr
]
qed.

let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝
  match b with
  [ bret B ⇒
    match l with
    [ nil ⇒ Some ? B
    | _ ⇒ None ?
    ]
  | bnew f ⇒
    match l with
    [ nil ⇒ None ?
    | cons r l' ⇒
      bind_instantiate B X (f r) l'
    ]
  ].
  
lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X.
∀l : list B.∀x : X.
bind_instantiate B X b l = Some ? x → 
bind_new_instantiates B X x b l. 
#B #X #b elim b 
[#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) %
|#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H
 whd @IH assumption
]
qed.

lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
∀l : list B.∀x : X.
bind_new_instantiates B X x b l → 
bind_instantiate B X b l = Some ? x.
#B #X #b elim b
[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
| #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
]
qed.

coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
∀l : list B.∀x : X.
∀prf : bind_new_instantiates B X x b l. 
bind_instantiate B X b l = Some ? x ≝
bind_instantiate_instantiates
on _prf : bind_new_instantiates ?????
to eq (option ?) (bind_instantiate ????) (Some ??).

definition lbl_funct_type ≝  block → label → (list label).
definition regs_funct_type ≝ block → label → (list register).


definition preamble_length ≝ 
λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
λstack_size : (ident → option ℕ).
λinit : ∀globals.joint_closed_internal_function P_in globals
         →bound_b_graph_translate_data P_in P_out globals.
λinit_regs : block → list register.
λf_regs : regs_funct_type.λbl : block.λlbl : label.
! bl ← code_block_of_block bl ;
! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
                           (joint_globalenv P_in prog stack_size) bl);
! stmt ← stmt_at P_in … (joint_if_code … fn) lbl;
! data ← bind_instantiate ?? (init … fn) (init_regs bl);
match stmt with
[ sequential step nxt ⇒ 
    ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl);
    return |\fst (\fst step_block)|
| final fin ⇒ 
    ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl);
    return |\fst fin_block|
| FCOND abs _ _ _ ⇒ Ⓧabs
]. 


definition sigma_label : ∀p_in,p_out : sem_graph_params.
joint_program p_in → (ident → option ℕ) → 
(∀globals.joint_closed_internal_function p_in globals
         →bound_b_graph_translate_data p_in p_out globals) → 
(block → list register) → lbl_funct_type → regs_funct_type → 
block → label → option label ≝ 
λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
! bl ← code_block_of_block bl ;
! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 
                           (joint_globalenv p_in prog stack_size) bl);
! 〈res,s〉 ← 
 find ?? (joint_if_code ?? fn)
  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
             [ None ⇒ false
             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
                         [ None ⇒ false
                         | Some x ⇒ eq_identifier … searched x
                         ]
             ]);
return res.

lemma partial_inj_sigma : 
∀p_in,p_out,prog,stack_size,init,init_regs.
∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2. 
sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→ 
sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 = 
sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 → 
lbl1 = lbl2.
#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2 
inversion(sigma_label ????????? lbl1)
[ #_ * #H @⊥ @H %]
#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???) 
normalize nodelta
[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
[2: #_ *] #EQ destruct(EQ) #_ %
qed.

definition sigma_pc_opt :  
∀p_in,p_out : sem_graph_params.
joint_program p_in → (ident → option ℕ) → 
(∀globals.joint_closed_internal_function p_in globals
         →bound_b_graph_translate_data p_in p_out globals) → 
(block → list register) → lbl_funct_type → regs_funct_type → 
program_counter → option program_counter ≝
λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
let target_point ≝ point_of_pc p_out pc in
if eqZb (block_id (pc_block pc)) (-1) then
 return pc
else 
 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs 
                   f_lbls f_regs (pc_block pc) target_point;
 return pc_of_point p_in (pc_block pc) source_point.

lemma sigma_stored_pc_inj :
∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. 
sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc = 
sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → 
pc = pc'.
#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs 
* #bl1 #p1 * #bl2 #p2
inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta 
@eqZb_elim [2: *] normalize nodelta #Hbl 
[ #H @('bind_inversion H) -H * #pt1 #EQpt1] 
whd in ⊢ (??%? → ?); #EQ destruct(EQ)
#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt; 
normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
[1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
normalize nodelta whd in match (offset_of_point ??);
whd in ⊢ (??%% → ?); #EQ destruct(EQ)
[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
whd in match (offset_of_point ??) in EQpt2;
<EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))
[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
whd in match (point_of_offset ??); whd in match (point_of_offset ??); 
#EQ -prog destruct(EQ) %
qed.

lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 
(∀ prf : r = Code.P (g prf)) → 
P ((match r return λx.(r = x → ?) with
    [XData ⇒ f | Code ⇒ g])(refl ? r)).
#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
qed. 

definition sigma_stored_pc ≝ 
λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
      
lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
code_block_of_block bl = return bl.
* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
qed.

(*TO BE MOVED*)
lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
#A #l1 elim l1 [#l2 #P *] #hd #tl #IH * 
[#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
qed.

lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
[#a normalize // ] #hd1 #tl1 #a normalize * 
[ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
| #H %2 >append_cons @IH assumption] 
qed.

lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
#p #globals #code #src #l1 lapply src -src elim l1 
[ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
#hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
#hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
qed.

lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
∀f_lbls : lbl_funct_type.∀f_regs.
b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs → 
∀id,fn.
∀bl:Σb.block_region b = Code. ∀pt,stmt. 
block_id … bl ≠ -1 → 
fetch_internal_function … 
   (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
stmt_at p_in … (joint_if_code … fn) pt = return stmt →  
∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
match n with
[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt
].
#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
#bl #pt #stmt * #Hbl #EQfn #EQstmt    
lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H 
lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
[ * #pre_instr #instr #post_instr | #pre_instr #instr] * 
[ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
 [ @eq_identifier_elim #EQentry normalize nodelta 
   [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
     whd in ⊢ (???% → ?); #EQ destruct(EQ) 
   |*: #Hregs
   ]
 | #Hregs
 ]
| #Hregs
]
#syntax_spec
[4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
[1,2,4,5: %{(|pre_instr|)} | %{O}]
cut(? : Prop) 
[3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
   >m_return_bind >EQfn >m_return_bind inversion(find ????)
   [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
   >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
   normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
   whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
   >m_return_bind cases stmt1 in EQfind; -stmt1
   [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
   cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
   [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
   >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
   whd in match (length ??); normalize nodelta 
   [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %]
   whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
   #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
   #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
   cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) **
   #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
   whd in match code_has_point; normalize nodelta >EQstmt @I
 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
     #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?); 
     [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
     |*:   #EQt_stmt
     ]
     %{mid1} cut(? : Prop)
     [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta 
       >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
       [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
         whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
         [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
       lapply(find_predicate ?????? EQfind) whd in match preamble_length;
       normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
       whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 
       >m_return_bind cases stmt1 in EQfind; -stmt1
       [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
       cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *] 
       [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
       >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
       whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
       [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
         #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
         #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
         @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
         >e0 @Exists_append2 % %
       |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
         lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
         @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
         whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
         >(find_lookup ?????? EQfind) @I
       ]    
     |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
                whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
                #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
                [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
                try % try( #n %) #n <minus_n_n %
     |*:
     ]
  ] 
 |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
   >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
   normalize nodelta 
   [1,2,3,4: >Hregs % 
   | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
     #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
     whd in match (bind_instantiate ????); %
   ]
 |*:
 ]
qed.

lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
f_regs,pc. 
sigma_pc_opt p_in p_out prog stack_sizes init 
   init_regs f_lbls f_regs pc ≠ None ? → 
 pc_block … pc = 
 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init 
                                           init_regs f_lbls f_regs pc).
#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
whd in match sigma_stored_pc; normalize nodelta
inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1 
whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta
[ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) -H
#lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
qed.

lemma fetch_statement_sigma_stored_pc : 
∀p_in,p_out,prog,stack_sizes,
init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
b_graph_transform_program_props p_in p_out stack_sizes
  init prog init_regs f_lbls f_regs → 
block_id … (pc_block pc) ≠ -1 → 
let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 
fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
return 〈f,fn,stmt〉 → 
∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
match stmt with
[ sequential step nxt ⇒ 
    ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 
                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 
                                           init_regs f_lbls f_regs pc' = pc ∧
    ∃fn',nxt'.
    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
    if not_emptyb … (added_prologue … data) ∧
       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
    then return 〈f,fn',sequential ?? (NOOP …) nxt'〉
    else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉
| final fin ⇒ 
    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 
                                           init_regs f_lbls f_regs pc' = pc ∧
    ∃fn'.fetch_statement p_out … 
       (joint_globalenv p_out trans_prog stack_sizes) pc' 
       = return 〈f,fn',final ?? (\snd fin_block)〉            
| FCOND abs _ _ _ ⇒ Ⓧabs
].
#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
#good #Hbl #EQfetch
lapply(b_graph_transform_program_fetch_statement … good pc f fn ?)
[2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta 
      #H cases(H EQfetch) -H |*:]
#data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H;
[ #step #nxt | #fin | *] normalize nodelta #EQfetch -stmt
[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta 
  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
* #block * 
[ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
  #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
  * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
|*: #Hregs #syntax_spec
]
cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt; 
  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
  % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
  @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_
|*: %{block} >Hregs %{(refl …)}
]
cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
[   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt}
    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H %
|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
|6,7,8: %{pc}
]
whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
@eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
[1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
%{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
[1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
[1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
|*: #l1 * #mid **
]
#EQmid #EQpre whd in ⊢ (% → ?);
[1,2,3,4: * #nxt1 *] #EQt_stmt 
[1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}]
whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
@('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
#EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
[1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
   #EQ destruct(EQ)]
[1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
[1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
   * #mid * #rest ** #EQ destruct(EQ)]
[1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
[4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %]
        #EQ <EQ in EQentry; * #H @⊥ @H %]
* #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??); 
whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt; 
lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
>nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
#EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1 
[1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %]
      @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_
      >point_of_pc_of_point %]
destruct(EQ3) >point_of_pc_of_point >EQt_stmt %
qed.

definition make_is_relation_from_beval : (beval → beval → Prop) → 
internal_stack → internal_stack → Prop≝ 
λR,is1,is2.
match is1 with
[ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
| one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
| both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
].

lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
∀Ristack1 : internal_stack → internal_stack → Prop.
∀Ristack2 : internal_stack → internal_stack → Prop.
(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 
(∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 → 
                                   Ristack2 (one_is bv1) (one_is bv2)) → 
(∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 → 
                         Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) → 
                         gen_preserving2 ?? gen_res_preserve …
                              Ristack1 Rbeval Ristack2 is_push is_push.
#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4 
whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta 
[2:#x|3: #x #y #_ @res_preserve_error_gen]
cases is2 normalize nodelta
 [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
 [@H2 [assumption | @(H … H5) ] | @H1 assumption]
qed.
(*
lemma is_push_ok : ∀R : beval → beval → Prop.
               gen_preserving2 ?? gen_res_preserve …
                       (make_is_relation_from_beval R) R 
                       (make_is_relation_from_beval R) 
                       is_push is_push.
#R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
qed.
*)
lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
∀Ristack1 : internal_stack → internal_stack → Prop.
∀Ristack2 : internal_stack → internal_stack → Prop.
(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 
Ristack2 empty_is empty_is → 
(∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) → 
          gen_preserving ?? gen_res_preserve …
                              Ristack1 
                              (λx,y.Rbeval (\fst x) (\fst y) ∧
                                Ristack2 (\snd x) (\snd y)) is_pop is_pop.
#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
[1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
@m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
qed.

(*
lemma is_pop_ok1 : ∀R : beval → beval → Prop.
           gen_preserving ?? gen_res_preserve …
                         (make_is_relation_from_beval R)
                         (λx,y.R (\fst x) (\fst y) ∧
                               (make_is_relation_from_beval R) (\snd x) (\snd y))
                         is_pop is_pop.
#R @is_pop_ok //
qed.


definition make_weak_state_relation ≝ 
λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
(make_is_relation_from_beval R) (istack … st1) (istack … st2).
*)


lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 
                  make_is_relation_from_beval Rbeval is1 is2) →
(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 
 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
(∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 → 
 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) → 
                    gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
                                   (push p_in) (push p_out).
#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
whd in match push; normalize nodelta 
@(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
[ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
  [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
  | @(H … H3) %
  ]
| * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?); 
  [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return 
  [ @(H2 … H3) assumption
  | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
    #EQ destruct(EQ)
  | @(H1 … H3) assumption
  ]
]
qed.


lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 
                  make_is_relation_from_beval Rbeval is1 is2) →
(∀st1,st2.Rstate1 st1 st2 → 
 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) → 
(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 
 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → 
               gen_preserving ?? gen_res_preserve …
                 Rstate1
                (λx,y.Rbeval (\fst x) (\fst y) ∧
                 Rstate2(\snd x) (\snd y))
                (pop p_in) (pop p_out).
#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3 
whd in match pop; normalize nodelta
@(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧ 
           (make_is_relation_from_beval Rbeval (\snd x) (\snd y))))  
[ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
| * #bv1 * [|#x|#x1 #x2] * #bv2 * 
[1,4,7:|2,5,8: #y
|*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
#_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
% // [ @(H1 … H3) | @(H2 … H3) assumption]
qed.


definition joint_state_relation ≝ 
λP_in,P_out.program_counter → state P_in → state P_out → Prop.

definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.


record good_state_relation (P_in : sem_graph_params) 
   (P_out : sem_graph_params) (prog : joint_program P_in)
   (stack_sizes : ident → option ℕ)
   (init : ∀globals.joint_closed_internal_function P_in globals
         →bound_b_graph_translate_data P_in P_out globals)
   (init_regs : block → list register) (f_lbls : lbl_funct_type) 
   (f_regs : regs_funct_type)
   (st_no_pc_rel : joint_state_relation P_in P_out)
   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝ 
{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init 
                     prog init_regs f_lbls f_regs
; fetch_ok_sigma_state_ok : 
   ∀st1,st2,f,fn. st_rel st1 st2 → 
    fetch_internal_function … 
     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))  
     = return 〈f,fn〉 →
     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
; fetch_ok_pc_ok : 
  ∀st1,st2,f,fn.st_rel st1 st2 → 
   fetch_internal_function … 
     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))  
     = return 〈f,fn〉 → 
   pc … st1 = pc … st2
; fetch_ok_sigma_last_pop_ok : 
  ∀st1,st2,f,fn.st_rel st1 st2 → 
   fetch_internal_function … 
     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))  
     = return 〈f,fn〉 → 
   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 
                       f_lbls f_regs (last_pop … st2)
; st_rel_def : 
  ∀st1,st2,pc,lp1,lp2,f,fn.
  fetch_internal_function … 
     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
   st_no_pc_rel pc st1 st2 →
   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 
          f_lbls f_regs lp2 → 
  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
; as_label_ok_non_entry :
  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
  ∀st1,st2,f,fn,stmt. 
  fetch_statement … 
  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 → 
  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn → 
  as_label (joint_status P_in prog stack_sizes) st1 = 
  as_label (joint_status P_out trans_prog stack_sizes) st2
; pre_main_ok :
  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    block_id … (pc_block (pc … st1)) = -1 → 
    st_rel st1 st2 → 
    as_label (joint_status P_in prog stack_sizes) st1 =
    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
    (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
      st1 = return st1' → 
    ∃st2'. st_rel st1' st2' ∧ 
    eval_state P_out … 
     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
; cond_commutation :
    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    ∀f,fn,a,ltrue,lfalse,bv,b.
    block_id … (pc_block (pc … st1)) ≠ -1 → 
    let cond ≝ (COND P_in ? a ltrue) in
    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 
    return 〈f, fn,  sequential … cond lfalse〉 →  
    acca_retrieve … P_in (st_no_pc … st1) a = return bv → 
    bool_of_beval … bv = return b → 
    st_rel st1 st2 → 
    ∀t_fn.
    fetch_internal_function … 
     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
     return 〈f,t_fn〉 → 
    bind_new_P' ??
     (λregs1.λdata.bind_new_P' ?? 
     (λregs2.λblp.(\snd blp) = [ ] ∧
        ∀mid.
          stmt_at P_out … (joint_if_code ?? t_fn) mid
          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 
         ∃st2_pre_mid_no_pc. 
            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 
             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) 
            = return st2_pre_mid_no_pc ∧
            let new_pc ≝ if b then 
                           (pc_of_point P_in (pc_block (pc … st1)) ltrue) 
                         else 
                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
                  bool_of_beval … bv' = return b
            (*let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc 
                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
            eval_statement_advance P_out (prog_var_names … trans_prog)
             (joint_globalenv P_out trans_prog stack_sizes) f t_fn
             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*)
   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
  ) (init ? fn) 
; seq_commutation :
  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
  ∀f,fn,stmt,nxt.
  block_id … (pc_block (pc … st1)) ≠ -1 → 
  let seq ≝ (step_seq P_in ? stmt) in
  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 
  return 〈f, fn,  sequential … seq nxt〉 →  
  eval_state P_in … (joint_globalenv P_in prog stack_sizes) 
  st1 = return st1' → 
  st_rel st1 st2 → 
  ∀t_fn.
  fetch_internal_function …
     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
  return 〈f,t_fn〉 → 
  bind_new_P' ??
     (λregs1.λdata.bind_new_P' ?? 
      (λregs2.λblp.
       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
                            blp = (ensure_step_block ?? l) ∧
       ∃st2_fin_no_pc.
           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 
              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
     ) (init ? fn)
; cost_commutation : 
  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
  ∀st1,st2,pc.∀f,fn,c,nxt.
  block_id … (pc_block pc) ≠ -1 → 
  st_no_pc_rel pc st1 st2 → 
  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc = 
  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 →  
  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2 
}.

lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
In ? (stmt_labels p ? stmt) lbl→ 
fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
pc' = pc_of_point p (pc_block pc) lbl → 
∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?) 
[3: * cases lbl #x #y cases(decidable_eq_pos … x y) 
    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
  whd in match code_has_label; whd in match code_has_point; normalize nodelta
  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
  >point_of_pc_of_point >EQstmt' %
| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_ 
    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
    >point_of_pc_of_point >EQstmt' %
  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
  ]
]
qed. 



lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
∀f,fn,stmt,st1,st2.
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
                    st_no_pc_rel st_rel → 
st_rel st1 st2 → 
fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
 return 〈f,fn,stmt〉 → 
st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
qed.

lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀st_no_pc_rel,st_rel.
∀f,fn,stmt,st1,st2.
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs  
                    st_no_pc_rel st_rel→ 
st_rel st1 st2 → 
fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
 return 〈f,fn,stmt〉 → 
pc … st1 = pc … st2.
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
@(fetch_ok_pc_ok … goodR … EQfn) assumption
qed.

lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀st_no_pc_rel,st_rel.
∀f,fn,stmt,st1,st2.
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
                    st_no_pc_rel st_rel → 
st_rel st1 st2 → 
fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
 return 〈f,fn,stmt〉 → 
(last_pop … st1) = 
 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls 
  f_regs (last_pop … st2).
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
qed.

(*
lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
∀st_no_pc_rel,st_rel.
∀f,fn,stmt,st1,st2.
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 
                    st_no_pc_rel st_rel → 
st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) → 
(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) → 
fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
 return 〈f,fn,stmt〉 → st_rel st1 st2.
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ) 
#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
@(st_rel_def … goodR … EQfn) assumption
qed.
*)

(*
(*CSC: Isn't this already proved somewhere else??? *) 
lemma point_of_pc_pc_of_point:
 ∀P_in: sem_graph_params.∀l,st.
   point_of_pc P_in
    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
     (pc_block (pc P_in st)) l) = l.
 #P * //
qed.*)


lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀st_no_pc_rel,st_rel.
let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
                    st_no_pc_rel st_rel → 
∀st1,st1' : joint_abstract_status prog_pars_in.
∀st2 : joint_abstract_status prog_pars_out.
∀f : ident.
∀fn : joint_closed_internal_function P_in ?.
∀a,ltrue,lfalse.
block_id … (pc_block (pc … st1)) ≠ -1 → 
st_rel st1 st2 → 
 let cond ≝ (COND P_in ? a ltrue) in
  fetch_statement P_in ?
   (joint_globalenv P_in prog stack_sizes) (pc … st1) = 
     return 〈f, fn, sequential … cond lfalse〉 → 
 eval_state P_in …
  (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 
as_costed (joint_abstract_status prog_pars_in) st1' →
∃ st2'. st_rel st1' st2' ∧ 
∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
bool_to_Prop (taaf_non_empty … taf).
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel 
#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 
#EQfetch #EQeval
@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
[ >(pc_of_label_eq … EQfn)
  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
] 
#EQ destruct(EQ) #n_costed
lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 
      #H cases(H EQfetch) -H |*:]
#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta 
*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *] 
      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ 
      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
      <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
]
#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * 
#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 
* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
[2,4: % assumption]
#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
normalize nodelta
#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue) 
     (last_pop … st2))}
| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
     (last_pop … st2))}
]
letin st1' ≝ (mk_state_pc P_in ???)
letin st2' ≝ (mk_state_pc P_out ???)
cut(st_rel st1' st2')
[1,3: @(st_rel_def … goodR … f fn ?) 
      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
      |2,5: assumption
      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
      ]
]
#H_fin
%
[1,3: assumption]
>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
lapply(taaf_to_taa ??? 
           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
                                       seq_pre_l EQst_pre_mid_no_pc) ?)
[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
      #H @H %
] 
#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
[1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
      whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin) 
      [1,3: assumption 
      |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
            [ whd in match stmt_forall_labels; whd in match stmt_labels;
              normalize nodelta #H cases(append_All … H) #_
              whd in match stmt_explicit_labels; whd in match step_labels;
              normalize nodelta * whd in match (point_of_label ????); 
              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc; 
              normalize nodelta whd in match pc_of_point; normalize nodelta
              >point_of_offset_of_point %
            ]
      ]
|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
      >EQt_cond %
|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
    >rel_v_v' >m_return_bind normalize nodelta
    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
]
qed.


lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀st_no_pc_rel,st_rel.
let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
                    st_no_pc_rel st_rel → 
∀st1,st1' : joint_abstract_status prog_pars_in.
∀st2 : joint_abstract_status prog_pars_out.
∀f.∀fn : joint_closed_internal_function P_in ?.
∀stmt,nxt.
block_id … (pc_block (pc … st1)) ≠ -1 → 
st_rel st1 st2 → 
 let seq ≝ (step_seq P_in ? stmt) in
  fetch_statement P_in …
   (joint_globalenv P_in prog stack_sizes) (pc … st1) = 
     return 〈f, fn,  sequential ?? seq nxt〉 → 
 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
  st1 = return st1' → 
∃st2'. st_rel st1' st2' ∧            
∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.            
 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 
 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 
#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel 
#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 
      #H cases(H EQfetch) -H |*:]
#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc; 
  normalize nodelta whd in match (point_of_offset ??); #ABS #_ 
  lapply(fetch_statement_inv … EQfetch) * #_ 
  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; 
  normalize nodelta whd in match (point_of_offset ??); <ABS 
  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
]
#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl 
>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC 
cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
               [2: % assumption]
#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
#EQfn #_
%
[ @(st_rel_def ?????????? goodR … f fn)
      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
      ]
]
%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 
                                      SBiC EQst2_fin_no_pc)}
@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
qed.


lemma general_eval_cost_ok :
∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀st_no_pc_rel,st_rel.
let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
                    st_no_pc_rel st_rel → 
∀st1,st1' : joint_abstract_status prog_pars_in.
∀st2 : joint_abstract_status prog_pars_out.
∀f.
∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
block_id … (pc_block (pc … st1)) ≠ -1 → 
st_rel st1 st2 → 
let cost ≝ COST_LABEL P_in ? c in
 fetch_statement P_in …
  (joint_globalenv P_in prog stack_sizes) (pc … st1) = 
    return 〈f, fn,  sequential ?? cost nxt〉 → 
 eval_state P_in … (ev_genv … prog_pars_in) 
            st1 = return st1' → 
∃ st2'. st_rel st1' st2' ∧
∃taf : trace_any_any_free 
        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
        st2 st2'.
bool_to_Prop (taaf_non_empty … taf).
#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta 
#EQfetch 
whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta 
>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); 
#EQ destruct(EQ) 
%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
                 (last_pop … st2))} %
[ cases(fetch_statement_inv … EQfetch) #EQfn #_ 
  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
  whd in match (succ_pc ???); whd in match (point_of_succ ???);
  >set_no_pc_eta
  @(st_rel_def … prog … stack_size … goodR 
          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
  ]
| lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 
      #H cases(H EQfetch) -H |*:]
  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
  #EQt_fn #Hinit normalize nodelta * #bl * 
  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    * #EQ1 #EQ2 destruct(EQ1 EQ2)
  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * 
   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    * #EQ1 #EQ2 destruct(EQ1 EQ2)
  ]  
  %{(taaf_step … (taa_base …) …)} 
  [3,6,9: @I
  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
  ]
]
qed.

(*
lemma eval_return_ok : 
∀ P_in , P_out: sem_graph_params.
∀prog : joint_program P_in.
∀stack_sizes.
∀ f_lbls,f_regs.∀f_bl_r.∀init.
∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
∀st_no_pc_rel,st_rel.
let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 
                    st_no_pc_rel st_rel → 
∀st1,st1' :  joint_abstract_status prog_pars_in.
∀st2 : joint_abstract_status prog_pars_out.
∀f.
∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
*)