Theory CSP_T_law_SKIP_DIV (Isabelle2005: October 2005)

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

theory CSP_T_law_SKIP_DIV
imports CSP_T_law_SKIP CSP_T_law_DIV
begin

(*********************************************************
                   (SKIP [+] DIV)
 *********************************************************)

lemma cspT_SKIP_DIV_Ext_choice1: "(SKIP [+] DIV) =T[M1,M2] SKIP"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces)
done

lemma cspT_SKIP_DIV_Ext_choice2: "(DIV [+] SKIP) =T[M1,M2] SKIP"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

lemmas cspT_SKIP_DIV_Ext_choice =
       cspT_SKIP_DIV_Ext_choice1
       cspT_SKIP_DIV_Ext_choice2

(*********************************************************
                    SKIP |[X]| DIV
 *********************************************************)

lemma cspT_SKIP_DIV_Parallel1:
   "SKIP |[X]| DIV =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE)
 apply (simp_all)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
done

lemma cspT_SKIP_DIV_Parallel2:
   "DIV |[X]| SKIP =T[M1,M2] DIV"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_SKIP_DIV_Parallel1)
apply (rule cspT_reflex)
done

lemmas cspT_SKIP_DIV_Parallel =
       cspT_SKIP_DIV_Parallel1
       cspT_SKIP_DIV_Parallel2
       cspT_Parallel_term
       cspT_DIV_Parallel

(*********************************************************
                 DIV and Parallel-SKIP
 *********************************************************)

(*** SKIP and DIV ***)

lemma cspT_DIV_Parallel_Ext_choice_SKIP_l:
  "(P [+] SKIP) |[X]| DIV =T[M,M] (P |[X]| DIV)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces)
 apply (elim conjE exE disjE)
 apply (simp_all)
  apply (simp add: par_tr_nil_right)
  apply (elim conjE)
  apply (simp add: image_iff)

(* <= *)
 apply (rule, simp add: in_traces)
 apply (elim conjE exE disjE)
  apply (simp add: par_tr_nil_right)
  apply (elim conjE)
  apply (simp add: image_iff)
done

lemma cspT_DIV_Parallel_Ext_choice_SKIP_r:
  "DIV |[X]| (P [+] SKIP) =T[M,M] (DIV |[X]| P)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_DIV_Parallel_Ext_choice_SKIP_l)
apply (rule cspT_commut)
done

lemmas cspT_DIV_Parallel_Ext_choice_SKIP =
       cspT_DIV_Parallel_Ext_choice_SKIP_l
       cspT_DIV_Parallel_Ext_choice_SKIP_r

lemmas cspT_DIV_Parallel_Ext_choice =
       cspT_DIV_Parallel_Ext_choice_SKIP
       cspT_DIV_Parallel_Ext_choice_DIV

(*********************************************************
                 SKIP and Parallel-DIV
 *********************************************************)

(*** DIV and SKIP ***)

lemma cspT_SKIP_Parallel_Ext_choice_DIV_l:
  "((? :Y -> Pf) [+] DIV) |[X]| SKIP =T[M,M] 
   (? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces)
 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (rule disjI2)
  apply (simp add: par_tr_nil_right)
  apply (elim conjE)
  apply (simp add: image_iff)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)

  apply (rule disjI2)
  apply (simp add: par_tr_Tick_right)
  apply (elim conjE)
  apply (simp add: image_iff)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)

(* <= *)
 apply (rule, simp add: in_traces)
 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (simp add: par_tr_nil_right)
  apply (elim conjE)
  apply (rule_tac x="<Ev a> ^^ sa" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)
  apply (simp add: image_iff)

  apply (simp add: par_tr_Tick_right)
  apply (elim conjE)
  apply (rule_tac x="<Ev a> ^^ sa" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)
  apply (simp add: image_iff)
done

lemma cspT_SKIP_Parallel_Ext_choice_DIV_r:
  "SKIP |[X]| ((? :Y -> Pf) [+] DIV) =T[M,M]
   (? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] DIV"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_SKIP_Parallel_Ext_choice_DIV_l)
apply (rule cspT_rw_left)
apply (rule cspT_decompo)
apply (rule cspT_decompo)
apply (simp)
apply (rule cspT_commut)
apply (rule cspT_reflex)
apply (rule cspT_reflex)
done

lemmas cspT_SKIP_Parallel_Ext_choice_DIV =
       cspT_SKIP_Parallel_Ext_choice_DIV_l
       cspT_SKIP_Parallel_Ext_choice_DIV_r

lemmas cspT_SKIP_Parallel_Ext_choice =
       cspT_SKIP_Parallel_Ext_choice_SKIP
       cspT_SKIP_Parallel_Ext_choice_DIV

