Theory CSP_F_failures

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_failures
imports CSP_F_semantics
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005 (modified)    |
            |                 August 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_failures = CSP_F_semantics:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*********************************************************
                        setF
 *********************************************************)

(*--------------------------------*
 |             STOP               |
 *--------------------------------*)

(*** STOP_setF ***)

lemma STOP_setF: "{f. EX X. f = (<>, X)} : setF"
by (simp add: setF_def HC_F2_def)

(*** STOP ***)

lemma in_failures_STOP : "(f :f failures(STOP)) = (EX X. f = (<>, X))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF STOP_setF)

(*--------------------------------*
 |             SKIP               |
 *--------------------------------*)

(*** SKIP_setF ***)

lemma SKIP_setF: "{f. (EX X. f = (<>, X) & X <= Evset) |
                      (EX X. f = (<Tick>, X)) } : setF"
by (auto simp add: setF_def HC_F2_def)

(*** SKIP ***)

lemma in_failures_SKIP :
  "(f :f failures(SKIP)) = ((EX X. f = (<>, X) & X <= Evset) |
                            (EX X. f = (<Tick>, X)))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF SKIP_setF)

(*--------------------------------*
 |              DIV               |
 *--------------------------------*)

(*** DIV ***)

lemma in_failures_DIV : "(f ~:f failures(DIV))"
by (simp add: failures_def)

(*--------------------------------*
 |          Act_prefix            |
 *--------------------------------*)

(*** Act_prefix_setF ***)

lemma Act_prefix_setF: 
  "{f. (EX X.   f = (<>,X) & Ev a ~: X) |
       (EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f F) } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule memF_F2, simp_all)
done

(*** Act_prefix ***)

lemma in_failures_Act_prefix: 
  "(f :f failures(a -> P)) 
    = ((EX X.   f = (<>,X) & Ev a ~: X) |
       (EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f failures(P)))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF Act_prefix_setF)

(*--------------------------------*
 |        Ext_pre_choice          |
 *--------------------------------*)

(*** Ext_pre_choice_setF ***)

lemma Ext_pre_choice_setF: 
  "{f. (EX Y. f = (<>,Y) & Ev`X Int Y = {}) |
       (EX a s Y. f = (<Ev a> ^^ s, Y) & (s,Y) :f Ff a & a : X) } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule memF_F2, simp_all)
done

(*** Ext_pre_choice ***)

