Theory CSP_T

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

theory CSP_T
imports CSP_T_tactic CSP_T_surj
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |               February 2005  (modified)   |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T
imports CSP_T_tactic CSP_T_surj
begin

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

lemmas cspT_mono_ref = cspT_free_mono
   cspT_Act_prefix_mono cspT_Ext_pre_choice_mono 
   cspT_IF_mono cspT_decompo_subset

lemmas cspT_decompo_ref = cspT_mono_ref cspT_cong

(*-------------------------------------------------------*
 |                                                       |
 |      adding ... to automatically check Procfun        |
 |                                                       |
 *-------------------------------------------------------*)


(*-------------------------------------------------------------*
 |                                                             |
 |  Users may be sometimes required to apply "Int_prefix_def"  |
 |  for unfoling "! x:X -> P". Do you like the following ?     |
 |                                                             |
 |  declare Int_pre_choice_def                     [simp]      |
 |                                                             |
 |  Users may be sometimes required to apply "Send_prefix_def" |
 |  for unfoling "a ! x: -> P". Do you like the following ?    |
 |                                                             |
 |  declare Send_prefix_def                        [simp]      |
 |                                                             |
 |  Users may be sometimes required to apply "Rec_prefix_def"  |
 |  for unfoling "a ? x:X -> P". Do you like the following ?   |
 |                                                             |
 |  declare Rec_prefix_def                         [simp]      |
 |                                                             |
 *-------------------------------------------------------------*)

(*                           NO                                *)

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

(*---------------------------------------------------------------------*
 | Nondet_send_prefix_def : non-deterministic sending                  |
 | Rep_int_choice_fun_def : Replicated internal choice with a function |
 *---------------------------------------------------------------------*)

(*   "inj_on_def" is needed for resolving (inv f) in R_Prefix_def *)
(*  declare inj_on_def                                 [simp]     *)

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

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

(* CSP_T_law_basic *)

declare cspT_commut                                  [simp]

(* CSP_T_law_ref *)

declare cspT_Int_choice_right                        [intro!]
declare cspT_Rep_int_choice_right                    [intro!]

(* CSP_T_law_SKIP *)

declare cspT_SKIP_DIV_resolve                        [simp]
lemmas  cspT_SKIP_DIV_resolve_sym                    [simp]
      = cspT_SKIP_DIV_resolve[THEN cspT_sym]

(* CSP_T_law_decompo *)

declare cspT_rm_head                                 [intro!]
declare cspT_decompo                                 [simp]

(* CSP_T_law_dist *)

declare cspT_all_dist                                [simp]
lemmas  cspT_all_dist_sym                            [simp]
      = cspT_all_dist[THEN cspT_sym]

declare cspT_unwind                                  [simp]
lemmas  cspT_unwind_sym                              [simp]
      = cspT_unwind[THEN cspT_sym]

(* CSP_T_law_step *)

declare cspT_step                                    [simp]
lemmas  cspT_step_sym                                [simp]
      = cspT_step[THEN cspT_sym]

(* CSP_T_law_etc *)

declare cspT_choice_IF                               [simp]

(* top *)

declare cspT_top                                     [simp]
declare cspT_Ent_choice_left_ref                     [simp]

