:: SUBSTUT1 semantic presentation begin definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"vSUB"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: SUBSTUT1:def 1 (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ); end; :: deftheorem defines :::"vSUB"::: SUBSTUT1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k1_substut1 :::"vSUB"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode CQC_Substitution of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A"); end; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k1_substut1 :::"vSUB"::: ) "A") -> ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"@"::: "Sub" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) equals :: SUBSTUT1:def 2 "Sub"; end; :: deftheorem defines :::"@"::: SUBSTUT1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_substut1 :::"@"::: ) (Set (Var "Sub"))) ($#r1_hidden :::"="::: ) (Set (Var "Sub"))))); theorem :: SUBSTUT1:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Sub"))))) "holds" (Bool (Set (Set (Var "Sub")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))))))) ; 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 "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"CQC_Subst"::: "(" "l" "," "Sub" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") means :: SUBSTUT1:def 3 (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"::: ) "Sub"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "Sub" ($#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"::: ) "Sub")))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"CQC_Subst"::: SUBSTUT1:def 3 : (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 "Sub")) "being" ($#m1_subset_1 :::"CQC_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 ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "l")) "," (Set (Var "Sub")) ")" )) "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 "Sub"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Sub")) ($#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 "Sub")))))) "implies" (Bool (Set (Set (Var "b4")) ($#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"::: ) ; let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A"))); func :::"@"::: "l" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") equals :: SUBSTUT1:def 4 "l"; end; :: deftheorem defines :::"@"::: SUBSTUT1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k4_substut1 :::"@"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Var "l"))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A"))); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"CQC_Subst"::: "(" "l" "," "Sub" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") equals :: SUBSTUT1:def 5 (Set ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set "(" ($#k4_substut1 :::"@"::: ) "l" ")" ) "," "Sub" ")" ); end; :: deftheorem defines :::"CQC_Subst"::: SUBSTUT1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "l")) "," (Set (Var "Sub")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set "(" ($#k4_substut1 :::"@"::: ) (Set (Var "l")) ")" ) "," (Set (Var "Sub")) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"|"::: redefine func "Sub" :::"|"::: "X" -> ($#m1_subset_1 :::"CQC_Substitution":::) "of" "A"; end; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"RestrictSub"::: "(" "x" "," "p" "," "Sub" ")" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" "A" equals :: SUBSTUT1:def 6 (Set "Sub" ($#k6_substut1 :::"|"::: ) "{" (Set (Var "y")) where y "is" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" : (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) "p")) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "Sub")) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x") & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set "Sub" ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) "}" ); end; :: deftheorem defines :::"RestrictSub"::: SUBSTUT1:def 6 : (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 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "Sub")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Sub")) ($#k6_substut1 :::"|"::: ) "{" (Set (Var "y")) where y "is" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) : (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "Sub")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "Sub")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) "}" )))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "l1" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); func :::"Bound_Vars"::: "l1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) equals :: SUBSTUT1:def 7 "{" (Set "(" "l1" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "l1")) & (Bool (Set "l1" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A")) ")" ) "}" ; end; :: deftheorem defines :::"Bound_Vars"::: SUBSTUT1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k8_substut1 :::"Bound_Vars"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l1")))) & (Bool (Set (Set (Var "l1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); func :::"Bound_Vars"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) means :: SUBSTUT1:def 8 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "p")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) "A"))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "d2")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ")" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Bound_Vars"::: SUBSTUT1:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A"))))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "d2")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ")" ")" )) ")" ) ")" )) ")" )))); theorem :: SUBSTUT1:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SUBSTUT1:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))))) ; theorem :: SUBSTUT1:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ))))) ; theorem :: SUBSTUT1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: SUBSTUT1:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); cluster (Set ($#k9_substut1 :::"Bound_Vars"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); func :::"Dom_Bound_Vars"::: "p" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) equals :: SUBSTUT1:def 9 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" : (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) "p")) "}" ; end; :: deftheorem defines :::"Dom_Bound_Vars"::: SUBSTUT1:def 9 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k10_substut1 :::"Dom_Bound_Vars"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) : (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p")))) "}" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "finSub" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"Sub_Var"::: "finSub" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) equals :: SUBSTUT1:def 10 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" : (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "finSub")) "}" ; end; :: deftheorem defines :::"Sub_Var"::: SUBSTUT1:def 10 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "finSub")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k11_substut1 :::"Sub_Var"::: ) (Set (Var "finSub"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) : (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "finSub")))) "}" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); let "finSub" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); func :::"NSub"::: "(" "p" "," "finSub" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) equals :: SUBSTUT1:def 11 (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k10_substut1 :::"Dom_Bound_Vars"::: ) "p" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k11_substut1 :::"Sub_Var"::: ) "finSub" ")" ) ")" )); end; :: deftheorem defines :::"NSub"::: SUBSTUT1:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "finSub")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k12_substut1 :::"NSub"::: ) "(" (Set (Var "p")) "," (Set (Var "finSub")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k10_substut1 :::"Dom_Bound_Vars"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k11_substut1 :::"Sub_Var"::: ) (Set (Var "finSub")) ")" ) ")" )))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "finSub" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); func :::"upVar"::: "(" "finSub" "," "p" ")" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" equals :: SUBSTUT1:def 12 "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_substut1 :::"NSub"::: ) "(" "p" "," "finSub" ")" ); end; :: deftheorem defines :::"upVar"::: SUBSTUT1:def 12 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "finSub")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k13_substut1 :::"upVar"::: ) "(" (Set (Var "finSub")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k12_substut1 :::"NSub"::: ) "(" (Set (Var "p")) "," (Set (Var "finSub")) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); let "finSub" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); assume (Bool "ex" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")) "st" (Bool (Set (Const "finSub")) ($#r1_hidden :::"="::: ) (Set ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Const "x")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Const "x")) "," (Set (Const "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ))) ; func :::"ExpandSub"::: "(" "x" "," "p" "," "finSub" ")" -> ($#m1_subset_1 :::"CQC_Substitution":::) "of" "A" equals :: SUBSTUT1:def 13 (Set "finSub" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) "x" "," (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" "finSub" "," "p" ")" ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )) if (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "finSub")) otherwise (Set "finSub" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) "x" "," "x" ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"ExpandSub"::: SUBSTUT1:def 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 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "finSub")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "st" (Bool (Bool "ex" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "st" (Bool (Set (Var "finSub")) ($#r1_hidden :::"="::: ) (Set ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "finSub"))))) "implies" (Bool (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "finSub")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "finSub")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" (Set (Var "finSub")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "finSub")))))) "implies" (Bool (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "finSub")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "finSub")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ")" ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "A")); let "b" be ($#m1_hidden :::"set"::: ) ; pred "p" "," "Sub" :::"PQSub"::: "b" means :: SUBSTUT1:def 14 (Bool "(" "(" (Bool (Bool "p" "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) "p" ")" ) "," (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) "p" ")" ) "," (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) "p" ")" ) "," "p" "," "Sub" ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" "p" "is" ($#v5_qc_lang1 :::"universal"::: ) ))) "implies" (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ); end; :: deftheorem defines :::"PQSub"::: SUBSTUT1:def 14 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "Sub")) ($#r1_substut1 :::"PQSub"::: ) (Set (Var "b"))) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) "," (Set (Var "p")) "," (Set (Var "Sub")) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"QSub"::: "A" -> ($#m1_hidden :::"Function":::) means :: SUBSTUT1:def 15 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" "A"(Bool "ex" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" "A"(Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "p")) "," (Set (Var "Sub")) ($#r1_substut1 :::"PQSub"::: ) (Set (Var "b"))) ")" )))) ")" )); end; :: deftheorem defines :::"QSub"::: SUBSTUT1:def 15 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_substut1 :::"QSub"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "Sub")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "p")) "," (Set (Var "Sub")) ($#r1_substut1 :::"PQSub"::: ) (Set (Var "b"))) ")" )))) ")" )) ")" ))); begin theorem :: SUBSTUT1:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool "(" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (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 "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ")" ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set "(" (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ")" ) ")" )) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is "A" :::"-Sub-closed"::: means :: SUBSTUT1:def 16 (Bool "(" (Bool "IT" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (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")) "," "A" (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")))) ")" ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT") ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set "(" (Set "(" ($#k15_substut1 :::"QSub"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "IT"))) ")" ) ")" ); end; :: deftheorem defines :::"-Sub-closed"::: SUBSTUT1:def 16 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" (Set (Var "A")) ($#v1_substut1 :::"-Sub-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (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 "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))))) ")" ) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set "(" (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))))) ")" ) ")" ) ")" ))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) "A" ($#v1_substut1 :::"-Sub-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"QC-Sub-WFF"::: "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: SUBSTUT1:def 17 (Bool "(" (Bool it "is" "A" ($#v1_substut1 :::"-Sub-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" "A" ($#v1_substut1 :::"-Sub-closed"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"QC-Sub-WFF"::: SUBSTUT1:def 17 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" (Set (Var "A")) ($#v1_substut1 :::"-Sub-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" (Set (Var "A")) ($#v1_substut1 :::"-Sub-closed"::: ) )) "holds" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))); theorem :: SUBSTUT1:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )))))) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) "A" ($#v1_substut1 :::"-Sub-closed"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "P" be ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "A")); let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Const "A"))); assume (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Const "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "l")))) ; func :::"Sub_P"::: "(" "P" "," "l" "," "e" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") equals :: SUBSTUT1:def 18 (Set ($#k1_domain_1 :::"["::: ) (Set "(" "P" ($#k10_qc_lang1 :::"!"::: ) "l" ")" ) "," "e" ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"Sub_P"::: SUBSTUT1:def 18 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )))))); theorem :: SUBSTUT1:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) (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 "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")) ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); attr "S" is "A" :::"-Sub_VERUM"::: means :: SUBSTUT1:def 19 (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "A" ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"-Sub_VERUM"::: SUBSTUT1:def 19 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) ))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); :: original: :::"`1"::: redefine func "S" :::"`1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A"); :: original: :::"`2"::: redefine func "S" :::"`2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A"); end; theorem :: SUBSTUT1:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); func :::"Sub_not"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") equals :: SUBSTUT1:def 20 (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" "S" ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" "S" ($#k19_substut1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"Sub_not"::: SUBSTUT1:def 20 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S", "S9" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Set (Const "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Const "S9")) ($#k19_substut1 :::"`2"::: ) )) ; func :::"Sub_&"::: "(" "S" "," "S9" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") equals :: SUBSTUT1:def 21 (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" "S" ($#k18_substut1 :::"`1"::: ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" "S9" ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" "S" ($#k19_substut1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"Sub_&"::: SUBSTUT1:def 21 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S")) "," (Set (Var "S9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "S9")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "B" :::"`1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A"); :: original: :::"`2"::: redefine func "B" :::"`2"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); attr "B" is :::"quantifiable"::: means :: SUBSTUT1:def 22 (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool (Set (Set "(" "B" ($#k22_substut1 :::"`1"::: ) ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" "B" ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" "B" ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )))); end; :: deftheorem defines :::"quantifiable"::: SUBSTUT1:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Set (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); assume (Bool (Set (Const "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ; mode :::"second_Q_comp"::: "of" "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") means :: SUBSTUT1:def 23 (Bool (Set (Set "(" "B" ($#k22_substut1 :::"`1"::: ) ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" "B" ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" "B" ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," it ($#k1_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"second_Q_comp"::: SUBSTUT1:def 23 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B"))) "iff" (Bool (Set (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "b3")) ($#k1_domain_1 :::"]"::: ) ))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); let "SQ" be ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Const "B")); assume (Bool (Set (Const "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ; func :::"Sub_All"::: "(" "B" "," "SQ" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") equals :: SUBSTUT1:def 24 (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" "B" ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" "B" ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," "SQ" ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"Sub_All"::: SUBSTUT1:def 24 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "SQ")) ($#k1_domain_1 :::"]"::: ) ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); :: original: :::"["::: redefine func :::"[":::"S" "," "x":::"]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; scheme :: SUBSTUT1:sch 1 SubQCInd{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ))] } : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "S"))])) provided (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 F1 "(" ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )]))))) and (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "holds" (Bool P1[(Set (Var "S"))])) and (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "S"))])) "holds" (Bool P1[(Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")))])) and (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) )) & (Bool P1[(Set (Var "S"))]) & (Bool P1[(Set (Var "S9"))])) "holds" (Bool P1[(Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S")) "," (Set (Var "S9")) ")" )])) and (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "st" (Bool (Bool (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool P1[(Set (Var "S"))])) "holds" (Bool P1[(Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "," (Set (Var "SQ")) ")" )])))) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); attr "S" is :::"Sub_atomic"::: means :: SUBSTUT1:def 25 (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )))))); end; :: deftheorem defines :::"Sub_atomic"::: SUBSTUT1:def 25 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )))))) ")" ))); theorem :: SUBSTUT1:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "holds" (Bool (Set (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ) "is" ($#v2_qc_lang1 :::"atomic"::: ) ))) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "P" be ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "ll" be ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Const "A"))); cluster (Set ($#k17_substut1 :::"Sub_P"::: ) "(" "P" "," "ll" "," "e" ")" ) -> ($#v4_substut1 :::"Sub_atomic"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); attr "S" is :::"Sub_negative"::: means :: SUBSTUT1:def 26 (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") "st" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S9"))))); attr "S" is :::"Sub_conjunctive"::: means :: SUBSTUT1:def 27 (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )) & (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) )) ")" )); end; :: deftheorem defines :::"Sub_negative"::: SUBSTUT1:def 26 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) "iff" (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S9"))))) ")" ))); :: deftheorem defines :::"Sub_conjunctive"::: SUBSTUT1:def 27 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )) & (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) )) ")" )) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); attr "S" is :::"Sub_universal"::: means :: SUBSTUT1:def 28 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))); end; :: deftheorem defines :::"Sub_universal"::: SUBSTUT1:def 28 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))) ")" ))); theorem :: SUBSTUT1:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) "or" (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) "or" (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) "or" (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) "or" (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) ; func :::"Sub_the_arguments_of"::: "S" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") means :: SUBSTUT1:def 29 (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) "A") "st" (Bool "(" (Bool it ($#r2_relset_1 :::"="::: ) (Set (Var "ll"))) & (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )) ")" ))))); end; :: deftheorem defines :::"Sub_the_arguments_of"::: SUBSTUT1:def 29 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r2_relset_1 :::"="::: ) (Set (Var "ll"))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )) ")" ))))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) ; func :::"Sub_the_argument_of"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") means :: SUBSTUT1:def 30 (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k20_substut1 :::"Sub_not"::: ) it)); end; :: deftheorem defines :::"Sub_the_argument_of"::: SUBSTUT1:def 30 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "b3")))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) ; func :::"Sub_the_left_argument_of"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") means :: SUBSTUT1:def 31 (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" it "," (Set (Var "S9")) ")" )) & (Bool (Set it ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) )) ")" )); end; :: deftheorem defines :::"Sub_the_left_argument_of"::: SUBSTUT1:def 31 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "b3")) "," (Set (Var "S9")) ")" )) & (Bool (Set (Set (Var "b3")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) )) ")" )) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) ; func :::"Sub_the_right_argument_of"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") means :: SUBSTUT1:def 32 (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S9")) "," it ")" )) & (Bool (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set it ($#k19_substut1 :::"`2"::: ) )) ")" )); end; :: deftheorem defines :::"Sub_the_right_argument_of"::: SUBSTUT1:def 32 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S9")) "," (Set (Var "b3")) ")" )) & (Bool (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k19_substut1 :::"`2"::: ) )) ")" )) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ; func :::"Sub_the_bound_of"::: "S" -> ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" means :: SUBSTUT1:def 33 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool "S" ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) it) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))); end; :: deftheorem defines :::"Sub_the_bound_of"::: SUBSTUT1:def 33 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k30_substut1 :::"Sub_the_bound_of"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "A2")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ; func :::"Sub_the_scope_of"::: "A2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") means :: SUBSTUT1:def 34 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool "A2" ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) it) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))); end; :: deftheorem defines :::"Sub_the_scope_of"::: SUBSTUT1:def 34 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "A2")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "A2")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" )) & (Bool (Set (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) & (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) ")" ))) ")" )))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); cluster (Set ($#k20_substut1 :::"Sub_not"::: ) "S") -> ($#v5_substut1 :::"Sub_negative"::: ) ; end; theorem :: SUBSTUT1:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ))) ; theorem :: SUBSTUT1:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) "is" ($#v7_substut1 :::"Sub_universal"::: ) )))) ; theorem :: SUBSTUT1:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S9"))))) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "S9"))))) ; theorem :: SUBSTUT1:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set "(" ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S"))))) ; theorem :: SUBSTUT1:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S19")) "," (Set (Var "S29")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) )) & (Bool (Set (Set (Var "S19")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S29")) ($#k19_substut1 :::"`2"::: ) )) & (Bool (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S19")) "," (Set (Var "S29")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S19"))) & (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Var "S29"))) ")" ))) ; theorem :: SUBSTUT1:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set "(" ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S1"))))) ; theorem :: SUBSTUT1:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set "(" ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S2"))))) ; theorem :: SUBSTUT1:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ1")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B1")) (Bool "for" (Set (Var "SQ2")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B2")) "st" (Bool (Bool (Set (Var "B1")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set (Var "B2")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B1")) "," (Set (Var "SQ1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B2")) "," (Set (Var "SQ2")) ")" ))) "holds" (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2"))))))) ; theorem :: SUBSTUT1:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set "(" ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ))))) ; scheme :: SUBSTUT1:sch 2 SubQCInd2{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ))] } : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "S"))])) provided (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool P1[(Set (Var "S"))]) ")" & "(" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool P1[(Set (Var "S"))]) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool P1[(Set ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")))])) "implies" (Bool P1[(Set (Var "S"))]) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) & (Bool P1[(Set ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")))]) & (Bool P1[(Set ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")))])) "implies" (Bool P1[(Set (Var "S"))]) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) & (Bool P1[(Set ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")))])) "implies" (Bool P1[(Set (Var "S"))]) ")" ")" )) proof end; theorem :: SUBSTUT1:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ))))) ; theorem :: SUBSTUT1:23 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ))) ")" ))) ; theorem :: SUBSTUT1:24 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ))))) ; theorem :: SUBSTUT1:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")))) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) ")" ")" ))) ; theorem :: SUBSTUT1:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 2)) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 3)) ")" ))) ; theorem :: SUBSTUT1:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) & (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) & (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) & (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) & (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) & (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) ) & (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ")" )) ")" ))) ; scheme :: SUBSTUT1:sch 3 SubFuncEx{ 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_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "S")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set F1 "(" ")" ) "," (Set (Var "S")) "," (Set (Var "d1")) ")" )) ")" ")" )))) proof end; scheme :: SUBSTUT1:sch 4 SubQCFuncUniq{ 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 "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#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_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set F1 "(" ")" ) "," (Set (Var "S")) "," (Set (Var "d1")) ")" )) ")" ")" ))) and (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "S")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set F1 "(" ")" ) "," (Set (Var "S")) "," (Set (Var "d1")) ")" )) ")" ")" ))) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); func :::"@"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: SUBSTUT1:def 35 "S"; end; :: deftheorem defines :::"@"::: SUBSTUT1:def 35 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k32_substut1 :::"@"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "Z" :::"`1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A"); :: original: :::"`2"::: redefine func "Z" :::"`2"::: -> ($#m1_subset_1 :::"CQC_Substitution":::) "of" "A"; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Const "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"S_Bound"::: "Z" -> ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" equals :: SUBSTUT1:def 36 (Set ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" ) "," (Set "(" "Z" ($#k34_substut1 :::"`2"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) ")" ")" )) if (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" ) "," (Set "(" "Z" ($#k34_substut1 :::"`2"::: ) ")" ) ")" ")" ))) otherwise (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" "Z" ($#k33_substut1 :::"`1"::: ) ")" )); end; :: deftheorem defines :::"S_Bound"::: SUBSTUT1:def 36 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k34_substut1 :::"`2"::: ) ")" ) ")" ")" )))) "implies" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k34_substut1 :::"`2"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "Z")) ($#k34_substut1 :::"`2"::: ) ")" ) ")" ")" ))))) "implies" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" (Set (Var "Z")) ($#k33_substut1 :::"`1"::: ) ")" ))) ")" ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); func :::"Quant"::: "(" "S" "," "p" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") equals :: SUBSTUT1:def 37 (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) "S" ")" ) ")" ) "," "p" ")" ); end; :: deftheorem defines :::"Quant"::: SUBSTUT1:def 37 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k36_substut1 :::"Quant"::: ) "(" (Set (Var "S")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set (Var "p")) ")" ))))); begin definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "A"))); func :::"CQC_Sub"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") means :: SUBSTUT1:def 38 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) "," (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "S")) & (Bool "(" "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S9")) "is" "A" ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) "A")) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set "(" (Set (Var "S9")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set "(" ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set (Var "S9")) ")" ) "," (Set "(" (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k36_substut1 :::"Quant"::: ) "(" (Set (Var "S9")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S9")) ")" ) ")" ) ")" )) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"CQC_Sub"::: SUBSTUT1:def 38 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S9")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set "(" (Set (Var "S9")) ($#k18_substut1 :::"`1"::: ) ")" ) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set "(" ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set (Var "S9")) ")" ) "," (Set "(" (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S9")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "S9"))) ($#r1_hidden :::"="::: ) (Set ($#k36_substut1 :::"Quant"::: ) "(" (Set (Var "S9")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S9")) ")" ) ")" ) ")" )) ")" ")" ) ")" ) ")" )) ")" )))); theorem :: SUBSTUT1:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v5_substut1 :::"Sub_negative"::: ) )) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k27_substut1 :::"Sub_the_argument_of"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: SUBSTUT1:29 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S")) ")" ))))) ; theorem :: SUBSTUT1:30 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_substut1 :::"Sub_conjunctive"::: ) )) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k28_substut1 :::"Sub_the_left_argument_of"::: ) (Set (Var "S")) ")" ) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k29_substut1 :::"Sub_the_right_argument_of"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: SUBSTUT1:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S1")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S2")) ")" ))))) ; theorem :: SUBSTUT1:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k36_substut1 :::"Quant"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")) ")" ) ")" ) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"CQC-Sub-WFF"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A" ")" ) equals :: SUBSTUT1:def 39 "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) "A") : (Bool (Set (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A")) "}" ; end; :: deftheorem defines :::"CQC-Sub-WFF"::: SUBSTUT1:def 39 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) : (Bool (Set (Set (Var "S")) ($#k18_substut1 :::"`1"::: ) ) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) "}" )); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: SUBSTUT1:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "S")) "is" (Set (Var "A")) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; theorem :: SUBSTUT1:34 (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 "h")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "h")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" )))) ; theorem :: SUBSTUT1:35 (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 "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))))))))) ; theorem :: SUBSTUT1:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")) ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; theorem :: SUBSTUT1:37 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) )) & (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S1"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) & (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S2"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))) ; theorem :: SUBSTUT1:38 (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 "S")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "st" (Bool (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))) & (Bool (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k37_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k24_substut1 :::"Sub_All"::: ) "(" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))))))) ; scheme :: SUBSTUT1:sch 5 SubCQCInd{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "S"))])) provided (Bool "for" (Set (Var "S")) "," (Set (Var "S9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "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 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_substut1 :::"vSUB"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" (Bool P1[(Set ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "e")) ")" )]) & "(" (Bool (Bool (Set (Var "S")) "is" (Set F1 "(" ")" ) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "implies" (Bool P1[(Set (Var "S"))]) ")" & "(" (Bool (Bool P1[(Set (Var "S"))])) "implies" (Bool P1[(Set ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")))]) ")" & "(" (Bool (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S9")) ($#k19_substut1 :::"`2"::: ) )) & (Bool P1[(Set (Var "S"))]) & (Bool P1[(Set (Var "S9"))])) "implies" (Bool P1[(Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S")) "," (Set (Var "S9")) ")" )]) ")" & "(" (Bool (Bool (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool P1[(Set (Var "S"))])) "implies" (Bool P1[(Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set ($#k25_substut1 :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k25_substut1 :::"]"::: ) ) "," (Set (Var "SQ")) ")" )]) ")" ")" )))))))) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "A"))); :: original: :::"CQC_Sub"::: redefine func :::"CQC_Sub"::: "S" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A"); end; theorem :: SUBSTUT1:39 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))))) ;