Theory CSP_F_law_SKIP_DIV

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

theory CSP_F_law_SKIP_DIV
imports CSP_F_law_SKIP CSP_F_law_DIV CSP_T_law_SKIP_DIV
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_SKIP_DIV = CSP_F_law_SKIP + CSP_F_law_DIV + CSP_T_law_SKIP_DIV:

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

lemma cspF_SKIP_DIV_Ext_choice1: "(SKIP [+] DIV) =F SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_DIV_Ext_choice)
apply (rule order_antisym)

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

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

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

lemma cspF_SKIP_DIV_Ext_choice2: "(DIV [+] SKIP) =F SKIP"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_SKIP_DIV_Ext_choice1)
done

lemmas cspF_SKIP_DIV_Ext_choice =
       cspF_SKIP_DIV_Ext_choice1
       cspF_SKIP_DIV_Ext_choice2

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

lemma cspF_SKIP_DIV_Parallel1:
   "SKIP |[X]| DIV =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_DIV_Parallel1)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)

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

lemma cspF_SKIP_DIV_Parallel2:
   "DIV |[X]| SKIP =F DIV"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_SKIP_DIV_Parallel1)
apply (rule cspF_reflex)
done

lemmas cspF_SKIP_DIV_Parallel =
       cspF_SKIP_DIV_Parallel1
       cspF_SKIP_DIV_Parallel2
       cspF_Parallel_term
       cspF_DIV_Parallel

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

(*********************************************************
                      SKIP and Parallel
 *********************************************************)

(*** SKIP and DIV ***)

lemma cspF_DIV_Parallel_Ext_choice_SKIP_l:
  "(P [+] SKIP) |[X]| DIV =F (P |[X]| DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Parallel_Ext_choice_SKIP_l)
apply (rule order_antisym)
apply (rule, simp add: in_failures)+
done

lemma cspF_DIV_Parallel_Ext_choice_SKIP_r:
  "DIV |[X]| (P [+] SKIP) =F (DIV |[X]| P)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_DIV_Parallel_Ext_choice_SKIP_l)
apply (rule cspF_commut)
done

lemmas cspF_DIV_Parallel_Ext_choice_SKIP =
       cspF_DIV_Parallel_Ext_choice_SKIP_l
       cspF_DIV_Parallel_Ext_choice_SKIP_r

lemmas cspF_DIV_Parallel_Ext_choice =
       cspF_DIV_Parallel_Ext_choice_SKIP
       cspF_DIV_Parallel_Ext_choice_DIV

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

(*** DIV and SKIP ***)