(*-------------------[test of CSP_T]------------------------*

datatype Event = eva | evb

datatype PNSpec = AB
datatype PNImpl = A

consts 
  PNfunSpec :: "PNSpec => (PNSpec, Event) proc"
  PNfunImpl :: "PNImpl => (PNImpl, Event) proc"

primrec
  "PNfunSpec   AB = eva -> $AB |~| evb -> $AB"

primrec
  "PNfunImpl   A = eva -> $A"

defs (overloaded)
Set_PNfunSpec_def : "PNfun == PNfunSpec"
Set_PNfunImpl_def : "PNfun == PNfunImpl"
FPmode_def        : "FPmode == CMSmode"

declare Set_PNfunSpec_def [simp]
declare Set_PNfunImpl_def [simp]
declare FPmode_def        [simp]

lemma example_test_01: "PNfun AB = eva -> $AB |~| evb -> $AB"
by (simp)

lemma example_test_02: "PNfun A = eva -> $A"
by (simp)

consts 
  Spec_Impl :: "PNSpec => (PNImpl, Event) proc"

primrec
  "Spec_Impl  AB = $A"

consts 
  Spec :: "(PNSpec, Event) proc"
  Impl :: "(PNImpl, Event) proc"

defs
  Spec_def : "Spec == $AB"
  Impl_def : "Impl == $A"

lemma guardedfun_ex[simp]: 
  "guardedfun PNfunSpec"
  "guardedfun PNfunImpl"
by (simp add: guardedfun_def, rule allI, induct_tac p, simp)+

lemma example_test_fp: "Spec <=T Impl"
apply (simp add: Spec_def Impl_def)
apply (rule cspT_fp_induct_left[of _ "Spec_Impl"])
apply (simp_all)
apply (simp)

apply (induct_tac p)
apply (simp)

apply (rule cspT_rw_right)
apply (rule cspT_unwind)
apply (simp_all)
apply (simp)

apply (rule cspT_Int_choice_left1)
apply (simp)
done

-- you have to note that you cannot prove "$AB <=T $A"
-- because $AB has a wider type "(PNSpec,'s) proc" than
-- "(PNSpec,Event) proc".

 *-------------------[test of CSP_T]------------------------*)

end

