source: LTS/Traces.ma @ 3554

(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "arithmetics/nat.ma".
include "basics/types.ma".
include "basics/deqsets.ma".
include "../src/ASM/Util.ma".
include "basics/finset.ma".
include "../src/utilities/hide.ma".
include "utils.ma".

(*Label parameters*)

record label_params : Type[1] ≝ 
{ label_type :> monoid
; abelian_magg : is_abelian … label_type
; succ_label : label_type → label_type
; po_label : partial_order label_type
; no_maps_in_id : ∀x.succ_label x ≠ x
; le_lab_ok : ∀x,y.po_label … (op … x (succ_label y)) (succ_label (op … x y))
; magg_def : ∀x,y.po_label … x (op … x y)
; monotonic_magg : ∀x,y,z.po_label … x y → po_label … (op … x z) (op … y z)
}.

notation "hvbox(a break ⊑ ^ {b} break term 46 c)" 
  non associative with precedence 45
for @{ 'lab_leq $a $b $c}.

interpretation "label 'less or equal to'" 'lab_leq x y z = (po_rel ? (po_label y) x z).

lemma max_1 : ∀p : label_params.∀n,m,k : p.k ⊑^{p} m → k ⊑^{p} op … p m n.
#p #m #n #k #H /2 by magg_def, trans_po_rel/ 
qed.

lemma max_2 : ∀p : label_params.∀n,m,k: p.k ⊑^{p} n → k ⊑^{p} op … p m n.
#p #m #n #k #H >(abelian_magg … p) /2 by magg_def, trans_po_rel/
qed.

lemma lab_po_rel_succ : ∀p : label_params.∀x : p.x ⊑^{p} succ_label … x.
#p #x @(trans_po_rel … (op … p … x (succ_label … (e … p)))) [ @(magg_def … p)] 
@(trans_po_rel … (le_lab_ok … p …)) >neutral_r //
qed.

(*flat labels*)

definition deqnat_monoid ≝ mk_monoid DeqNat max O ???.
@hide_prf // [* //] #x #y #z normalize inversion(leb x y) normalize nodelta
#leb_xy
[ inversion(leb y z) normalize nodelta #leb_yz
  [ >(le_to_leb_true …) // @(transitive_le … y) @leb_true_to_le //
  | >leb_xy %
  ]
| inversion(leb x z) normalize nodelta #leb_xz
  [ >(le_to_leb_true … y z) normalize nodelta [>leb_xz %] @(transitive_le … x) /2 by leb_true_to_le/
    lapply(not_le_to_lt … (leb_false_to_not_le … leb_xy)) #H1 /2/
  | cases(leb y z) normalize nodelta [ >leb_xz | >leb_xy ] //
  ]
]
qed.

definition part_order_nat ≝ mk_partial_order ℕ le ???.
/2 by le_to_le_to_eq, transitive_le, le_n/
qed.

definition flat_labels ≝ mk_label_params deqnat_monoid ? S part_order_nat ????.
@hide_prf
[ normalize #x #y @leb_elim normalize nodelta
  [2: #H >le_to_leb_true //  lapply(not_le_to_lt …  H) #H1 /2/
  | * -y [ >le_to_leb_true //] #y #H >not_le_to_leb_false // @lt_to_not_le /2 by le_to_lt_to_lt/
  ]
| normalize #x /2 by sym_not_eq/
| normalize #x #y @(leb_elim … x y) normalize nodelta
  [ #H >le_to_leb_true /3 by le_to_lt_to_lt, monotonic_pred, le_n/
  | #H @leb_elim normalize nodelta [ #H1 @le_S_S lapply(not_le_to_lt …  H) #H3 /2/ ]
    #_ /2/
  ]
| normalize #x #y @leb_elim //
| normalize #x #y #z #H @(leb_elim … y z) 
  [ #H1 >(le_to_leb_true … (transitive_le … H H1)) //
  | #H1 normalize cases(leb ??) normalize /3 by not_le_to_lt, lt_to_le/
  ]
]
qed.

(*LABELS*)

inductive FunctionName : Type[0] ≝
 | a_function_id : ℕ → FunctionName.
 
inductive CallCostLabel (p : label_params) : Type[0] ≝ 
 | a_call_label : p → CallCostLabel p.
 
inductive ReturnPostCostLabel (p : label_params) : Type[0] ≝ 
 | a_return_cost_label : p → ReturnPostCostLabel p.
 
inductive NonFunctionalLabel (p : label_params) : Type[0] ≝ 
 | a_non_functional_label : p → NonFunctionalLabel p.
 
inductive CostLabel (p : label_params) : Type[0] ≝ 
 | a_call : CallCostLabel p → CostLabel p
 | a_return_post : ReturnPostCostLabel p → CostLabel p
 | a_non_functional_label : NonFunctionalLabel p → CostLabel p.

coercion a_call.
coercion a_return_post.
coercion a_non_functional_label.

definition eq_nf_label : ∀p.NonFunctionalLabel p → NonFunctionalLabel p → bool ≝
λp,x,y.match x with [ a_non_functional_label n ⇒ 
                    match y with [a_non_functional_label m ⇒ eqb … n m ] ].

lemma eq_fn_label_elim : ∀P : bool → Prop.∀p.∀l1,l2 : NonFunctionalLabel p.
(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label … l1 l2).
#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H 
[ @H1 >(\P H) %
| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
]
qed. 
 
definition DEQNonFunctionalLabel ≝ λp.mk_DeqSet (NonFunctionalLabel p) (eq_nf_label p) ?.
#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 
assumption 
qed.

unification hint  0 ≔ p; 
    X ≟ (DEQNonFunctionalLabel p)
(* ---------------------------------------- *) ⊢ 
    (NonFunctionalLabel p) ≡ carr X.

unification hint  0 ≔ p,p1,p2; 
    X ≟ (DEQNonFunctionalLabel p)
(* ---------------------------------------- *) ⊢ 
    eq_nf_label p p1 p2 ≡ eqb X p1 p2.

definition eq_function_name : FunctionName → FunctionName → bool ≝ 
λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].

lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.

definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 
assumption 
qed.

unification hint  0 ≔ ; 
    X ≟ DEQFunctionName
(* ---------------------------------------- *) ⊢ 
    FunctionName ≡ carr X.

unification hint  0 ≔ p1,p2; 
    X ≟ DEQFunctionName
(* ---------------------------------------- *) ⊢ 
    eq_function_name p1 p2 ≡ eqb X p1 p2.

definition eq_return_cost_lab :∀p.ReturnPostCostLabel p → ReturnPostCostLabel p → bool ≝ 
λp,c1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb … n m]].

lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) → 
(c1 ≠ c2 → P false) → P (eq_return_cost_lab p c1 c2).
#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H 
[ @H1 >(\P H) %
| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
]
qed.

definition DEQReturnPostCostLabel ≝ λp.mk_DeqSet (ReturnPostCostLabel p) (eq_return_cost_lab …) ?.
#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 
assumption 
qed.

unification hint  0 ≔ p ; 
    X ≟ (DEQReturnPostCostLabel p)
(* ---------------------------------------- *) ⊢ 
    (ReturnPostCostLabel p) ≡ carr X.

unification hint  0 ≔ p,p1,p2; 
    X ≟ (DEQReturnPostCostLabel p)
(* ---------------------------------------- *) ⊢ 
    eq_return_cost_lab p p1 p2 ≡ eqb X p1 p2.

definition eq_call_cost_lab : ∀p.(CallCostLabel p) → (CallCostLabel p) → bool ≝ 
λp,c1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb … x y ]].

lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) → 
(c1 ≠ c2 → P false) → P (eq_call_cost_lab p c1 c2).
#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H 
[ @H1 >(\P H) %
| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
]
qed. 

definition DEQCallCostLabel ≝ λp.mk_DeqSet (CallCostLabel p) (eq_call_cost_lab p) ?.
#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 
assumption 
qed.

unification hint  0 ≔ p; 
    X ≟ (DEQCallCostLabel p)
