include "ERTLptr/ERTLptrToLTL.ma".
include "ERTLptr/ERTLptr_semantics.ma".
include "LTL/LTL_semantics.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".
include "common/AssocList.ma".

(* Inefficient, replace with Trie lookup *)
definition lookup_stack_cost ≝
 λp.λid : ident.
  assoc_list_lookup ? ℕ id (eq_identifier …) p.

(*TO BE MOVED*)
definition ERTLptr_status ≝ 
λprog : ertlptr_program.λstack_sizes.
joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).

definition LTL_status ≝
λprog : ltl_program.λstack_sizes.
joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).

definition local_clear_sb_type ≝ decision → bool.
definition clear_sb_type ≝ label → local_clear_sb_type.
  
axiom to_be_cleared_sb :  
∀live_before : valuation register_lattice. coloured_graph live_before → clear_sb_type.

definition local_clear_fb_type ≝ vertex → bool.
definition clear_fb_type ≝ label → local_clear_fb_type.

axiom to_be_cleared_fb :
∀live_before : valuation register_lattice.clear_fb_type.

axiom sigma_fb_state:
 ertlptr_program → local_clear_fb_type →
  state ERTLptr_semantics → state ERTLptr_semantics.

axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). ∀l.
 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
  ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).

axiom dead_registers_in_dead :
 ∀fix_comp.∀build : coloured_graph_computer.
 ∀prog : ertlptr_program.
 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
 ∀l.
 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
 let coloured_graph ≝ build … fn after in
 ∀R : Register.
  ¬ lives (inr ? ? R) (livebefore  … fn after l) → 
   to_be_cleared_sb … coloured_graph l R.

axiom sigma_sb_state:
 ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics.

definition dummy_state : state ERTLptr_semantics ≝ 
mk_state ERTL_semantics
   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.

definition dummy_state_pc : state_pc ERTLptr_semantics ≝ 
mk_state_pc ? dummy_state (null_pc one) (null_pc one).


definition sigma_fb_state_pc :
 fixpoint_computer → ertlptr_program → 
  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝ 
 λfix_comp,prog,st.
 let ge ≝ globalenv_noinit … prog in 
 let globals ≝ prog_var_names … prog in 
 match fetch_internal_function … ge (pc_block (pc … st)) with
  [ OK y ⇒ 
     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     let before ≝ livebefore … (\snd y) after in 
     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st)  
      (last_pop … st)
  | Error e ⇒ dummy_state_pc
  ].

include "joint/StatusSimulationHelper.ma".

definition sigma_sb_state_pc:
 fixpoint_computer → coloured_graph_computer →  
  ertlptr_program → lbl_funct → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝ 
 λfix_comp,build,prog,f_lbls,st. 
  let ge ≝ globalenv_noinit … prog in 
  let globals ≝ prog_var_names … prog in 
  match fetch_internal_function … ge (pc_block (pc … st)) with
  [ OK y ⇒  
     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     let coloured_graph ≝ build … (\snd y) after in
     mk_state_pc ? (sigma_sb_state prog 
                       (to_be_cleared_sb … coloured_graph pt) st) (pc … st)  
                   (sigma_stored_pc ERTLptr_semantics LTL_semantics 
                                    prog f_lbls (last_pop … st)) 
  | Error e ⇒ dummy_state_pc
  ].

definition state_rel : fixpoint_computer → coloured_graph_computer → 
ertlptr_program →
 (Σb:block.block_region b = Code) → label → state ERTL_state → state LTL_LIN_state → Prop ≝ 
λfix_comp,build,prog,bl,pc,st1,st2.
∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
let before ≝ livebefore … fn after in
let coloured_graph ≝ build … fn after in
(sigma_fb_state prog (to_be_cleared_fb before pc) st1) =
(sigma_sb_state prog (to_be_cleared_sb … coloured_graph pc) st2). 

axiom write_decision :
 decision → beval → state LTL_LIN_state → state LTL_LIN_state.

axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.

