Theory CSP_F

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |               February 2005  (modified)   |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F
imports CSP_F_tactic CSP_F_surj CSP_T CSP_F_T_domain CSP_F_MF_MT
begin

(*--------------------------------------------*
 |                                            |
 |    decomposition considering refinement    |
 |                                            |
 *--------------------------------------------*)

lemmas cspF_mono_ref = cspF_free_mono
   cspF_Act_prefix_mono cspF_Ext_pre_choice_mono 
   cspF_IF_mono cspF_decompo_subset

lemmas cspF_decompo_ref = cspF_mono_ref cspF_cong

(*-------------------------------------------------------*
 |                                                       |
 |  The folloing def have already added in CSP_T         |
 |                                                       |
 |   Procfun_def                                         |
 |   ProcX_def                                           |
 |   gSKIPX_def                                          |
 |   gProcX_def                                          |
 |   nohideX_def                                         |
 |                                                       |
 *-------------------------------------------------------*)

(*----------------------------------------------------------------------*
 |                                                                      |
 |  To unfold (resp. fold) syntactic-sugar for Ext_ and Int_pre_choices |
 |  choices, use "unfold csp_prefix_ss_def"                             |
 |                                                                      |
 *----------------------------------------------------------------------*)

(*------------------------------------*
 |                                    |
 |    laws automatically applied      |
 |                                    |
 *------------------------------------*)

(* intro! intro? are automatically applied by "rule".     *)
(* intro! is automatically applied by "rules" and "auto". *)

(* CSP_F_law_basic *)

declare cspF_commut                                  [simp]

(* CSP_F_law_ref *)

declare cspF_Int_choice_right                        [intro!]
declare cspF_Rep_int_choice_right                    [intro!]

(* CSP_F_law_SKIP *)

declare cspF_SKIP_DIV_resolve                        [simp]
lemmas  cspF_SKIP_DIV_resolve_sym                    [simp]
      = cspF_SKIP_DIV_resolve[THEN cspF_sym]

(* CSP_F_law_decompo *)

declare cspF_rm_head                                 [intro!]
declare cspF_decompo                                 [simp]

(* CSP_F_law_dist *)

declare cspF_all_dist                                [simp]
lemmas  cspF_all_dist_sym                            [simp]
      = cspF_all_dist[THEN cspF_sym]

declare cspF_unwind                                  [simp]
lemmas  cspF_unwind_sym                              [simp]
      = cspF_unwind[THEN cspF_sym]

(* CSP_F_law_step *)

declare cspF_step                                    [simp]
lemmas  cspF_step_sym                                [simp]
      = cspF_step[THEN cspF_sym]

(* CSP_F_law_etc *)

declare cspF_choice_IF                               [simp]

(* CSP_F_DIV_top *)

declare cspF_DIV_top                                 [simp]

end