lemma in_failures_Ext_pre_choice: 
  "(f :f failures(? :X -> Pf)) = 
   ((EX Y.     f = (<>,Y) & Ev`X Int Y = {}) |
    (EX a s Y. f = (<Ev a> ^^ s, Y) & (s,Y) :f failures(Pf a) & a : X))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF Ext_pre_choice_setF)

(*--------------------------------*
 |          Ext_choice            |
 *--------------------------------*)

(*** Ext_choice_setF ***)

lemma Ext_choice_setF: 
  "{f. (EX X. f = (<>, X)) & f :f F & f :f E |
              (EX s. (EX X. f = (s, X)) & (f :f F | f :f E) & s ~= <>) |
              (EX X. f = (<>, X) &
                     (<Tick> :t T | <Tick> :t S) & X <= Evset)} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE)
apply (simp_all)

(* part1 *)
apply (rule disjI1)
apply (rule conjI)
apply (rule memF_F2, simp_all)
apply (rule memF_F2, simp_all)

(* part2 *)
apply (rule disjI1)
apply (rule memF_F2, simp_all)
apply (rule disjI2)
apply (rule memF_F2, simp_all)

(* part3 *)
apply (auto)
done

(*** Ext_choice ***)

lemma in_failures_Ext_choice: 
  "(f :f failures(P [+] Q)) =
    ((EX X. f = (<>, X)) & f :f failures P & f :f failures Q |
     (EX s. (EX X. f = (s, X)) &
            (f :f failures P | f :f failures Q) & s ~= <>) |
     (EX X. f = (<>, X) &
            (<Tick> :t traces P | <Tick> :t traces Q) & X <= Evset))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Ext_choice_setF)

(*--------------------------------*
 |          Int_choice            |
 *--------------------------------*)

(*** Int_choice ***)

lemma in_failures_Int_choice: 
  "(f :f failures(P |~| Q)) = (f :f failures(P) | f :f failures(Q))"
by (simp add: failures_def)

(*--------------------------------*
 |        Rep_int_choice          |
 *--------------------------------*)

(*** Rep_int_choice_setF ***)

lemma Rep_int_choice_setF: 
  "{f. EX a:X. f :f Ff a} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE bexE)
apply (rule_tac x="a" in bexI)
apply (rule memF_F2, simp_all)
done

(*** Union_proc ***)

lemma in_failures_Union_proc:
   "f :f {f. EX a:X. f :f Ff a}f = (EX a:X. f :f Ff a)"
by (simp add: CollectF_open_memF Rep_int_choice_setF)

lemma in_failures_UNIV_Union_proc:
   "f :f {f. EX a. f :f Ff a}f = (EX a. f :f Ff a)"
apply (insert in_failures_Union_proc[of f UNIV Ff])
by (simp)

(*** Rep_int_choice ***)

lemma in_failures_Rep_int_choice_var: 
  "(f :f failures(!! :C .. Pf)) = (EX c:C. f :f failures(Pf c))"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemma in_failures_Rep_int_choice_fun: 
  "inj g ==> (f :f failures(!!<g> :X .. Pf)) = (EX a:X. f :f failures(Pf a))"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemma in_failures_Rep_int_choice_com: 
  "(f :f failures(! :X .. Pf)) = (EX a:X. f :f failures(Pf a))"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemmas in_failures_Rep_int_choice = in_failures_Rep_int_choice_var
                                    in_failures_Rep_int_choice_fun
                                    in_failures_Rep_int_choice_com

(*--------------------------------*
 |               IF               |
 *--------------------------------*)

(*** IF ***)

lemma in_failures_IF: 
  "(f :f failures(IF b THEN P ELSE Q))
 = (if b then f :f failures(P) else f :f failures(Q))"
by (simp add: failures_def)

(*--------------------------------*
 |           Parallel             |
 *--------------------------------*)

(*** Parallel_setF ***)

lemma Parallel_setF : 
  "{(u, Y Un Z) |u Y Z.
     Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) &
     (EX s t. u : s |[X]|tr t & (s, Y) :f F & (t, Z) :f E)}
    : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac u Y Z Y1 Y2 s t)
apply (rule_tac x="Z Int (Y1 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)
apply (rule_tac x="Z Int (Y2 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)

(* (s,Y), Z <= Y, Y = Y1 Un Y2, Z = Z1 Un Z2 *)

apply (rule conjI, force)
apply (rule conjI, force)

apply (rule_tac x="s" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (rule conjI)
apply (rule memF_F2, simp, force)+
done

lemma in_failures_Parallel:
  "(f :f failures(P |[X]| Q)) = 
   (EX u Y Z. f = (u, Y Un Z) & Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) &
      (EX s t. u : s |[X]|tr t & (s,Y) :f failures(P) & (t,Z) :f failures(Q)))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Parallel_setF)

(*--------------------------------*
 |            Hiding              |
 *--------------------------------*)

(*** Hiding_setF ***)

lemma Hiding_setF : 
  "{f. EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f F} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac t Y Z s)
apply (rule_tac x="s" in exI)
apply (simp)
by (rule memF_F2, simp, force)

lemma in_failures_Hiding:
  "(f :f failures(P -- X)) = 
   (EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f failures(P))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Hiding_setF)

(*--------------------------------*
 |           Renaming             |
 *--------------------------------*)

(*** Renaming_setF ***)

lemma Renaming_setF : 
  "{f. EX s t X. f = (t,X) & s [[r]]* t & 
                 (s, [[r]]inv X) :f F } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp)
apply (rule memF_F2, simp)
apply (rule ren_inv_sub, simp)
done

lemma in_failures_Renaming:
  "(f :f failures(P[[r]])) =
   (EX s t X. f = (t,X) & s [[r]]* t & (s, [[r]]inv X) :f failures(P))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Renaming_setF)

(*--------------------------------*
 |           Seq_compo            |
 *--------------------------------*)

(*** Seq_compo_setF ***)

lemma Seq_compo_setF : 
  "{f. (EX t X. f = (t, X) & (t, insert Tick X) :f F & noTick t) |
        (EX s t X.
            f = (s ^^ t, X) & s ^^ <Tick> :t T & (t, X) :f E & noTick s)}
    : setF"
apply (simp add: setF_def HC_F2_def)
 apply (intro allI impI)
 apply (elim conjE exE disjE)

  (* case 1 *)
  apply (rule disjI1, simp)
  apply (rule memF_F2, simp, force)

  (* case 2 *)
  apply (rule disjI2)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)
  apply (rule memF_F2, simp, simp)
done

lemma in_failures_Seq_compo:
  "(f :f failures(P ;; Q)) =
   ((EX t X.   f = (t,X) & (t, X Un {Tick}) :f failures(P) & noTick t) |
    (EX s t X. f = (s ^^ t,X) & s ^^ <Tick> :t traces(P) 
               & (t, X) :f failures(Q) & noTick s))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Seq_compo_setF)

(*--------------------------------*
 |          Depth_rest            |
 *--------------------------------*)

(*** Depth_rest ***)

lemma in_failures_Depth_rest:
  "(f :f failures(P |. n)) =
   (EX t X. f = (t,X) & (t, X) :f  failures(P) &
                (lengtht t < n |
                 lengtht t = n & (EX s. t = s ^^ <Tick> & noTick s)))"
apply (simp add: failures_def)
apply (subgoal_tac "EX t X. f = (t, X)")
apply (elim exE)
apply (simp add: in_rest_setF)
apply (auto)
done

(*--------------------------------*
 |             alias              |
 *--------------------------------*)

lemmas failures_setF = STOP_setF       SKIP_setF
                       Act_prefix_setF Ext_pre_choice_setF
                       Ext_choice_setF Rep_int_choice_setF
                       Parallel_setF   Hiding_setF
                       Renaming_setF   Seq_compo_setF

lemmas in_failures = in_failures_STOP  in_failures_SKIP  in_failures_DIV
                     in_failures_Act_prefix     in_failures_Ext_pre_choice
                     in_failures_Ext_choice     in_failures_Int_choice
                     in_failures_Rep_int_choice in_failures_IF
                     in_failures_Parallel       in_failures_Hiding
                     in_failures_Renaming       in_failures_Seq_compo
                     in_failures_Union_proc     in_failures_UNIV_Union_proc
                     in_failures_Depth_rest

(****************** to add them again ******************)

declare disj_not1   [simp]

end

lemma STOP_setF: 

  {f. ∃X. f = (<>, X)} ∈ setF

lemma in_failures_STOP: 

  (f :f failures STOP) = (∃X. f = (<>, X))

lemma SKIP_setF: 

  {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))} ∈ setF

lemma in_failures_SKIP: 

  (f :f failures SKIP) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))

lemma in_failures_DIV: 

  f ~:f failures DIV

lemma Act_prefix_setF: 

  {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f F)}
  ∈ setF

lemma in_failures_Act_prefix: 

  (f :f failures (a -> P)) =
  ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨
   (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failures P))

lemma Ext_pre_choice_setF: 

  {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
      (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f Ff a ∧ a ∈ X)}
  ∈ setF

lemma in_failures_Ext_pre_choice: 

  (f :f failures (? :X -> Pf)) =
  ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
   (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failures (Pf a) ∧ a ∈ X))

lemma Ext_choice_setF: 

  {f. (∃X. f = (<>, X)) ∧ f :f F ∧ f :f E ∨
      (∃s. (∃X. f = (s, X)) ∧ (f :f F ∨ f :f E) ∧ s ≠ <>) ∨
      (∃X. f = (<>, X) ∧ (<Tick> :t T ∨ <Tick> :t S) ∧ X ⊆ Evset)}
  ∈ setF

lemma in_failures_Ext_choice: 

  (f :f failures (P [+] Q)) =
  ((∃X. f = (<>, X)) ∧ f :f failures P ∧ f :f failures Q ∨
   (∃s. (∃X. f = (s, X)) ∧ (f :f failures P ∨ f :f failures Q) ∧ s ≠ <>) ∨
   (∃X. f = (<>, X) ∧ (<Tick> :t traces P ∨ <Tick> :t traces Q) ∧ X ⊆ Evset))

lemma in_failures_Int_choice: 

  (f :f failures (P |~| Q)) = (f :f failures P ∨ f :f failures Q)

lemma Rep_int_choice_setF: 

  {f. ∃a∈X. f :f Ff a} ∈ setF

lemma in_failures_Union_proc: 

  (f :f {f. ∃a∈X. f :f Ff a}f) = (∃a∈X. f :f Ff a)

lemma in_failures_UNIV_Union_proc: 

  (f :f {f. ∃a. f :f Ff a}f) = (∃a. f :f Ff a)

lemma in_failures_Rep_int_choice_var: 

  (f :f failures (!! :C .. Pf)) = (∃c∈C. f :f failures (Pf c))

lemma in_failures_Rep_int_choice_fun: 

  inj g ==> (f :f failures (!!<g> :X .. Pf)) = (∃a∈X. f :f failures (Pf a))

lemma in_failures_Rep_int_choice_com: 

  (f :f failures (! :X .. Pf)) = (∃a∈X. f :f failures (Pf a))

lemmas in_failures_Rep_int_choice: 

  (f :f failures (!! :C .. Pf)) = (∃c∈C. f :f failures (Pf c))
  inj g ==> (f :f failures (!!<g> :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (! :X .. Pf)) = (∃a∈X. f :f failures (Pf a))

lemmas in_failures_Rep_int_choice: 

  (f :f failures (!! :C .. Pf)) = (∃c∈C. f :f failures (Pf c))
  inj g ==> (f :f failures (!!<g> :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (! :X .. Pf)) = (∃a∈X. f :f failures (Pf a))

lemma in_failures_IF: 

  (f :f failures (IF b THEN P ELSE Q)) =
  (if b then f :f failures P else f :f failures Q)

lemma Parallel_setF: 

  {(u, Y ∪ Z) |u Y Z.
   Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
   (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f F ∧ (t, Z) :f E)}
  ∈ setF

lemma in_failures_Parallel: 

  (f :f failures (P |[X]| Q)) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
      (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failures P ∧ (t, Z) :f failures Q))

lemma Hiding_setF: 

  {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f F} ∈ setF

lemma in_failures_Hiding: 

  (f :f failures (P -- X)) =
  (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failures P)

lemma Renaming_setF: 

  {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f F} ∈ setF

lemma in_failures_Renaming: 

  (f :f failures (P [[r]])) =
  (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failures P)

lemma Seq_compo_setF: 

  {f. (∃t X. f = (t, X) ∧ (t, insert Tick X) :f F ∧ noTick t) ∨
      (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t T ∧ (t, X) :f E ∧ noTick s)}
  ∈ setF

lemma in_failures_Seq_compo: 

  (f :f failures (P ;; Q)) =
  ((∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failures P ∧ noTick t) ∨
   (∃s t X.
       f = (s ^^ t, X) ∧
       s ^^ <Tick> :t traces P ∧ (t, X) :f failures Q ∧ noTick s))

lemma in_failures_Depth_rest: 

  (f :f failures (P |. n)) =
  (∃t X. f = (t, X) ∧
         (t, X) :f failures P ∧
         (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))

lemmas failures_setF: 

  {f. ∃X. f = (<>, X)} ∈ setF
  {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))} ∈ setF
  {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f F)}
  ∈ setF
  {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
      (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f Ff a ∧ a ∈ X)}
  ∈ setF
  {f. (∃X. f = (<>, X)) ∧ f :f F ∧ f :f E ∨
      (∃s. (∃X. f = (s, X)) ∧ (f :f F ∨ f :f E) ∧ s ≠ <>) ∨
      (∃X. f = (<>, X) ∧ (<Tick> :t T ∨ <Tick> :t S) ∧ X ⊆ Evset)}
  ∈ setF
  {f. ∃a∈X. f :f Ff a} ∈ setF
  {(u, Y ∪ Z) |u Y Z.
   Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
   (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f F ∧ (t, Z) :f E)}
  ∈ setF
  {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f F} ∈ setF
  {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f F} ∈ setF
  {f. (∃t X. f = (t, X) ∧ (t, insert Tick X) :f F ∧ noTick t) ∨
      (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t T ∧ (t, X) :f E ∧ noTick s)}
  ∈ setF

lemmas failures_setF: 

  {f. ∃X. f = (<>, X)} ∈ setF
  {f. (∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X))} ∈ setF
  {f. (∃X. f = (<>, X) ∧ Ev a ∉ X) ∨ (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f F)}
  ∈ setF
  {f. (∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
      (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f Ff a ∧ a ∈ X)}
  ∈ setF
  {f. (∃X. f = (<>, X)) ∧ f :f F ∧ f :f E ∨
      (∃s. (∃X. f = (s, X)) ∧ (f :f F ∨ f :f E) ∧ s ≠ <>) ∨
      (∃X. f = (<>, X) ∧ (<Tick> :t T ∨ <Tick> :t S) ∧ X ⊆ Evset)}
  ∈ setF
  {f. ∃a∈X. f :f Ff a} ∈ setF
  {(u, Y ∪ Z) |u Y Z.
   Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
   (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f F ∧ (t, Z) :f E)}
  ∈ setF
  {(s --tr X, Y) |s Y. (s, Ev ` X ∪ Y) :f F} ∈ setF
  {f. ∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f F} ∈ setF
  {f. (∃t X. f = (t, X) ∧ (t, insert Tick X) :f F ∧ noTick t) ∨
      (∃s t X. f = (s ^^ t, X) ∧ s ^^ <Tick> :t T ∧ (t, X) :f E ∧ noTick s)}
  ∈ setF