axiom insensitive_to_be_cleared_sb :
 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
  ∀d : decision.∀bv.tb d → 
   sigma_sb_state prog tb st =
    sigma_sb_state prog tb (write_decision d bv st).


definition ERTLptr_to_LTL_StatusSimulation :
∀fix_comp : fixpoint_computer.
∀colour : coloured_graph_computer.
∀ prog : ertlptr_program.
∀ f_lbls, f_regs. ∀f_bl_r.
b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 
let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
let stacksizes ≝ lookup_stack_cost … m in  
status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝ 
λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
    mk_status_rel ??
    (* sem_rel ≝ *) 
         (λs1:ERTLptr_status ? ?
          .λs2:LTL_status ? ?
           .sigma_fb_state_pc fix_comp prog s1
            =sigma_sb_state_pc fix_comp colour prog f_lbls s2) 
    (* call_rel ≝ *)  
       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
           .pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics 
                                                          prog f_lbls (pc ? s2))
    (* sim_final ≝ *) ?.
cases daemon
qed.

axiom as_label_ok :
∀fix_comp,colour.
∀prog.∀f_lbls,f_regs. ∀f_bl_r.
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀st1,st2,fn,id,stmt.
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
R st1 st2 →  
fetch_statement ERTLptr_semantics (prog_var_names … prog) 
      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 → 
as_label ? st2 = as_label ? st1.

(*
(* Copy the proof too from previous pass *)
axiom fetch_stmt_ok_sigma_state_ok :
∀prog : ertlptr_program.
∀ f_lbls,f_regs,id,fn,stmt,st.
fetch_statement ERTLptr_semantics (prog_var_names … prog) 
    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
               return 〈id,fn,stmt〉 → 
let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn 
                                               (f_regs (pc_block (pc … st)))) in
st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) = 
sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
*)

axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
∀prog.∀ f_lbls,f_regs.∀f_bl_r. 
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀st1,st2.
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
R st1 st2 →
pc_block (pc … st1) = pc_block (pc … st2).

axiom pc_eq_sigma_commute : ∀fix_comp,colour.
∀prog.∀ f_lbls,f_regs.∀f_bl_r. 
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀st1,st2,f,fn.
fetch_internal_function ? (globalenv_noinit … prog)
                (pc_block (pc … st1)) = return 〈f,fn〉 → 
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
R st1 st2 →
(pc … st1) = (pc … st2).

(*
axiom change_pc_sigma_commute : ∀fix_comp,colour.
∀prog.∀ f_lbls,f_regs.∀f_bl_r. 
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀st1,st2.
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
R st1 st2 → 
∀pc1,pc2.pc1 = pc2 → 
R (set_pc … pc1 st1) (set_pc … pc2 st2).

axiom globals_commute : ∀fix_comp,colour.
∀prog.
∀p_out,m,n.
∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
prog_var_names … prog = prog_var_names … p_out.

lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
qed.*)

include "joint/semantics_blocks.ma".
include "ASM/Util.ma".

axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
∀st : state LTL_LIN_state.
hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.

axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
∀f : ident.
∀s : state LTL_LIN_state. 
repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f 
   (move (prog_var_names … prog) localss carry_lives_after dest src) s =
   return write_decision dest (read_arg_decision src s) s.

axiom sigma_beval:
 ertlptr_program → (block → label → list label) → beval → beval.
 

axiom ps_reg_retrieve_hw_reg_retrieve_commute : 
∀fix_comp,colour,prog. 
∀ f_lbls,f_regs.∀f_bl_r. 
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
∀st1 : state_pc ERTL_state.
∀st2 : state_pc LTL_LIN_state.
∀bv.
∀r : register.R st1 st2 → 
lives (inl ? ? r) (livebefore  … fn after (point_of_pc ERTLptr_semantics (pc … st1))) → 
ps_reg_retrieve (regs … st1) r = return bv →
∃bv'.bv = sigma_beval prog f_lbls bv' ∧
 read_arg_decision
  (colouring … (colour (prog_var_names … prog) fn after)
   (inl register Register r))
  st2 = bv'.
                              
axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x → 
set_member A DEC a (set_union … x y).
axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y → 
set_member A DEC a (set_union … x y).
axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x → 
¬set_member A DEC a y → 
set_member A DEC a (set_diff … x y).

lemma all_used_are_live_before :
∀fix_comp. 
∀prog : ertlptr_program.
∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
∀l,stmt.
stmt_at … (joint_if_code … fn) l = return stmt → 
∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) → 
let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in 
eliminable ? (after l) stmt = false → 
lives (inl ? ? r)  (livebefore  … fn after l).
#fix_comp #prog #fn #l *
[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | * 
[ #str
| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
| #a
| * [ #r | #b]
| #i #i_spec #dpl #dph
| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
| #op #a #a'
| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
|
|
| #a #dpl #dph
| #dpl #dph #a
| * [ * [|| #r] | #r #lbl | #r #lbl ]
]
] #nxt| * [ #lbl | | *] |*]
#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta 
whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
normalize nodelta -EQstmt whd in match (statement_semantics ???); 
whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
qed.

axiom bool_of_beval_sigma_commute : 
∀prog.∀f_lbls.∀bv,b.
bool_of_beval (sigma_beval prog f_lbls bv) = return b → 
bool_of_beval bv = return b.

lemma map_eval_add_dummy_variance_id :
∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
qed.

lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
%{(refl …)} %{(refl …)} %
qed.

(* Cut&paste da un altro file con nome split_on_last_append, unificare*) 
lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
whd in ⊢ (??%? → ?); #EQ >EQ %
qed.

lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
 OptPred True (λres.
  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
  (split_on_last … l2).
#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
#hd #tl #IH #l1 whd >split_on_last_append_singl whd
<associative_append @split_on_last_append_singl 
qed.

lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
 #A #a #b #EQ destruct %
qed.

lemma eq_notb_true_to_eq_false:
 ∀b. (¬b) = true → b = false.
* // #abs normalize in abs; destruct
qed.

axiom sigma_fb_state_insensitive_to_dead_reg:
 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
 ∀r: register. ∀before.
  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
  sigma_fb_state prog
   (to_be_cleared_fb before l)
   (set_regs ERTLptr_semantics
    〈reg_store r bv (\fst  (regs ERTLptr_semantics st)),
    \snd  (regs ERTLptr_semantics st)〉 st)
  = sigma_fb_state prog (to_be_cleared_fb before l) st.

axiom sigma_fb_state_insensitive_to_dead_Reg:
 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
 ∀r: Register. ∀before.
  set_member … eq_Register r (\snd  (before l)) = false →
  sigma_fb_state prog
   (to_be_cleared_fb before l)
   (set_regs ERTLptr_semantics
     〈\fst  (regs ERTLptr_semantics st),
      hwreg_store r bv (\snd  (regs ERTLptr_semantics st))〉
      st)
  = sigma_fb_state prog (to_be_cleared_fb before l) st.

axiom sigma_fb_state_insensitive_to_dead_carry:
 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. ∀before.
  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTLptr_semantics bv st) =
   sigma_fb_state prog (to_be_cleared_fb before l) st.

lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
 ** normalize #abs destruct /2/
qed.

lemma eta_set_carry:
 ∀P,st. set_carry P (carry P st) st = st.
#P * //
qed.

lemma set_carry_set_regs_commute:
 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
 #P * //
qed.

lemma eliminable_step_to_eq_livebefore_liveafter:
 ∀prog,stackcost,fn.
 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
 ∀st1: joint_abstract_status p_in.
 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
 ∀liveafter.
 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
  livebefore … fn liveafter pt = liveafter pt.
 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
 whd in match eliminable; normalize nodelta >Helim %
qed.

lemma sigma_fb_state_insensitive_to_eliminable:
 ∀fix_comp: fixpoint_computer.
 ∀prog: ertlptr_program.
 ∀stackcost.
 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
 ∀f,fn.
 ∀after: valuation ?.
 let before ≝ livebefore … fn after in
 ∀st1 : joint_abstract_status p_in.
 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
 ∀Heval_seq_no_pc:
   eval_seq_no_pc ERTLptr_semantics
   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
   (ev_genv
    (mk_prog_params ERTLptr_semantics prog stackcost))
   f stms (st_no_pc … st1)
   =return st1_no_pc.
 ∀Heliminable:
   eliminable_step (globals p_in)
    (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
 sigma_fb_state prog (to_be_cleared_fb before pt) st1_no_pc =
  sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn #after
#st1 #st1' #stms #next #stmt_at #Heval #Helim
lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
#EQ_livebefore_after -next
cases stms in Heval Helim;
try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
try (#arg1 #Heval #Helim) try (#Heval #Helim)
whd in Heval:(??%?);
whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
    try (change with (false=true) in Helim; destruct (Helim))
    [4,8: cases arg1 in Heval Helim; normalize nodelta
      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
        inversion ps_reg_retrieve normalize nodelta
        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
        #bv #EQbv ]
|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
    #vres * #Hvres #X cases (bind_inversion ????? X) -X
    #st1'' * #Hst1''
|9: inversion (opt_to_res ???) in Heval;
    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
    #bv normalize nodelta #EQbv
|10,11: inversion (get_pc_from_label ?????) in Heval;
     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     #bv normalize nodelta #EQbv
|12: lapply Heval -Heval
|14: inversion (acca_retrieve ???) in Heval;
    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
    #v1 * #Hv1
|15: inversion (dph_arg_retrieve ???) in Heval;
    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
    #vres * #Hvres #X cases (bind_inversion ????? X) -X
    #v1 * #Hv2 ]
whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
[1,2,3: 
  >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
  @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta 
    [2: #error #abs destruct (abs) ]
    #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
    whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
      try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
      try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
      try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
      try (destruct (Hvres) @I)
      [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
          cases andb normalize nodelta #Hvres
      |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
          normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
      whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
      @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
   >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
   @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
qed.

axiom to_be_cleared_sb_respects_equal_valuations:
 ∀live,coloured,l1,l2.
  live l1 = live l2 →
   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.

axiom to_be_cleared_fb_respects_equal_valuations:
 ∀live,l1,l2.
  live l1 = live l2 →
   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.

lemma make_ERTLptr_To_LTL_good_state_relation :
∀fix_comp,colour,prog. 
let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
let stacksizes ≝ lookup_stack_cost … m in
∃init_regs : block → list register.
∃f_lbls : block → label → list label.
∃f_regs : block → label → list register.
∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») 
        prog init_regs f_lbls f_regs.
good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
 init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
#fix_comp #colour #prog
cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
%
[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc; 
  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn 
  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
  assumption
| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc; 
  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
   #H cases(state_pc_eq … H) * #_ #_ //
| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
  >EQfn >EQfn normalize nodelta //
| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc; 
  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
  whd in match eval_statement_advance; normalize nodelta 
  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
  #t_fn1 #EQt_fn1 whd normalize nodelta
  letin trans_prog ≝ (b_graph_transform_program ????)
  letin stacksizes ≝ (lookup_stack_cost ?)
  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
  #mid #EQmid
  letin st2_pre_mid_no_pc ≝ 
  (write_decision RegisterA 
          (read_arg_decision 
              (colouring 
                  …
                  (colour (globals prog_pars_in) fn
                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
              (inl register Register a)) st2) st2)
  %{st2_pre_mid_no_pc}
  %
  [1,3: >map_eval_add_dummy_variance_id % 
       [1,3: % 
            [1,3: % 
                 [1,3: @move_spec 
                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 
                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn 
                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 
                     normalize nodelta #EQ cases(state_pc_eq … EQ) * 
                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
                     <(insensitive_to_be_cleared_sb prog … st2)
                     [2,4: @dead_registers_in_dead @acc_is_dead ]
                     whd >point_of_pc_of_point
                     letin after ≝ (analyse_liveness fix_comp … fn)
                     letin before ≝ (livebefore … fn after) 
                     [ cut
                        (before ltrue =
                          before (point_of_pc ERTLptr_semantics (pc … st1)))
                       [ cases daemon (*CSC: Genuine proof obligation! *)
                       | #Hext ]
                     |  cut
                        (before lfalse =
                          before (point_of_pc ERTLptr_semantics (pc … st1)))
                       [ cases daemon (*CSC: Genuine proof obligation! *)
                       | #Hext ]]
                     >(to_be_cleared_sb_respects_equal_valuations …
                        (colour … fn …) … Hext) <EQst1st2
                     >(to_be_cleared_fb_respects_equal_valuations … Hext) %
                 ]
            |*: %
            ]
       |*: %
       ]
  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
      >hw_reg_retrieve_write_decision_hit >m_return_bind
      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … 
                                                        good fn … Rst1st2 … EQbv)
        [2,4: @(all_used_are_live_before … EQstmt)
            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
        change with (prog_var_names … prog) in match (globals ?); >EQbv1 
        >EQbv' in EQbool; #EQbool
        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
        normalize nodelta 
        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %] 
        whd in match goto; normalize nodelta
        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
  ]
| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
  letin p_out ≝ (mk_prog_params LTL_semantics ??)
  letin trans_prog ≝ (b_graph_transform_program ????)
  #st1 #st1' #st2 #f #fn
  #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 
  normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
  #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
  #Heval_seq_no_pc
  whd in match eval_statement_advance; normalize nodelta
  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
  whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
  whd normalize nodelta
  change with p_out in match p_out;
  change with p_in in match p_in;
  change with trans_prog in match trans_prog;
  inversion eliminable_step #Heliminable normalize nodelta %
  [ @([ ])
  | % [%] % [2: % [%] | skip] whd
    cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
    % [2: % [2: % [%] | skip] | skip]
    (* CSC: BEGIN cut&paste from previous case: make lemma? *)
    lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 
    whd in match sigma_sb_state_pc; normalize nodelta >EQfn
    <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 
    normalize nodelta #EQ cases(state_pc_eq … EQ) *
    #EQst1st2 #_ #_
    (* CSC: END *)
    letin before ≝ (livebefore ???)
    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
    whd in match (point_of_succ ???);
    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
      (* Ha funzionato solo a dx, non a sinistra...*)
      normalize nodelta whd in match statement_semantics; normalize nodelta
      >Heliminable
     cases daemon (*CSC: Genuine proof obligation! *)
    | #Hext ]
    >(to_be_cleared_fb_respects_equal_valuations … Hext)
    >(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
    >EQst1st2
    >(to_be_cleared_sb_respects_equal_valuations … Hext) %
|
|
  
  XXXX
  
  *
  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 
      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
      whd in match eval_seq_no_pc; normalize  nodelta
      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
      whd in match eval_statement_advance; normalize nodelta
      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
      whd normalize nodelta whd in match translate_op1;
      normalize nodelta
      change with p_out in match p_out;
      change with p_in in match p_in;
      change with trans_prog in match trans_prog;
      inversion eliminable_step #Heliminable normalize nodelta %
      [ @([ ])
      | % [%] % [2: % [%] | skip] whd
        cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
        % [2: % [2: % [%] | skip] | skip]
        (* CSC: BEGIN cut&paste from previous case: make lemma? *)
        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 
        whd in match sigma_sb_state_pc; normalize nodelta >EQfn
        <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 
        normalize nodelta #EQ cases(state_pc_eq … EQ) *
        #EQst1st2 #_ #_
        (* CSC: END *)
        <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
        change with (set_regs ???) in match (st_no_pc ??);

        
        
        
        
        
        
        
         destruct (EQst1_no_pc)
        
        <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 … 
          (point_of_pc ERTLptr_semantics (pc … st2)))
                     [2,4: @dead_registers_in_dead @acc_is_dead ]
                     assumption
      
      Rst1st2
      
      % [2: % [ % | ] | skip]
qed.


lemma eval_cond_ok :
∀fix_comp,colour.
∀prog.
∀ f_lbls,f_regs.∀f_bl_r. 
∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 
∀st1,st2,st1',f,fn,a,ltrue,lfalse.
let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
R st1 st2 → 
 fetch_statement ERTLptr_semantics …
  (globalenv_noinit ? prog) (pc … st1) =
    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
let stacksizes ≝ lookup_stack_cost … 
                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in  
 eval_state ERTLptr_semantics
   (prog_var_names … ℕ prog) 
   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes)) 
   st1 = return st1' → 
as_costed (ERTLptr_status prog stacksizes) st1' → 
∃ st2'. R st1' st2' ∧
∃taf : trace_any_any_free (LTL_status ? ?)
st2 st2'.
bool_to_Prop (taaf_non_empty … taf).
#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a 
#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
% 
[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
|



whd in match eval_state; normalize nodelta 
>EQfetch >m_return_bind
whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
whd in match eval_statement_advance; normalize nodelta
change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 
[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
| whd in match next; normalize nodelta
] 
whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
cases(b_graph_transform_program_fetch_statement … good … EQfetch)
#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
whd in match translate_step; normalize nodelta *** #blp #blm #bls * 
whd in ⊢ (% → ?); #EQbl
whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 
#seq_pre_l
letin stacksizes ≝ (lookup_stack_cost … 
                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
letin p≝ (mk_prog_params LTL_semantics 
                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) 
                         stacksizes)
cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
           last_pop … st2' = last_pop … st2)
   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ 
>EQ in EQmid ⊢ %; -nxt1 #EQmid
lapply(taaf_to_taa ??? 
           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1 
                                       seq_pre_l res_st2_pre_mid) ?)
[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta 
      whd in match (as_label ??); whd in match (as_pc_of ??); 
      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
      >m_return_bind whd in match point_of_pc; normalize nodelta 
      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta 
      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
#taa_pre_mid whd in ⊢ (% → ?);
cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
                     return st2_cond )
[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
#st2_mid #EQst2_mid 
cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump) 
[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption] 
     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
]
qed.


theorem ERTLptrToLTL_ok :
∀fix_comp : fixpoint_computer.
∀colour : coloured_graph_computer.
∀p_in : ertlptr_program.
let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
(* what should we do with n? *)
let stacksizes ≝ lookup_stack_cost m in
∃[1] R.
  status_simulation
    (joint_status ERTLptr_semantics p_in stacksizes)
    (joint_status LTL_semantics p_out stacksizes)
    R.
#fix_comp #colour #p_in
cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics 
          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
#fregs * #f_lbls * #f_bl_r #good
%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
whd in match status_simulation; normalize nodelta
whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
change with
  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?)  
#EQeval @('bind_inversion EQeval)
** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
cases stmt in EQfetch; -stmt
[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] 
#EQfetch
change with (joint_classify ??) in 
                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
  (* XXX
  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
  *) cases daemon
| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
          normalize nodelta #is_call_st1
          (* XXX
          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
          #call_rel * #taa * #st2' * #sem_rel #eval_rel
          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
          *) cases daemon
| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
          normalize nodelta #n_costed
          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
          normalize nodelta 
          cases (eval_seq_no_call_ok … good … EQfetch EQeval) 
          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf}  
          % [% //] whd >(as_label_ok … good … st3) [%]
          cases daemon (*needs lemma about preservation of fetch_statement *)
|  cases fin_step in EQfetch;
  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
     >EQfetch normalize nodelta
    cases (eval_goto_ok … good  … EQfetch EQeval)
    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
    % [% //] whd >(as_label_ok … good … st3) [%]
    cases daemon (*needs lemma about preservation of fetch_statement *)
  | (*RETURN*) #EQfetch
     whd in match joint_classify; normalize nodelta
    >EQfetch  normalize nodelta
    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
    % [2: assumption] % [2: %] % [2: assumption] % assumption
  | (*TAILCALL*) * 
  ]
]