lemmas cspT_mono_ref: 

  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
  [| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
  [| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf

lemmas cspT_mono_ref: 

  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
  [| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
  [| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf

lemmas cspT_decompo_ref: 

  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
  [| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
  [| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 =T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 =T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 =T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P =T[M1.0,M2.0] Q |] ==> P -- X =T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P =T[M1.0,M2.0] Q |] ==> P [[r1.0]] =T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 =T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P =T[M1.0,M2.0] Q |] ==> P |. n1.0 =T[M1.0,M2.0] Q |. n2.0
  [| a = b; P =T[M1.0,M2.0] Q |] ==> a -> P =T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a =T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf =T[M1.0,M2.0] ? :Y -> Qf
  [| C1.0 = C2.0; !!c. c ∈ sumset C1.0 ==> Pf c =T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf =T[M1.0,M2.0] !! :C2.0 .. Qf
  [| Xs1.0 = Xs2.0; !!X. X ∈ Xs1.0 ==> Pf X =T[M1.0,M2.0] Qf X |]
  ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
  [| N1.0 = N2.0; !!n. n ∈ N1.0 ==> Pf n =T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
  ==> ! :X1.0 .. Pf =T[M1.0,M2.0] ! :X2.0 .. Qf
  [| inj f; X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
  ==> !<f> :X1.0 .. Pf =T[M1.0,M2.0] !<f> :X2.0 .. Qf
  [| b1.0 = b2.0; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 =T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

lemmas cspT_decompo_ref: 

  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
  [| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
  [| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 [+] P2.0 =T[M1.0,M2.0] Q1.0 [+] Q2.0
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |~| P2.0 =T[M1.0,M2.0] Q1.0 |~| Q2.0
  [| X = Y; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 |[X]| P2.0 =T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
  [| X = Y; P =T[M1.0,M2.0] Q |] ==> P -- X =T[M1.0,M2.0] Q -- Y
  [| r1.0 = r2.0; P =T[M1.0,M2.0] Q |] ==> P [[r1.0]] =T[M1.0,M2.0] Q [[r2.0]]
  [| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> P1.0 ;; P2.0 =T[M1.0,M2.0] Q1.0 ;; Q2.0
  [| n1.0 = n2.0; P =T[M1.0,M2.0] Q |] ==> P |. n1.0 =T[M1.0,M2.0] Q |. n2.0
  [| a = b; P =T[M1.0,M2.0] Q |] ==> a -> P =T[M1.0,M2.0] b -> Q
  [| X = Y; !!a. a ∈ Y ==> Pf a =T[M1.0,M2.0] Qf a |]
  ==> ? :X -> Pf =T[M1.0,M2.0] ? :Y -> Qf
  [| C1.0 = C2.0; !!c. c ∈ sumset C1.0 ==> Pf c =T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf =T[M1.0,M2.0] !! :C2.0 .. Qf
  [| Xs1.0 = Xs2.0; !!X. X ∈ Xs1.0 ==> Pf X =T[M1.0,M2.0] Qf X |]
  ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
  [| N1.0 = N2.0; !!n. n ∈ N1.0 ==> Pf n =T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
  [| X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
  ==> ! :X1.0 .. Pf =T[M1.0,M2.0] ! :X2.0 .. Qf
  [| inj f; X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
  ==> !<f> :X1.0 .. Pf =T[M1.0,M2.0] !<f> :X2.0 .. Qf
  [| b1.0 = b2.0; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
  ==> IF b1.0 THEN P1.0 ELSE P2.0 =T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0

lemmas cspT_SKIP_DIV_resolve_sym: 

  ? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =T[M1.0,M1.0] SKIP |[X1]| ? :Y1 -> Qf1
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =T[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| SKIP
  ? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =T[M1.0,M1.0] 
  DIV |[X1]| ? :Y1 -> Qf1
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| DIV) [+] DIV =T[M1.0,M1.0] 
  ? :Y1 -> Pf1 |[X1]| DIV
  SKIP =T[M2.0,M1.0] SKIP [+] DIV
  SKIP =T[M2.0,M1.0] DIV [+] SKIP
  DIV =T[M2.0,M1.0] SKIP |[X1]| DIV
  DIV =T[M2.0,M1.0] DIV |[X1]| SKIP
  SKIP =T[M2.0,M1.0] SKIP |[X1]| SKIP
  DIV =T[M2.0,M1.0] DIV |[X1]| DIV
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =T[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP
  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =T[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =T[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP
  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =T[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)
  P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] SKIP) |[X1]| DIV
  DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] SKIP)
  P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] DIV) |[X1]| DIV
  DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] DIV)
  SKIP =T[M2.0,M1.0] SKIP -- X1
  DIV =T[M2.0,M1.0] DIV -- X1
  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =T[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) -- X1
  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =T[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) -- X1
  SKIP =T[M2.0,M1.0] SKIP [[r1]]
  DIV =T[M2.0,M1.0] DIV [[r1]]
  P2.0 =T[M1.0,M1.0] SKIP ;; P2.0
  P2.0 =T[M1.0,M1.0] P2.0 ;; SKIP
  DIV =T[M2.0,M1.0] DIV ;; P1
  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [> SKIP) ;; Q1
  ? x:X1 -> (Pf1 x ;; Q1) [> DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [> DIV) ;; Q1
  SKIP =T[M2.0,M1.0] SKIP |. Suc n1
  DIV =T[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) 
  =T[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) 
  =T[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) 
  =T[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) 
  =T[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 
  =T[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 
  =T[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 
  =T[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 
  =T[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)
  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [+] SKIP) ;; Q1
  ? x:X1 -> (Pf1 x ;; Q1) [+] DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [+] DIV) ;; Q1

lemmas cspT_SKIP_DIV_resolve_sym: 

  ? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =T[M1.0,M1.0] SKIP |[X1]| ? :Y1 -> Qf1
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =T[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| SKIP
  ? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =T[M1.0,M1.0] 
  DIV |[X1]| ? :Y1 -> Qf1
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| DIV) [+] DIV =T[M1.0,M1.0] 
  ? :Y1 -> Pf1 |[X1]| DIV
  SKIP =T[M2.0,M1.0] SKIP [+] DIV
  SKIP =T[M2.0,M1.0] DIV [+] SKIP
  DIV =T[M2.0,M1.0] SKIP |[X1]| DIV
  DIV =T[M2.0,M1.0] DIV |[X1]| SKIP
  SKIP =T[M2.0,M1.0] SKIP |[X1]| SKIP
  DIV =T[M2.0,M1.0] DIV |[X1]| DIV
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =T[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP
  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =T[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)
  ? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =T[M1.0,M1.0] 
  (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP
  ? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =T[M1.0,M1.0] 
  SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)
  P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] SKIP) |[X1]| DIV
  DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] SKIP)
  P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] DIV) |[X1]| DIV
  DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] DIV)
  SKIP =T[M2.0,M1.0] SKIP -- X1
  DIV =T[M2.0,M1.0] DIV -- X1
  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =T[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) -- X1
  ? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 
  =T[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) -- X1
  SKIP =T[M2.0,M1.0] SKIP [[r1]]
  DIV =T[M2.0,M1.0] DIV [[r1]]
  P2.0 =T[M1.0,M1.0] SKIP ;; P2.0
  P2.0 =T[M1.0,M1.0] P2.0 ;; SKIP
  DIV =T[M2.0,M1.0] DIV ;; P1
  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [> SKIP) ;; Q1
  ? x:X1 -> (Pf1 x ;; Q1) [> DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [> DIV) ;; Q1
  SKIP =T[M2.0,M1.0] SKIP |. Suc n1
  DIV =T[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) 
  =T[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) 
  =T[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) 
  =T[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) 
  =T[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 
  =T[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 
  =T[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 
  =T[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 
  =T[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)
  ? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [+] SKIP) ;; Q1
  ? x:X1 -> (Pf1 x ;; Q1) [+] DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [+] DIV) ;; Q1

lemmas cspT_all_dist_sym: 

  P1.1 [+] Q1 |~| P2.1 [+] Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) [+] Q1
  P1 [+] Q1.1 |~| P1 [+] Q2.1 =T[M1.0,M1.0] P1 [+] (Q1.1 |~| Q2.1)
  P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |[X1]| Q1
  P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =T[M1.0,M1.0] P1 |[X1]| (Q1.1 |~| Q2.1)
  P1.1 -- X1 |~| P2.1 -- X1 =T[M1.0,M1.0] (P1.1 |~| P2.1) -- X1
  P1.1 [[r1]] |~| P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 |~| P2.1) [[r1]]
  P1.1 ;; Q1 |~| P2.1 ;; Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) ;; Q1
  P1.1 |. n1 |~| P2.1 |. n1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |. n1
  !! :C1 .. Pf1 |~| !! :C1 .. Qf1 =T[M1.0,M1.0] !! c:C1 .. (Pf1 c |~| Qf1 c)
  !nat :N1 .. Pf1 |~| !nat :N1 .. Qf1 =T[M1.0,M1.0] !nat n:N1 .. (Pf1 n |~| Qf1 n)
  !set :Xs1 .. Pf1 |~| !set :Xs1 .. Qf1 =T[M1.0,M1.0] 
  !set X:Xs1 .. (Pf1 X |~| Qf1 X)
  ! :X1 .. Pf1 |~| ! :X1 .. Qf1 =T[M1.0,M1.0] ! a:X1 .. (Pf1 a |~| Qf1 a)
  inj f1
  ==> !<f1> :X1 .. Pf1 |~| !<f1> :X1 .. Qf1 =T[M1.0,M1.0] 
      !<f1> a:X1 .. (Pf1 a |~| Qf1 a)
  IF (sumset C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =T[M1.0,M1.0] 
  (!! :C1 .. Pf1) [+] Q1
  IF (sumset C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =T[M1.0,M1.0] 
  P1 [+] (!! :C1 .. Qf1)
  IF (sumset C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 
  =T[M1.0,M1.0] (!! :C1 .. Pf1) |[X1]| Q1
  IF (sumset C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c 
  =T[M1.0,M1.0] P1 |[X1]| (!! :C1 .. Qf1)
  !! c:C1 .. Pf1 c -- X1 =T[M1.0,M1.0] (!! :C1 .. Pf1) -- X1
  !! c:C1 .. Pf1 c [[r1]] =T[M1.0,M1.0] (!! :C1 .. Pf1) [[r1]]
  !! c:C1 .. Pf1 c ;; Q1 =T[M1.0,M1.0] (!! :C1 .. Pf1) ;; Q1
  !! c:C1 .. Pf1 c |. m1 =T[M1.0,M1.0] (!! :C1 .. Pf1) |. m1
  IF (N1 = {}) THEN DIV [+] Q1 ELSE !nat n:N1 .. Pf1 n [+] Q1 =T[M1.0,M1.0] 
  (!nat :N1 .. Pf1) [+] Q1
  IF (N1 = {}) THEN P1 [+] DIV ELSE !nat n:N1 .. P1 [+] Qf1 n =T[M1.0,M1.0] 
  P1 [+] (!nat :N1 .. Qf1)
  IF (N1 = {}) THEN DIV |[X1]| Q1 ELSE !nat n:N1 .. Pf1 n |[X1]| Q1 =T[M1.0,M1.0] 
  (!nat :N1 .. Pf1) |[X1]| Q1
  IF (N1 = {}) THEN P1 |[X1]| DIV ELSE !nat n:N1 .. P1 |[X1]| Qf1 n =T[M1.0,M1.0] 
  P1 |[X1]| (!nat :N1 .. Qf1)
  !nat n:N1 .. Pf1 n -- X1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) -- X1
  !nat n:N1 .. Pf1 n [[r1]] =T[M1.0,M1.0] (!nat :N1 .. Pf1) [[r1]]
  !nat n:N1 .. Pf1 n ;; Q1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) ;; Q1
  !nat n:N1 .. Pf1 n |. m1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) |. m1
  IF (Xs1 = {}) THEN DIV [+] Q1 ELSE !set X:Xs1 .. Pf1 X [+] Q1 =T[M1.0,M1.0] 
  (!set :Xs1 .. Pf1) [+] Q1
  IF (Xs1 = {}) THEN P1 [+] DIV ELSE !set X:Xs1 .. P1 [+] Qf1 X =T[M1.0,M1.0] 
  P1 [+] (!set :Xs1 .. Qf1)
  IF (Xs1 = {}) THEN DIV |[Y1]| Q1 ELSE !set X:Xs1 .. Pf1 X |[Y1]| Q1 
  =T[M1.0,M1.0] (!set :Xs1 .. Pf1) |[Y1]| Q1
  IF (Xs1 = {}) THEN P1 |[Y1]| DIV ELSE !set X:Xs1 .. P1 |[Y1]| Qf1 X 
  =T[M1.0,M1.0] P1 |[Y1]| (!set :Xs1 .. Qf1)
  !set X:Xs1 .. Pf1 X -- Y1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) -- Y1
  !set X:Xs1 .. Pf1 X [[r1]] =T[M1.0,M1.0] (!set :Xs1 .. Pf1) [[r1]]
  !set X:Xs1 .. Pf1 X ;; Q1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) ;; Q1
  !set X:Xs1 .. Pf1 X |. m1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) |. m1
  IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =T[M1.0,M1.0] 
  (! :X1 .. Pf1) [+] Q1
  IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =T[M1.0,M1.0] 
  P1 [+] (! :X1 .. Qf1)
  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =T[M1.0,M1.0] 
  (! :Y1 .. Pf1) |[X1]| Q1
  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =T[M1.0,M1.0] 
  P1 |[X1]| (! :Y1 .. Qf1)
  ! x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (! :Y1 .. Pf1) -- X1
  ! x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (! :X1 .. Pf1) [[r1]]
  ! x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (! :X1 .. Pf1) ;; Q1
  ! x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (! :X1 .. Pf1) |. n1
  IF (X1 = {}) THEN DIV [+] Q1 ELSE !<f1> x:X1 .. Pf1 x [+] Q1 =T[M1.0,M1.0] 
  (!<f1> :X1 .. Pf1) [+] Q1
  IF (X1 = {}) THEN P1 [+] DIV ELSE !<f1> x:X1 .. P1 [+] Qf1 x =T[M1.0,M1.0] 
  P1 [+] (!<f1> :X1 .. Qf1)
  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !<f1> x:Y1 .. Pf1 x |[X1]| Q1 
  =T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) |[X1]| Q1
  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !<f1> x:Y1 .. P1 |[X1]| Qf1 x 
  =T[M1.0,M1.0] P1 |[X1]| (!<f1> :Y1 .. Qf1)
  !<f1> x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) -- X1
  !<f1> x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) [[r1]]
  !<f1> x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) ;; Q1
  !<f1> x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) |. n1
  P1.1 [[r1]] [+] P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 [+] P2.1) [[r1]]
  P1.1 |. n1 [+] P2.1 |. n1 =T[M1.0,M1.0] (P1.1 [+] P2.1) |. n1

