Theory CSP_F_law_aux (Isabelle2005: October 2005)

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

theory CSP_F_law_aux
imports CSP_F_law
begin

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

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

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

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

lemma cspF_Rep_int_choice_sum1_singleton:
  "!! : type1 {c} .. Pf =F[M,M] Pf (type1 c)"
by (rule cspF_Rep_int_choice_const, auto)

lemma cspF_Rep_int_choice_sum2_singleton:
  "!! : type2 {c} .. Pf =F[M,M] Pf (type2 c)"
by (rule cspF_Rep_int_choice_const, auto)

lemma cspF_Rep_int_choice_nat_singleton:
  "!nat :{n} .. Pf =F[M,M] Pf n"
by (rule cspF_Rep_int_choice_const, auto)

lemma cspF_Rep_int_choice_set_singleton:
  "!set :{X} .. Pf =F[M,M] Pf X"
by (rule cspF_Rep_int_choice_const, auto)

lemma cspF_Rep_int_choice_com_singleton:
  "! :{a} .. Pf =F[M,M] Pf a"
by (rule cspF_Rep_int_choice_const, auto)

lemma cspF_Rep_int_choice_f_singleton:
  "inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x"
by (rule cspF_Rep_int_choice_const, auto)

lemmas cspF_Rep_int_choice_singleton =
       cspF_Rep_int_choice_sum1_singleton
       cspF_Rep_int_choice_sum2_singleton
       cspF_Rep_int_choice_nat_singleton
       cspF_Rep_int_choice_set_singleton
       cspF_Rep_int_choice_com_singleton
       cspF_Rep_int_choice_f_singleton

lemma cspF_Rep_int_choice_const_sum_rule:
  "!! c:C .. P =F[M,M] IF (sumset C={}) THEN DIV ELSE P"