(*---------------------------------------------*
 |                 SKIP , DIV                  |
 *---------------------------------------------*)

lemmas cspT_SKIP_DIV_Parallel_step =
       cspT_Parallel_preterm
       cspT_DIV_Parallel_step

lemmas cspT_SKIP_DIV_Parallel_Ext_choice =
       cspT_SKIP_Parallel_Ext_choice
       cspT_DIV_Parallel_Ext_choice

lemmas cspT_SKIP_DIV_Hiding_Id =
       cspT_SKIP_Hiding_Id
       cspT_DIV_Hiding_Id

lemmas cspT_SKIP_DIV_Hiding_step =
       cspT_DIV_Hiding_step
       cspT_SKIP_Hiding_step

lemmas cspT_SKIP_DIV_Renaming_Id =
       cspT_SKIP_Renaming_Id
       cspT_DIV_Renaming_Id

lemmas cspT_SKIP_DIV_Seq_compo =
       cspT_Seq_compo_unit
       cspT_DIV_Seq_compo

lemmas cspT_SKIP_DIV_Seq_compo_step =
       cspT_SKIP_Seq_compo_step
       cspT_DIV_Seq_compo_step

lemmas cspT_SKIP_DIV_Depth_rest =
       cspT_SKIP_Depth_rest
       cspT_DIV_Depth_rest

lemmas cspT_SKIP_DIV =
       cspT_SKIP_DIV_Parallel_step
       cspT_SKIP_DIV_Ext_choice
       cspT_SKIP_DIV_Parallel
       cspT_SKIP_DIV_Parallel_Ext_choice
       cspT_SKIP_DIV_Hiding_Id
       cspT_SKIP_DIV_Hiding_step
       cspT_SKIP_DIV_Renaming_Id
       cspT_SKIP_DIV_Seq_compo
       cspT_SKIP_DIV_Seq_compo_step
       cspT_SKIP_DIV_Depth_rest

(*** resolve ***)

lemmas cspT_Ext_choice_SKIP_DIV_resolve =
       cspT_Ext_choice_SKIP_resolve
       cspT_Ext_choice_DIV_resolve

(*----------------------------------------------*
 |                                              |
 |        for convenienve  (SKIP or DIV)        |
 |                                              |
 *----------------------------------------------*)

(*********************************************************
            (SKIP or DIV [+] SKIP or DIV)
 *********************************************************)