(* ---------------------------------------- *) ⊢ 
    (CallCostLabel p) ≡ carr X.

unification hint  0 ≔ p,p1,p2; 
    X ≟ (DEQCallCostLabel p)
(* ---------------------------------------- *) ⊢ 
    eq_call_cost_lab p p1 p2 ≡ eqb X p1 p2.

definition eq_costlabel :∀p. (CostLabel p) → (CostLabel p) → bool ≝ 
λp,c1.match c1 with
  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
  | a_return_post x1 ⇒ 
      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
  | a_non_functional_label x1 ⇒ 
     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
  ].

lemma eq_costlabel_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) → 
(c1 ≠ c2 → P false) → P (eq_costlabel p c1 c2).
#P #p * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
try (@H2 % #EQ destruct) 
[ change with (eq_call_cost_lab ???) in ⊢ (?%); @eq_call_cost_lab_elim
  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
| change with (eq_return_cost_lab ???) in ⊢ (?%);
   @eq_return_cost_lab_elim
   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
| change with (eq_nf_label ???) in ⊢ (?%); @eq_fn_label_elim
  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
]
qed.


definition DEQCostLabel ≝ λp.mk_DeqSet (CostLabel p) (eq_costlabel p) ?.
#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 
assumption 
qed.

unification hint  0 ≔ p ; 
    X ≟ (DEQCostLabel p)
(* ---------------------------------------- *) ⊢ 
    (CostLabel p) ≡ carr X.

unification hint  0 ≔ p,p1,p2; 
    X ≟ (DEQCostLabel p)
(* ---------------------------------------- *) ⊢ 
    eq_costlabel p p1 p2 ≡ eqb X p1 p2.

inductive ActionLabel (p : label_params) : Type[0] ≝ 
 | call_act : FunctionName → CallCostLabel p → ActionLabel p
 | ret_act : option(ReturnPostCostLabel p) → ActionLabel p
 | cost_act : option (NonFunctionalLabel p) → ActionLabel p.
 
definition eq_ActionLabel : ∀p.ActionLabel p → ActionLabel p → bool ≝ 
λp,c1,c2.
match c1 with
[ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false]
| ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
                                                      | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
                                                      ]
                            | _ ⇒ false
                            ]
| cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
                                                        | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
                                                        ]
                             | _ ⇒ false
                             ]
].

definition is_cost_label : ∀p.ActionLabel p → Prop ≝ 
λp,act.match act with [ cost_act nf ⇒ True | _ ⇒ False ].

definition is_non_silent_cost_act : ∀p.ActionLabel p → Prop ≝ 
λp,act. ∃l. act = cost_act … (Some ? l).

definition is_cost_act : ∀p.ActionLabel p → Prop ≝ 
λp,act.∃l.act = cost_act … l.

definition is_call_act : ∀p.ActionLabel p → Prop ≝ 
λp,act.∃f,l.act = call_act … f l.

definition is_labelled_ret_act : ∀p.(ActionLabel p) → Prop ≝ 
λp,act.∃l.act = ret_act … (Some ? l).

definition is_unlabelled_ret_act : ∀p.ActionLabel p → Prop ≝ 
λp,act.act = ret_act … (None ?).

definition is_costlabelled_act : ∀p.ActionLabel p → Prop ≝ 
λp,act.match act with [ call_act _ _ ⇒ True
                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
                    ].
                    
definition is_ret_call_act : ∀p.ActionLabel p → Prop ≝ 
λp,a.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].

definition is_silent_cost_act_b : ∀p.ActionLabel p → bool ≝ 
λp,act. match act with
 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
                    
lemma is_costlabelled_act_elim : ∀p. 
∀P : ActionLabel p → Prop.
(∀l. is_costlabelled_act p l → P l) → 
(∀l. ¬is_costlabelled_act p l → P l) → 
∀l.P l. #p
#P #H1 #H2 * /2/
[ * /2/ @H2 % *] * /2/ @H2 %*
qed.

