:: CQC_LANG semantic presentation begin theorem :: CQC_LANG:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))) ")" ) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode Substitution of "A" is ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k5_qc_lang1 :::"free_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) "A" ")" ); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); let "f" be ($#m1_subset_1 :::"Substitution":::) "of" (Set (Const "A")); func :::"Subst"::: "(" "l" "," "f" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") means :: CQC_LANG:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "l")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "l"))) "holds" (Bool "(" "(" (Bool (Bool (Set "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Subst"::: CQC_LANG:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Substitution":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_lang :::"Subst"::: ) "(" (Set (Var "l")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" ) ")" ) ")" ))))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "l" be ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "f" be ($#m1_subset_1 :::"Substitution":::) "of" (Set (Const "A")); cluster (Set ($#k1_cqc_lang :::"Subst"::: ) "(" "l" "," "f" ")" ) -> "k" ($#v3_card_1 :::"-element"::: ) ; end; theorem :: CQC_LANG:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Substitution":::) "of" (Set (Var "A")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "a" be ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Const "A")); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); :: original: :::".-->"::: redefine func "a" :::".-->"::: "x" -> ($#m1_subset_1 :::"Substitution":::) "of" "A"; end; theorem :: CQC_LANG:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Substitution":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "l")) "," (Set (Var "ll")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")))) & (Bool (Set (Var "ll")) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_lang :::"Subst"::: ) "(" (Set (Var "l")) "," (Set (Var "f")) ")" )) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "implies" (Bool (Set (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "implies" (Bool (Set (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ")" ))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"CQC-WFF"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) equals :: CQC_LANG:def 2 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-formula":::) "of" "A" : (Bool "(" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "}" ; end; :: deftheorem defines :::"CQC-WFF"::: CQC_LANG:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) : (Bool "(" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "}" )); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: CQC_LANG:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") ($#v5_relat_1 :::"-valued"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) "k" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode CQC-variable_list of "k" "," "A" is (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") ($#v5_relat_1 :::"-valued"::: ) ($#m2_finseq_1 :::"QC-variable_list":::) "of" "k" "," "A"; end; theorem :: CQC_LANG:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "l")) "is" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A"))) "iff" (Bool "(" (Bool "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )))) ; theorem :: CQC_LANG:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))))) ; theorem :: CQC_LANG:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))))) ; definitionlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "P" be ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "l" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "A")); :: original: :::"!"::: redefine func "P" :::"!"::: "l" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; theorem :: CQC_LANG:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "p")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) ")" ))) ; theorem :: CQC_LANG:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "p")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) & (Bool (Set (Var "q")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) ")" ) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; :: original: :::"VERUM"::: redefine func :::"VERUM"::: "A" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); let "r" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"'not'"::: redefine func :::"'not'"::: "r" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); let "s" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"'&'"::: redefine func "r" :::"'&'"::: "s" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; theorem :: CQC_LANG:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "r")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "s"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; theorem :: CQC_LANG:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "r")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "s"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; theorem :: CQC_LANG:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "r")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "s"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "r", "s" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"=>"::: redefine func "r" :::"=>"::: "s" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); :: original: :::"'or'"::: redefine func "r" :::"'or'"::: "s" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); :: original: :::"<=>"::: redefine func "r" :::"<=>"::: "s" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; theorem :: CQC_LANG:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "p")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "r" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"All"::: redefine func :::"All"::: "(" "x" "," "r" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; theorem :: CQC_LANG:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "r" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"Ex"::: redefine func :::"Ex"::: "(" "x" "," "r" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; scheme :: CQC_LANG:sch 1 CQCInd{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "r"))])) provided (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ))]) & (Bool P1[(Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")))]) & "(" (Bool (Bool P1[(Set (Var "r"))])) "implies" (Bool P1[(Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")))]) ")" & "(" (Bool (Bool P1[(Set (Var "r"))]) & (Bool P1[(Set (Var "s"))])) "implies" (Bool P1[(Set (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")))]) ")" & "(" (Bool (Bool P1[(Set (Var "r"))])) "implies" (Bool P1[(Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )]) ")" ")" )))))) proof end; scheme :: CQC_LANG:sch 2 CQCFuncEx{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) proof end; scheme :: CQC_LANG:sch 3 CQCFuncUniq{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "(" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "x")) "," (Set "(" (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" ) and (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "x")) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" ) proof end; scheme :: CQC_LANG:sch 4 CQCDefcorrectness{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) & (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" ))) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) ")" ) ")" ) proof end; scheme :: CQC_LANG:sch 5 CQCDefVERUM{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" ))) proof end; scheme :: CQC_LANG:sch 6 CQCDefatomic{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F7() -> ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set F6 "(" ")" ) "," (Set F1 "(" ")" ), F8() -> ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set F6 "(" ")" ) "," (Set F1 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F10( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F11( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F4 "(" (Set "(" (Set F7 "(" ")" ) ($#k4_cqc_lang :::"!"::: ) (Set F8 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set F6 "(" ")" ) "," (Set F7 "(" ")" ) "," (Set F8 "(" ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F10 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F11 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" ))) proof end; scheme :: CQC_LANG:sch 7 CQCDefnegative{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set F7 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set F3 "(" (Set F7 "(" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" ))) proof end; scheme :: CQC_LANG:sch 8 QCDefconjunctive{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )), F9() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )), F10( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" (Set "(" (Set F8 "(" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set F9 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set F3 "(" (Set F8 "(" ")" ) ")" ) "," (Set F3 "(" (Set F9 "(" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F10 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" ))) proof end; scheme :: CQC_LANG:sch 9 QCDefuniversal{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9() -> ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ), F10() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) } : (Bool (Set F3 "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set F9 "(" ")" ) "," (Set F10 "(" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set F9 "(" ")" ) "," (Set F3 "(" (Set F10 "(" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" ))) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); func "p" :::"."::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") means :: CQC_LANG:def 3 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "p")) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) "A")) & "(" (Bool (Bool (Set (Var "q")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set (Var "q")) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set "(" "A" ($#k3_qc_lang3 :::"a."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_cqc_lang :::".-->"::: ) "x" ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "q")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "q")) ")" ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "q")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "q")) ")" ) "," "x" "," (Set (Var "q")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "q")) ")" ) ")" ) ")" ")" ) ")" )) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"."::: CQC_LANG:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")))) & "(" (Bool (Bool (Set (Var "q")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set (Var "q")) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k3_qc_lang3 :::"a."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "q")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "q")) ")" ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "q")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "q")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) "," (Set (Var "q")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "q")) ")" ) ")" ) ")" ")" ) ")" )) ")" ")" ) ")" ) ")" )) ")" ))))); theorem :: CQC_LANG:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")))))) ; theorem :: CQC_LANG:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set (Var "p")) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k3_qc_lang3 :::"a."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")) ")" ) ")" ")" )))))) ; theorem :: CQC_LANG:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "A")) ($#k3_qc_lang3 :::"a."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")) ")" ) ")" ")" )))))))) ; theorem :: CQC_LANG:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_LANG:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_LANG:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_LANG:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_LANG:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: CQC_LANG:23 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: CQC_LANG:24 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))))) ; theorem :: CQC_LANG:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")) ")" ) ")" ))))) ; theorem :: CQC_LANG:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: CQC_LANG:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "r")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: CQC_LANG:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p"))))))) ; begin theorem :: CQC_LANG:29 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "k"))))) ; theorem :: CQC_LANG:30 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "k")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "k")))) ; theorem :: CQC_LANG:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "a")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c"))))) ; theorem :: CQC_LANG:32 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))))) ; theorem :: CQC_LANG:33 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))) ;