Theory CSP_F_law_aux

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |                  April 2006               |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_aux = CSP_F_law:

(*---------------------------------------------------------------*
 |                                                               |
 |           convenient laws, especially for tactics             |
 |                                                               |
 *---------------------------------------------------------------*)

(*****************************************************************
                            Internal                 
 *****************************************************************)

(*------------------*
 |     singleton    |
 *------------------*)

(*** ! :{a} ***)

lemma cspF_Rep_int_choice0_singleton:
  "!! :{c} .. Pf =F Pf c"
apply (rule cspF_Rep_int_choice_const)
apply (auto)
done

lemma cspF_Rep_int_choice_fun_singleton:
  "inj f ==> !!<f> :{x} .. Pf =F Pf x"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice_const)
apply (auto)
done

lemma cspF_Rep_int_choice1_singleton:
  "! :{a} .. Pf =F Pf a"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_const)
apply (auto)
done

lemma cspF_Rep_int_choice2_singleton:
  "!set :{X} .. Pf =F Pf X"
by (simp add: cspF_Rep_int_choice_fun_singleton)

lemma cspF_Rep_int_choice3_singleton:
  "!nat :{n} .. Pf =F Pf n"
by (simp add: cspF_Rep_int_choice_fun_singleton)

lemmas cspF_Rep_int_choice_singleton = cspF_Rep_int_choice0_singleton
                                       cspF_Rep_int_choice1_singleton
                                       cspF_Rep_int_choice2_singleton
                                       cspF_Rep_int_choice3_singleton

lemma cspF_Rep_int_choice_const0_rule:
  "!! c:C .. P =F IF (C={}) THEN DIV ELSE P"
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Rep_int_choice_empty)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Rep_int_choice_const)
apply (simp_all)
done

lemma cspF_Rep_int_choice_const_fun_rule:
  "!!<f> x:X .. P =F IF (X={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const0_rule)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Rep_int_choice_const1_rule:
  "! x:X .. P =F IF (X={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_fun_rule)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Rep_int_choice_const2_rule:
  "!set X:Xs .. P =F IF (Xs={}) THEN DIV ELSE P"
by (simp add: cspF_Rep_int_choice_const_fun_rule)

lemma cspF_Rep_int_choice_const3_rule:
  "!nat n:N .. P =F IF (N={}) THEN DIV ELSE P"
by (simp add: cspF_Rep_int_choice_const_fun_rule)

lemmas cspF_Rep_int_choice_const_rule =
       cspF_Rep_int_choice_const0_rule
       cspF_Rep_int_choice_const1_rule
       cspF_Rep_int_choice_const2_rule
       cspF_Rep_int_choice_const3_rule

lemmas cspF_Int_choice_rule = cspF_Rep_int_choice_empty
                              cspF_Rep_int_choice_singleton 
                              cspF_Int_choice_idem
                              cspF_Rep_int_choice_const_rule

(*****************************************************************
                          External
 *****************************************************************)

(* to make produced process be concrete *)

lemma cspF_Ext_pre_choice_empty_DIV:
   "? :{} -> Pf =F ? a:{} -> DIV"
apply (rule cspF_rw_left)
apply (rule cspF_STOP_step[THEN cspF_sym])
apply (rule cspF_STOP_step)
done

lemma cspF_Ext_choice_unit_l_hsf: 
  "? :{} -> Qf [+] P =F P"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_step[THEN cspF_sym])
apply (rule cspF_reflex)
apply (simp add: cspF_unit)
done

lemma cspF_Ext_choice_unit_r_hsf: 
  "P [+] ? :{} -> Qf =F P"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (simp add: cspF_Ext_choice_unit_l_hsf)
done

lemmas cspF_Ext_choice_rule = cspF_Ext_pre_choice_empty_DIV
                              cspF_Ext_choice_unit_l
                              cspF_Ext_choice_unit_l_hsf
                              cspF_Ext_choice_unit_r
                              cspF_Ext_choice_unit_r_hsf
                              cspF_Ext_choice_idem

(*-----------------------------*
 |      simp rule for cspF     |
 *-----------------------------*)

lemmas cspF_choice_rule  = cspF_Int_choice_rule cspF_Ext_choice_rule

(*****************************************************************
                          Timeout
 *****************************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

(*** <= Timeout ***)

lemma cspF_Timeout_right:
  "[| P <=F Q1 ; P <=F Q2 |] ==> P <=F Q1 [> Q2"
apply (rule cspF_rw_right)
apply (rule cspF_dist)
apply (rule cspF_Int_choice_right)
apply (rule cspF_Ext_choice_right, simp_all)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_unit_l, simp_all)
done