lemma eq_a_call_label : ∀p.
∀c1,c2.c1 == c2 → a_call p c1 == a_call p c2.
#p #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
#EQ destruct >(\b (refl …)) @I
qed.

lemma eq_a_non_functional_label : ∀p.
∀c1,c2.c1 == c2 → a_non_functional_label p c1 == a_non_functional_label p c2.
#p #c1 #c2 #EQ cases(eqb_true (DEQNonFunctionalLabel ?) c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
#EQ destruct >(\b (refl …)) @I
qed.

(* TOOLS FOR FRESHING LABELS *)

definition fresh_nf_label : ∀p : label_params.p → NonFunctionalLabel p × p ≝ 
λp,x.〈a_non_functional_label … (succ_label … p x),(succ_label … p x)〉.

definition fresh_cc_labe : ∀p : label_params.p → CallCostLabel p × p ≝ 
λp,x.〈a_call_label … (succ_label … p x),(succ_label … p x)〉.

definition fresh_rc_label : ∀p : label_params.p → ReturnPostCostLabel p × p ≝ 
λp,x.〈a_return_cost_label … (succ_label … p x),(succ_label … p x)〉.


(*ABSTRACT STATUS*)

inductive status_class : Type[0] ≝ 
 | cl_jump : status_class
 | cl_io : status_class
 | cl_other : status_class.
 
record abstract_status (p : label_params) : Type[2] ≝ 
 { as_status :> Type[0]
 ; as_execute : (ActionLabel p) → relation as_status
 ; as_syntactical_succ : relation as_status
 ; as_classify : as_status → status_class
 ; is_call_post_label : as_status → bool
 ; as_initial : as_status → bool
 ; as_final : as_status → bool
 ; jump_emits : ∀s1,s2,l.
      as_classify … s1 = cl_jump → 
      as_execute l s1 s2 → is_non_silent_cost_act … l
 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io → 
      as_execute l s1 s2 → is_non_silent_cost_act … l
 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io → 
     as_execute l s1 s2 → is_non_silent_cost_act … l
 }.

(* RAW TRACES *)

inductive raw_trace (p : label_params) (S : abstract_status p) : S → S → Type[0] ≝ 
  | t_base : ∀st : S.raw_trace … S st st
  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel p.
             as_execute … S l st1 st2 → raw_trace … S st2 st3 → 
             raw_trace … S st1 st3.
             

let rec append_on_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S) (st3 : S)
(t1 : raw_trace … S st1 st2) on t1 : raw_trace …  S st2 st3 → raw_trace … S st1 st3 ≝ 
match t1
return λst1,st2,tr.raw_trace … S st2 st3 → raw_trace … S st1 st3
with
[ t_base st ⇒ λt2.t2
| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
].

interpretation "trace_append" 'append t1 t2 = (append_on_trace ????? t1 t2).

let rec len (p : label_params) (s : abstract_status p) (st1 : s) (st2 : s) (t : raw_trace p s st1 st2)
on t : ℕ ≝ 
match t with
[ t_base s ⇒ O
| t_ind s1 s2 s3 l prf lt ⇒ S (len … lt)
].

lemma len_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
len  ???? (t1 @ t2)  = (len  ????  t1) + (len  ???? t2).
#p #S #st1 #st2 #st3 #t1 elim t1 normalize //
qed.

lemma append_nil_is_nil : ∀p. ∀S : abstract_status p.
∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
#p #S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
[ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
#s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
qed.

lemma append_associative : ∀p.∀S,st1,st2,st3,st4.
∀t1 : raw_trace p S st1 st2.∀t2 : raw_trace … S st2 st3.
∀t3 : raw_trace … S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
#p #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
qed.

definition trace_prefix: ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st1 st2 → 
raw_trace … st1 st3 → Prop≝ 
λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.

definition trace_suffix : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st2 st3 → 
raw_trace … st1 st3 → Prop≝ 
λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.

definition actionlabel_to_costlabel ≝ λp.
λl : ActionLabel p.match l with
    [ call_act f c ⇒ [ c ]
    | ret_act x ⇒ match x with 
                  [ Some c ⇒ [ a_return_post … c ]
                  | None ⇒ []
                  ]
    | cost_act x ⇒ match x with 
                  [ Some c ⇒ [ a_non_functional_label  … c ]
                  | None ⇒ [] 
                  ]
   ].

let rec get_costlabels_of_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S)
(t : raw_trace p S st1 st2) on t : list (CostLabel p) ≝ 
match t with
[ t_base st ⇒ [ ]
| t_ind st1' st2' st3' l prf t' ⇒ 
    let tl ≝ get_costlabels_of_trace … t' in
    actionlabel_to_costlabel … l  @ tl
].

