:: SUBLEMMA semantic presentation begin theorem :: SUBLEMMA:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h1"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h2"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h1")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h2")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; theorem :: SUBLEMMA:2 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "vS1")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool (Set (Set "(" (Set (Var "vS1")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "vS1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "vS1")))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode Val_Sub of "A" "," "Al" is ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al" ")" ) "," "A"; end; notationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); let "vS" be ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Const "A")) "," (Set (Const "Al")); synonym "v" :::"."::: "vS" for "Al" :::"+*"::: "A"; end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); let "vS" be ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Const "A")) "," (Set (Const "Al")); :: original: :::"."::: redefine func "v" :::"."::: "vS" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); :: original: :::"`1"::: redefine func "S" :::"`1"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al"); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); func :::"Val_S"::: "(" "v" "," "S" ")" -> ($#m1_subset_1 :::"Val_Sub":::) "of" "A" "," "Al" equals :: SUBLEMMA:def 1 (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" "S" ($#k19_substut1 :::"`2"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) "v"); end; :: deftheorem defines :::"Val_S"::: SUBLEMMA:def 1 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "v")))))))); theorem :: SUBLEMMA:3 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S")) "is" (Set (Var "Al")) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "holds" (Bool (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); let "J" be ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Const "Al")) "," (Set (Const "A")); pred "J" "," "v" :::"|="::: "S" means :: SUBLEMMA:def 2 (Bool "J" "," "v" ($#r1_valuat_1 :::"|="::: ) (Set "S" ($#k2_sublemma :::"`1"::: ) )); end; :: deftheorem defines :::"|="::: SUBLEMMA:def 2 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) )) ")" )))))); theorem :: SUBLEMMA:4 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S")) "is" (Set (Var "Al")) ($#v2_substut1 :::"-Sub_VERUM"::: ) )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" )))))) ; theorem :: SUBLEMMA:5 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "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 (Var "Al")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "ll"))))) "holds" (Bool (Set (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")))))) ; theorem :: SUBLEMMA:6 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_substut1 :::"Sub_atomic"::: ) )) "holds" (Bool (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set "(" ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set (Var "S")) ")" ) "," (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ")" ))))) ; theorem :: SUBLEMMA:7 (Bool "for" (Set (Var "Al")) "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")) "," (Set (Var "P9")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "," (Set (Var "ll9")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "," (Set (Var "Sub9")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set "(" ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k26_substut1 :::"Sub_the_arguments_of"::: ) (Set "(" ($#k17_substut1 :::"Sub_P"::: ) "(" (Set (Var "P9")) "," (Set (Var "ll9")) "," (Set (Var "Sub9")) ")" ")" )))) "holds" (Bool (Set (Var "ll")) ($#r2_relset_1 :::"="::: ) (Set (Var "ll9")))))))) ; definitionlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "P" be ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "ll" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); :: original: :::"Sub_P"::: redefine func :::"Sub_P"::: "(" "P" "," "ll" "," "Sub" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al"); end; theorem :: SUBLEMMA:8 (Bool "for" (Set (Var "Al")) "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 "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" )))))))) ; theorem :: SUBLEMMA:9 (Bool "for" (Set (Var "Al")) "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 "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))))))))) ; theorem :: SUBLEMMA:10 (Bool "for" (Set (Var "Al")) "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 "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "ll")) "," (Set (Var "Sub")) ")" ) "is" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al"))))))) ; registrationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "ll" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); cluster (Set ($#k3_substut1 :::"CQC_Subst"::: ) "(" "ll" "," "Sub" ")" ) -> (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al") ($#v5_relat_1 :::"-valued"::: ) "k" ($#v3_card_1 :::"-element"::: ) ; end; theorem :: SUBLEMMA:11 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ))))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: SUBLEMMA:12 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: SUBLEMMA:13 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" ) ")" ")" ) ")" ) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set "(" ($#k3_substut1 :::"CQC_Subst"::: ) "(" (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" )))))))))) ; theorem :: SUBLEMMA:14 (Bool "for" (Set (Var "Al")) "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 "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" ) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll"))))))))) ; theorem :: SUBLEMMA:15 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" ))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k4_sublemma :::"Sub_P"::: ) "(" (Set (Var "P")) "," (Set (Var "ll")) "," (Set (Var "Sub")) ")" )) ")" ))))))))) ; theorem :: SUBLEMMA:16 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")) ")" ) ($#k18_substut1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" ($#k20_substut1 :::"Sub_not"::: ) (Set (Var "S")) ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) )) ")" ))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); :: original: :::"Sub_not"::: redefine func :::"Sub_not"::: "S" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al"); end; theorem :: SUBLEMMA:17 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k5_sublemma :::"Sub_not"::: ) (Set (Var "S")))) ")" )))))) ; theorem :: SUBLEMMA:18 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k5_sublemma :::"Sub_not"::: ) (Set (Var "S")) ")" ) ")" )))))) ; theorem :: SUBLEMMA:19 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k5_sublemma :::"Sub_not"::: ) (Set (Var "S")) ")" ))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k5_sublemma :::"Sub_not"::: ) (Set (Var "S")) ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k5_sublemma :::"Sub_not"::: ) (Set (Var "S")))) ")" )))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S1", "S2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); assume (Bool (Set (Set (Const "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Const "S2")) ($#k19_substut1 :::"`2"::: ) )) ; func :::"CQCSub_&"::: "(" "S1" "," "S2" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al") equals :: SUBLEMMA:def 3 (Set ($#k21_substut1 :::"Sub_&"::: ) "(" "S1" "," "S2" ")" ); end; :: deftheorem defines :::"CQCSub_&"::: SUBLEMMA:def 3 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_substut1 :::"Sub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )))); theorem :: SUBLEMMA:20 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k2_sublemma :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S1")) ($#k2_sublemma :::"`1"::: ) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "S2")) ($#k2_sublemma :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) )) ")" ))) ; theorem :: SUBLEMMA:21 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) )))) ; theorem :: SUBLEMMA:22 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S1")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ")" )) & (Bool (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SUBLEMMA:23 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S1")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S2")) ")" ))))) ; theorem :: SUBLEMMA:24 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S1")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S1"))) & (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S2")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S2"))) ")" ) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )) ")" )))))) ; theorem :: SUBLEMMA:25 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Set (Var "S1")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S2")) ($#k19_substut1 :::"`2"::: ) )) & (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S1")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S1")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S1"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S2")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S2")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S2"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" )) ")" )))))) ; theorem :: SUBLEMMA:26 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#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 "(" (Bool (Set (Set "(" ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ")" ) ($#k18_substut1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ")" ) ($#k18_substut1 :::"`1"::: ) ")" ) ")" )) & (Bool (Set (Set "(" ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ")" ) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "SQ"))) ")" )))) ; definitionlet "Al" 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 "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); attr "B" is :::"CQC-WFF-like"::: means :: SUBLEMMA:def 4 (Bool (Set "B" ($#k22_substut1 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al")); end; :: deftheorem defines :::"CQC-WFF-like"::: SUBLEMMA:def 4 : (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_sublemma :::"CQC-WFF-like"::: ) ) "iff" (Bool (Set (Set (Var "B")) ($#k22_substut1 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al")))) ")" ))); registrationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster ($#v1_sublemma :::"CQC-WFF-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); :: original: :::"["::: redefine func :::"[":::"S" "," "x":::"]"::: -> ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "B" :::"`1"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al"); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "B" be ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "Al")) ")" ) ($#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 :::"CQCSub_All"::: "(" "B" "," "SQ" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al") equals :: SUBLEMMA:def 5 (Set ($#k24_substut1 :::"Sub_All"::: ) "(" "B" "," "SQ" ")" ); end; :: deftheorem defines :::"CQCSub_All"::: SUBLEMMA:def 5 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#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 ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ))))); theorem :: SUBLEMMA:27 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#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 ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) "is" ($#v7_substut1 :::"Sub_universal"::: ) )))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); assume (Bool (Set (Const "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) ; func :::"CQCSub_the_scope_of"::: "S" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) "Al") equals :: SUBLEMMA:def 6 (Set ($#k31_substut1 :::"Sub_the_scope_of"::: ) "S"); end; :: deftheorem defines :::"CQCSub_the_scope_of"::: SUBLEMMA:def 6 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool (Set ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k31_substut1 :::"Sub_the_scope_of"::: ) (Set (Var "S")))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S1" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); assume that (Bool (Set (Const "S1")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) and (Bool (Set (Const "p")) ($#r1_hidden :::"="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set (Const "S1")) ")" ))) ; func :::"CQCQuant"::: "(" "S1" "," "p" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") equals :: SUBLEMMA:def 7 (Set ($#k36_substut1 :::"Quant"::: ) "(" "S1" "," "p" ")" ); end; :: deftheorem defines :::"CQCQuant"::: SUBLEMMA:def 7 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S1")) "is" ($#v7_substut1 :::"Sub_universal"::: ) ) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set (Var "S1")) ")" )))) "holds" (Bool (Set ($#k11_sublemma :::"CQCQuant"::: ) "(" (Set (Var "S1")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k36_substut1 :::"Quant"::: ) "(" (Set (Var "S1")) "," (Set (Var "p")) ")" ))))); theorem :: SUBLEMMA:28 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "S")) "is" ($#v7_substut1 :::"Sub_universal"::: ) )) "holds" (Bool (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k11_sublemma :::"CQCQuant"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set (Var "S")) ")" ) ")" ) ")" )))) ; theorem :: SUBLEMMA:29 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#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 ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k8_sublemma :::"`1"::: ) ))))) ; begin theorem :: SUBLEMMA:30 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "(" (Bool (Set ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set ($#k11_sublemma :::"CQCQuant"::: ) "(" (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) "," (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k10_sublemma :::"CQCSub_the_scope_of"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_sublemma :::"CQCQuant"::: ) "(" (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) "," (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")) ")" ) ")" )) ")" ))))) ; theorem :: SUBLEMMA:31 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k11_sublemma :::"CQCQuant"::: ) "(" (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) "," (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")) ")" ) ")" )))))) ; theorem :: SUBLEMMA:32 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" )))) "holds" (Bool (Set (Set (Var "v")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: SUBLEMMA:33 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")))))) ; theorem :: SUBLEMMA:34 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k1_substut1 :::"vSUB"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k15_substut1 :::"QSub"::: ) (Set (Var "Al")) ")" )))) ; theorem :: SUBLEMMA:35 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ1")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B1")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set (Var "B1")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B1")) "," (Set (Var "SQ1")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B1")) ($#k23_substut1 :::"`2"::: ) )) & (Bool (Set (Var "SQ")) ($#r1_hidden :::"="::: ) (Set (Var "SQ1"))) ")" )))))) ; theorem :: SUBLEMMA:36 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "B")) "being" ($#v1_sublemma :::"CQC-WFF-like"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k16_substut1 :::"QC-Sub-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "SQ1")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set (Var "B1")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set (Var "B1")) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set (Var "B")) "," (Set (Var "SQ")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_substut1 :::"Sub_All"::: ) "(" (Set (Var "B1")) "," (Set (Var "SQ1")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k23_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B1")) ($#k23_substut1 :::"`2"::: ) )) & (Bool (Set (Var "SQ")) ($#r1_hidden :::"="::: ) (Set (Var "SQ1"))) ")" )))))) ; theorem :: SUBLEMMA:37 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k30_substut1 :::"Sub_the_bound_of"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; theorem :: SUBLEMMA:38 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )))) & (Bool (Bool "not" (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" )))) ")" ))))) ; theorem :: SUBLEMMA:39 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ))))) "holds" (Bool "not" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )))))))) ; theorem :: SUBLEMMA:40 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "not" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )))))))) ; theorem :: SUBLEMMA:41 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set (Set (Var "S")) ($#k19_substut1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k14_substut1 :::"ExpandSub"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) "," (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ) ")" )))))) ; theorem :: SUBLEMMA:42 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" )))) ; theorem :: SUBLEMMA:43 (Bool "for" (Set (Var "Al")) "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 "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" ))))))) ; theorem :: SUBLEMMA:44 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ))))) ; theorem :: SUBLEMMA:45 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p")))) & (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ))))) ; theorem :: SUBLEMMA:46 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )))))) ; theorem :: SUBLEMMA:47 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_substut1 :::"Bound_Vars"::: ) (Set (Var "p")))))) ; notationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); synonym "x" :::"|"::: "a" for "Al" :::".-->"::: "A"; end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"|"::: redefine func "x" :::"|"::: "a" -> ($#m1_subset_1 :::"Val_Sub":::) "of" "A" "," "Al"; end; theorem :: SUBLEMMA:48 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))))))) ; theorem :: SUBLEMMA:49 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))))) ; theorem :: SUBLEMMA:50 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))) ")" ))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "S" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Const "Al"))); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "xSQ" be ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Const "S")) "," (Set (Const "x")) ($#k7_sublemma :::"]"::: ) ); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); func :::"NEx_Val"::: "(" "v" "," "S" "," "x" "," "xSQ" ")" -> ($#m1_subset_1 :::"Val_Sub":::) "of" "A" "," "Al" equals :: SUBLEMMA:def 8 (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" "x" "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" "x" "," (Set "(" "S" ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," "xSQ" ")" ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) "v"); end; :: deftheorem defines :::"NEx_Val"::: SUBLEMMA:def 8 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "v")))))))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "v", "w" be ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Const "A")) "," (Set (Const "Al")); :: original: :::"."::: redefine func "v" :::"+*"::: "w" -> ($#m1_subset_1 :::"Val_Sub":::) "of" "A" "," "Al"; end; theorem :: SUBLEMMA:51 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )))) "holds" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_qc_lang3 :::"x."::: ) (Set "(" ($#k13_substut1 :::"upVar"::: ) "(" (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ))))))) ; theorem :: SUBLEMMA:52 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ))))) "holds" (Bool (Set ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; theorem :: SUBLEMMA:53 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k3_sublemma :::"Val_S"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ")" )))))))) ; theorem :: SUBLEMMA:54 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S")))) ")" )))))))) ; theorem :: SUBLEMMA:55 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ))))))))) ; theorem :: SUBLEMMA:56 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S")))) ")" )))))))) ; begin theorem :: SUBLEMMA:57 (Bool "for" (Set (Var "Al")) "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 "Al"))) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l1"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al"))))) "holds" (Bool (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l1")))))) ; theorem :: SUBLEMMA:58 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ")" )))))) ; theorem :: SUBLEMMA:59 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "ll")) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "ll")) ")" ) ")" )))))))) ; theorem :: SUBLEMMA:60 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) ")" )))))))) ; theorem :: SUBLEMMA:61 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) ")" )))))) ; theorem :: SUBLEMMA:62 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) ")" )))))) ; theorem :: SUBLEMMA:63 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al"))))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))))))) ; theorem :: SUBLEMMA:64 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "w")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ))))))))) ; theorem :: SUBLEMMA:65 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: SUBLEMMA:66 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "w")) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ))))))))) ; theorem :: SUBLEMMA:67 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) ")" ))))))) ; theorem :: SUBLEMMA:68 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "w")) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" )))))) ; theorem :: SUBLEMMA:69 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" )))))))))) ; theorem :: SUBLEMMA:70 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k35_substut1 :::"S_Bound"::: ) (Set "(" ($#k32_substut1 :::"@"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ")" ) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S")))) ")" )))))))) ; theorem :: SUBLEMMA:71 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ))))))))) ; theorem :: SUBLEMMA:72 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S")))) ")" )))))))) ; theorem :: SUBLEMMA:73 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ($#k1_sublemma :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_sublemma :::"|"::: ) (Set (Var "a")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ))) ")" )))))))) ; theorem :: SUBLEMMA:74 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "ll"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS")) ")" ) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" ) ")" ) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll")))))))))) ; theorem :: SUBLEMMA:75 (Bool "for" (Set (Var "Al")) "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 "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) ")" ))))))))) ; theorem :: SUBLEMMA:76 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) ")" ))))))) ; theorem :: SUBLEMMA:77 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) ")" ))))))) ; theorem :: SUBLEMMA:78 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "vS1")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )))) ")" )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))))))))) ; theorem :: SUBLEMMA:79 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) (Bool "for" (Set (Var "vS1")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool (Set (Set (Var "vS1")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "vS1")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "vS1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))))))))) ; theorem :: SUBLEMMA:80 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) ")" )))))))) ; theorem :: SUBLEMMA:81 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "vS")) "," (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set (Var "vS"))) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set (Var "vS")) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" )) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) ")" ))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); func :::"RSub1"::: "p" -> ($#m1_hidden :::"set"::: ) means :: SUBLEMMA:def 9 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) "p"))) ")" )) ")" )); end; :: deftheorem defines :::"RSub1"::: SUBLEMMA:def 9 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_sublemma :::"RSub1"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) ")" )) ")" )) ")" )))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "Sub" be ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Const "Al")); func :::"RSub2"::: "(" "p" "," "Sub" ")" -> ($#m1_hidden :::"set"::: ) means :: SUBLEMMA:def 10 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) "p")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) "Sub" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) ")" )); end; :: deftheorem defines :::"RSub2"::: SUBLEMMA:def 10 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_sublemma :::"RSub2"::: ) "(" (Set (Var "p")) "," (Set (Var "Sub")) ")" )) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) ")" )) ")" ))))); theorem :: SUBLEMMA:82 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k15_sublemma :::"RSub1"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k16_sublemma :::"RSub2"::: ) "(" (Set (Var "p")) "," (Set (Var "Sub")) ")" ")" ) ")" )))))) ; theorem :: SUBLEMMA:83 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k15_sublemma :::"RSub1"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ) ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k16_sublemma :::"RSub2"::: ) "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "Sub")) ")" ")" ) ")" ) ")" ))))))) ; theorem :: SUBLEMMA:84 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "Sub")) "being" ($#m1_subset_1 :::"CQC_Substitution":::) "of" (Set (Var "Al")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "Sub")) ")" ")" ) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k15_sublemma :::"RSub1"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "Sub")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k16_sublemma :::"RSub2"::: ) "(" (Set (Var "p")) "," (Set (Var "Sub")) ")" ")" ) ")" ) ")" ))))))) ; theorem :: SUBLEMMA:85 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool (Set ($#k2_substut1 :::"@"::: ) (Set "(" (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ($#k19_substut1 :::"`2"::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set "(" ($#k7_substut1 :::"RestrictSub"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ) ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "xSQ")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k15_sublemma :::"RSub1"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ) ($#k14_sublemma :::"+*"::: ) (Set "(" (Set "(" ($#k2_substut1 :::"@"::: ) (Set (Var "xSQ")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k16_sublemma :::"RSub2"::: ) "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" ) "," (Set (Var "xSQ")) ")" ")" ) ")" ))))))) ; theorem :: SUBLEMMA:86 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "ex" (Set (Var "vS1")) "," (Set (Var "vS2")) "being" ($#m1_subset_1 :::"Val_Sub":::) "of" (Set (Var "A")) "," (Set (Var "Al")) "st" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS1"))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" ")" )))) ")" ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2"))))) "holds" (Bool (Set (Set (Var "vS2")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "vS2")))) & (Bool (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS1")) ")" ) ($#k14_sublemma :::"+*"::: ) (Set (Var "vS2")) ")" ))) ")" )))))))) ; theorem :: SUBLEMMA:87 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k13_sublemma :::"NEx_Val"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) "," (Set (Var "x")) "," (Set (Var "xSQ")) ")" ")" )) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "S")) ($#k2_sublemma :::"`1"::: ) ")" ) ")" )) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" )) ")" )))))))) ; theorem :: SUBLEMMA:88 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "xSQ")) "being" ($#m1_substut1 :::"second_Q_comp"::: ) "of" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "st" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set "(" ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" ")" ) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "xSQ")) ")" )) ")" )))))))) ; scheme :: SUBLEMMA:sch 1 SubCQCInd1{ 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 ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) (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 ($#k4_sublemma :::"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 ($#k5_sublemma :::"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 ($#k6_sublemma :::"CQCSub_&"::: ) "(" (Set (Var "S")) "," (Set (Var "S9")) ")" )]) ")" & "(" (Bool (Bool (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "is" ($#v3_substut1 :::"quantifiable"::: ) ) & (Bool P1[(Set (Var "S"))])) "implies" (Bool P1[(Set ($#k9_sublemma :::"CQCSub_All"::: ) "(" (Set ($#k7_sublemma :::"["::: ) (Set (Var "S")) "," (Set (Var "x")) ($#k7_sublemma :::"]"::: ) ) "," (Set (Var "SQ")) ")" )]) ")" ")" )))))))) proof end; theorem :: SUBLEMMA:89 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "S")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k38_substut1 :::"CQC-Sub-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k39_substut1 :::"CQC_Sub"::: ) (Set (Var "S")))) "iff" (Bool (Set (Var "J")) "," (Set (Set (Var "v")) ($#k1_sublemma :::"."::: ) (Set "(" ($#k3_sublemma :::"Val_S"::: ) "(" (Set (Var "v")) "," (Set (Var "S")) ")" ")" )) ($#r1_sublemma :::"|="::: ) (Set (Var "S"))) ")" )))))) ;