lemmas cspT_all_dist_sym: 

  P1.1 [+] Q1 |~| P2.1 [+] Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) [+] Q1
  P1 [+] Q1.1 |~| P1 [+] Q2.1 =T[M1.0,M1.0] P1 [+] (Q1.1 |~| Q2.1)
  P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |[X1]| Q1
  P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =T[M1.0,M1.0] P1 |[X1]| (Q1.1 |~| Q2.1)
  P1.1 -- X1 |~| P2.1 -- X1 =T[M1.0,M1.0] (P1.1 |~| P2.1) -- X1
  P1.1 [[r1]] |~| P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 |~| P2.1) [[r1]]
  P1.1 ;; Q1 |~| P2.1 ;; Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) ;; Q1
  P1.1 |. n1 |~| P2.1 |. n1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |. n1
  !! :C1 .. Pf1 |~| !! :C1 .. Qf1 =T[M1.0,M1.0] !! c:C1 .. (Pf1 c |~| Qf1 c)
  !nat :N1 .. Pf1 |~| !nat :N1 .. Qf1 =T[M1.0,M1.0] !nat n:N1 .. (Pf1 n |~| Qf1 n)
  !set :Xs1 .. Pf1 |~| !set :Xs1 .. Qf1 =T[M1.0,M1.0] 
  !set X:Xs1 .. (Pf1 X |~| Qf1 X)
  ! :X1 .. Pf1 |~| ! :X1 .. Qf1 =T[M1.0,M1.0] ! a:X1 .. (Pf1 a |~| Qf1 a)
  inj f1
  ==> !<f1> :X1 .. Pf1 |~| !<f1> :X1 .. Qf1 =T[M1.0,M1.0] 
      !<f1> a:X1 .. (Pf1 a |~| Qf1 a)
  IF (sumset C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =T[M1.0,M1.0] 
  (!! :C1 .. Pf1) [+] Q1
  IF (sumset C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =T[M1.0,M1.0] 
  P1 [+] (!! :C1 .. Qf1)
  IF (sumset C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 
  =T[M1.0,M1.0] (!! :C1 .. Pf1) |[X1]| Q1
  IF (sumset C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c 
  =T[M1.0,M1.0] P1 |[X1]| (!! :C1 .. Qf1)
  !! c:C1 .. Pf1 c -- X1 =T[M1.0,M1.0] (!! :C1 .. Pf1) -- X1
  !! c:C1 .. Pf1 c [[r1]] =T[M1.0,M1.0] (!! :C1 .. Pf1) [[r1]]
  !! c:C1 .. Pf1 c ;; Q1 =T[M1.0,M1.0] (!! :C1 .. Pf1) ;; Q1
  !! c:C1 .. Pf1 c |. m1 =T[M1.0,M1.0] (!! :C1 .. Pf1) |. m1
  IF (N1 = {}) THEN DIV [+] Q1 ELSE !nat n:N1 .. Pf1 n [+] Q1 =T[M1.0,M1.0] 
  (!nat :N1 .. Pf1) [+] Q1
  IF (N1 = {}) THEN P1 [+] DIV ELSE !nat n:N1 .. P1 [+] Qf1 n =T[M1.0,M1.0] 
  P1 [+] (!nat :N1 .. Qf1)
  IF (N1 = {}) THEN DIV |[X1]| Q1 ELSE !nat n:N1 .. Pf1 n |[X1]| Q1 =T[M1.0,M1.0] 
  (!nat :N1 .. Pf1) |[X1]| Q1
  IF (N1 = {}) THEN P1 |[X1]| DIV ELSE !nat n:N1 .. P1 |[X1]| Qf1 n =T[M1.0,M1.0] 
  P1 |[X1]| (!nat :N1 .. Qf1)
  !nat n:N1 .. Pf1 n -- X1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) -- X1
  !nat n:N1 .. Pf1 n [[r1]] =T[M1.0,M1.0] (!nat :N1 .. Pf1) [[r1]]
  !nat n:N1 .. Pf1 n ;; Q1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) ;; Q1
  !nat n:N1 .. Pf1 n |. m1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) |. m1
  IF (Xs1 = {}) THEN DIV [+] Q1 ELSE !set X:Xs1 .. Pf1 X [+] Q1 =T[M1.0,M1.0] 
  (!set :Xs1 .. Pf1) [+] Q1
  IF (Xs1 = {}) THEN P1 [+] DIV ELSE !set X:Xs1 .. P1 [+] Qf1 X =T[M1.0,M1.0] 
  P1 [+] (!set :Xs1 .. Qf1)
  IF (Xs1 = {}) THEN DIV |[Y1]| Q1 ELSE !set X:Xs1 .. Pf1 X |[Y1]| Q1 
  =T[M1.0,M1.0] (!set :Xs1 .. Pf1) |[Y1]| Q1
  IF (Xs1 = {}) THEN P1 |[Y1]| DIV ELSE !set X:Xs1 .. P1 |[Y1]| Qf1 X 
  =T[M1.0,M1.0] P1 |[Y1]| (!set :Xs1 .. Qf1)
  !set X:Xs1 .. Pf1 X -- Y1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) -- Y1
  !set X:Xs1 .. Pf1 X [[r1]] =T[M1.0,M1.0] (!set :Xs1 .. Pf1) [[r1]]
  !set X:Xs1 .. Pf1 X ;; Q1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) ;; Q1
  !set X:Xs1 .. Pf1 X |. m1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) |. m1
  IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =T[M1.0,M1.0] 
  (! :X1 .. Pf1) [+] Q1
  IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =T[M1.0,M1.0] 
  P1 [+] (! :X1 .. Qf1)
  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =T[M1.0,M1.0] 
  (! :Y1 .. Pf1) |[X1]| Q1
  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =T[M1.0,M1.0] 
  P1 |[X1]| (! :Y1 .. Qf1)
  ! x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (! :Y1 .. Pf1) -- X1
  ! x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (! :X1 .. Pf1) [[r1]]
  ! x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (! :X1 .. Pf1) ;; Q1
  ! x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (! :X1 .. Pf1) |. n1
  IF (X1 = {}) THEN DIV [+] Q1 ELSE !<f1> x:X1 .. Pf1 x [+] Q1 =T[M1.0,M1.0] 
  (!<f1> :X1 .. Pf1) [+] Q1
  IF (X1 = {}) THEN P1 [+] DIV ELSE !<f1> x:X1 .. P1 [+] Qf1 x =T[M1.0,M1.0] 
  P1 [+] (!<f1> :X1 .. Qf1)
  IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !<f1> x:Y1 .. Pf1 x |[X1]| Q1 
  =T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) |[X1]| Q1
  IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !<f1> x:Y1 .. P1 |[X1]| Qf1 x 
  =T[M1.0,M1.0] P1 |[X1]| (!<f1> :Y1 .. Qf1)
  !<f1> x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) -- X1
  !<f1> x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) [[r1]]
  !<f1> x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) ;; Q1
  !<f1> x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) |. n1
  P1.1 [[r1]] [+] P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 [+] P2.1) [[r1]]
  P1.1 |. n1 [+] P2.1 |. n1 =T[M1.0,M1.0] (P1.1 [+] P2.1) |. n1