lemma get_cost_label_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
get_costlabels_of_trace … (t1 @ t2) = 
 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
#p #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
qed.

lemma append_tind_commute : ∀p.∀S : abstract_status p.∀st1,st2,st3,st4 : S.∀l.
    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace p S st2 st3.
    ∀t2 : raw_trace p S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
#p #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.

lemma get_costlabelled_is_costlabelled :
∀p.∀S : abstract_status p.∀s1,s2,s3 : S. ∀l.
∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
is_costlabelled_act p l → 
|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
#p #S #s1 #s2 #s3 * normalize 
  [ /2 by monotonic_pred/
  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
  ]
qed.

(*SILENT TRACES*)

inductive pre_silent_trace (p : label_params) (S : abstract_status p) :
∀st1,st2 : S.raw_trace p S st1 st2 → Prop ≝ 
| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base p S st)
| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute p S (cost_act  … (None ?)) st1 st2.
                ∀tl : raw_trace p S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl → 
                pre_silent_trace … (t_ind … prf … tl).
                
definition is_trace_non_empty : ∀p.∀S : abstract_status p.∀st1,st2.
raw_trace p S st1 st2 → bool ≝ 
λp,S,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].

definition silent_trace : ∀p.∀S:abstract_status p.∀s1,s2 : S.
raw_trace p S s1 s2 → Prop ≝ λp,S,s1,s2,t.pre_silent_trace … t ∨ 
¬ (bool_to_Prop (is_trace_non_empty … t)).

lemma pre_silent_io : ∀p.∀S : abstract_status p.
∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → 
as_classify … s2 ≠ cl_io.
#p #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
#st1 #st2 #st3 #l #prf #tl #IH #H inversion H // 
#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
#EQ destruct #_ @IH assumption
qed.