lemma cspT_SKIP_or_DIV_Ext_choice:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P [+] Q) =T[M1,M2] (if (P = SKIP | Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all)
apply (rule cspT_rw_left)
apply (rule cspT_Ext_choice_idem)
apply (simp)
apply (simp add: cspT_SKIP_DIV)
apply (simp add: cspT_SKIP_DIV)
apply (rule cspT_rw_left)
apply (rule cspT_Ext_choice_idem)
apply (simp)
done

(*********************************************************
            (SKIP or DIV |[X]| SKIP or DIV)
 *********************************************************)

lemma cspT_SKIP_or_DIV_Parallel:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P |[X]| Q) =T[M1,M2] (if (P = SKIP & Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all add: cspT_SKIP_DIV)
done

(*********************************************************
                  (SKIP or DIV) and Hiding
 *********************************************************)

lemma cspT_SKIP_or_DIV_Hiding_step:
  "Q = SKIP | Q = DIV ==>
   ((? :Y -> Pf) [+] Q) -- X =T[M,M] 
   (((? x:(Y-X) -> (Pf x -- X)) [+] Q) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (erule disjE)
apply (simp_all add: cspT_SKIP_DIV)
done

(*********************************************************
                  SKIP or DIV |. Suc n
 *********************************************************)

lemma cspT_SKIP_or_DIV_Depth_rest: 
   "Q = SKIP | Q = DIV ==> Q |. (Suc n) =T[M1,M2] Q"
apply (erule disjE)
apply (simp_all add: cspT_SKIP_DIV)
done

(*********************************************************
                    P [+] (SKIP or DIV)
 *********************************************************)

lemma cspT_Ext_choice_SKIP_or_DIV_resolve:
  "Q = SKIP | Q = DIV ==> P [+] Q =T[M,M] P [> Q"
apply (erule disjE)
apply (simp_all add: cspT_Ext_choice_SKIP_DIV_resolve)
done

lemmas cspT_SKIP_or_DIV =
       cspT_SKIP_or_DIV_Ext_choice
       cspT_SKIP_or_DIV_Parallel
       cspT_SKIP_or_DIV_Hiding_step
       cspT_SKIP_or_DIV_Depth_rest

       (* no resolve *)

end

lemma cspT_SKIP_DIV_Ext_choice1:

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

lemma cspT_SKIP_DIV_Ext_choice2:

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

lemmas cspT_SKIP_DIV_Ext_choice:

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

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

lemmas cspT_SKIP_DIV_Ext_choice:

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

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

lemma cspT_SKIP_DIV_Parallel1:

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

lemma cspT_SKIP_DIV_Parallel2:

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

lemmas cspT_SKIP_DIV_Parallel:

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

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

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

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

lemmas cspT_SKIP_DIV_Parallel:

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

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

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

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

lemma cspT_DIV_Parallel_Ext_choice_SKIP_l:

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

lemma cspT_DIV_Parallel_Ext_choice_SKIP_r:

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

lemmas cspT_DIV_Parallel_Ext_choice_SKIP:

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

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

lemmas cspT_DIV_Parallel_Ext_choice_SKIP:

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

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

lemmas cspT_DIV_Parallel_Ext_choice:

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

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

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

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

lemmas cspT_DIV_Parallel_Ext_choice:

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

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

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

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

lemma cspT_SKIP_Parallel_Ext_choice_DIV_l:

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

lemma cspT_SKIP_Parallel_Ext_choice_DIV_r:

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

lemmas cspT_SKIP_Parallel_Ext_choice_DIV:

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

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

lemmas cspT_SKIP_Parallel_Ext_choice_DIV:

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

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

lemmas cspT_SKIP_Parallel_Ext_choice:

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

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

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

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

lemmas cspT_SKIP_Parallel_Ext_choice:

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

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

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

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

lemmas cspT_SKIP_DIV_Parallel_step:

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

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

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

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

lemmas cspT_SKIP_DIV_Parallel_step:

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

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

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

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

lemmas cspT_SKIP_DIV_Parallel_Ext_choice:

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

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

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

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

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

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

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

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

lemmas cspT_SKIP_DIV_Parallel_Ext_choice:

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

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

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

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

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

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

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

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

lemmas cspT_SKIP_DIV_Hiding_Id:

  SKIP -- X =T[M1.0,M2.0] SKIP

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

lemmas cspT_SKIP_DIV_Hiding_Id:

  SKIP -- X =T[M1.0,M2.0] SKIP

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

lemmas cspT_SKIP_DIV_Hiding_step:

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

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

lemmas cspT_SKIP_DIV_Hiding_step:

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

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

lemmas cspT_SKIP_DIV_Renaming_Id:

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

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

lemmas cspT_SKIP_DIV_Renaming_Id:

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

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

lemmas cspT_SKIP_DIV_Seq_compo:

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

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

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

lemmas cspT_SKIP_DIV_Seq_compo:

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

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

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

lemmas cspT_SKIP_DIV_Seq_compo_step:

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

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

lemmas cspT_SKIP_DIV_Seq_compo_step:

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

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

lemmas cspT_SKIP_DIV_Depth_rest:

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

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

lemmas cspT_SKIP_DIV_Depth_rest:

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

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

lemmas cspT_SKIP_DIV:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  SKIP -- X =T[M1.0,M2.0] SKIP

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

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

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

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

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

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

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

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

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

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

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

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

lemmas cspT_SKIP_DIV:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  SKIP -- X =T[M1.0,M2.0] SKIP

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

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

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

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

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

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

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

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

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

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

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

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

lemmas cspT_Ext_choice_SKIP_DIV_resolve:

  P [+] SKIP =T[M,M] P [> SKIP

  P [+] DIV =T[M,M] P [> DIV

lemmas cspT_Ext_choice_SKIP_DIV_resolve:

  P [+] SKIP =T[M,M] P [> SKIP

  P [+] DIV =T[M,M] P [> DIV

lemma cspT_SKIP_or_DIV_Ext_choice:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =T[M1.0,M2.0] (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

lemma cspT_SKIP_or_DIV_Parallel:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =T[M1.0,M2.0] (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

lemma cspT_SKIP_or_DIV_Hiding_step:

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

lemma cspT_SKIP_or_DIV_Depth_rest:

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =T[M1.0,M2.0] Q

lemma cspT_Ext_choice_SKIP_or_DIV_resolve:

  Q = SKIP ∨ Q = DIV ==> P [+] Q =T[M,M] P [> Q

lemmas cspT_SKIP_or_DIV:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =T[M1.0,M2.0] (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =T[M1.0,M2.0] (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

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

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =T[M1.0,M2.0] Q

lemmas cspT_SKIP_or_DIV:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =T[M1.0,M2.0] (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =T[M1.0,M2.0] (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

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

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =T[M1.0,M2.0] Q