Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_law_decompo (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| June 2005 (modified) |
| September 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| December 2005 (modified) |
| April 2006 (modified) |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_law_decompo
imports CSP_T_traces
begin
(*------------------------------------------------*
| |
| laws for monotonicity and congruence |
| |
*------------------------------------------------*)
(*********************************************************
Act_prefix mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Act_prefix_mono:
"[| a = b ; P <=T[M1,M2] Q |] ==> a -> P <=T[M1,M2] b -> Q"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Act_prefix_cong:
"[| a = b ; P =T[M1,M2] Q |] ==> a -> P =T[M1,M2] b -> Q"
apply (simp add: cspT_eq_ref_iff)
apply (simp add: cspT_Act_prefix_mono)
done
(*********************************************************
Ext_pre_choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Ext_pre_choice_mono:
"[| X = Y ; !! a. a:Y ==> Pf a <=T[M1,M2] Qf a |] ==> ? :X -> Pf <=T[M1,M2] ? :Y -> Qf"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Ext_pre_choice_cong:
"[| X = Y ; !! a. a:Y ==> Pf a =T[M1,M2] Qf a |] ==> ? :X -> Pf =T[M1,M2] ? :Y -> Qf"
by (simp add: cspT_eq_ref_iff cspT_Ext_pre_choice_mono)
(*********************************************************
Ext choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Ext_choice_mono:
"[| P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |] ==> P1 [+] P2 <=T[M1,M2] Q1 [+] Q2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Ext_choice_cong:
"[| P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |] ==> P1 [+] P2 =T[M1,M2] Q1 [+] Q2"
by (simp add: cspT_eq_ref_iff cspT_Ext_choice_mono)
(*********************************************************
Int choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Int_choice_mono:
"[| P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |] ==> P1 |~| P2 <=T[M1,M2] Q1 |~| Q2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Int_choice_cong:
"[| P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |] ==> P1 |~| P2 =T[M1,M2] Q1 |~| Q2"
by (simp add: cspT_eq_ref_iff cspT_Int_choice_mono)
(*********************************************************
replicated internal choice
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Rep_int_choice_mono_traces:
"[| ALL z:Z. traces (Qf z) M1 <= traces (Pf z) M2 |]
==> (!traces :Z .. Qf) M1 <= (!traces :Z .. Pf) M2"
apply (simp add: Rep_int_choice_traces_def)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Rep_int_choice_cong_traces:
"[| ALL z:Z. traces (Pf z) M1 = traces (Qf z) M2 |]
==> (!traces :Z .. Pf) M1 = (!traces :Z .. Qf) M2"
apply (rule order_antisym)
apply (simp_all add: cspT_Rep_int_choice_mono_traces)
done
(*** mono --- nat set com fun ***)
lemma cspT_Rep_int_choice_mono_nat:
"[| N1 = N2 ; !! n. n:N1 ==> Pf n <=T[M1,M2] Qf n |]
==> !nat :N1 .. Pf <=T[M1,M2] !nat :N2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_mono_traces)
done
lemma cspT_Rep_int_choice_mono_set:
"[| Xs1 = Xs2 ; !! X. X:Xs1 ==> Pf X <=T[M1,M2] Qf X |]
==> !set :Xs1 .. Pf <=T[M1,M2] !set :Xs2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_mono_traces)
done
lemma cspT_Rep_int_choice_mono_com:
"[| X1 = X2 ; !! x. x:X1 ==> Pf x <=T[M1,M2] Qf x |]
==> ! :X1 .. Pf <=T[M1,M2] ! :X2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_mono_traces)
done
lemma cspT_Rep_int_choice_mono_f:
"[| inj f ; X1 = X2 ; !! x. x:X1 ==> Pf x <=T[M1,M2] Qf x |]
==> !<f> :X1 .. Pf <=T[M1,M2] !<f> :X2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_mono_traces)
done
lemmas cspT_Rep_int_choice_mono = cspT_Rep_int_choice_mono_nat
cspT_Rep_int_choice_mono_set
cspT_Rep_int_choice_mono_com
cspT_Rep_int_choice_mono_f
(*** cong --- nat set com fun ***)
lemma cspT_Rep_int_choice_cong_nat:
"[| N1 = N2 ; !! n. n:N1 ==> Pf n =T[M1,M2] Qf n |]
==> !nat :N1 .. Pf =T[M1,M2] !nat :N2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_cong_traces)
done
lemma cspT_Rep_int_choice_cong_set:
"[| Xs1 = Xs2 ; !! X. X:Xs1 ==> Pf X =T[M1,M2] Qf X |]
==> !set :Xs1 .. Pf =T[M1,M2] !set :Xs2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_cong_traces)
done
lemma cspT_Rep_int_choice_cong_com:
"[| X1 = X2 ; !! x. x:X1 ==> Pf x =T[M1,M2] Qf x |]
==> ! :X1 .. Pf =T[M1,M2] ! :X2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_cong_traces)
done
lemma cspT_Rep_int_choice_cong_f:
"[| inj f ; X1 = X2 ; !! x. x:X1 ==> Pf x =T[M1,M2] Qf x |]
==> !<f> :X1 .. Pf =T[M1,M2] !<f> :X2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_cong_traces)
done
lemmas cspT_Rep_int_choice_cong = cspT_Rep_int_choice_cong_nat
cspT_Rep_int_choice_cong_set
cspT_Rep_int_choice_cong_com
cspT_Rep_int_choice_cong_f
(*********************************************************
IF mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_IF_mono:
"[| b1 = b2 ; P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |]
==> IF b1 THEN P1 ELSE P2 <=T[M1,M2]
IF b2 THEN Q1 ELSE Q2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
done
lemma cspT_IF_cong:
"[| b1 = b2 ; P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |]
==> IF b1 THEN P1 ELSE P2 =T[M1,M2]
IF b2 THEN Q1 ELSE Q2"
by (simp add: cspT_eq_ref_iff cspT_IF_mono)
(*********************************************************
Parallel mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Parallel_mono:
"[| X = Y ; P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |]
==> P1 |[X]| P2 <=T[M1,M2] Q1 |[Y]| Q2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Parallel_cong:
"[| X = Y ; P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |]
==> P1 |[X]| P2 =T[M1,M2] Q1 |[Y]| Q2"
by (simp add: cspT_eq_ref_iff cspT_Parallel_mono)
(*********************************************************
Hiding mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Hiding_mono:
"[| X = Y ; P <=T[M1,M2] Q |] ==> P -- X <=T[M1,M2] Q -- Y"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Hiding_cong:
"[| X = Y ; P =T[M1,M2] Q |] ==> P -- X =T[M1,M2] Q -- Y"
by (simp add: cspT_eq_ref_iff cspT_Hiding_mono)
(*********************************************************
Renaming mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Renaming_mono:
"[| r1 = r2 ; P <=T[M1,M2] Q |] ==> P [[r1]] <=T[M1,M2] Q [[r2]]"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Renaming_cong:
"[| r1 = r2 ; P =T[M1,M2] Q |] ==> P [[r1]] =T[M1,M2] Q [[r2]]"
by (simp add: cspT_eq_ref_iff cspT_Renaming_mono)
(*********************************************************
Sequential composition mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Seq_compo_mono:
"[| P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |]
==> P1 ;; P2 <=T[M1,M2] Q1 ;; Q2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
apply (fast)
done
lemma cspT_Seq_compo_cong:
"[| P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |] ==> P1 ;; P2 =T[M1,M2] Q1 ;; Q2"
by (simp add: cspT_eq_ref_iff cspT_Seq_compo_mono)
(*********************************************************
Depth_rest mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Depth_rest_mono:
"[| n1 = n2 ; P <=T[M1,M2] Q |] ==> P |. n1 <=T[M1,M2] Q |. n2"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_traces)
done
lemma cspT_Depth_rest_cong:
"[| n1 = n2 ; P =T[M1,M2] Q |] ==> P |. n1 =T[M1,M2] Q |. n2"
by (simp add: cspT_eq_ref_iff cspT_Depth_rest_mono)
(*********************************************************
Timeout mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspT_Timeout_mono:
"[| P1 <=T[M1,M2] Q1 ; P2 <=T[M1,M2] Q2 |]
==> P1 [> P2 <=T[M1,M2] Q1 [> Q2"
apply (rule cspT_Ext_choice_mono)
apply (rule cspT_Int_choice_mono)
apply (simp_all)
done
lemma cspT_Timeout_cong:
"[| P1 =T[M1,M2] Q1 ; P2 =T[M1,M2] Q2 |]
==> P1 [> P2 =T[M1,M2] Q1 [> Q2"
by (simp add: cspT_eq_ref_iff cspT_Timeout_mono)
(*------------------------------------------------------*
| alias |
*------------------------------------------------------*)
lemmas cspT_free_mono =
cspT_Ext_choice_mono cspT_Int_choice_mono cspT_Parallel_mono
cspT_Hiding_mono cspT_Renaming_mono cspT_Seq_compo_mono
cspT_Depth_rest_mono
lemmas cspT_mono = cspT_free_mono
cspT_Act_prefix_mono cspT_Ext_pre_choice_mono
cspT_Rep_int_choice_mono cspT_IF_mono
lemmas cspT_free_cong =
cspT_Ext_choice_cong cspT_Int_choice_cong cspT_Parallel_cong
cspT_Hiding_cong cspT_Renaming_cong cspT_Seq_compo_cong
cspT_Depth_rest_cong
lemmas cspT_cong = cspT_free_cong
cspT_Act_prefix_cong cspT_Ext_pre_choice_cong
cspT_Rep_int_choice_cong cspT_IF_cong
lemmas cspT_free_decompo = cspT_free_mono cspT_free_cong
lemmas cspT_decompo = cspT_mono cspT_cong
lemmas cspT_rm_head_mono = cspT_Act_prefix_mono cspT_Ext_pre_choice_mono
lemmas cspT_rm_head_cong = cspT_Act_prefix_cong cspT_Ext_pre_choice_cong
lemmas cspT_rm_head = cspT_rm_head_mono cspT_rm_head_cong
(*-------------------------------------------------------*
| decomposition with ALL and EX |
*-------------------------------------------------------*)
(*** Rep_int_choice ***)
lemma cspT_Rep_int_choice_traces_decompo_ALL_EX_ref:
"ALL z1:Z1. EX z2:Z2. traces (Pf z1) M1 <= traces (Qf z2) M2
==> (!traces :Z1 .. Pf) M1 <= (!traces :Z2 .. Qf) M2"
apply (simp add: Rep_int_choice_traces_def)
apply (rule, simp add: in_traces)
apply (erule disjE)
apply (simp)
apply (elim bexE)
apply (drule_tac x="z" in bspec, simp)
apply (erule bexE)
apply (rule disjI2)
apply (rule_tac x="z2" in bexI)
apply (erule subdomTE)
apply (simp_all)
done
lemma cspT_Rep_int_choice_nat_decompo_ALL_EX_ref:
"ALL n2:N2. EX n1:N1. (Pf n1) <=T[M1,M2] (Qf n2)
==> !nat :N1 .. Pf <=T[M1,M2] !nat :N2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_decompo_ALL_EX_ref)
done
lemma cspT_Rep_int_choice_set_decompo_ALL_EX_ref:
"ALL X2:Xs2. EX X1:Xs1. (Pf X1) <=T[M1,M2] (Qf X2)
==> !set :Xs1 .. Pf <=T[M1,M2] !set :Xs2 .. Qf"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_decompo_ALL_EX_ref)
done
lemmas cspT_Rep_int_choice_decompo_ALL_EX_ref =
cspT_Rep_int_choice_nat_decompo_ALL_EX_ref
cspT_Rep_int_choice_set_decompo_ALL_EX_ref
lemma cspT_Rep_int_choice_nat_decompo_ALL_EX_eq:
"[| ALL n1:N1. EX n2:N2. (Pf n1) =T[M1,M2] (Qf n2) ;
ALL n2:N2. EX n1:N1. (Pf n1) =T[M1,M2] (Qf n2) |]
==> !nat :N1 .. Pf =T[M1,M2] !nat :N2 .. Qf"
apply (simp add: cspT_eq_ref_iff)
apply (rule conjI)
apply (rule cspT_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
apply (rule cspT_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
done
lemma cspT_Rep_int_choice_set_decompo_ALL_EX_eq:
"[| ALL X1:Xs1. EX X2:Xs2. (Pf X1) =T[M1,M2] (Qf X2) ;
ALL X2:Xs2. EX X1:Xs1. (Pf X1) =T[M1,M2] (Qf X2) |]
==> !set :Xs1 .. Pf =T[M1,M2] !set :Xs2 .. Qf"
apply (simp add: cspT_eq_ref_iff)
apply (rule conjI)
apply (rule cspT_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
apply (rule cspT_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
done
lemmas cspT_Rep_int_choice_decompo_ALL_EX_eq =
cspT_Rep_int_choice_nat_decompo_ALL_EX_eq
cspT_Rep_int_choice_set_decompo_ALL_EX_eq
lemmas cspT_Rep_int_choice_decompo_ALL_EX
= cspT_Rep_int_choice_decompo_ALL_EX_ref
cspT_Rep_int_choice_decompo_ALL_EX_eq
end
lemma cspT_Act_prefix_mono:
[| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
lemma cspT_Act_prefix_cong:
[| a = b; P =T[M1.0,M2.0] Q |] ==> a -> P =T[M1.0,M2.0] b -> Q
lemma cspT_Ext_pre_choice_mono:
[| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |] ==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
lemma cspT_Ext_pre_choice_cong:
[| X = Y; !!a. a ∈ Y ==> Pf a =T[M1.0,M2.0] Qf a |] ==> ? :X -> Pf =T[M1.0,M2.0] ? :Y -> Qf
lemma cspT_Ext_choice_mono:
[| 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
lemma cspT_Ext_choice_cong:
[| 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
lemma cspT_Int_choice_mono:
[| 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
lemma cspT_Int_choice_cong:
[| 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
lemma cspT_Rep_int_choice_mono_traces:
∀z∈Z. traces (Qf z) M1.0 ≤ traces (Pf z) M2.0 ==> (!traces :Z .. Qf) M1.0 ≤ (!traces :Z .. Pf) M2.0
lemma cspT_Rep_int_choice_cong_traces:
∀z∈Z. traces (Pf z) M1.0 = traces (Qf z) M2.0 ==> (!traces :Z .. Pf) M1.0 = (!traces :Z .. Qf) M2.0
lemma cspT_Rep_int_choice_mono_nat:
[| 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
lemma cspT_Rep_int_choice_mono_set:
[| 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
lemma cspT_Rep_int_choice_mono_com:
[| 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
lemma cspT_Rep_int_choice_mono_f:
[| 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
lemmas cspT_Rep_int_choice_mono:
[| 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
[| 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
[| 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
lemmas cspT_Rep_int_choice_mono:
[| 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
[| 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
[| 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
lemma cspT_Rep_int_choice_cong_nat:
[| 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
lemma cspT_Rep_int_choice_cong_set:
[| 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
lemma cspT_Rep_int_choice_cong_com:
[| 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
lemma cspT_Rep_int_choice_cong_f:
[| 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
lemmas cspT_Rep_int_choice_cong:
[| 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
[| 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
[| 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
lemmas cspT_Rep_int_choice_cong:
[| 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
[| 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
[| 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
lemma cspT_IF_mono:
[| 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
lemma cspT_IF_cong:
[| 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
lemma cspT_Parallel_mono:
[| 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
lemma cspT_Parallel_cong:
[| 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
lemma cspT_Hiding_mono:
[| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
lemma cspT_Hiding_cong:
[| X = Y; P =T[M1.0,M2.0] Q |] ==> P -- X =T[M1.0,M2.0] Q -- Y
lemma cspT_Renaming_mono:
[| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
lemma cspT_Renaming_cong:
[| r1.0 = r2.0; P =T[M1.0,M2.0] Q |] ==> P [[r1.0]] =T[M1.0,M2.0] Q [[r2.0]]
lemma cspT_Seq_compo_mono:
[| 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
lemma cspT_Seq_compo_cong:
[| 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
lemma cspT_Depth_rest_mono:
[| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
lemma cspT_Depth_rest_cong:
[| n1.0 = n2.0; P =T[M1.0,M2.0] Q |] ==> P |. n1.0 =T[M1.0,M2.0] Q |. n2.0
lemma cspT_Timeout_mono:
[| 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
lemma cspT_Timeout_cong:
[| 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
lemmas cspT_free_mono:
[| 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
lemmas cspT_free_mono:
[| 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
lemmas cspT_mono:
[| 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
[| 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
[| 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
[| 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_mono:
[| 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
[| 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
[| 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
[| 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_free_cong:
[| 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
lemmas cspT_free_cong:
[| 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
lemmas cspT_cong:
[| 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
[| 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
[| 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
[| 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_cong:
[| 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
[| 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
[| 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
[| 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_free_decompo:
[| 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
[| 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
lemmas cspT_free_decompo:
[| 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
[| 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
lemmas cspT_decompo:
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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:
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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
[| 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_rm_head_mono:
[| 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
lemmas cspT_rm_head_mono:
[| 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
lemmas cspT_rm_head_cong:
[| 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
lemmas cspT_rm_head_cong:
[| 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
lemmas cspT_rm_head:
[| 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
[| 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
lemmas cspT_rm_head:
[| 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
[| 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
lemma cspT_Rep_int_choice_traces_decompo_ALL_EX_ref:
∀z1∈Z1.0. ∃z2∈Z2.0. traces (Pf z1) M1.0 ≤ traces (Qf z2) M2.0 ==> (!traces :Z1.0 .. Pf) M1.0 ≤ (!traces :Z2.0 .. Qf) M2.0
lemma cspT_Rep_int_choice_nat_decompo_ALL_EX_ref:
∀n2∈N2.0. ∃n1∈N1.0. Pf n1 <=T[M1.0,M2.0] Qf n2 ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
lemma cspT_Rep_int_choice_set_decompo_ALL_EX_ref:
∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 <=T[M1.0,M2.0] Qf X2 ==> !set :Xs1.0 .. Pf <=T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX_ref:
∀n2∈N2.0. ∃n1∈N1.0. Pf n1 <=T[M1.0,M2.0] Qf n2 ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 <=T[M1.0,M2.0] Qf X2 ==> !set :Xs1.0 .. Pf <=T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX_ref:
∀n2∈N2.0. ∃n1∈N1.0. Pf n1 <=T[M1.0,M2.0] Qf n2 ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 <=T[M1.0,M2.0] Qf X2 ==> !set :Xs1.0 .. Pf <=T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemma cspT_Rep_int_choice_nat_decompo_ALL_EX_eq:
[| ∀n1∈N1.0. ∃n2∈N2.0. Pf n1 =T[M1.0,M2.0] Qf n2; ∀n2∈N2.0. ∃n1∈N1.0. Pf n1 =T[M1.0,M2.0] Qf n2 |] ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
lemma cspT_Rep_int_choice_set_decompo_ALL_EX_eq:
[| ∀X1∈Xs1.0. ∃X2∈Xs2.0. Pf X1 =T[M1.0,M2.0] Qf X2; ∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 =T[M1.0,M2.0] Qf X2 |] ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX_eq:
[| ∀n1∈N1.0. ∃n2∈N2.0. Pf n1 =T[M1.0,M2.0] Qf n2; ∀n2∈N2.0. ∃n1∈N1.0. Pf n1 =T[M1.0,M2.0] Qf n2 |] ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
[| ∀X1∈Xs1.0. ∃X2∈Xs2.0. Pf X1 =T[M1.0,M2.0] Qf X2; ∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 =T[M1.0,M2.0] Qf X2 |] ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX_eq:
[| ∀n1∈N1.0. ∃n2∈N2.0. Pf n1 =T[M1.0,M2.0] Qf n2; ∀n2∈N2.0. ∃n1∈N1.0. Pf n1 =T[M1.0,M2.0] Qf n2 |] ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
[| ∀X1∈Xs1.0. ∃X2∈Xs2.0. Pf X1 =T[M1.0,M2.0] Qf X2; ∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 =T[M1.0,M2.0] Qf X2 |] ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX:
∀n2∈N2.0. ∃n1∈N1.0. Pf n1 <=T[M1.0,M2.0] Qf n2 ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 <=T[M1.0,M2.0] Qf X2 ==> !set :Xs1.0 .. Pf <=T[M1.0,M2.0] !set :Xs2.0 .. Qf
[| ∀n1∈N1.0. ∃n2∈N2.0. Pf n1 =T[M1.0,M2.0] Qf n2; ∀n2∈N2.0. ∃n1∈N1.0. Pf n1 =T[M1.0,M2.0] Qf n2 |] ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
[| ∀X1∈Xs1.0. ∃X2∈Xs2.0. Pf X1 =T[M1.0,M2.0] Qf X2; ∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 =T[M1.0,M2.0] Qf X2 |] ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
lemmas cspT_Rep_int_choice_decompo_ALL_EX:
∀n2∈N2.0. ∃n1∈N1.0. Pf n1 <=T[M1.0,M2.0] Qf n2 ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 <=T[M1.0,M2.0] Qf X2 ==> !set :Xs1.0 .. Pf <=T[M1.0,M2.0] !set :Xs2.0 .. Qf
[| ∀n1∈N1.0. ∃n2∈N2.0. Pf n1 =T[M1.0,M2.0] Qf n2; ∀n2∈N2.0. ∃n1∈N1.0. Pf n1 =T[M1.0,M2.0] Qf n2 |] ==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
[| ∀X1∈Xs1.0. ∃X2∈Xs2.0. Pf X1 =T[M1.0,M2.0] Qf X2; ∀X2∈Xs2.0. ∃X1∈Xs1.0. Pf X1 =T[M1.0,M2.0] Qf X2 |] ==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf