Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F
theory CSP_F_law_decompo (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| June 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_F_law_decompo = CSP_F_domain + CSP_T_law_decompo:
(*------------------------------------------------*
| |
| laws for monotonicity and congruence |
| |
*------------------------------------------------*)
(*********************************************************
Act_prefix mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Act_prefix_mono:
"[| a = b ; P <=F Q |] ==> a -> P <=F b -> Q"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Act_prefix_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Act_prefix_cong:
"[| a = b ; P =F Q |] ==> a -> P =F b -> Q"
apply (simp add: cspF_eq_ref_iff)
apply (simp add: cspF_Act_prefix_mono)
done
(*********************************************************
Ext_pre_choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Ext_pre_choice_mono:
"[| X = Y ; !! a. a:Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_pre_choice_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Ext_pre_choice_cong:
"[| X = Y ; !! a. a:Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf"
by (simp add: cspF_eq_ref_iff cspF_Ext_pre_choice_mono)
(*********************************************************
Ext choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Ext_choice_mono:
"[| P1 <=F Q1 ; P2 <=F Q2 |] ==> P1 [+] P2 <=F Q1 [+] Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_mono)
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (elim conjE disjE)
apply (force)+
done
lemma cspF_Ext_choice_cong:
"[| P1 =F Q1 ; P2 =F Q2 |] ==> P1 [+] P2 =F Q1 [+] Q2"
by (simp add: cspF_eq_ref_iff cspF_Ext_choice_mono)
(*********************************************************
Int choice mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Int_choice_mono:
"[| P1 <=F Q1 ; P2 <=F Q2 |] ==> P1 |~| P2 <=F Q1 |~| Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Int_choice_cong:
"[| P1 =F Q1 ; P2 =F Q2 |] ==> P1 |~| P2 =F Q1 |~| Q2"
by (simp add: cspF_eq_ref_iff cspF_Int_choice_mono)
(*********************************************************
replicated internal choice
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Rep_int_choice_mono0:
"[| C1 = C2 ; !! c. c:C2 ==> Pf c <=F Qf c |]
==> !! :C1 .. Pf <=F !! :C2 .. Qf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_mono0)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Rep_int_choice_cong0:
"[| C1 = C2 ; !! c. c:C2 ==> Pf c =F Qf c |]
==> !! :C1 .. Pf =F !! :C2 .. Qf"
by (simp add: cspF_eq_ref_iff cspF_Rep_int_choice_mono0)
(*** fun ***)
lemma cspF_Rep_int_choice_mono_fun:
"[| inj f ; X = Y ; !! a. a:Y ==> Pf a <=F Qf a |]
==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice_mono0)
apply (auto)
done
lemma cspF_Rep_int_choice_cong_fun:
"[| inj f ; X = Y ; !! a. a:Y ==> Pf a =F Qf a |]
==> !!<f> :X .. Pf =F !!<f> :Y .. Qf"
by (simp add: cspF_eq_ref_iff cspF_Rep_int_choice_mono_fun)
(*** set ***)
lemma cspF_Rep_int_choice_mono_set:
"[| Xs = Ys ; !! X. X:Ys ==> Pf X <=F Qf X |]
==> !set :Xs .. Pf <=F !set :Ys .. Qf"
by (simp add: cspF_Rep_int_choice_mono_fun)
lemma cspF_Rep_int_choice_cong_set:
"[| Xs = Ys ; !! X. X:Ys ==> Pf X =F Qf X |]
==> !set :Xs .. Pf =F !set :Ys .. Qf"
by (simp add: cspF_Rep_int_choice_cong_fun)
(*** nat ***)
lemma cspF_Rep_int_choice_mono_nat:
"[| N1 = N2 ; !! n. n:N2 ==> Pf n <=F Qf n |]
==> !nat :N1 .. Pf <=F !nat :N2 .. Qf"
by (simp add: cspF_Rep_int_choice_mono_fun)
lemma cspF_Rep_int_choice_cong_nat:
"[| N1 = N2 ; !! n. n:N2 ==> Pf n =F Qf n |]
==> !nat :N1 .. Pf =F !nat :N2 .. Qf"
by (simp add: cspF_Rep_int_choice_cong_fun)
(*** com ***)
lemma cspF_Rep_int_choice_mono_com:
"[| X = Y ; !! a. a:Y ==> Pf a <=F Qf a |]
==> ! :X .. Pf <=F ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_mono_set)
by (auto)
lemma cspF_Rep_int_choice_cong_com:
"[| X = Y ; !! a. a:Y ==> Pf a =F Qf a |]
==> ! :X .. Pf =F ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_cong_set)
by (auto)
(*** f ***)
lemma cspF_Rep_int_choice_mono_f:
"[| inj f ; X = Y ; !! a. a:Y ==> Pf a <=F Qf a |]
==> !<f> :X .. Pf <=F !<f> :Y .. Qf"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice_mono_com)
apply (auto)
done
lemma cspF_Rep_int_choice_cong_f:
"[| inj f ; X = Y ; !! a. a:Y ==> Pf a =F Qf a |]
==> !<f> :X .. Pf =F !<f> :Y .. Qf"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice_cong_com)
apply (auto)
done
lemmas cspF_Rep_int_choice_mono = cspF_Rep_int_choice_mono0
cspF_Rep_int_choice_mono_com
cspF_Rep_int_choice_mono_set
cspF_Rep_int_choice_mono_nat
cspF_Rep_int_choice_mono_f
lemmas cspF_Rep_int_choice_cong = cspF_Rep_int_choice_cong0
cspF_Rep_int_choice_cong_com
cspF_Rep_int_choice_cong_set
cspF_Rep_int_choice_cong_nat
cspF_Rep_int_choice_cong_f
(*********************************************************
IF mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_IF_mono:
"[| b1 = b2 ; P1 <=F Q1 ; P2 <=F Q2 |]
==> IF b1 THEN P1 ELSE P2 <=F
IF b2 THEN Q1 ELSE Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_IF_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
done
lemma cspF_IF_cong:
"[| b1 = b2 ; P1 =F Q1 ; P2 =F Q2 |]
==> IF b1 THEN P1 ELSE P2 =F
IF b2 THEN Q1 ELSE Q2"
by (simp add: cspF_eq_ref_iff cspF_IF_mono)
(*********************************************************
Parallel mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Parallel_mono:
"[| X = Y ; P1 <=F Q1 ; P2 <=F Q2 |]
==> P1 |[X]| P2 <=F Q1 |[Y]| Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Parallel_cong:
"[| X = Y ; P1 =F Q1 ; P2 =F Q2 |]
==> P1 |[X]| P2 =F Q1 |[Y]| Q2"
by (simp add: cspF_eq_ref_iff cspF_Parallel_mono)
(*********************************************************
Hiding mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Hiding_mono:
"[| X = Y ; P <=F Q |] ==> P -- X <=F Q -- Y"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Hiding_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Hiding_cong:
"[| X = Y ; P =F Q |] ==> P -- X =F Q -- Y"
by (simp add: cspF_eq_ref_iff cspF_Hiding_mono)
(*********************************************************
Renaming mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Renaming_mono:
"[| r1 = r2 ; P <=F Q |] ==> P [[r1]] <=F Q [[r2]]"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Renaming_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Renaming_cong:
"[| r1 = r2 ; P =F Q |] ==> P [[r1]] =F Q [[r2]]"
by (simp add: cspF_eq_ref_iff cspF_Renaming_mono)
(*********************************************************
Sequential composition mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Seq_compo_mono:
"[| P1 <=F Q1 ; P2 <=F Q2 |]
==> P1 ;; P2 <=F Q1 ;; Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_mono)
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
apply (fast)
done
lemma cspF_Seq_compo_cong:
"[| P1 =F Q1 ; P2 =F Q2 |] ==> P1 ;; P2 =F Q1 ;; Q2"
by (simp add: cspF_eq_ref_iff cspF_Seq_compo_mono)
(*********************************************************
Depth_rest mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Depth_rest_mono:
"[| n1 = n2 ; P <=F Q |] ==> P |. n1 <=F Q |. n2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_mono)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_failures)
done
lemma cspF_Depth_rest_cong:
"[| n1 = n2 ; P =F Q |] ==> P |. n1 =F Q |. n2"
by (simp add: cspF_eq_ref_iff cspF_Depth_rest_mono)
(*********************************************************
Timeout mono
*********************************************************)
(*------------------*
| csp law |
*------------------*)
lemma cspF_Timeout_mono:
"[| P1 <=F Q1 ; P2 <=F Q2 |]
==> P1 [> P2 <=F Q1 [> Q2"
apply (rule cspF_Ext_choice_mono)
apply (rule cspF_Int_choice_mono)
by (simp_all)
lemma cspF_Timeout_cong:
"[| P1 =F Q1 ; P2 =F Q2 |]
==> P1 [> P2 =F Q1 [> Q2"
by (simp add: cspF_eq_ref_iff cspF_Timeout_mono)
(*------------------------------------------------------*
| alias |
*------------------------------------------------------*)
lemmas cspF_free_mono =
cspF_Ext_choice_mono cspF_Int_choice_mono cspF_Parallel_mono
cspF_Hiding_mono cspF_Renaming_mono cspF_Seq_compo_mono
cspF_Depth_rest_mono
lemmas cspF_mono = cspF_free_mono
cspF_Act_prefix_mono cspF_Ext_pre_choice_mono
cspF_Rep_int_choice_mono cspF_IF_mono
lemmas cspF_free_cong =
cspF_Ext_choice_cong cspF_Int_choice_cong cspF_Parallel_cong
cspF_Hiding_cong cspF_Renaming_cong cspF_Seq_compo_cong
cspF_Depth_rest_cong
lemmas cspF_cong = cspF_free_cong
cspF_Act_prefix_cong cspF_Ext_pre_choice_cong
cspF_Rep_int_choice_cong cspF_IF_cong
lemmas cspF_free_decompo = cspF_free_mono cspF_free_cong
lemmas cspF_decompo = cspF_mono cspF_cong
lemmas cspF_rm_head_mono = cspF_Act_prefix_mono cspF_Ext_pre_choice_mono
lemmas cspF_rm_head_cong = cspF_Act_prefix_cong cspF_Ext_pre_choice_cong
lemmas cspF_rm_head = cspF_rm_head_mono cspF_rm_head_cong
(*-------------------------------------------------------*
| decomposition with ALL and EX |
*-------------------------------------------------------*)
(*** Rep_int_choice ***)
lemma cspF_Rep_int_choice_decompo_ALL_EX_ref:
"ALL c2:C2. EX c1:C1. Pf c1 <=F Qf c2
==> !! :C1 .. Pf <=F !! :C2 .. Qf"
apply (simp add: cspF_cspT_semantics)
apply (rule conjI)
apply (rule cspT_Rep_int_choice_decompo_ALL_EX_ref)
apply (fast)
apply (rule)
apply (simp add: in_failures)
apply (erule bexE)
apply (drule_tac x="c" in bspec, simp)
apply (erule bexE)
apply (rule_tac x="c1" in bexI)
apply (erule conjE)
apply (erule subsetFE)
apply (simp_all)
done
lemma cspF_Rep_int_choice_decompo_ALL_EX_eq:
"[| ALL c1:C1. EX c2:C2. Pf c1 =F Qf c2 ;
ALL c2:C2. EX c1:C1. Pf c1 =F Qf c2 |]
==> !! :C1 .. Pf =F !! :C2 .. Qf"
apply (simp add: cspF_eq_ref_iff)
apply (rule conjI)
apply (rule cspF_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
apply (rule cspF_Rep_int_choice_decompo_ALL_EX_ref)
apply (force)
done
lemmas cspF_Rep_int_choice_decompo_ALL_EX
= cspF_Rep_int_choice_decompo_ALL_EX_ref
cspF_Rep_int_choice_decompo_ALL_EX_eq
lemma cspF_Rep_int_choice_fun_decompo_ALL_EX_ref:
"[| inj f ; ALL y:Y. EX x:X. Pf x <=F Qf y |]
==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice_decompo_ALL_EX_ref)
apply (auto)
done
lemma cspF_Rep_int_choice_fun_decompo_ALL_EX_eq:
"[| inj f;
ALL x:X. EX y:Y. Pf x =F Qf y ;
ALL y:Y. EX x:X. Pf x =F Qf y |]
==> !!<f> :X .. Pf =F !!<f> :Y .. Qf"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice_decompo_ALL_EX_eq)
apply (auto)
done
lemmas cspF_Rep_int_choice_fun_decompo_ALL_EX
= cspF_Rep_int_choice_fun_decompo_ALL_EX_ref
cspF_Rep_int_choice_fun_decompo_ALL_EX_eq
lemma cspF_Rep_int_choice_com_decompo_ALL_EX_ref:
"[| ALL y:Y. EX x:X. Pf x <=F Qf y |]
==> ! :X .. Pf <=F ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_fun_decompo_ALL_EX_ref)
apply (simp)
apply (intro ballI)
apply (drule_tac x="contents y" in bspec)
apply (force)
apply (simp)
apply (elim exE bexE conjE)
apply (rule_tac x="{x}" in exI)
apply (simp)
done
lemma cspF_Rep_int_choice_com_decompo_ALL_EX_eq:
"[| ALL x:X. EX y:Y. Pf x =F Qf y ;
ALL y:Y. EX x:X. Pf x =F Qf y |]
==> ! :X .. Pf =F ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_fun_decompo_ALL_EX_eq)
apply (simp)
apply (intro ballI)
apply (drule_tac x="contents x" in bspec)
apply (force)
apply (simp)
apply (elim exE bexE conjE)
apply (rule_tac x="{y}" in exI)
apply (simp)
apply (intro ballI)
apply (rotate_tac 1)
apply (drule_tac x="contents y" in bspec)
apply (force)
apply (simp)
apply (elim exE bexE conjE)
apply (rule_tac x="{x}" in exI)
apply (simp)
done
lemmas cspF_Rep_int_choice_com_decompo_ALL_EX
= cspF_Rep_int_choice_com_decompo_ALL_EX_ref
cspF_Rep_int_choice_com_decompo_ALL_EX_eq
end
lemma cspF_Act_prefix_mono:
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
lemma cspF_Act_prefix_cong:
[| a = b; P =F Q |] ==> a -> P =F b -> Q
lemma cspF_Ext_pre_choice_mono:
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
lemma cspF_Ext_pre_choice_cong:
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
lemma cspF_Ext_choice_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
lemma cspF_Ext_choice_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
lemma cspF_Int_choice_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
lemma cspF_Int_choice_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
lemma cspF_Rep_int_choice_mono0:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
lemma cspF_Rep_int_choice_cong0:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
lemma cspF_Rep_int_choice_mono_fun:
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf
lemma cspF_Rep_int_choice_cong_fun:
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !!<f> :X .. Pf =F !!<f> :Y .. Qf
lemma cspF_Rep_int_choice_mono_set:
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
lemma cspF_Rep_int_choice_cong_set:
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
lemma cspF_Rep_int_choice_mono_nat:
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
lemma cspF_Rep_int_choice_cong_nat:
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
lemma cspF_Rep_int_choice_mono_com:
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
lemma cspF_Rep_int_choice_cong_com:
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
lemma cspF_Rep_int_choice_mono_f:
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
lemma cspF_Rep_int_choice_cong_f:
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
lemmas cspF_Rep_int_choice_mono:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
lemmas cspF_Rep_int_choice_mono:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
lemmas cspF_Rep_int_choice_cong:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
lemmas cspF_Rep_int_choice_cong:
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
lemma cspF_IF_mono:
[| b1.0 = b2.0; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F IF b2.0 THEN Q1.0 ELSE Q2.0
lemma cspF_IF_cong:
[| b1.0 = b2.0; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 =F IF b2.0 THEN Q1.0 ELSE Q2.0
lemma cspF_Parallel_mono:
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
lemma cspF_Parallel_cong:
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
lemma cspF_Hiding_mono:
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
lemma cspF_Hiding_cong:
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
lemma cspF_Renaming_mono:
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
lemma cspF_Renaming_cong:
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
lemma cspF_Seq_compo_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
lemma cspF_Seq_compo_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
lemma cspF_Depth_rest_mono:
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
lemma cspF_Depth_rest_cong:
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
lemma cspF_Timeout_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [> P2.0 <=F Q1.0 [> Q2.0
lemma cspF_Timeout_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [> P2.0 =F Q1.0 [> Q2.0
lemmas cspF_free_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
lemmas cspF_free_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
lemmas cspF_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_mono:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_free_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
lemmas cspF_free_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
lemmas cspF_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 =F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_cong:
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 =F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_free_decompo:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
lemmas cspF_free_decompo:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
lemmas cspF_decompo:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F IF b2.0 THEN Q1.0 ELSE Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 =F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_decompo:
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 [+] P2.0 <=F Q1.0 [+] Q2.0
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |~| P2.0 <=F Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 |[X]| P2.0 <=F Q1.0 |[Y]| Q2.0
[| X = Y; P <=F Q |] ==> P -- X <=F Q -- Y
[| r1.0 = r2.0; P <=F Q |] ==> P [[r1.0]] <=F Q [[r2.0]]
[| P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> P1.0 ;; P2.0 <=F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F Q |] ==> P |. n1.0 <=F Q |. n2.0
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |] ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X <=F Qf X |] ==> !set :Xs .. Pf <=F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |] ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 <=F Q1.0; P2.0 <=F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 <=F IF b2.0 THEN Q1.0 ELSE Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 [+] P2.0 =F Q1.0 [+] Q2.0
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |~| P2.0 =F Q1.0 |~| Q2.0
[| X = Y; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 |[X]| P2.0 =F Q1.0 |[Y]| Q2.0
[| X = Y; P =F Q |] ==> P -- X =F Q -- Y
[| r1.0 = r2.0; P =F Q |] ==> P [[r1.0]] =F Q [[r2.0]]
[| P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> P1.0 ;; P2.0 =F Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F Q |] ==> P |. n1.0 =F Q |. n2.0
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ C2.0 ==> Pf c =F Qf c |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ! :X .. Pf =F ! :Y .. Qf
[| Xs = Ys; !!X. X ∈ Ys ==> Pf X =F Qf X |] ==> !set :Xs .. Pf =F !set :Ys .. Qf
[| N1.0 = N2.0; !!n. n ∈ N2.0 ==> Pf n =F Qf n |] ==> !nat :N1.0 .. Pf =F !nat :N2.0 .. Qf
[| inj f; X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> !<f> :X .. Pf =F !<f> :Y .. Qf
[| b1.0 = b2.0; P1.0 =F Q1.0; P2.0 =F Q2.0 |] ==> IF b1.0 THEN P1.0 ELSE P2.0 =F IF b2.0 THEN Q1.0 ELSE Q2.0
lemmas cspF_rm_head_mono:
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
lemmas cspF_rm_head_mono:
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
lemmas cspF_rm_head_cong:
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
lemmas cspF_rm_head_cong:
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
lemmas cspF_rm_head:
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
lemmas cspF_rm_head:
[| a = b; P <=F Q |] ==> a -> P <=F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ? :X -> Pf <=F ? :Y -> Qf
[| a = b; P =F Q |] ==> a -> P =F b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =F Qf a |] ==> ? :X -> Pf =F ? :Y -> Qf
lemma cspF_Rep_int_choice_decompo_ALL_EX_ref:
∀c2∈C2.0. ∃c1∈C1.0. Pf c1 <=F Qf c2 ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
lemma cspF_Rep_int_choice_decompo_ALL_EX_eq:
[| ∀c1∈C1.0. ∃c2∈C2.0. Pf c1 =F Qf c2; ∀c2∈C2.0. ∃c1∈C1.0. Pf c1 =F Qf c2 |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
lemmas cspF_Rep_int_choice_decompo_ALL_EX:
∀c2∈C2.0. ∃c1∈C1.0. Pf c1 <=F Qf c2 ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| ∀c1∈C1.0. ∃c2∈C2.0. Pf c1 =F Qf c2; ∀c2∈C2.0. ∃c1∈C1.0. Pf c1 =F Qf c2 |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
lemmas cspF_Rep_int_choice_decompo_ALL_EX:
∀c2∈C2.0. ∃c1∈C1.0. Pf c1 <=F Qf c2 ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
[| ∀c1∈C1.0. ∃c2∈C2.0. Pf c1 =F Qf c2; ∀c2∈C2.0. ∃c1∈C1.0. Pf c1 =F Qf c2 |] ==> !! :C1.0 .. Pf =F !! :C2.0 .. Qf
lemma cspF_Rep_int_choice_fun_decompo_ALL_EX_ref:
[| inj f; ∀y∈Y. ∃x∈X. Pf x <=F Qf y |] ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf
lemma cspF_Rep_int_choice_fun_decompo_ALL_EX_eq:
[| inj f; ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> !!<f> :X .. Pf =F !!<f> :Y .. Qf
lemmas cspF_Rep_int_choice_fun_decompo_ALL_EX:
[| inj f; ∀y∈Y. ∃x∈X. Pf x <=F Qf y |] ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf
[| inj f; ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> !!<f> :X .. Pf =F !!<f> :Y .. Qf
lemmas cspF_Rep_int_choice_fun_decompo_ALL_EX:
[| inj f; ∀y∈Y. ∃x∈X. Pf x <=F Qf y |] ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf
[| inj f; ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> !!<f> :X .. Pf =F !!<f> :Y .. Qf
lemma cspF_Rep_int_choice_com_decompo_ALL_EX_ref:
∀y∈Y. ∃x∈X. Pf x <=F Qf y ==> ! :X .. Pf <=F ! :Y .. Qf
lemma cspF_Rep_int_choice_com_decompo_ALL_EX_eq:
[| ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> ! :X .. Pf =F ! :Y .. Qf
lemmas cspF_Rep_int_choice_com_decompo_ALL_EX:
∀y∈Y. ∃x∈X. Pf x <=F Qf y ==> ! :X .. Pf <=F ! :Y .. Qf
[| ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> ! :X .. Pf =F ! :Y .. Qf
lemmas cspF_Rep_int_choice_com_decompo_ALL_EX:
∀y∈Y. ∃x∈X. Pf x <=F Qf y ==> ! :X .. Pf <=F ! :Y .. Qf
[| ∀x∈X. ∃y∈Y. Pf x =F Qf y; ∀y∈Y. ∃x∈X. Pf x =F Qf y |] ==> ! :X .. Pf =F ! :Y .. Qf