lemma append_silent : ∀p.∀S : abstract_status p.
∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
∀t2 : raw_trace … s2 s3.silent_trace … t1 → 
silent_trace … t2 → 
silent_trace … (t1 @ t2).
#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
#st1 #st2 #st3 #l #prf #tl #IH #t2 *
[2: * #H cases(H I) ] #H inversion H in ⊢ ?;
[ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
#st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
#Ht2 % %2 // cases(IH … Ht2) /2/ 
inversion(tl' @ t2)
[2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
#st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
qed.

lemma silent_append_l2 : ∀p.∀S : abstract_status p.
∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
silent_trace … (t1 @ t2) → silent_trace … t2.
#p #S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
#H @IH % inversion H in ⊢ ?;
[ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
]
qed.

lemma silent_append_l1 : ∀p.∀S : abstract_status p.
∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
silent_trace … (t1 @ t2) → silent_trace … t1.
#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
[ #st #t2 #_ %2 % *]
#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
% inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
#z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
%2 // cases(IH t2 …) /2/ inversion tl
[2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
#st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
[ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
| #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
]
qed.

lemma get_cost_label_silent_is_empty : ∀p.∀S : abstract_status p.
∀st1,st2.∀t : raw_trace p S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
#p #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
#H inversion H
[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
destruct #_ @IH % assumption
qed.

lemma get_cost_label_invariant_for_append_silent_trace_l :∀p.∀S : abstract_status p.
∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
silent_trace … t1 → 
get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
#p #S #st1 #st2 #st3 #t1 elim t1
[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 * 
[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
#_ whd in ⊢ (??%?); >IH [%] %1 assumption
qed.

lemma silent_suffix_cancellable : ∀p.∀S : abstract_status p.
∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
∀t2 : raw_trace … s3 s4.
∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
∀t2' : raw_trace … s3' s4.
is_costlabelled_act … l → is_costlabelled_act … l' → 
silent_trace … t2 → silent_trace … t2' → 
t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') → 
s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
#p #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
[ normalize #st * normalize 
  [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
  | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
    ]
  ]
]
#st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
[ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
    ]
| #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
]
qed.

(*PRE-MEASURABLE TRACES*)

inductive pre_measurable_trace (p : label_params) (S : abstract_status p) :
∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝ 
 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base … st)
 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel p.
                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
                      as_classify … st1 ≠ cl_io → is_cost_act … l → pre_measurable_trace … tl → 
                      pre_measurable_trace … (t_ind … prf … tl)
 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel p.
                      as_classify … st1 ≠ cl_io → 
                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
                      is_labelled_ret_act … l → pre_measurable_trace … tl → 
                      pre_measurable_trace … (t_ind … prf … tl)
 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel p.
                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
                      as_classify … st1 ≠ cl_io → is_call_act … l → is_call_post_label … st1 → 
                      pre_measurable_trace … tl → 
                      pre_measurable_trace … (t_ind … prf … tl)
 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
                      ∀prf : as_execute … l1 st1 st2.∀t1 : raw_trace … st2 st3.
                      ∀t2 : raw_trace … st4 st5.∀prf' : as_execute … l2 st3 st4.
                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 
                      →  is_call_act … l1 → ¬ is_call_post_label … st1 → 
                      pre_measurable_trace … t1 → pre_measurable_trace … t2 → 
                      as_syntactical_succ … st1 st4 → 
                      is_unlabelled_ret_act … l2 → 
                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).

lemma append_premeasurable : ∀p.∀S : abstract_status p.
∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
pre_measurable_trace … t1 → pre_measurable_trace … t2 → 
pre_measurable_trace … (t1 @ t2).
#p #S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
  %2 // @IH //
| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
  normalize >append_associative in ⊢ (?????(????????%)); %5 // @IH2 //
]
qed.

lemma append_premeasurable_silent : ∀p.∀S : abstract_status p.
∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
pre_measurable_trace … t → silent_trace … t' →  
pre_measurable_trace … (t' @ t).
#p #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
[ #st #t #Hpre #_ whd in ⊢ (?????%); assumption]
#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 
destruct #_ whd in ⊢ (?????%); %2 
[ assumption
| %{(None ?)} %
| @IH try assumption
]
% assumption
qed.

lemma pre_silent_is_premeasurable : ∀p.∀S : abstract_status p.
∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_silent_trace … t 
→ pre_measurable_trace … t.
#p #S #st1 #st2 #t elim t 
[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
@IH assumption
qed.

lemma append_silent_premeasurable : ∀p.∀S : abstract_status p.
∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
pre_measurable_trace … t' → silent_trace … t →
pre_measurable_trace … (t' @ t).
#p #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11 
  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_ 
  %1 assumption 
|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct 
  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
  try ( %{x} %) try @IH try assumption % ]
#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
#r #pre_r normalize
>append_tind_commute >append_tind_commute >append_associative 
<append_tind_commute in ⊢ (?????(???????%)); %5
try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
qed.

lemma head_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p.
∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → 
as_classify … st1 ≠ cl_io. #p
#S #st1 #st2 #t #H inversion H //
qed.

lemma get_costlabels_of_trace_empty : ∀p.∀S : abstract_status p.∀s1,s2 : S.∀t : raw_trace … s1 s2.
get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
#p #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 
| #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
  #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
  destruct
]
whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
#prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl; 
[2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
#st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
qed.

(*NO-IO TRACES*)

inductive no_io_trace (p : label_params) (S : abstract_status p) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝ 
  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace … S … (t_base … st)
| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io → 
                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).

lemma no_io_append : ∀p.∀S : abstract_status p.
∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
∀t2 : raw_trace … st2 st3.
no_io_trace … t1 → no_io_trace … t2 → 
no_io_trace … (t1 @ t2).
#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1
[ #st #st3 #t2 #_ //]
#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
#H3 %2 // @IH //
qed.

lemma pre_measurable_no_io : ∀p.∀S : abstract_status p.
∀st1,st2 : S. ∀t : raw_trace … st1 st2.
pre_measurable_trace … t →
no_io_trace … t.
#p #S #st1 #st2 #t #H elim H /2/ -st1-st2
#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
qed.

lemma head_of_no_io_is_no_io : ∀p.∀S : abstract_status p.
∀st1,st2 : S. ∀t : raw_trace … st1 st2.
no_io_trace … t → as_classify … st1 ≠ cl_io.
#p #S #st1 #st2 #t #H elim H //
qed.


lemma no_io_append_l1 : ∀p.∀S : abstract_status p.
∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 
no_io_trace … t1.
#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
%2 // @IH //
qed.

lemma no_io_append_l2 : ∀p.∀S : abstract_status p.
∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 
no_io_trace … t2.
#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
qed.

(*MEASURABLE TRACES*)

definition measurable : ∀p.
 ∀S: abstract_status p. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
λp,S,si,s1,s3,sn,t.
 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
 ∃l1,l2,prf1,prf2.
 pre_measurable_trace p … t12 ∧ 
  t = ti0 @  t_ind … s0 s1 sn l1 prf1 … (t12 @ (t_ind … s2 s3 sn l2 prf2 … t3n))
 ∧ is_costlabelled_act … l1 ∧ is_costlabelled_act … l2 ∧ (is_call_act … l2 → bool_to_Prop (is_call_post_label … s2)) 
 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act … l1 → bool_to_Prop (is_call_post_label … s0)).

 
definition measurable_prefix ≝  λp.
λS : abstract_status p.
λs1,s4 :S.
λt : raw_trace … s1 s4.
∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
∃l.∃prf : as_execute … l s2 s3.
∃t34 : raw_trace … s3 s4.
silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act … l.

lemma measurable_prefix_of_premeasurable : 
∀p.
∀S : abstract_status p.
∀s1,s4 : S.
∀t : raw_trace … s1 s4.
pre_measurable_trace … t → 
get_costlabels_of_trace … t ≠ nil ? → 
measurable_prefix … t.
#p #S #s1 #s4 #t elim t
[ #st #_ * #H @⊥ @H %]
#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l 
[ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
  % // % // %2 normalize % *]
#l #Hl #prf #t' #IH #H inversion H
[ #st #H1 #H2 #H3 #H4 #H5 destruct
| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
  cases l2 in Hl Hl2 prf2;
  [ #f #c #_ * #z #EQ destruct
  | * [|#lbl] #_ * #z #EQ destruct
  | * [|#lbl * #H cases(H I)]
  ]
| #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
  cases l2 in Hl Hl2 prf2;
  [ #f #c #_ * #z #EQ destruct
  | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
  | #lbl #_ * #z #EQ destruct
  ]
| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
  cases l2 in Hl Hl2 prf2;
  [ #f #c * #H @⊥ @H %
  | #lbl1 #_ * #z * #z1 #EQ destruct
  | #lbl #_ * #z * #z1 #EQ destruct
  ]
| #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
  #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
  cases l2 in Hl Hl2 prf2;
  [ #f #c * #H @⊥ @H %
  | #lbl1 #_ * #z * #z1 #EQ destruct
  | #lbl #_ * #z * #z1 #EQ destruct
  ]
]
#_ #_ #prf #H1 cases(IH pre_tl ?)
[2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
#s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
%{l1} %{prf1} %{t34} % // %
[ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
  #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
| >H3 //
]
qed.

definition measurable_suffix ≝
λp. λS : abstract_status p.λs1,s1' : S.λt : raw_trace … s1 s1'.
∃s1_em : S.
∃t_pre_em : raw_trace … s1 s1_em.
∃s1_postem : S.
     ∃t_post_em : raw_trace … s1_postem s1'.
     silent_trace … S ?? t_post_em ∧ 
     ∃l_em : ActionLabel p.
     ∃ex_em : as_execute … l_em s1_em s1_postem.
     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
     (is_call_act … l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
     is_costlabelled_act … l_em.
     

lemma measurable_suffix_tind : ∀p.∀S : abstract_status p.
∀s1,s2,s3 : S.∀l : ActionLabel p.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
measurable_suffix … (t_ind … prf t) → (is_costlabelled_act … l ∧ silent_trace … t) ∨ measurable_suffix … t.
#p #S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
 inversion t_pre in ⊢ ?; 
 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  #_ /4 by or_introl, conj/
 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
   lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
   [ #H38 #H39 #H40 #H41 destruct
   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
   ]
 normalize in e0; destruct
]
]
#s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
[ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
| #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
  #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
  >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
]
qed.

lemma measurable_suffix_append : ∀p.∀S : abstract_status p.
∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
#p #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
qed.

lemma measurable_suffix_append_l1 : ∀p.∀S : abstract_status p.
∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
]
#st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
[ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
  * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
  #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
  %{l_em} %{ex_em} /4 by refl, conj/
| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
  change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append @(IH t2) //
  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
]
qed.

lemma measurable_suffix_append_case : ∀p.∀S : abstract_status p.
∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
[ #st #t2 #H %2 assumption]
#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
cases(measurable_suffix_tind … Hsuff)
[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ??????? tl) @ t2) in Hsuff : (?????%);
 @(measurable_suffix_append_l1 … Hsuff) /2/
| #H cases(IH … H)
  [ * #H1 #H2 %% // change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append //
  | /2/
  ]
]
qed.

lemma measurable_is_measurable_suffix : ∀p.∀S : abstract_status p.
∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
#p #S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
#EQ destruct /11 width=20 by conj,ex_intro/
qed.

lemma prefix_of_measurable_suffix_is_premeasurable : ∀p.∀S : abstract_status p.
∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act … l →
silent_trace … t2 → (is_call_act … l → bool_to_Prop(is_call_post_label … s2)) → 
pre_measurable_trace … t1.
#p #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
lapply s3 -s3 elim H -t -s1 -s4
[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?; 
  [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
  | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
    normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
  ]
| #st1 #st2 #st3 #lbl #prf #tl #Hclass **
  [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
      destruct *
    | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); 
      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
    ]
  | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
      destruct #_ #_ #_ % //
    | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 
      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
   ]
 ]
| #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
  #t1 #t2 inversion t2 in ⊢ ?;
  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    destruct #_ #_ #_ % //
  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 
      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
  ]
| #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
  #t1 #t2 inversion t2 in ⊢ ?;
  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    destruct #_ #_ #_ % //
  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 
      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
  ]
| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
  #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
  #t3 #t4 inversion t4 in ⊢ ?;
  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    destruct #_ #_ #_ % // 
  | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ 
    lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
    cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
    [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
    #Hmeas cases(measurable_suffix_append_case … Hmeas)
    [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
      [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
      | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
      ]
    | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
      * #l_em * #ex_em ** #EQ destruct #H1 #H2
      change with (t_ind … (t_base …) @ ?) in match (t_ind ????????) in e0;
      <append_associative in e0; <append_associative #e0
      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct 
      >append_associative %5 /2/ [ %{f} %{c} //] normalize
      @(IH2 … (refl …)) /2/
     ]
   ]
 ]
qed.

(*

lemma measurable_suffix_is_measurable:
∀S : abstract_status.
∀s1,s4 : S.
∀t : raw_trace … s1 s4.
pre_measurable_trace … t → 
2 ≤ |get_costlabels_of_trace … t | → 
measurable_suffix … t → ∃s1,s3.
measurable … s1 … s3 … t.
#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
>(get_cost_label_silent_is_empty … sil_tpost) #CARD
cases(measurable_prefix_of_premeasurable … t_pre)
[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct] 
|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
  /20 width=20 by conj,ex_intro/
]
qed.*)