lemmas in_failures: 

  (f :f failures STOP) = (∃X. f = (<>, X))
  (f :f failures SKIP) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))
  f ~:f failures DIV
  (f :f failures (a -> P)) =
  ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨
   (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failures P))
  (f :f failures (? :X -> Pf)) =
  ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
   (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failures (Pf a) ∧ a ∈ X))
  (f :f failures (P [+] Q)) =
  ((∃X. f = (<>, X)) ∧ f :f failures P ∧ f :f failures Q ∨
   (∃s. (∃X. f = (s, X)) ∧ (f :f failures P ∨ f :f failures Q) ∧ s ≠ <>) ∨
   (∃X. f = (<>, X) ∧ (<Tick> :t traces P ∨ <Tick> :t traces Q) ∧ X ⊆ Evset))
  (f :f failures (P |~| Q)) = (f :f failures P ∨ f :f failures Q)
  (f :f failures (!! :C .. Pf)) = (∃c∈C. f :f failures (Pf c))
  inj g ==> (f :f failures (!!<g> :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (! :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (IF b THEN P ELSE Q)) =
  (if b then f :f failures P else f :f failures Q)
  (f :f failures (P |[X]| Q)) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
      (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failures P ∧ (t, Z) :f failures Q))
  (f :f failures (P -- X)) =
  (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failures P)
  (f :f failures (P [[r]])) =
  (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failures P)
  (f :f failures (P ;; Q)) =
  ((∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failures P ∧ noTick t) ∨
   (∃s t X.
       f = (s ^^ t, X) ∧
       s ^^ <Tick> :t traces P ∧ (t, X) :f failures Q ∧ noTick s))
  (f :f {f. ∃a∈X. f :f Ff a}f) = (∃a∈X. f :f Ff a)
  (f :f {f. ∃a. f :f Ff a}f) = (∃a. f :f Ff a)
  (f :f failures (P |. n)) =
  (∃t X. f = (t, X) ∧
         (t, X) :f failures P ∧
         (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))

lemmas in_failures: 

  (f :f failures STOP) = (∃X. f = (<>, X))
  (f :f failures SKIP) = ((∃X. f = (<>, X) ∧ X ⊆ Evset) ∨ (∃X. f = (<Tick>, X)))
  f ~:f failures DIV
  (f :f failures (a -> P)) =
  ((∃X. f = (<>, X) ∧ Ev a ∉ X) ∨
   (∃s X. f = (<Ev a> ^^ s, X) ∧ (s, X) :f failures P))
  (f :f failures (? :X -> Pf)) =
  ((∃Y. f = (<>, Y) ∧ Ev ` X ∩ Y = {}) ∨
   (∃a s Y. f = (<Ev a> ^^ s, Y) ∧ (s, Y) :f failures (Pf a) ∧ a ∈ X))
  (f :f failures (P [+] Q)) =
  ((∃X. f = (<>, X)) ∧ f :f failures P ∧ f :f failures Q ∨
   (∃s. (∃X. f = (s, X)) ∧ (f :f failures P ∨ f :f failures Q) ∧ s ≠ <>) ∨
   (∃X. f = (<>, X) ∧ (<Tick> :t traces P ∨ <Tick> :t traces Q) ∧ X ⊆ Evset))
  (f :f failures (P |~| Q)) = (f :f failures P ∨ f :f failures Q)
  (f :f failures (!! :C .. Pf)) = (∃c∈C. f :f failures (Pf c))
  inj g ==> (f :f failures (!!<g> :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (! :X .. Pf)) = (∃a∈X. f :f failures (Pf a))
  (f :f failures (IF b THEN P ELSE Q)) =
  (if b then f :f failures P else f :f failures Q)
  (f :f failures (P |[X]| Q)) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ∧
      (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f failures P ∧ (t, Z) :f failures Q))
  (f :f failures (P -- X)) =
  (∃s Y. f = (s --tr X, Y) ∧ (s, Ev ` X ∪ Y) :f failures P)
  (f :f failures (P [[r]])) =
  (∃s t X. f = (t, X) ∧ s [[r]]* t ∧ (s, [[r]]inv X) :f failures P)
  (f :f failures (P ;; Q)) =
  ((∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f failures P ∧ noTick t) ∨
   (∃s t X.
       f = (s ^^ t, X) ∧
       s ^^ <Tick> :t traces P ∧ (t, X) :f failures Q ∧ noTick s))
  (f :f {f. ∃a∈X. f :f Ff a}f) = (∃a∈X. f :f Ff a)
  (f :f {f. ∃a. f :f Ff a}f) = (∃a. f :f Ff a)
  (f :f failures (P |. n)) =
  (∃t X. f = (t, X) ∧
         (t, X) :f failures P ∧
         (lengtht t < n ∨ lengtht t = n ∧ (∃s. t = s ^^ <Tick> ∧ noTick s)))