lemmas cspF_mono_ref:

  [| 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; 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

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

  [| X = Y; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=F[M1.0,M2.0] ? :Y -> Qf

  [| b1.0 = b2.0; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=F[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=F[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=F[M1.0,M2.0] !<f> :Y .. Qf

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=F[M1.0,M2.0] ? :Y -> Qf

lemmas cspF_mono_ref:

  [| 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; 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

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

  [| X = Y; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=F[M1.0,M2.0] ? :Y -> Qf

  [| b1.0 = b2.0; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=F[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=F[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=F[M1.0,M2.0] !<f> :Y .. Qf

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=F[M1.0,M2.0] ? :Y -> Qf

lemmas cspF_decompo_ref:

  [| 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; 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

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

  [| X = Y; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=F[M1.0,M2.0] ? :Y -> Qf

  [| b1.0 = b2.0; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=F[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=F[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=F[M1.0,M2.0] !<f> :Y .. Qf

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=F[M1.0,M2.0] ? :Y -> Qf

  [| 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; 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

  [| a = b; P =F[M1.0,M2.0] Q |] ==> a -> P =F[M1.0,M2.0] b -> Q

  [| X = Y; !!a. a ∈ Y ==> Pf a =F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf =F[M1.0,M2.0] ? :Y -> Qf

  [| C1.0 = C2.0; !!c. c ∈ sumset C1.0 ==> Pf c =F[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf =F[M1.0,M2.0] !! :C2.0 .. Qf

  [| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf =F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Xs1.0 = Xs2.0; !!X. X ∈ Xs2.0 ==> Pf X =F[M1.0,M2.0] Qf X |]
  ==> !set :Xs1.0 .. Pf =F[M1.0,M2.0] !set :Xs2.0 .. Qf

  [| X1.0 = X2.0; !!x. x ∈ X2.0 ==> Pf x =F[M1.0,M2.0] Qf x |]
  ==> ! :X1.0 .. Pf =F[M1.0,M2.0] ! :X2.0 .. Qf

  [| inj f; X1.0 = X2.0; !!x. x ∈ X2.0 ==> Pf x =F[M1.0,M2.0] Qf x |]
  ==> !<f> :X1.0 .. Pf =F[M1.0,M2.0] !<f> :X2.0 .. Qf

  [| b1.0 = b2.0; P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 =F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

lemmas cspF_decompo_ref:

  [| 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; 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

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

  [| X = Y; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=F[M1.0,M2.0] ? :Y -> Qf

  [| b1.0 = b2.0; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=F[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=F[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=F[M1.0,M2.0] !<f> :Y .. Qf

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=F[M1.0,M2.0] ? :Y -> Qf

  [| 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; 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

  [| a = b; P =F[M1.0,M2.0] Q |] ==> a -> P =F[M1.0,M2.0] b -> Q

  [| X = Y; !!a. a ∈ Y ==> Pf a =F[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf =F[M1.0,M2.0] ? :Y -> Qf

  [| C1.0 = C2.0; !!c. c ∈ sumset C1.0 ==> Pf c =F[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf =F[M1.0,M2.0] !! :C2.0 .. Qf

  [| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf =F[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Xs1.0 = Xs2.0; !!X. X ∈ Xs2.0 ==> Pf X =F[M1.0,M2.0] Qf X |]
  ==> !set :Xs1.0 .. Pf =F[M1.0,M2.0] !set :Xs2.0 .. Qf

  [| X1.0 = X2.0; !!x. x ∈ X2.0 ==> Pf x =F[M1.0,M2.0] Qf x |]
  ==> ! :X1.0 .. Pf =F[M1.0,M2.0] ! :X2.0 .. Qf

  [| inj f; X1.0 = X2.0; !!x. x ∈ X2.0 ==> Pf x =F[M1.0,M2.0] Qf x |]
  ==> !<f> :X1.0 .. Pf =F[M1.0,M2.0] !<f> :X2.0 .. Qf

  [| b1.0 = b2.0; P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 =F[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

lemmas cspF_SKIP_DIV_resolve_sym:

  ? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =F[M1.0,M1.0] SKIP |[X1]| ? :Y1 -> Qf1

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| SKIP

  ? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =F[M1.0,M1.0] 
  DIV |[X1]| ? :Y1 -> Qf1

  ? x:(Y1 - X1) -> (Qf1 x |[X1]| DIV) [+] DIV =F[M1.0,M1.0] 
  ? :Y1 -> Qf1 |[X1]| DIV

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

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

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

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

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

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

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =F[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP

  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =F[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =F[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP

  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =F[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)

  P1 |[X1]| DIV =F[M1.0,M1.0] (P1 [+] SKIP) |[X1]| DIV

  DIV |[X1]| P1 =F[M1.0,M1.0] DIV |[X1]| (P1 [+] SKIP)

  P1 |[X1]| DIV =F[M1.0,M1.0] (P1 [+] DIV) |[X1]| DIV

  DIV |[X1]| P1 =F[M1.0,M1.0] DIV |[X1]| (P1 [+] DIV)

  SKIP =F[M1.0,M1.0] SKIP -- X1

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

  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) -- X1

  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) -- X1

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

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

  P2.0 =F[M1.0,M1.0] SKIP ;; P2.0

  P2.0 =F[M1.0,M1.0] P2.0 ;; SKIP

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

  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =F[M1.0,M1.0] (? :X1 -> Pf1 [> SKIP) ;; Q1

  ? x:X1 -> (Pf1 x ;; Q1) [> DIV =F[M1.0,M1.0] (? :X1 -> Pf1 [> DIV) ;; Q1

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

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

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
        |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> (DIV |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| DIV) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| DIV) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> (DIV |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> SKIP |[X1]| ? :Z1 -> Qf1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| ? :Z1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
   [> ? :Y1 -> Pf1 |[X1]| SKIP 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> DIV |[X1]| ? :Z1 -> Qf1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| ? :Z1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
   [> ? :Y1 -> Pf1 |[X1]| DIV 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =F[M1.0,M1.0] (? :X1 -> Pf1 [+] SKIP) ;; Q1

  ? x:X1 -> (Pf1 x ;; Q1) [+] DIV =F[M1.0,M1.0] (? :X1 -> Pf1 [+] DIV) ;; Q1

lemmas cspF_SKIP_DIV_resolve_sym:

  ? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =F[M1.0,M1.0] SKIP |[X1]| ? :Y1 -> Qf1

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| SKIP

  ? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =F[M1.0,M1.0] 
  DIV |[X1]| ? :Y1 -> Qf1

  ? x:(Y1 - X1) -> (Qf1 x |[X1]| DIV) [+] DIV =F[M1.0,M1.0] 
  ? :Y1 -> Qf1 |[X1]| DIV

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

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

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

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

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

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

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =F[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP

  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =F[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)

  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =F[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP

  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =F[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)

  P1 |[X1]| DIV =F[M1.0,M1.0] (P1 [+] SKIP) |[X1]| DIV

  DIV |[X1]| P1 =F[M1.0,M1.0] DIV |[X1]| (P1 [+] SKIP)

  P1 |[X1]| DIV =F[M1.0,M1.0] (P1 [+] DIV) |[X1]| DIV

  DIV |[X1]| P1 =F[M1.0,M1.0] DIV |[X1]| (P1 [+] DIV)

  SKIP =F[M1.0,M1.0] SKIP -- X1

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

  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) -- X1

  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) -- X1

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

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

  P2.0 =F[M1.0,M1.0] SKIP ;; P2.0

  P2.0 =F[M1.0,M1.0] P2.0 ;; SKIP

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

  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =F[M1.0,M1.0] (? :X1 -> Pf1 [> SKIP) ;; Q1

  ? x:X1 -> (Pf1 x ;; Q1) [> DIV =F[M1.0,M1.0] (? :X1 -> Pf1 [> DIV) ;; Q1

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

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

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
        |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> (DIV |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| DIV) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| DIV) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> (DIV |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x 
   [> SKIP |[X1]| ? :Z1 -> Qf1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) |[X1]| ? :Z1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
   [> ? :Y1 -> Pf1 |[X1]| SKIP 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] SKIP)

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x 
   [> DIV |[X1]| ? :Z1 -> Qf1 
  =F[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) |[X1]| ? :Z1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
   [> ? :Y1 -> Pf1 |[X1]| DIV 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)

  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =F[M1.0,M1.0] (? :X1 -> Pf1 [+] SKIP) ;; Q1

  ? x:X1 -> (Pf1 x ;; Q1) [+] DIV =F[M1.0,M1.0] (? :X1 -> Pf1 [+] DIV) ;; Q1

lemmas cspF_all_dist_sym:

  P1.1 [+] Q1 |~| P2.1 [+] Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) [+] Q1

  P1 [+] Q1.1 |~| P1 [+] Q2.1 =F[M1.0,M1.0] P1 [+] (Q1.1 |~| Q2.1)

  P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) |[X1]| Q1

  P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =F[M1.0,M1.0] P1 |[X1]| (Q1.1 |~| Q2.1)

  P1.1 -- X1 |~| P2.1 -- X1 =F[M1.0,M1.0] (P1.1 |~| P2.1) -- X1

  P1.1 [[r1]] |~| P2.1 [[r1]] =F[M1.0,M1.0] (P1.1 |~| P2.1) [[r1]]

  P1.1 ;; Q1 |~| P2.1 ;; Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) ;; Q1

  P1.1 |. n1 |~| P2.1 |. n1 =F[M1.0,M1.0] (P1.1 |~| P2.1) |. n1

  !! :C1 .. Pf1 |~| !! :C1 .. Qf1 =F[M1.0,M1.0] !! c:C1 .. (Pf1 c |~| Qf1 c)

  !nat :N1 .. Pf1 |~| !nat :N1 .. Qf1 =F[M1.0,M1.0] !nat n:N1 .. (Pf1 n |~| Qf1 n)

  !set :Xs1 .. Pf1 |~| !set :Xs1 .. Qf1 =F[M1.0,M1.0] 
  !set X:Xs1 .. (Pf1 X |~| Qf1 X)

  ! :X1 .. Pf1 |~| ! :X1 .. Qf1 =F[M1.0,M1.0] ! a:X1 .. (Pf1 a |~| Qf1 a)

  inj f1
  ==> !<f1> :X1 .. Pf1 |~| !<f1> :X1 .. Qf1 =F[M1.0,M1.0] 
      !<f1> a:X1 .. (Pf1 a |~| Qf1 a)

  IF (sumset C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =F[M1.0,M1.0] 
  (!! :C1 .. Pf1) [+] Q1

  IF (sumset C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =F[M1.0,M1.0] 
  P1 [+] (!! :C1 .. Qf1)

  IF (sumset C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 
  =F[M1.0,M1.0] (!! :C1 .. Pf1) |[X1]| Q1

  IF (sumset C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c 
  =F[M1.0,M1.0] P1 |[X1]| (!! :C1 .. Qf1)

  !! c:C1 .. Pf1 c -- X1 =F[M1.0,M1.0] (!! :C1 .. Pf1) -- X1

  !! c:C1 .. Pf1 c [[r1]] =F[M1.0,M1.0] (!! :C1 .. Pf1) [[r1]]

  !! c:C1 .. Pf1 c ;; Q1 =F[M1.0,M1.0] (!! :C1 .. Pf1) ;; Q1

  !! c:C1 .. Pf1 c |. m1 =F[M1.0,M1.0] (!! :C1 .. Pf1) |. m1

  IF (N1 = {}) THEN DIV [+] Q1 ELSE !nat n:N1 .. Pf1 n [+] Q1 =F[M1.0,M1.0] 
  (!nat :N1 .. Pf1) [+] Q1

  IF (N1 = {}) THEN P1 [+] DIV ELSE !nat n:N1 .. P1 [+] Qf1 n =F[M1.0,M1.0] 
  P1 [+] (!nat :N1 .. Qf1)

  IF (N1 = {}) THEN DIV |[X1]| Q1 ELSE !nat n:N1 .. Pf1 n |[X1]| Q1 =F[M1.0,M1.0] 
  (!nat :N1 .. Pf1) |[X1]| Q1

  IF (N1 = {}) THEN P1 |[X1]| DIV ELSE !nat n:N1 .. P1 |[X1]| Qf1 n =F[M1.0,M1.0] 
  P1 |[X1]| (!nat :N1 .. Qf1)

  !nat n:N1 .. Pf1 n -- X1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) -- X1

  !nat n:N1 .. Pf1 n [[r1]] =F[M1.0,M1.0] (!nat :N1 .. Pf1) [[r1]]

  !nat n:N1 .. Pf1 n ;; Q1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) ;; Q1

  !nat n:N1 .. Pf1 n |. m1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) |. m1

  IF (Xs1 = {}) THEN DIV [+] Q1 ELSE !set X:Xs1 .. Pf1 X [+] Q1 =F[M1.0,M1.0] 
  (!set :Xs1 .. Pf1) [+] Q1

  IF (Xs1 = {}) THEN P1 [+] DIV ELSE !set X:Xs1 .. P1 [+] Qf1 X =F[M1.0,M1.0] 
  P1 [+] (!set :Xs1 .. Qf1)

  IF (Xs1 = {}) THEN DIV |[Y1]| Q1 ELSE !set X:Xs1 .. Pf1 X |[Y1]| Q1 
  =F[M1.0,M1.0] (!set :Xs1 .. Pf1) |[Y1]| Q1

  IF (Xs1 = {}) THEN P1 |[Y1]| DIV ELSE !set X:Xs1 .. P1 |[Y1]| Qf1 X 
  =F[M1.0,M1.0] P1 |[Y1]| (!set :Xs1 .. Qf1)

  !set X:Xs1 .. Pf1 X -- Y1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) -- Y1

  !set X:Xs1 .. Pf1 X [[r1]] =F[M1.0,M1.0] (!set :Xs1 .. Pf1) [[r1]]

  !set X:Xs1 .. Pf1 X ;; Q1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) ;; Q1

  !set X:Xs1 .. Pf1 X |. m1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) |. m1

  IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =F[M1.0,M1.0] 
  (! :X1 .. Pf1) [+] Q1

  IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =F[M1.0,M1.0] 
  P1 [+] (! :X1 .. Qf1)

  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =F[M1.0,M1.0] 
  (! :Y1 .. Pf1) |[X1]| Q1

  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =F[M1.0,M1.0] 
  P1 |[X1]| (! :Y1 .. Qf1)

  ! x:Y1 .. Pf1 x -- X1 =F[M1.0,M1.0] (! :Y1 .. Pf1) -- X1

  ! x:X1 .. Pf1 x [[r1]] =F[M1.0,M1.0] (! :X1 .. Pf1) [[r1]]

  ! x:X1 .. Pf1 x ;; Q1 =F[M1.0,M1.0] (! :X1 .. Pf1) ;; Q1

  ! x:X1 .. Pf1 x |. n1 =F[M1.0,M1.0] (! :X1 .. Pf1) |. n1

  IF (X1 = {}) THEN DIV [+] Q1 ELSE !<f1> x:X1 .. Pf1 x [+] Q1 =F[M1.0,M1.0] 
  (!<f1> :X1 .. Pf1) [+] Q1

  IF (X1 = {}) THEN P1 [+] DIV ELSE !<f1> x:X1 .. P1 [+] Qf1 x =F[M1.0,M1.0] 
  P1 [+] (!<f1> :X1 .. Qf1)

  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !<f1> x:Y1 .. Pf1 x |[X1]| Q1 
  =F[M1.0,M1.0] (!<f1> :Y1 .. Pf1) |[X1]| Q1

  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !<f1> x:Y1 .. P1 |[X1]| Qf1 x 
  =F[M1.0,M1.0] P1 |[X1]| (!<f1> :Y1 .. Qf1)

  !<f1> x:Y1 .. Pf1 x -- X1 =F[M1.0,M1.0] (!<f1> :Y1 .. Pf1) -- X1

  !<f1> x:X1 .. Pf1 x [[r1]] =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) [[r1]]

  !<f1> x:X1 .. Pf1 x ;; Q1 =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) ;; Q1

  !<f1> x:X1 .. Pf1 x |. n1 =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) |. n1

  P1.1 [[r1]] [+] P2.1 [[r1]] =F[M1.0,M1.0] (P1.1 [+] P2.1) [[r1]]

  P1.1 |. n1 [+] P2.1 |. n1 =F[M1.0,M1.0] (P1.1 [+] P2.1) |. n1

lemmas cspF_all_dist_sym:

  P1.1 [+] Q1 |~| P2.1 [+] Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) [+] Q1

  P1 [+] Q1.1 |~| P1 [+] Q2.1 =F[M1.0,M1.0] P1 [+] (Q1.1 |~| Q2.1)

  P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) |[X1]| Q1

  P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =F[M1.0,M1.0] P1 |[X1]| (Q1.1 |~| Q2.1)

  P1.1 -- X1 |~| P2.1 -- X1 =F[M1.0,M1.0] (P1.1 |~| P2.1) -- X1

  P1.1 [[r1]] |~| P2.1 [[r1]] =F[M1.0,M1.0] (P1.1 |~| P2.1) [[r1]]

  P1.1 ;; Q1 |~| P2.1 ;; Q1 =F[M1.0,M1.0] (P1.1 |~| P2.1) ;; Q1

  P1.1 |. n1 |~| P2.1 |. n1 =F[M1.0,M1.0] (P1.1 |~| P2.1) |. n1

  !! :C1 .. Pf1 |~| !! :C1 .. Qf1 =F[M1.0,M1.0] !! c:C1 .. (Pf1 c |~| Qf1 c)

  !nat :N1 .. Pf1 |~| !nat :N1 .. Qf1 =F[M1.0,M1.0] !nat n:N1 .. (Pf1 n |~| Qf1 n)

  !set :Xs1 .. Pf1 |~| !set :Xs1 .. Qf1 =F[M1.0,M1.0] 
  !set X:Xs1 .. (Pf1 X |~| Qf1 X)

  ! :X1 .. Pf1 |~| ! :X1 .. Qf1 =F[M1.0,M1.0] ! a:X1 .. (Pf1 a |~| Qf1 a)

  inj f1
  ==> !<f1> :X1 .. Pf1 |~| !<f1> :X1 .. Qf1 =F[M1.0,M1.0] 
      !<f1> a:X1 .. (Pf1 a |~| Qf1 a)

  IF (sumset C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =F[M1.0,M1.0] 
  (!! :C1 .. Pf1) [+] Q1

  IF (sumset C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =F[M1.0,M1.0] 
  P1 [+] (!! :C1 .. Qf1)

  IF (sumset C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 
  =F[M1.0,M1.0] (!! :C1 .. Pf1) |[X1]| Q1

  IF (sumset C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c 
  =F[M1.0,M1.0] P1 |[X1]| (!! :C1 .. Qf1)

  !! c:C1 .. Pf1 c -- X1 =F[M1.0,M1.0] (!! :C1 .. Pf1) -- X1

  !! c:C1 .. Pf1 c [[r1]] =F[M1.0,M1.0] (!! :C1 .. Pf1) [[r1]]

  !! c:C1 .. Pf1 c ;; Q1 =F[M1.0,M1.0] (!! :C1 .. Pf1) ;; Q1

  !! c:C1 .. Pf1 c |. m1 =F[M1.0,M1.0] (!! :C1 .. Pf1) |. m1

  IF (N1 = {}) THEN DIV [+] Q1 ELSE !nat n:N1 .. Pf1 n [+] Q1 =F[M1.0,M1.0] 
  (!nat :N1 .. Pf1) [+] Q1

  IF (N1 = {}) THEN P1 [+] DIV ELSE !nat n:N1 .. P1 [+] Qf1 n =F[M1.0,M1.0] 
  P1 [+] (!nat :N1 .. Qf1)

  IF (N1 = {}) THEN DIV |[X1]| Q1 ELSE !nat n:N1 .. Pf1 n |[X1]| Q1 =F[M1.0,M1.0] 
  (!nat :N1 .. Pf1) |[X1]| Q1

  IF (N1 = {}) THEN P1 |[X1]| DIV ELSE !nat n:N1 .. P1 |[X1]| Qf1 n =F[M1.0,M1.0] 
  P1 |[X1]| (!nat :N1 .. Qf1)

  !nat n:N1 .. Pf1 n -- X1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) -- X1

  !nat n:N1 .. Pf1 n [[r1]] =F[M1.0,M1.0] (!nat :N1 .. Pf1) [[r1]]

  !nat n:N1 .. Pf1 n ;; Q1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) ;; Q1

  !nat n:N1 .. Pf1 n |. m1 =F[M1.0,M1.0] (!nat :N1 .. Pf1) |. m1

  IF (Xs1 = {}) THEN DIV [+] Q1 ELSE !set X:Xs1 .. Pf1 X [+] Q1 =F[M1.0,M1.0] 
  (!set :Xs1 .. Pf1) [+] Q1

  IF (Xs1 = {}) THEN P1 [+] DIV ELSE !set X:Xs1 .. P1 [+] Qf1 X =F[M1.0,M1.0] 
  P1 [+] (!set :Xs1 .. Qf1)

  IF (Xs1 = {}) THEN DIV |[Y1]| Q1 ELSE !set X:Xs1 .. Pf1 X |[Y1]| Q1 
  =F[M1.0,M1.0] (!set :Xs1 .. Pf1) |[Y1]| Q1

  IF (Xs1 = {}) THEN P1 |[Y1]| DIV ELSE !set X:Xs1 .. P1 |[Y1]| Qf1 X 
  =F[M1.0,M1.0] P1 |[Y1]| (!set :Xs1 .. Qf1)

  !set X:Xs1 .. Pf1 X -- Y1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) -- Y1

  !set X:Xs1 .. Pf1 X [[r1]] =F[M1.0,M1.0] (!set :Xs1 .. Pf1) [[r1]]

  !set X:Xs1 .. Pf1 X ;; Q1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) ;; Q1

  !set X:Xs1 .. Pf1 X |. m1 =F[M1.0,M1.0] (!set :Xs1 .. Pf1) |. m1

  IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =F[M1.0,M1.0] 
  (! :X1 .. Pf1) [+] Q1

  IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =F[M1.0,M1.0] 
  P1 [+] (! :X1 .. Qf1)

  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =F[M1.0,M1.0] 
  (! :Y1 .. Pf1) |[X1]| Q1

  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =F[M1.0,M1.0] 
  P1 |[X1]| (! :Y1 .. Qf1)

  ! x:Y1 .. Pf1 x -- X1 =F[M1.0,M1.0] (! :Y1 .. Pf1) -- X1

  ! x:X1 .. Pf1 x [[r1]] =F[M1.0,M1.0] (! :X1 .. Pf1) [[r1]]

  ! x:X1 .. Pf1 x ;; Q1 =F[M1.0,M1.0] (! :X1 .. Pf1) ;; Q1

  ! x:X1 .. Pf1 x |. n1 =F[M1.0,M1.0] (! :X1 .. Pf1) |. n1

  IF (X1 = {}) THEN DIV [+] Q1 ELSE !<f1> x:X1 .. Pf1 x [+] Q1 =F[M1.0,M1.0] 
  (!<f1> :X1 .. Pf1) [+] Q1

  IF (X1 = {}) THEN P1 [+] DIV ELSE !<f1> x:X1 .. P1 [+] Qf1 x =F[M1.0,M1.0] 
  P1 [+] (!<f1> :X1 .. Qf1)

  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !<f1> x:Y1 .. Pf1 x |[X1]| Q1 
  =F[M1.0,M1.0] (!<f1> :Y1 .. Pf1) |[X1]| Q1

  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !<f1> x:Y1 .. P1 |[X1]| Qf1 x 
  =F[M1.0,M1.0] P1 |[X1]| (!<f1> :Y1 .. Qf1)

  !<f1> x:Y1 .. Pf1 x -- X1 =F[M1.0,M1.0] (!<f1> :Y1 .. Pf1) -- X1

  !<f1> x:X1 .. Pf1 x [[r1]] =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) [[r1]]

  !<f1> x:X1 .. Pf1 x ;; Q1 =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) ;; Q1

  !<f1> x:X1 .. Pf1 x |. n1 =F[M1.0,M1.0] (!<f1> :X1 .. Pf1) |. n1

  P1.1 [[r1]] [+] P2.1 [[r1]] =F[M1.0,M1.0] (P1.1 [+] P2.1) [[r1]]

  P1.1 |. n1 [+] P2.1 |. n1 =F[M1.0,M1.0] (P1.1 [+] P2.1) |. n1

lemmas cspF_unwind_sym:

  [| Pf1 = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf1 ∨ FPmode = MIXmode |]
  ==> Pf1 p1 =F $p1

lemmas cspF_unwind_sym:

  [| Pf1 = PNfun;
     FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf1 ∨ FPmode = MIXmode |]
  ==> Pf1 p1 =F $p1

lemmas cspF_step_sym:

  ? :{} -> Pf1 =F[M2.0,M1.0] STOP

  ? x:{a1} -> P1 =F[M1.0,M1.0] a1 -> P1

  ? x:(X1 ∪ Y1) 
   -> IF (x ∈ X1 ∧ x ∈ Y1) THEN Pf1 x |~| Qf1 x 
      ELSE IF (x ∈ X1) THEN Pf1 x ELSE Qf1 x 
  =F[M1.0,M1.0] ? :X1 -> Pf1 [+] ? :Y1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| ? :Z1 -> Qf1

  IF (Y1 ∩ X1 = {}) THEN ? x:Y1 -> Pf1 x -- X1 
  ELSE ? x:(Y1 - X1) -> Pf1 x -- X1 [> (! x:(Y1 ∩ X1) .. Pf1 x -- X1) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1) -- X1

  ? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =F[M1.0,M1.0] 
  (? :X1 -> Pf1) [[r1]]

  ? x:X1 -> (Pf1 x ;; Q1) =F[M1.0,M1.0] ? :X1 -> Pf1 ;; Q1

  ? x:X1 -> Pf1 x |. n1 =F[M1.0,M1.0] (? :X1 -> Pf1) |. Suc n1

lemmas cspF_step_sym:

  ? :{} -> Pf1 =F[M2.0,M1.0] STOP

  ? x:{a1} -> P1 =F[M1.0,M1.0] a1 -> P1

  ? x:(X1 ∪ Y1) 
   -> IF (x ∈ X1 ∧ x ∈ Y1) THEN Pf1 x |~| Qf1 x 
      ELSE IF (x ∈ X1) THEN Pf1 x ELSE Qf1 x 
  =F[M1.0,M1.0] ? :X1 -> Pf1 [+] ? :Y1 -> Qf1

  ? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) 
   -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x 
      ELSE IF (x ∈ Y1 ∧ x ∈ Z1) 
           THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x 
           ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 
                ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x 
  =F[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| ? :Z1 -> Qf1

  IF (Y1 ∩ X1 = {}) THEN ? x:Y1 -> Pf1 x -- X1 
  ELSE ? x:(Y1 - X1) -> Pf1 x -- X1 [> (! x:(Y1 ∩ X1) .. Pf1 x -- X1) 
  =F[M1.0,M1.0] (? :Y1 -> Pf1) -- X1

  ? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =F[M1.0,M1.0] 
  (? :X1 -> Pf1) [[r1]]

  ? x:X1 -> (Pf1 x ;; Q1) =F[M1.0,M1.0] ? :X1 -> Pf1 ;; Q1

  ? x:X1 -> Pf1 x |. n1 =F[M1.0,M1.0] (? :X1 -> Pf1) |. Suc n1