(*** STOP [> P  =  P ***)

lemma cspF_STOP_Timeout:
  "STOP [> P =F P"
apply (rule cspF_rw_left)
apply (rule cspF_dist)
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_idem)
apply (rule cspF_unit)
done

(*================================================*
 |                                                |
 |               auxiliary step laws              |
 |                                                |
 *================================================*)

(* split + resolve *)

lemma cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
    ((? :Y -> Pf) [+] P) |[X]| ((? :Z -> Qf) [+] Q) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
                                        |~| (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
               ELSE (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
     [> (((P |[X]| ((? :Z -> Qf) [+] Q)) |~|
         (((? :Y -> Pf) [+] P) |[X]| Q)))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)

apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_split)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)

apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)

apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)

apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
done

lemma cspF_Parallel_Timeout_split_resolve_SKIP_SKIP:
  "((? :Y -> Pf) [+] SKIP) |[X]| ((? :Z -> Qf) [+] SKIP) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
                                        |~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
               ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
     [> (((SKIP |[X]| ((? :Z -> Qf) [+] SKIP)) |~|
         (((? :Y -> Pf) [+] SKIP) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_split_resolve_DIV_DIV:
  "((? :Y -> Pf) [+] DIV) |[X]| ((? :Z -> Qf) [+] DIV) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
                                        |~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
               ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
     [> (((DIV |[X]| ((? :Z -> Qf) [+] DIV)) |~|
         (((? :Y -> Pf) [+] DIV) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_split_resolve_SKIP_DIV:
  "((? :Y -> Pf) [+] SKIP) |[X]| ((? :Z -> Qf) [+] DIV) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
                                        |~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
               ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
     [> (((SKIP |[X]| ((? :Z -> Qf) [+] DIV)) |~|
         (((? :Y -> Pf) [+] SKIP) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_split_resolve_DIV_SKIP:
  "((? :Y -> Pf) [+] DIV) |[X]| ((? :Z -> Qf) [+] SKIP) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
                                        |~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
               ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
     [> (((DIV |[X]| ((? :Z -> Qf) [+] SKIP)) |~|
         (((? :Y -> Pf) [+] DIV) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)

lemmas cspF_Parallel_Timeout_split_resolve =
       cspF_Parallel_Timeout_split_resolve_SKIP_SKIP
       cspF_Parallel_Timeout_split_resolve_DIV_DIV
       cspF_Parallel_Timeout_split_resolve_SKIP_DIV
       cspF_Parallel_Timeout_split_resolve_DIV_SKIP

(* input + resolve *)

lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l:
  "P = SKIP | P = DIV ==>
   ((? :Y -> Pf) [+] P) |[X]| (? :Z -> Qf) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
                                        |~| (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
               ELSE (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
     [> (((P |[X]| (? :Z -> Qf))))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)

apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_input)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)

apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)

apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)

apply (simp)
done

lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r:
  "Q = SKIP | Q = DIV ==>
   (? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] Q) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
                                        |~| ((? x:Y -> Pf x) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
               ELSE ((? x:Y -> Pf x) |[X]| Qf x))
     [> ((((? :Y -> Pf) |[X]| Q)))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)

apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_input)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)

apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)

apply (simp)
done

lemmas cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV =
       cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l
       cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r

lemma cspF_Parallel_Timeout_input_resolve_SKIP_l:
  "((? :Y -> Pf) [+] SKIP) |[X]| (? :Z -> Qf) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
                                        |~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
               ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
     [> (((SKIP |[X]| (? :Z -> Qf))))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_input_resolve_DIV_l:
  "((? :Y -> Pf) [+] DIV) |[X]| (? :Z -> Qf) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
                                        |~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
               ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
     [> (((DIV |[X]| (? :Z -> Qf))))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_input_resolve_SKIP_r:
  "(? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] SKIP) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
                                        |~| ((? x:Y -> Pf x) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
               ELSE ((? x:Y -> Pf x) |[X]| Qf x))
     [> ((((? :Y -> Pf) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)

lemma cspF_Parallel_Timeout_input_resolve_DIV_r:
  "(? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] DIV) =F
     (? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
                                        |~| ((? x:Y -> Pf x) |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
               ELSE ((? x:Y -> Pf x) |[X]| Qf x))
     [> ((((? :Y -> Pf) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)

lemmas cspF_Parallel_Timeout_input_resolve =
       cspF_Parallel_Timeout_input_resolve_SKIP_l
       cspF_Parallel_Timeout_input_resolve_SKIP_r
       cspF_Parallel_Timeout_input_resolve_DIV_l
       cspF_Parallel_Timeout_input_resolve_DIV_r

(**************** ;; + resolve ****************)

lemma cspF_SKIP_Seq_compo_step_resolve:
  "((? :X -> Pf) [+] SKIP) ;; Q =F (? x:X -> (Pf x ;; Q)) [> Q"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_Seq_compo_step)
done

lemma cspF_DIV_Seq_compo_step_resolve:
  "((? :X -> Pf) [+] DIV) ;; Q =F (? x:X -> (Pf x ;; Q)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)

apply (rule cspF_rw_left)
apply (rule cspF_DIV_Seq_compo_step)
apply (rule cspF_Ext_choice_SKIP_DIV_resolve[THEN cspF_sym])
done

lemmas cspF_SKIP_DIV_Seq_compo_step_resolve =
       cspF_SKIP_Seq_compo_step_resolve
       cspF_DIV_Seq_compo_step_resolve

(****** for sequentilising processes with SKIP or DIV ******)

lemmas cspF_SKIP_DIV_resolve =
       cspF_SKIP_DIV
       cspF_Parallel_Timeout_split_resolve
       cspF_Parallel_Timeout_input_resolve
       cspF_SKIP_DIV_Seq_compo_step_resolve

lemmas cspF_SKIP_or_DIV_resolve =
       cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV
       cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV

(*=========================================================*
 |                                                         |
 |   for convenience, especially for fully sequntialising  |
 |                                                         |
 *=========================================================*)

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l:
  "Q = SKIP | Q = DIV | Q = STOP ==>
   (P [+] Q) |[X]| DIV =F (P |[X]| DIV)"
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_unit)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r:
  "Q = SKIP | Q = DIV | Q = STOP ==>
   DIV |[X]| (P [+] Q) =F (DIV |[X]| P)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_right)
apply (rule cspF_commut)
apply (simp add: cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l)
done

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV =
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l:
  "Q = SKIP | Q = DIV | Q = STOP ==>
   ((? :Y -> Pf) [+] Q) |[X]| SKIP =F 
   (? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] Q"
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)

apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_unit)
apply (rule cspF_reflex)

apply (rule cspF_rw_right)
apply (rule cspF_unit)
apply (rule cspF_SKIP_DIV)
done

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r:
  "Q = SKIP | Q = DIV | Q = STOP ==>
   SKIP |[X]| ((? :Y -> Pf) [+] Q) =F 
   (? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] Q"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (simp add: cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l)
done

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP =
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice =
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV
       cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP

(* renaming *)

lemma cspF_SKIP_or_DIV_or_STOP_Renaming_Id: 
   "P = SKIP | P = DIV | P = STOP ==> P [[r]] =F P"
apply (erule disjE)
apply (simp add: cspF_SKIP_DIV)
apply (erule disjE)
apply (simp add: cspF_SKIP_DIV)

apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_step)

apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_pre_choice_empty_DIV)

apply (rule cspF_rw_left)
apply (rule cspF_step)

apply (rule cspF_rw_right)
apply (rule cspF_step)

apply (rule cspF_decompo)
apply (auto)
done

(* restg *)

lemma cspF_STOP_Depth_rest:
   "STOP |. Suc n =F STOP"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_step)
apply (rule cspF_rw_left)
apply (rule cspF_step)
apply (rule cspF_rw_right)
apply (rule cspF_step)

apply (rule cspF_decompo)
apply (auto)
done

(*==============================================================*
 |                                                              |
 |       Associativity and Commutativity for SKIP and DIV       |
 |                    (for sequentialising)                     |
 |                                                              |
 *==============================================================*)

lemma cspF_Ext_pre_choice_SKIP_commut:
  "SKIP [+] (? :X -> Pf) =F (? :X -> Pf) [+] SKIP"
by (rule cspF_commut)

lemma cspF_Ext_pre_choice_DIV_commut:
  "DIV [+] (? :X -> Pf) =F (? :X -> Pf) [+] DIV"
by (rule cspF_commut)

lemma cspF_Ext_pre_choice_SKIP_assoc:
  "((? :X -> Pf) [+] SKIP) [+] (? :Y -> Qf)
   =F ((? :X -> Pf) [+] (? :Y -> Qf)) [+] SKIP"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_commut)
apply (rule cspF_assoc)
done

lemma cspF_Ext_pre_choice_DIV_assoc:
  "((? :X -> Pf) [+] DIV) [+] (? :Y -> Qf)
   =F ((? :X -> Pf) [+] (? :Y -> Qf)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_commut)
apply (rule cspF_assoc)
done

lemma cspF_Ext_choice_idem_assoc:
  "(P [+] Q) [+] Q =F (P [+] Q)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_idem)
apply (rule cspF_reflex)
done

lemma cspF_Ext_choice_SKIP_DIV_assoc:
  "(P [+] SKIP) [+] DIV =F (P [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_DIV)
apply (rule cspF_reflex)
done

lemma cspF_Ext_choice_DIV_SKIP_assoc:
  "(P [+] DIV) [+] SKIP =F (P [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_DIV)
apply (rule cspF_reflex)
done

lemmas cspF_SKIP_DIV_sort =
       cspF_Ext_choice_assoc
       cspF_Ext_pre_choice_SKIP_commut
       cspF_Ext_pre_choice_DIV_commut
       cspF_Ext_pre_choice_SKIP_assoc
       cspF_Ext_pre_choice_DIV_assoc
       cspF_Ext_choice_idem_assoc
       cspF_Ext_choice_SKIP_DIV_assoc
       cspF_Ext_choice_DIV_SKIP_assoc

(*==============================================================*
 |                                                              |
 |    decompostion control by the flag "Not_Decompo_Flag"       |
 |                                                              |
 *==============================================================*)

(*------------------------------------------------*
 |              trans with Flag                   |
 *------------------------------------------------*)

(*** rewrite (eq) ***)

lemma cspF_rw_flag_left_eq:
  "[| R1 =F R2 ; Not_Decompo_Flag & R2 =F R3 |] ==> R1 =F R3"
by (simp add: eqF_def Not_Decompo_Flag_def)

lemma cspF_rw_flag_left_ref:
  "[| R1 =F R2 ; Not_Decompo_Flag & R2 <=F R3 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)

lemmas cspF_rw_flag_left = cspF_rw_flag_left_eq cspF_rw_flag_left_ref

lemma cspF_rw_flag_right_eq:
  "[| R3 =F R2 ; Not_Decompo_Flag & R1 =F R2 |] ==> R1 =F R3"
by (simp add: eqF_def Not_Decompo_Flag_def)

lemma cspF_rw_flag_right_ref:
  "[| R3 =F R2 ; Not_Decompo_Flag & R1 <=F R2 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)

lemmas cspF_rw_flag_right = cspF_rw_flag_right_eq cspF_rw_flag_right_ref

(*==============================================================*
 |  decompostion of Sequential composition with a flag          |
 |  It is often useful that the second process is not expanded. |
 *==============================================================*)

lemma cspF_Seq_compo_mono_flag:
  "[| P1 <=F Q1 ; 
      Not_Decompo_Flag & P2 <=F Q2 |]
           ==> P1 ;; P2 <=F Q1 ;; Q2"
by (simp add: cspF_Seq_compo_mono)

lemma cspF_Seq_compo_cong_flag:
  "[| P1 =F Q1 ; 
      Not_Decompo_Flag & P2 =F Q2 |]
           ==> P1 ;; P2 =F Q1 ;; Q2"
by (simp add: cspF_Seq_compo_cong)

lemmas cspF_free_mono_flag =
       cspF_Ext_choice_mono cspF_Int_choice_mono cspF_Parallel_mono
       cspF_Hiding_mono cspF_Renaming_mono cspF_Seq_compo_mono_flag
       cspF_Depth_rest_mono

lemmas cspF_free_cong_flag =
       cspF_Ext_choice_cong cspF_Int_choice_cong cspF_Parallel_cong
       cspF_Hiding_cong cspF_Renaming_cong cspF_Seq_compo_cong_flag
       cspF_Depth_rest_cong

lemmas cspF_free_decompo_flag = cspF_free_mono_flag cspF_free_cong_flag

end

lemma cspF_Rep_int_choice0_singleton:

  !! :{c} .. Pf =F Pf c

lemma cspF_Rep_int_choice_fun_singleton:

  inj f ==> !!<f> :{x} .. Pf =F Pf x

lemma cspF_Rep_int_choice1_singleton:

  ! :{a} .. Pf =F Pf a

lemma cspF_Rep_int_choice2_singleton:

  !set :{X} .. Pf =F Pf X

lemma cspF_Rep_int_choice3_singleton:

  !nat :{n} .. Pf =F Pf n

lemmas cspF_Rep_int_choice_singleton:

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

lemmas cspF_Rep_int_choice_singleton:

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

lemma cspF_Rep_int_choice_const0_rule:

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

lemma cspF_Rep_int_choice_const_fun_rule:

  !!<f> x:X .. P =F IF (X = {}) THEN DIV ELSE P

lemma cspF_Rep_int_choice_const1_rule:

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

lemma cspF_Rep_int_choice_const2_rule:

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

lemma cspF_Rep_int_choice_const3_rule:

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

lemmas cspF_Rep_int_choice_const_rule:

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

lemmas cspF_Rep_int_choice_const_rule:

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

lemmas cspF_Int_choice_rule:

  !! :{} .. Pf =F DIV

  ! :{} .. Pf =F DIV

  !set :{} .. Pf =F DIV

  !nat :{} .. Pf =F DIV

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

  P |~| P =F P

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

lemmas cspF_Int_choice_rule:

  !! :{} .. Pf =F DIV

  ! :{} .. Pf =F DIV

  !set :{} .. Pf =F DIV

  !nat :{} .. Pf =F DIV

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

  P |~| P =F P

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

lemma cspF_Ext_pre_choice_empty_DIV:

  ? :{} -> Pf =F ? a:{} -> DIV

lemma cspF_Ext_choice_unit_l_hsf:

  ? :{} -> Qf [+] P =F P

lemma cspF_Ext_choice_unit_r_hsf:

  P [+] ? :{} -> Qf =F P

lemmas cspF_Ext_choice_rule:

  ? :{} -> Pf =F ? a:{} -> DIV

  STOP [+] P =F P

  ? :{} -> Qf [+] P =F P

  P [+] STOP =F P

  P [+] ? :{} -> Qf =F P

  P [+] P =F P

lemmas cspF_Ext_choice_rule:

  ? :{} -> Pf =F ? a:{} -> DIV

  STOP [+] P =F P

  ? :{} -> Qf [+] P =F P

  P [+] STOP =F P

  P [+] ? :{} -> Qf =F P

  P [+] P =F P

lemmas cspF_choice_rule:

  !! :{} .. Pf =F DIV

  ! :{} .. Pf =F DIV

  !set :{} .. Pf =F DIV

  !nat :{} .. Pf =F DIV

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

  P |~| P =F P

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

  ? :{} -> Pf =F ? a:{} -> DIV

  STOP [+] P =F P

  ? :{} -> Qf [+] P =F P

  P [+] STOP =F P

  P [+] ? :{} -> Qf =F P

  P [+] P =F P

lemmas cspF_choice_rule:

  !! :{} .. Pf =F DIV

  ! :{} .. Pf =F DIV

  !set :{} .. Pf =F DIV

  !nat :{} .. Pf =F DIV

  !! :{c} .. Pf =F Pf c

  ! :{a} .. Pf =F Pf a

  !set :{X} .. Pf =F Pf X

  !nat :{n} .. Pf =F Pf n

  P |~| P =F P

  !! c:C .. P =F IF (C = {}) THEN DIV ELSE P

  ! x:X .. P =F IF (X = {}) THEN DIV ELSE P

  !set X:Xs .. P =F IF (Xs = {}) THEN DIV ELSE P

  !nat n:N .. P =F IF (N = {}) THEN DIV ELSE P

  ? :{} -> Pf =F ? a:{} -> DIV

  STOP [+] P =F P

  ? :{} -> Qf [+] P =F P

  P [+] STOP =F P

  P [+] ? :{} -> Qf =F P

  P [+] P =F P

lemma cspF_Timeout_right:

  [| P <=F Q1.0; P <=F Q2.0 |] ==> P <=F Q1.0 [> Q2.0

lemma cspF_STOP_Timeout:

  STOP [> P =F P

lemma cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> (? :Y -> Pf [+] P) |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                     |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> (P |[X]| (? :Z -> Qf [+] Q) |~| (? :Y -> Pf [+] P) |[X]| Q)

lemma cspF_Parallel_Timeout_split_resolve_SKIP_SKIP:

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)

lemma cspF_Parallel_Timeout_split_resolve_DIV_DIV:

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)

lemma cspF_Parallel_Timeout_split_resolve_SKIP_DIV:

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)

lemma cspF_Parallel_Timeout_split_resolve_DIV_SKIP:

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)

lemmas cspF_Parallel_Timeout_split_resolve:

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)

lemmas cspF_Parallel_Timeout_split_resolve:

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)

lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l:

  P = SKIP ∨ P = DIV
  ==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> P |[X]| ? :Z -> Qf

lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r:

  Q = SKIP ∨ Q = DIV
  ==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE ? :Y -> Pf |[X]| Qf x 
       [> ? :Y -> Pf |[X]| Q

lemmas cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV:

  P = SKIP ∨ P = DIV
  ==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> P |[X]| ? :Z -> Qf

  Q = SKIP ∨ Q = DIV
  ==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE ? :Y -> Pf |[X]| Qf x 
       [> ? :Y -> Pf |[X]| Q

lemmas cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV:

  P = SKIP ∨ P = DIV
  ==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> P |[X]| ? :Z -> Qf

  Q = SKIP ∨ Q = DIV
  ==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE ? :Y -> Pf |[X]| Qf x 
       [> ? :Y -> Pf |[X]| Q

lemma cspF_Parallel_Timeout_input_resolve_SKIP_l:

  (? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> SKIP |[X]| ? :Z -> Qf

lemma cspF_Parallel_Timeout_input_resolve_DIV_l:

  (? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> DIV |[X]| ? :Z -> Qf

lemma cspF_Parallel_Timeout_input_resolve_SKIP_r:

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| SKIP

lemma cspF_Parallel_Timeout_input_resolve_DIV_r:

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| DIV

lemmas cspF_Parallel_Timeout_input_resolve:

  (? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> SKIP |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| SKIP

  (? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> DIV |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| DIV

lemmas cspF_Parallel_Timeout_input_resolve:

  (? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> SKIP |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| SKIP

  (? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> DIV |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| DIV

lemma cspF_SKIP_Seq_compo_step_resolve:

  (? :X -> Pf [+] SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

lemma cspF_DIV_Seq_compo_step_resolve:

  (? :X -> Pf [+] DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [+] DIV

lemmas cspF_SKIP_DIV_Seq_compo_step_resolve:

  (? :X -> Pf [+] SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [+] DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [+] DIV

lemmas cspF_SKIP_DIV_Seq_compo_step_resolve:

  (? :X -> Pf [+] SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [+] DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [+] DIV

lemmas cspF_SKIP_DIV_resolve:

  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)

  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)

  DIV |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV

  ? :Y -> Qf |[X]| DIV =F ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV

  SKIP [+] DIV =F SKIP

  DIV [+] SKIP =F SKIP

  SKIP |[X]| DIV =F DIV

  DIV |[X]| SKIP =F DIV

  SKIP |[X]| SKIP =F SKIP

  DIV |[X]| DIV =F DIV

  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP

  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

  (P [+] SKIP) |[X]| DIV =F P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F DIV |[X]| P

  (P [+] DIV) |[X]| DIV =F P |[X]| DIV

  DIV |[X]| (P [+] DIV) =F DIV |[X]| P

  SKIP -- X =F SKIP

  DIV -- X =F DIV

  (? :Y -> Pf [+] DIV) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X

  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X

  SKIP [[r]] =F SKIP

  DIV [[r]] =F DIV

  SKIP ;; P =F P

  P ;; SKIP =F P

  DIV ;; P =F DIV

  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [> DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [> DIV

  SKIP |. Suc n =F SKIP

  DIV |. n =F DIV

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)

  (? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> SKIP |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| SKIP

  (? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> DIV |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| DIV

  (? :X -> Pf [+] SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [+] DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [+] DIV

lemmas cspF_SKIP_DIV_resolve:

  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)

  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)

  DIV |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV

  ? :Y -> Qf |[X]| DIV =F ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV

  SKIP [+] DIV =F SKIP

  DIV [+] SKIP =F SKIP

  SKIP |[X]| DIV =F DIV

  DIV |[X]| SKIP =F DIV

  SKIP |[X]| SKIP =F SKIP

  DIV |[X]| DIV =F DIV

  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP

  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

  (P [+] SKIP) |[X]| DIV =F P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F DIV |[X]| P

  (P [+] DIV) |[X]| DIV =F P |[X]| DIV

  DIV |[X]| (P [+] DIV) =F DIV |[X]| P

  SKIP -- X =F SKIP

  DIV -- X =F DIV

  (? :Y -> Pf [+] DIV) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X

  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X

  SKIP [[r]] =F SKIP

  DIV [[r]] =F DIV

  SKIP ;; P =F P

  P ;; SKIP =F P

  DIV ;; P =F DIV

  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [> DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [> DIV

  SKIP |. Suc n =F SKIP

  DIV |. n =F DIV

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                 |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)

  (? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                 |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)

  (? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] SKIP) |[X]| Qf x 
   [> SKIP |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] SKIP) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| SKIP

  (? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                ELSE (? :Y -> Pf [+] DIV) |[X]| Qf x 
   [> DIV |[X]| ? :Z -> Qf

  ? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] DIV) 
                ELSE ? :Y -> Pf |[X]| Qf x 
   [> ? :Y -> Pf |[X]| DIV

  (? :X -> Pf [+] SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [+] DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [+] DIV

lemmas cspF_SKIP_or_DIV_resolve:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> (? :Y -> Pf [+] P) |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                     |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> (P |[X]| (? :Z -> Qf [+] Q) |~| (? :Y -> Pf [+] P) |[X]| Q)

  P = SKIP ∨ P = DIV
  ==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> P |[X]| ? :Z -> Qf

  Q = SKIP ∨ Q = DIV
  ==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE ? :Y -> Pf |[X]| Qf x 
       [> ? :Y -> Pf |[X]| Q

lemmas cspF_SKIP_or_DIV_resolve:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> (? :Y -> Pf [+] P) |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                     |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> (P |[X]| (? :Z -> Qf [+] Q) |~| (? :Y -> Pf [+] P) |[X]| Q)

  P = SKIP ∨ P = DIV
  ==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf 
                    ELSE (? :Y -> Pf [+] P) |[X]| Qf x 
       [> P |[X]| ? :Z -> Qf

  Q = SKIP ∨ Q = DIV
  ==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F 
      ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
       -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
          ELSE IF (x ∈ Y ∧ x ∈ Z) 
               THEN Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x 
               ELSE IF (x ∈ Y) THEN Pf x |[X]| (? :Z -> Qf [+] Q) 
                    ELSE ? :Y -> Pf |[X]| Qf x 
       [> ? :Y -> Pf |[X]| Q

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F P |[X]| DIV

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F DIV |[X]| P

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F DIV |[X]| P

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F DIV |[X]| P

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> (? :Y -> Pf [+] Q) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> (? :Y -> Pf [+] Q) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> (? :Y -> Pf [+] Q) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F DIV |[X]| P

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> (? :Y -> Pf [+] Q) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q

lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice:

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F DIV |[X]| P

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> (? :Y -> Pf [+] Q) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q

lemma cspF_SKIP_or_DIV_or_STOP_Renaming_Id:

  P = SKIP ∨ P = DIV ∨ P = STOP ==> P [[r]] =F P

lemma cspF_STOP_Depth_rest:

  STOP |. Suc n =F STOP

lemma cspF_Ext_pre_choice_SKIP_commut:

  SKIP [+] ? :X -> Pf =F ? :X -> Pf [+] SKIP

lemma cspF_Ext_pre_choice_DIV_commut:

  DIV [+] ? :X -> Pf =F ? :X -> Pf [+] DIV

lemma cspF_Ext_pre_choice_SKIP_assoc:

  ? :X -> Pf [+] SKIP [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] SKIP

lemma cspF_Ext_pre_choice_DIV_assoc:

  ? :X -> Pf [+] DIV [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] DIV

lemma cspF_Ext_choice_idem_assoc:

  P [+] Q [+] Q =F P [+] Q

lemma cspF_Ext_choice_SKIP_DIV_assoc:

  P [+] SKIP [+] DIV =F P [+] SKIP

lemma cspF_Ext_choice_DIV_SKIP_assoc:

  P [+] DIV [+] SKIP =F P [+] SKIP

lemmas cspF_SKIP_DIV_sort:

  P [+] (Q [+] R) =F P [+] Q [+] R

  SKIP [+] ? :X -> Pf =F ? :X -> Pf [+] SKIP

  DIV [+] ? :X -> Pf =F ? :X -> Pf [+] DIV

  ? :X -> Pf [+] SKIP [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] SKIP

  ? :X -> Pf [+] DIV [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] DIV

  P [+] Q [+] Q =F P [+] Q

  P [+] SKIP [+] DIV =F P [+] SKIP

  P [+] DIV [+] SKIP =F P [+] SKIP

lemmas cspF_SKIP_DIV_sort:

  P [+] (Q [+] R) =F P [+] Q [+] R

  SKIP [+] ? :X -> Pf =F ? :X -> Pf [+] SKIP

  DIV [+] ? :X -> Pf =F ? :X -> Pf [+] DIV

  ? :X -> Pf [+] SKIP [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] SKIP

  ? :X -> Pf [+] DIV [+] ? :Y -> Qf =F ? :X -> Pf [+] ? :Y -> Qf [+] DIV

  P [+] Q [+] Q =F P [+] Q

  P [+] SKIP [+] DIV =F P [+] SKIP

  P [+] DIV [+] SKIP =F P [+] SKIP

lemma cspF_rw_flag_left_eq:

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 =F R3.0 |] ==> R1.0 =F R3.0

lemma cspF_rw_flag_left_ref:

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 <=F R3.0 |] ==> R1.0 <=F R3.0

lemmas cspF_rw_flag_left:

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 =F R3.0 |] ==> R1.0 =F R3.0

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 <=F R3.0 |] ==> R1.0 <=F R3.0

lemmas cspF_rw_flag_left:

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 =F R3.0 |] ==> R1.0 =F R3.0

  [| R1.0 =F R2.0; Not_Decompo_Flag ∧ R2.0 <=F R3.0 |] ==> R1.0 <=F R3.0

lemma cspF_rw_flag_right_eq:

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 =F R2.0 |] ==> R1.0 =F R3.0

lemma cspF_rw_flag_right_ref:

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 <=F R2.0 |] ==> R1.0 <=F R3.0

lemmas cspF_rw_flag_right:

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 =F R2.0 |] ==> R1.0 =F R3.0

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 <=F R2.0 |] ==> R1.0 <=F R3.0

lemmas cspF_rw_flag_right:

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 =F R2.0 |] ==> R1.0 =F R3.0

  [| R3.0 =F R2.0; Not_Decompo_Flag ∧ R1.0 <=F R2.0 |] ==> R1.0 <=F R3.0

lemma cspF_Seq_compo_mono_flag:

  [| P1.0 <=F Q1.0; Not_Decompo_Flag ∧ P2.0 <=F Q2.0 |]
  ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0

lemma cspF_Seq_compo_cong_flag:

  [| P1.0 =F Q1.0; Not_Decompo_Flag ∧ P2.0 =F Q2.0 |]
  ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0

lemmas cspF_free_mono_flag:

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0

  [| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0

  [| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y

  [| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]

  [| P1.0 <=F Q1.0; Not_Decompo_Flag ∧ P2.0 <=F Q2.0 |]
  ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0

lemmas cspF_free_mono_flag:

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0

  [| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0

  [| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y

  [| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]

  [| P1.0 <=F Q1.0; Not_Decompo_Flag ∧ P2.0 <=F Q2.0 |]
  ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0

lemmas cspF_free_cong_flag:

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0

  [| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0

  [| X = Y; P =F Q |] ==> P -- X =F Q -- Y

  [| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]

  [| P1.0 =F Q1.0; Not_Decompo_Flag ∧ P2.0 =F Q2.0 |]
  ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0

lemmas cspF_free_cong_flag:

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0

  [| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0

  [| X = Y; P =F Q |] ==> P -- X =F Q -- Y

  [| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]

  [| P1.0 =F Q1.0; Not_Decompo_Flag ∧ P2.0 =F Q2.0 |]
  ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0

lemmas cspF_free_decompo_flag:

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0

  [| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0

  [| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y

  [| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]

  [| P1.0 <=F Q1.0; Not_Decompo_Flag ∧ P2.0 <=F Q2.0 |]
  ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0

  [| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0

  [| X = Y; P =F Q |] ==> P -- X =F Q -- Y

  [| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]

  [| P1.0 =F Q1.0; Not_Decompo_Flag ∧ P2.0 =F Q2.0 |]
  ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0

lemmas cspF_free_decompo_flag:

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0

  [| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0

  [| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0

  [| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y

  [| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]

  [| P1.0 <=F Q1.0; Not_Decompo_Flag ∧ P2.0 <=F Q2.0 |]
  ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0

  [| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0

  [| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0

  [| X = Y; P =F Q |] ==> P -- X =F Q -- Y

  [| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]

  [| P1.0 =F Q1.0; Not_Decompo_Flag ∧ P2.0 =F Q2.0 |]
  ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0

  [| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0