lemmas cspT_unwind_sym: 

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

lemmas cspT_unwind_sym: 

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

lemmas cspT_step_sym: 

  ? :{} -> Pf1 =T[M2.0,M1.0] STOP
  ? x:{a1} -> P1 =T[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 
  =T[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 
  =T[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) 
  =T[M1.0,M1.0] (? :Y1 -> Pf1) -- X1
  ? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =T[M1.0,M1.0] 
  (? :X1 -> Pf1) [[r1]]
  ? x:X1 -> (Pf1 x ;; Q1) =T[M1.0,M1.0] ? :X1 -> Pf1 ;; Q1
  ? x:X1 -> Pf1 x |. n1 =T[M1.0,M1.0] (? :X1 -> Pf1) |. Suc n1

lemmas cspT_step_sym: 

  ? :{} -> Pf1 =T[M2.0,M1.0] STOP
  ? x:{a1} -> P1 =T[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 
  =T[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 
  =T[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) 
  =T[M1.0,M1.0] (? :Y1 -> Pf1) -- X1
  ? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =T[M1.0,M1.0] 
  (? :X1 -> Pf1) [[r1]]
  ? x:X1 -> (Pf1 x ;; Q1) =T[M1.0,M1.0] ? :X1 -> Pf1 ;; Q1
  ? x:X1 -> Pf1 x |. n1 =T[M1.0,M1.0] (? :X1 -> Pf1) |. Suc n1