apply (case_tac "sumset C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Rep_int_choice_empty)
apply (simp)
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_nat_rule:
  "!nat n:N .. P =F[M,M] IF (N={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_ss_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_sum_rule)
by (simp)

lemma cspF_Rep_int_choice_const_set_rule:
  "!set X:Xs .. P =F[M,M] IF (Xs={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_ss_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_sum_rule)
by (simp)

lemma cspF_Rep_int_choice_const_com_rule:
  "! x:X .. P =F[M,M] 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_set_rule)
by (simp)

lemma cspF_Rep_int_choice_const_f_rule:
  "!<f> x:X .. P =F[M,M] IF (X={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_com_rule)
by (simp)

lemmas cspF_Rep_int_choice_const_rule =
       cspF_Rep_int_choice_const_sum_rule
       cspF_Rep_int_choice_const_nat_rule
       cspF_Rep_int_choice_const_set_rule
       cspF_Rep_int_choice_const_com_rule
       cspF_Rep_int_choice_const_f_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[M1,M2] ? 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[M,M] 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[M,M] 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[M1,M2] Q1 ; P <=F[M1,M2] Q2 |] ==> P <=F[M1,M2] 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[M,M] 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M]
     (? 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[M,M] (? 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[M,M] (? 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[M,M] (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[M,M] (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[M,M] 
   (? 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[M,M] 
   (? 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[M,M] 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[M,M] 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[M,M] (? :X -> Pf) [+] SKIP"
by (rule cspF_commut)

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

lemma cspF_Ext_pre_choice_SKIP_assoc:
  "((? :X -> Pf) [+] SKIP) [+] (? :Y -> Qf)
   =F[M,M] ((? :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[M,M] ((? :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[M,M] (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[M,M] (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[M,M] (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[M1,M1] R2 ; Not_Decompo_Flag & R2 =F[M1,M3] R3 |] ==> R1 =F[M1,M3] R3"
by (simp add: eqF_def Not_Decompo_Flag_def)

lemma cspF_rw_flag_left_ref:
  "[| R1 =F[M1,M1] R2 ; Not_Decompo_Flag & R2 <=F[M1,M3] R3 |] ==> R1 <=F[M1,M3] 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[M3,M3] R2 ; Not_Decompo_Flag & R1 =F[M1,M3] R2 |] ==> R1 =F[M1,M3] R3"
by (simp add: eqF_def Not_Decompo_Flag_def)

lemma cspF_rw_flag_right_ref:
  "[| R3 =F[M3,M3] R2 ; Not_Decompo_Flag & R1 <=F[M1,M3] R2 |] ==> R1 <=F[M1,M3] 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

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

lemma cspF_tr_flag_left_eq:
   "[| P1 =F[M1,M1] P2 ; Not_Decompo_Flag & P2 =F[M1,M3] P3 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)

lemma cspF_tr_flag_left_ref:
   "[| P1 <=F[M1,M1] P2 ; Not_Decompo_Flag & P2 <=F[M1,M3] P3 |] ==> P1 <=F[M1,M3] P3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)

lemmas cspF_tr_flag_left = cspF_tr_flag_left_eq cspF_tr_flag_left_ref

lemma cspF_tr_flag_right_eq:
   "[| P2 =F[M3,M3] P3 ; Not_Decompo_Flag & P1 =F[M1,M3] P2 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)

lemma cspF_tr_flag_right_ref:
  "[| P2 <=F[M3,M3] P3 ; Not_Decompo_Flag & P1 <=F[M1,M3] P2 |] ==> P1 <=F[M1,M3] P3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)

lemmas cspF_tr_flag_right = cspF_tr_flag_right_eq cspF_tr_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[M1,M2] Q1 ; 
      Not_Decompo_Flag & P2 <=F[M1,M2] Q2 |]
           ==> P1 ;; P2 <=F[M1,M2] Q1 ;; Q2"
by (simp add: cspF_Seq_compo_mono)

lemma cspF_Seq_compo_cong_flag:
  "[| P1 =F[M1,M2] Q1 ; 
      Not_Decompo_Flag & P2 =F[M1,M2] Q2 |]
           ==> P1 ;; P2 =F[M1,M2] 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_choice_sum1_singleton:

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

lemma cspF_Rep_int_choice_sum2_singleton:

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

lemma cspF_Rep_int_choice_nat_singleton:

  !nat :{n} .. Pf =F[M,M] Pf n

lemma cspF_Rep_int_choice_set_singleton:

  !set :{X} .. Pf =F[M,M] Pf X

lemma cspF_Rep_int_choice_com_singleton:

  ! :{a} .. Pf =F[M,M] Pf a

lemma cspF_Rep_int_choice_f_singleton:

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

lemmas cspF_Rep_int_choice_singleton:

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

lemmas cspF_Rep_int_choice_singleton:

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

lemma cspF_Rep_int_choice_const_sum_rule:

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

lemma cspF_Rep_int_choice_const_nat_rule:

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

lemma cspF_Rep_int_choice_const_set_rule:

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

lemma cspF_Rep_int_choice_const_com_rule:

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

lemma cspF_Rep_int_choice_const_f_rule:

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

lemmas cspF_Rep_int_choice_const_rule:

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

lemmas cspF_Rep_int_choice_const_rule:

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

lemmas cspF_Int_choice_rule:

  sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV

  !nat :{} .. Pf =F[M1.0,M2.0] DIV

  !set :{} .. Pf =F[M1.0,M2.0] DIV

  ! :{} .. Pf =F[M1.0,M2.0] DIV

  inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

  P |~| P =F[M,M] P

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

lemmas cspF_Int_choice_rule:

  sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV

  !nat :{} .. Pf =F[M1.0,M2.0] DIV

  !set :{} .. Pf =F[M1.0,M2.0] DIV

  ! :{} .. Pf =F[M1.0,M2.0] DIV

  inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

  P |~| P =F[M,M] P

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

lemma cspF_Ext_pre_choice_empty_DIV:

  ? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV

lemma cspF_Ext_choice_unit_l_hsf:

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

lemma cspF_Ext_choice_unit_r_hsf:

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

lemmas cspF_Ext_choice_rule:

  ? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV

  STOP [+] P =F[M,M] P

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

  P [+] STOP =F[M,M] P

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

  P [+] P =F[M,M] P

lemmas cspF_Ext_choice_rule:

  ? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV

  STOP [+] P =F[M,M] P

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

  P [+] STOP =F[M,M] P

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

  P [+] P =F[M,M] P

lemmas cspF_choice_rule:

  sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV

  !nat :{} .. Pf =F[M1.0,M2.0] DIV

  !set :{} .. Pf =F[M1.0,M2.0] DIV

  ! :{} .. Pf =F[M1.0,M2.0] DIV

  inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

  P |~| P =F[M,M] P

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

  ? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV

  STOP [+] P =F[M,M] P

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

  P [+] STOP =F[M,M] P

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

  P [+] P =F[M,M] P

lemmas cspF_choice_rule:

  sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV

  !nat :{} .. Pf =F[M1.0,M2.0] DIV

  !set :{} .. Pf =F[M1.0,M2.0] DIV

  ! :{} .. Pf =F[M1.0,M2.0] DIV

  inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV

  !! :type1 {c} .. Pf =F[M,M] Pf (type1 c)

  !! :type2 {c} .. Pf =F[M,M] Pf (type2 c)

  !nat :{n} .. Pf =F[M,M] Pf n

  !set :{X} .. Pf =F[M,M] Pf X

  ! :{a} .. Pf =F[M,M] Pf a

  inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x

  P |~| P =F[M,M] P

  !! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P

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

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

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

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

  ? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV

  STOP [+] P =F[M,M] P

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

  P [+] STOP =F[M,M] P

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

  P [+] P =F[M,M] P

lemma cspF_Timeout_right:

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

lemma cspF_STOP_Timeout:

  STOP [> P =F[M,M] 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[M,M] 
      ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] ? x:X -> (Pf x ;; Q) [> Q

lemma cspF_DIV_Seq_compo_step_resolve:

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

lemmas cspF_SKIP_DIV_Seq_compo_step_resolve:

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

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

lemmas cspF_SKIP_DIV_Seq_compo_step_resolve:

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

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

lemmas cspF_SKIP_DIV_resolve:

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

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

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

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

  SKIP [+] DIV =F[M1.0,M2.0] SKIP

  DIV [+] SKIP =F[M1.0,M2.0] SKIP

  SKIP |[X]| DIV =F[M1.0,M2.0] DIV

  DIV |[X]| SKIP =F[M1.0,M2.0] DIV

  SKIP |[X]| SKIP =F[M1.0,M2.0] SKIP

  DIV |[X]| DIV =F[M1.0,M2.0] DIV

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

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

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

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

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

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

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

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

  SKIP -- X =F[M,M] SKIP

  DIV -- X =F[M1.0,M2.0] DIV

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

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

  SKIP [[r]] =F[M1.0,M2.0] SKIP

  DIV [[r]] =F[M1.0,M2.0] DIV

  SKIP ;; P =F[M,M] P

  P ;; SKIP =F[M,M] P

  DIV ;; P =F[M1.0,M2.0] DIV

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

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

  SKIP |. Suc n =F[M1.0,M2.0] SKIP

  DIV |. n =F[M1.0,M2.0] DIV

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] ? x:X -> (Pf x ;; Q) [> Q

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

lemmas cspF_SKIP_DIV_resolve:

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

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

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

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

  SKIP [+] DIV =F[M1.0,M2.0] SKIP

  DIV [+] SKIP =F[M1.0,M2.0] SKIP

  SKIP |[X]| DIV =F[M1.0,M2.0] DIV

  DIV |[X]| SKIP =F[M1.0,M2.0] DIV

  SKIP |[X]| SKIP =F[M1.0,M2.0] SKIP

  DIV |[X]| DIV =F[M1.0,M2.0] DIV

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

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

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

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

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

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

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

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

  SKIP -- X =F[M,M] SKIP

  DIV -- X =F[M1.0,M2.0] DIV

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

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

  SKIP [[r]] =F[M1.0,M2.0] SKIP

  DIV [[r]] =F[M1.0,M2.0] DIV

  SKIP ;; P =F[M,M] P

  P ;; SKIP =F[M,M] P

  DIV ;; P =F[M1.0,M2.0] DIV

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

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

  SKIP |. Suc n =F[M1.0,M2.0] SKIP

  DIV |. n =F[M1.0,M2.0] DIV

  (? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] 
  ? 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[M,M] ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [+] DIV) ;; Q =F[M,M] ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 
      ? 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[M,M] 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[M,M] 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[M,M] P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F[M,M] 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[M,M] P |[X]| DIV

  Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F[M,M] 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[M,M] ? 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[M,M] ? 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[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? 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[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? 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[M,M] P |[X]| DIV

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

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

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? 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[M,M] P |[X]| DIV

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

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

  Q = SKIP ∨ Q = DIV ∨ Q = STOP
  ==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? 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[M,M] P

lemma cspF_STOP_Depth_rest:

  STOP |. Suc n =F[M,M] STOP

lemma cspF_Ext_pre_choice_SKIP_commut:

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

lemma cspF_Ext_pre_choice_DIV_commut:

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

lemma cspF_Ext_pre_choice_SKIP_assoc:

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

lemma cspF_Ext_pre_choice_DIV_assoc:

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

lemma cspF_Ext_choice_idem_assoc:

  P [+] Q [+] Q =F[M,M] P [+] Q

lemma cspF_Ext_choice_SKIP_DIV_assoc:

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

lemma cspF_Ext_choice_DIV_SKIP_assoc:

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

lemmas cspF_SKIP_DIV_sort:

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

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

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

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

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

  P [+] Q [+] Q =F[M,M] P [+] Q

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

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

lemmas cspF_SKIP_DIV_sort:

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

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

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

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

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

  P [+] Q [+] Q =F[M,M] P [+] Q

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

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

lemma cspF_rw_flag_left_eq:

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

lemma cspF_rw_flag_left_ref:

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

lemmas cspF_rw_flag_left:

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

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

lemmas cspF_rw_flag_left:

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

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

lemma cspF_rw_flag_right_eq:

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

lemma cspF_rw_flag_right_ref:

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

lemmas cspF_rw_flag_right:

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

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

lemmas cspF_rw_flag_right:

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

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

lemma cspF_tr_flag_left_eq:

  [| P1.0 =F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M3.0] P3.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

lemma cspF_tr_flag_left_ref:

  [| P1.0 <=F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M3.0] P3.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemmas cspF_tr_flag_left:

  [| P1.0 =F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M3.0] P3.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

  [| P1.0 <=F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M3.0] P3.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemmas cspF_tr_flag_left:

  [| P1.0 =F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M3.0] P3.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

  [| P1.0 <=F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M3.0] P3.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemma cspF_tr_flag_right_eq:

  [| P2.0 =F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 =F[M1.0,M3.0] P2.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

lemma cspF_tr_flag_right_ref:

  [| P2.0 <=F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 <=F[M1.0,M3.0] P2.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemmas cspF_tr_flag_right:

  [| P2.0 =F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 =F[M1.0,M3.0] P2.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

  [| P2.0 <=F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 <=F[M1.0,M3.0] P2.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemmas cspF_tr_flag_right:

  [| P2.0 =F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 =F[M1.0,M3.0] P2.0 |]
  ==> P1.0 =F[M1.0,M3.0] P3.0

  [| P2.0 <=F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 <=F[M1.0,M3.0] P2.0 |]
  ==> P1.0 <=F[M1.0,M3.0] P3.0

lemma cspF_Seq_compo_mono_flag:

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

lemma cspF_Seq_compo_cong_flag:

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

lemmas cspF_free_mono_flag:

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

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

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

  [| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y

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

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

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

lemmas cspF_free_mono_flag:

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

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

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

  [| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y

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

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

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

lemmas cspF_free_cong_flag:

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

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

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

  [| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y

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

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

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

lemmas cspF_free_cong_flag:

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

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

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

  [| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y

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

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

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

lemmas cspF_free_decompo_flag:

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

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

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

  [| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y

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

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

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

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

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

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

  [| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y

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

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

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

lemmas cspF_free_decompo_flag:

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

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

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

  [| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y

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

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

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

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

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

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

  [| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y

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

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

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