lemma cspF_SKIP_Parallel_Ext_choice_DIV_l:
  "((? :Y -> Pf) [+] DIV) |[X]| SKIP =F
   (? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Parallel_Ext_choice_DIV_l)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_failures)
 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_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)

  apply (simp add: par_tr_Tick_right)
  apply (elim conjE)
  apply (simp add: image_iff)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)

  apply (simp add: in_traces)

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

  apply (simp add: in_traces)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp add: par_tr_nil_right)
  apply (rule_tac x="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)
  apply (simp add: image_iff)
  apply (fast)

  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp add: par_tr_Tick_right)
  apply (rule_tac x="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)
  apply (simp add: image_iff)
  apply (fast)

  apply (simp add: in_traces)
  apply (simp add: in_traces)
done

lemma cspF_SKIP_Parallel_Ext_choice_DIV_r:
  "SKIP |[X]| ((? :Y -> Pf) [+] DIV) =F
   (? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_SKIP_Parallel_Ext_choice_DIV_l)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done

lemmas cspF_SKIP_Parallel_Ext_choice_DIV =
       cspF_SKIP_Parallel_Ext_choice_DIV_l
       cspF_SKIP_Parallel_Ext_choice_DIV_r

lemmas cspF_SKIP_Parallel_Ext_choice =
       cspF_SKIP_Parallel_Ext_choice_SKIP
       cspF_SKIP_Parallel_Ext_choice_DIV

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

lemmas cspF_SKIP_DIV_Parallel_step =
       cspF_Parallel_preterm
       cspF_DIV_Parallel_step

lemmas cspF_SKIP_DIV_Parallel_Ext_choice =
       cspF_SKIP_Parallel_Ext_choice
       cspF_DIV_Parallel_Ext_choice

lemmas cspF_SKIP_DIV_Hiding_Id =
       cspF_SKIP_Hiding_Id
       cspF_DIV_Hiding_Id

lemmas cspF_SKIP_DIV_Hiding_step =
       cspF_DIV_Hiding_step
       cspF_SKIP_Hiding_step

lemmas cspF_SKIP_DIV_Renaming_Id =
       cspF_SKIP_Renaming_Id
       cspF_DIV_Renaming_Id

lemmas cspF_SKIP_DIV_Seq_compo =
       cspF_Seq_compo_unit
       cspF_DIV_Seq_compo

lemmas cspF_SKIP_DIV_Seq_compo_step =
       cspF_SKIP_Seq_compo_step
       cspF_DIV_Seq_compo_step

lemmas cspF_SKIP_DIV_Depth_rest =
       cspF_SKIP_Depth_rest
       cspF_DIV_Depth_rest

lemmas cspF_SKIP_DIV =
       cspF_SKIP_DIV_Parallel_step
       cspF_SKIP_DIV_Ext_choice
       cspF_SKIP_DIV_Parallel
       cspF_SKIP_DIV_Parallel_Ext_choice
       cspF_SKIP_DIV_Hiding_Id
       cspF_SKIP_DIV_Hiding_step
       cspF_SKIP_DIV_Renaming_Id
       cspF_SKIP_DIV_Seq_compo
       cspF_SKIP_DIV_Seq_compo_step
       cspF_SKIP_DIV_Depth_rest

(*** resolve ***)

lemmas cspF_Ext_choice_SKIP_DIV_resolve =
       cspF_Ext_choice_SKIP_resolve
       cspF_Ext_choice_DIV_resolve

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

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

lemma cspF_SKIP_or_DIV_Ext_choice:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P [+] Q) =F (if (P = SKIP | Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp add: cspF_Ext_choice_idem)
apply (simp add: cspF_SKIP_DIV)
apply (simp add: cspF_Ext_choice_unit)
apply (simp add: cspF_SKIP_DIV)
apply (simp add: cspF_Ext_choice_unit)
apply (simp add: cspF_Ext_choice_idem)
done

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

lemma cspF_SKIP_or_DIV_Parallel:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P |[X]| Q) =F (if (P = SKIP & Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

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

lemma cspF_SKIP_or_DIV_Hiding_step:
  "Q = SKIP | Q = DIV ==>
   ((? :Y -> Pf) [+] Q) -- X =F 
   (((? x:(Y-X) -> (Pf x -- X)) [+] Q) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (erule disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

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

lemma cspF_SKIP_or_DIV_Depth_rest: 
   "Q = SKIP | Q = DIV ==> Q |. (Suc n) =F Q"
apply (erule disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

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

lemma cspF_Ext_choice_SKIP_or_DIV_resolve:
  "Q = SKIP | Q = DIV ==> P [+] Q =F P [> Q"
apply (erule disjE)
apply (simp_all add: cspF_Ext_choice_SKIP_DIV_resolve)
done

lemmas cspF_SKIP_or_DIV =
       cspF_SKIP_or_DIV_Ext_choice
       cspF_SKIP_or_DIV_Parallel
       cspF_SKIP_or_DIV_Hiding_step
       cspF_SKIP_or_DIV_Depth_rest

       (* no resolv *)

end

lemma cspF_SKIP_DIV_Ext_choice1: 

  SKIP [+] DIV =F SKIP

lemma cspF_SKIP_DIV_Ext_choice2: 

  DIV [+] SKIP =F SKIP

lemmas cspF_SKIP_DIV_Ext_choice: 

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

lemmas cspF_SKIP_DIV_Ext_choice: 

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

lemma cspF_SKIP_DIV_Parallel1: 

  SKIP |[X]| DIV =F DIV

lemma cspF_SKIP_DIV_Parallel2: 

  DIV |[X]| SKIP =F DIV

lemmas cspF_SKIP_DIV_Parallel: 

  SKIP |[X]| DIV =F DIV
  DIV |[X]| SKIP =F DIV
  SKIP |[X]| SKIP =F SKIP
  DIV |[X]| DIV =F DIV

lemmas cspF_SKIP_DIV_Parallel: 

  SKIP |[X]| DIV =F DIV
  DIV |[X]| SKIP =F DIV
  SKIP |[X]| SKIP =F SKIP
  DIV |[X]| DIV =F DIV

lemma cspF_DIV_Parallel_Ext_choice_SKIP_l: 

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

lemma cspF_DIV_Parallel_Ext_choice_SKIP_r: 

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

lemmas cspF_DIV_Parallel_Ext_choice_SKIP: 

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

lemmas cspF_DIV_Parallel_Ext_choice_SKIP: 

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

lemmas cspF_DIV_Parallel_Ext_choice: 

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

lemmas cspF_DIV_Parallel_Ext_choice: 

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

lemma cspF_SKIP_Parallel_Ext_choice_DIV_l: 

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

lemma cspF_SKIP_Parallel_Ext_choice_DIV_r: 

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

lemmas cspF_SKIP_Parallel_Ext_choice_DIV: 

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

lemmas cspF_SKIP_Parallel_Ext_choice_DIV: 

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

lemmas cspF_SKIP_Parallel_Ext_choice: 

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

lemmas cspF_SKIP_Parallel_Ext_choice: 

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

lemmas cspF_SKIP_DIV_Parallel_step: 

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

lemmas cspF_SKIP_DIV_Parallel_step: 

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

lemmas cspF_SKIP_DIV_Parallel_Ext_choice: 

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

lemmas cspF_SKIP_DIV_Parallel_Ext_choice: 

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

lemmas cspF_SKIP_DIV_Hiding_Id: 

  SKIP -- X =F SKIP
  DIV -- X =F DIV

lemmas cspF_SKIP_DIV_Hiding_Id: 

  SKIP -- X =F SKIP
  DIV -- X =F DIV

lemmas cspF_SKIP_DIV_Hiding_step: 

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

lemmas cspF_SKIP_DIV_Hiding_step: 

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

lemmas cspF_SKIP_DIV_Renaming_Id: 

  SKIP [[r]] =F SKIP
  DIV [[r]] =F DIV

lemmas cspF_SKIP_DIV_Renaming_Id: 

  SKIP [[r]] =F SKIP
  DIV [[r]] =F DIV

lemmas cspF_SKIP_DIV_Seq_compo: 

  SKIP ;; P =F P
  P ;; SKIP =F P
  DIV ;; P =F DIV

lemmas cspF_SKIP_DIV_Seq_compo: 

  SKIP ;; P =F P
  P ;; SKIP =F P
  DIV ;; P =F DIV

lemmas cspF_SKIP_DIV_Seq_compo_step: 

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

lemmas cspF_SKIP_DIV_Seq_compo_step: 

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

lemmas cspF_SKIP_DIV_Depth_rest: 

  SKIP |. Suc n =F SKIP
  DIV |. n =F DIV

lemmas cspF_SKIP_DIV_Depth_rest: 

  SKIP |. Suc n =F SKIP
  DIV |. n =F DIV

lemmas cspF_SKIP_DIV: 

  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)
  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)
  DIV |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV
  ? :Y -> Qf |[X]| DIV =F ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV
  SKIP [+] DIV =F SKIP
  DIV [+] SKIP =F SKIP
  SKIP |[X]| DIV =F DIV
  DIV |[X]| SKIP =F DIV
  SKIP |[X]| SKIP =F SKIP
  DIV |[X]| DIV =F DIV
  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP
  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP
  (? :Y -> Pf [+] DIV) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV
  SKIP |[X]| (? :Y -> Pf [+] DIV) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV
  (P [+] SKIP) |[X]| DIV =F P |[X]| DIV
  DIV |[X]| (P [+] SKIP) =F DIV |[X]| P
  (P [+] DIV) |[X]| DIV =F P |[X]| DIV
  DIV |[X]| (P [+] DIV) =F DIV |[X]| P
  SKIP -- X =F SKIP
  DIV -- X =F DIV
  (? :Y -> Pf [+] DIV) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X
  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X
  SKIP [[r]] =F SKIP
  DIV [[r]] =F DIV
  SKIP ;; P =F P
  P ;; SKIP =F P
  DIV ;; P =F DIV
  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q
  (? :X -> Pf [> DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [> DIV
  SKIP |. Suc n =F SKIP
  DIV |. n =F DIV

lemmas cspF_SKIP_DIV: 

  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)
  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)
  DIV |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV
  ? :Y -> Qf |[X]| DIV =F ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV
  SKIP [+] DIV =F SKIP
  DIV [+] SKIP =F SKIP
  SKIP |[X]| DIV =F DIV
  DIV |[X]| SKIP =F DIV
  SKIP |[X]| SKIP =F SKIP
  DIV |[X]| DIV =F DIV
  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP
  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP
  (? :Y -> Pf [+] DIV) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV
  SKIP |[X]| (? :Y -> Pf [+] DIV) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV
  (P [+] SKIP) |[X]| DIV =F P |[X]| DIV
  DIV |[X]| (P [+] SKIP) =F DIV |[X]| P
  (P [+] DIV) |[X]| DIV =F P |[X]| DIV
  DIV |[X]| (P [+] DIV) =F DIV |[X]| P
  SKIP -- X =F SKIP
  DIV -- X =F DIV
  (? :Y -> Pf [+] DIV) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X
  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X
  SKIP [[r]] =F SKIP
  DIV [[r]] =F DIV
  SKIP ;; P =F P
  P ;; SKIP =F P
  DIV ;; P =F DIV
  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q
  (? :X -> Pf [> DIV) ;; Q =F ? x:X -> (Pf x ;; Q) [> DIV
  SKIP |. Suc n =F SKIP
  DIV |. n =F DIV

lemmas cspF_Ext_choice_SKIP_DIV_resolve: 

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

lemmas cspF_Ext_choice_SKIP_DIV_resolve: 

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

lemma cspF_SKIP_or_DIV_Ext_choice: 

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =F (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

lemma cspF_SKIP_or_DIV_Parallel: 

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =F (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

lemma cspF_SKIP_or_DIV_Hiding_step: 

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

lemma cspF_SKIP_or_DIV_Depth_rest: 

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =F Q

lemma cspF_Ext_choice_SKIP_or_DIV_resolve: 

  Q = SKIP ∨ Q = DIV ==> P [+] Q =F P [> Q

lemmas cspF_SKIP_or_DIV: 

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =F (if P = SKIP ∨ Q = SKIP then SKIP else DIV)
  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =F (if P = SKIP ∧ Q = SKIP then SKIP else DIV)
  Q = SKIP ∨ Q = DIV
  ==> (? :Y -> Pf [+] Q) -- X =F 
      ? x:(Y - X) -> Pf x -- X [+] Q |~| ! x:(Y ∩ X) .. Pf x -- X
  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =F Q

lemmas cspF_SKIP_or_DIV: 

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =F (if P = SKIP ∨ Q = SKIP then SKIP else DIV)
  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =F (if P = SKIP ∧ Q = SKIP then SKIP else DIV)
  Q = SKIP ∨ Q = DIV
  ==> (? :Y -> Pf [+] Q) -- X =F 
      ? x:(Y - X) -> Pf x -- X [+] Q |~| ! x:(Y ∩ X) .. Pf x -- X
  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =F Q