:: CQC_SIM1 semantic presentation begin definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "b" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); func :::"x."::: "b" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" means :: CQC_SIM1:def 1 (Bool (Set ($#k2_qc_lang3 :::"x."::: ) it) ($#r1_hidden :::"="::: ) "b"); end; :: deftheorem defines :::"x."::: CQC_SIM1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_sim1 :::"x."::: ) (Set (Var "b")))) "iff" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))); theorem :: CQC_SIM1:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: CQC_SIM1:2 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "L")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "K"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "K")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: CQC_SIM1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )))))) ; theorem :: CQC_SIM1:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "g")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: CQC_SIM1:5 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll"))))))))) ; theorem :: CQC_SIM1:6 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))))))) ; theorem :: CQC_SIM1:7 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r"))))))) ; theorem :: CQC_SIM1:8 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))(Bool "ex" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" )))))) ; theorem :: CQC_SIM1:9 (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) ")" ) "}" )) ; scheme :: CQC_SIM1:sch 1 QCFuncExN{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set (Var "p")) ")" )) ")" ")" ) ")" ) ")" )) proof end; scheme :: CQC_SIM1:sch 2 CQCF2FuncEx{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "l")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) "," (Set (Var "r")) "," (Set (Var "s")) ")" )) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) ")" )) ")" ) ")" )) proof end; scheme :: CQC_SIM1:sch 3 CQCF2FUniq{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ")" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ), F10( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Function":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) } : (Bool (Set F4 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F5 "(" ")" )) provided (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) and (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 "(" ")" ) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "ll")) ")" ))))) and (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) "," (Set (Var "r")) "," (Set (Var "s")) ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F10 "(" (Set (Var "x")) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) ")" ))) and (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) and (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 "(" ")" ) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "k")) "," (Set (Var "P")) "," (Set (Var "ll")) ")" ))))) and (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" )) "holds" (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) "," (Set (Var "r")) "," (Set (Var "s")) ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F10 "(" (Set (Var "x")) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" )) ")" ))) proof end; theorem :: CQC_SIM1:10 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set (Var "p")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))))) ; theorem :: CQC_SIM1:11 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) & (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) ")" ))) ; theorem :: CQC_SIM1:12 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "p")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))))) ; theorem :: CQC_SIM1:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); func :::"NEGATIVE"::: "f" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "D" "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ) means :: CQC_SIM1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))))); end; :: deftheorem defines :::"NEGATIVE"::: CQC_SIM1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "D")) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_cqc_sim1 :::"NEGATIVE"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))))) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"CON"::: "(" "f" "," "g" "," "n" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ) means :: CQC_SIM1:def 3 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set "g" ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) "n" ")" ) "," (Set (Var "h")) ")" ))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))))))); end; :: deftheorem defines :::"CON"::: CQC_SIM1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_cqc_sim1 :::"CON"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "h")) ")" ))) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))))))) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); func :::"UNIVERSAL"::: "(" "x" "," "f" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ) means :: CQC_SIM1:def 4 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) "," (Set (Var "p")) ")" ))))); end; :: deftheorem defines :::"UNIVERSAL"::: CQC_SIM1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_cqc_sim1 :::"UNIVERSAL"::: ) "(" (Set (Var "x")) "," (Set (Var "f")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) "," (Set (Var "p")) ")" ))))) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "l" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ); :: original: :::"*"::: redefine func "f" :::"*"::: "l" -> ($#m2_finseq_1 :::"CQC-variable_list":::) "of" "k" "," "A"; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "P" be ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "k")) "," (Set (Const "A")); let "l" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "A")); func :::"ATOMIC"::: "(" "P" "," "l" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ) means :: CQC_SIM1:def 5 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set "P" ($#k4_cqc_lang :::"!"::: ) (Set "(" (Set (Var "h")) ($#k5_cqc_sim1 :::"*"::: ) "l" ")" ))))); end; :: deftheorem defines :::"ATOMIC"::: CQC_SIM1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "b5")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_sim1 :::"ATOMIC"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set "(" (Set (Var "h")) ($#k5_cqc_sim1 :::"*"::: ) (Set (Var "l")) ")" ))))) ")" )))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); func :::"QuantNbr"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: CQC_SIM1:def 6 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) "p")) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," "A" (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A" "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))))) ")" ) ")" )); end; :: deftheorem defines :::"QuantNbr"::: CQC_SIM1:def 6 : (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))))) ")" ) ")" )) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ) ")" ")" ); let "x" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"SepFunc"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) ")" ")" ) means :: CQC_SIM1:def 7 (Bool "(" (Bool (Set it ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "A" ")" )) ($#r8_binop_1 :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "A" ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," "A" (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A" "holds" (Bool (Set it ($#k8_cqc_sim1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k6_cqc_sim1 :::"ATOMIC"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") "holds" (Bool "(" (Bool (Set it ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k2_cqc_sim1 :::"NEGATIVE"::: ) (Set "(" it ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ))) & (Bool (Set it ($#k8_cqc_sim1 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k3_cqc_sim1 :::"CON"::: ) "(" (Set "(" it ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" it ($#k8_cqc_sim1 :::"."::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set it ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k4_cqc_sim1 :::"UNIVERSAL"::: ) "(" (Set (Var "x")) "," (Set "(" it ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"SepFunc"::: CQC_SIM1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_cqc_sim1 :::"SepFunc"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r8_binop_1 :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k6_cqc_sim1 :::"ATOMIC"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k2_cqc_sim1 :::"NEGATIVE"::: ) (Set "(" (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k3_cqc_sim1 :::"CON"::: ) "(" (Set "(" (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "r")) ")" ) ")" )) & (Bool (Set (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k4_cqc_sim1 :::"UNIVERSAL"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "b2")) ($#k8_cqc_sim1 :::"."::: ) (Set (Var "r")) ")" ) ")" )) ")" )) ")" ) ")" ) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); let "t" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ); func :::"SepFunc"::: "(" "p" "," "t" "," "f" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") equals :: CQC_SIM1:def 8 (Set (Set "(" (Set "(" ($#k9_cqc_sim1 :::"SepFunc"::: ) "A" ")" ) ($#k8_cqc_sim1 :::"."::: ) "p" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) "t" "," "f" ($#k1_domain_1 :::"]"::: ) )); end; :: deftheorem defines :::"SepFunc"::: CQC_SIM1:def 8 : (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool (Set ($#k10_cqc_sim1 :::"SepFunc"::: ) "(" (Set (Var "p")) "," (Set (Var "t")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_cqc_sim1 :::"SepFunc"::: ) (Set (Var "A")) ")" ) ($#k8_cqc_sim1 :::"."::: ) (Set (Var "p")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))))))); theorem :: CQC_SIM1:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: CQC_SIM1:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: CQC_SIM1:16 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p")))))) ; theorem :: CQC_SIM1:17 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q")) ")" ))))) ; theorem :: CQC_SIM1:18 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: CQC_SIM1:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; scheme :: CQC_SIM1:sch 4 MaxFinDomElem{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" )) provided (Bool "(" (Bool (Set F2 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set F2 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) ")" ) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "or" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]) ")" )) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "z"))])) proof end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "X" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "X" ")" ); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); func :::"NBI"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) equals :: CQC_SIM1:def 9 "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" : (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" "st" (Bool (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u")))) "holds" (Bool "not" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) "p")))) "}" ; end; :: deftheorem defines :::"NBI"::: CQC_SIM1:def 9 : (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k12_cqc_sim1 :::"NBI"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) : (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u")))) "holds" (Bool "not" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "}" ))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); cluster (Set ($#k12_cqc_sim1 :::"NBI"::: ) "p") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); func :::"index"::: "p" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" equals :: CQC_SIM1:def 10 (Set ($#k25_qc_lang1 :::"min"::: ) (Set "(" ($#k12_cqc_sim1 :::"NBI"::: ) "p" ")" )); end; :: deftheorem defines :::"index"::: CQC_SIM1:def 10 : (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k25_qc_lang1 :::"min"::: ) (Set "(" ($#k12_cqc_sim1 :::"NBI"::: ) (Set (Var "p")) ")" ))))); theorem :: CQC_SIM1:20 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool "(" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k26_qc_lang1 :::"0"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: CQC_SIM1:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "t")) ($#r2_qc_lang1 :::"<"::: ) (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p"))))))) ; theorem :: CQC_SIM1:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k26_qc_lang1 :::"0"::: ) (Set (Var "A"))))) ; theorem :: CQC_SIM1:23 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p")))))) ; theorem :: CQC_SIM1:24 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool "(" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p"))) ($#r1_qc_lang1 :::"<="::: ) (Set ($#k13_cqc_sim1 :::"index"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ))) & (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "q"))) ($#r1_qc_lang1 :::"<="::: ) (Set ($#k13_cqc_sim1 :::"index"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ))) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); func :::"SepVar"::: "p" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") equals :: CQC_SIM1:def 11 (Set ($#k10_cqc_sim1 :::"SepFunc"::: ) "(" "p" "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) "p" ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SepVar"::: CQC_SIM1:def 11 : (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cqc_sim1 :::"SepFunc"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ")" )))); theorem :: CQC_SIM1:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A"))))) ; scheme :: CQC_SIM1:sch 5 CQCInd{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "r"))])) provided (Bool P1[(Set ($#k5_cqc_lang :::"VERUM"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")))])))) and (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "r"))])) "holds" (Bool P1[(Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "r")))])) and (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "r"))]) & (Bool P1[(Set (Var "s"))])) "holds" (Bool P1[(Set (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")))])) and (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "r"))])) "holds" (Bool P1[(Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )]))) proof end; theorem :: CQC_SIM1:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))))))) ; theorem :: CQC_SIM1:27 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: CQC_SIM1:28 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p")) ")" ))))) ; theorem :: CQC_SIM1:29 (Bool "for" (Set (Var "A")) "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 "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "q")) ")" ))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Const "A")) ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ); pred "X" :::"is_Sep-closed_on"::: "p" means :: CQC_SIM1:def 12 (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) "p" "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) "p" ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")))) ")" ) & (Bool "(" "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "r")) "," (Set "(" (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q")) ")" ) ")" ) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X") ")" )))) ")" ) & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "q")) "," (Set "(" (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ")" ) "," (Set "(" (Set (Var "K")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X"))))) ")" ) ")" ); end; :: deftheorem defines :::"is_Sep-closed_on"::: CQC_SIM1:def 12 : (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_cqc_sim1 :::"is_Sep-closed_on"::: ) (Set (Var "p"))) "iff" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))))) ")" ) & (Bool "(" "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "r")) "," (Set "(" (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q")) ")" ) ")" ) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "q")) "," (Set "(" (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ")" ) "," (Set "(" (Set (Var "K")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))))) ")" ) ")" ) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); func :::"SepQuadruples"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) means :: CQC_SIM1:def 13 (Bool "(" (Bool it ($#r1_cqc_sim1 :::"is_Sep-closed_on"::: ) "p") & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "D")) ($#r1_cqc_sim1 :::"is_Sep-closed_on"::: ) "p")) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"SepQuadruples"::: CQC_SIM1:def 13 : (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_cqc_sim1 :::"is_Sep-closed_on"::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "D")) ($#r1_cqc_sim1 :::"is_Sep-closed_on"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )))); theorem :: CQC_SIM1:30 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))))) ; theorem :: CQC_SIM1:31 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))))))) ; theorem :: CQC_SIM1:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "r")) "," (Set "(" (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q")) ")" ) ")" ) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) ")" )))))) ; theorem :: CQC_SIM1:33 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "q")) "," (Set "(" (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ")" ) "," (Set "(" (Set (Var "K")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))))))))) ; theorem :: CQC_SIM1:34 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" "not" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) )) "or" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) "or" (Bool "ex" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "or" (Bool "ex" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")))(Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k30_qc_lang1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "r")) ")" ))) & (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "u")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) ")" ))) "or" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))(Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "u")) ($#k28_qc_lang1 :::"++"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "u")) "," (Set (Var "K")) "," (Set (Var "h")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "u")) "," (Set "(" (Set (Var "K")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "h")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) ")" ) ")" )))) ")" )))))) ; scheme :: CQC_SIM1:sch 6 Sepregression{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set F2 "(" ")" )))) "holds" (Bool P1[(Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))]))))) provided (Bool P1[(Set F2 "(" ")" ) "," (Set ($#k13_cqc_sim1 :::"index"::: ) (Set F2 "(" ")" )) "," (Set ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" )) "," (Set ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ))]) and (Bool "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set F2 "(" ")" ))) & (Bool P1[(Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))])) "holds" (Bool P1[(Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))]))))) and (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set F2 "(" ")" ))) & (Bool P1[(Set (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r"))) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))])) "holds" (Bool "(" (Bool P1[(Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "r")) "," (Set (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set "(" ($#k7_cqc_sim1 :::"QuantNbr"::: ) (Set (Var "q")) ")" )) "," (Set (Var "K")) "," (Set (Var "f"))]) ")" ))))) and (Bool "for" (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set F1 "(" ")" ) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set F2 "(" ")" ))) & (Bool P1[(Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f"))])) "holds" (Bool P1[(Set (Var "q")) "," (Set (Set (Var "t")) ($#k28_qc_lang1 :::"++"::: ) ) "," (Set (Set (Var "K")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) "," (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t")) ")" ) ")" ))])))))) proof end; theorem :: CQC_SIM1:35 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "p")))))))) ; theorem :: CQC_SIM1:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k5_domain_1 :::"["::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k26_qc_lang1 :::"0"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: CQC_SIM1:37 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k5_domain_1 :::"["::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" ) "," (Set "(" ($#k13_cqc_sim1 :::"index"::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "l")) ")" ) ")" ) "," (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k11_cqc_sim1 :::"id"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_domain_1 :::"]"::: ) ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: CQC_SIM1:38 (Bool "for" (Set (Var "A")) "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 "A"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "K"))))))))) ; theorem :: CQC_SIM1:39 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "K"))))) "holds" (Bool (Set (Var "u")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t")))))))) ; theorem :: CQC_SIM1:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool "not" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "K")))))))))) ; theorem :: CQC_SIM1:41 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Var "u")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t")))))))) ; theorem :: CQC_SIM1:42 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" )))) "holds" (Bool (Set (Var "u")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t")))))))) ; theorem :: CQC_SIM1:43 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) "," (Set (Var "K")) "," (Set (Var "f")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k15_cqc_sim1 :::"SepQuadruples"::: ) (Set (Var "p"))))) "holds" (Bool "not" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" ))))))))) ; theorem :: CQC_SIM1:44 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p")) ")" ))))) ; theorem :: CQC_SIM1:45 (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool (Set ($#k13_cqc_sim1 :::"index"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k13_cqc_sim1 :::"index"::: ) (Set "(" ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p")) ")" ))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); pred "p" "," "q" :::"are_similar"::: means :: CQC_SIM1:def 14 (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k14_cqc_sim1 :::"SepVar"::: ) "q")); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))))) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "st" (Bool (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))))) ; end; :: deftheorem defines :::"are_similar"::: CQC_SIM1:def 14 : (Bool "for" (Set (Var "A")) "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 "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_cqc_sim1 :::"are_similar"::: ) ) "iff" (Bool (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_cqc_sim1 :::"SepVar"::: ) (Set (Var "q")))) ")" ))); theorem :: CQC_SIM1:46 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_cqc_sim1 :::"are_similar"::: ) ) & (Bool (Set (Var "q")) "," (Set (Var "r")) ($#r2_cqc_sim1 :::"are_similar"::: ) )) "holds" (Bool (Set (Var "p")) "," (Set (Var "r")) ($#r2_cqc_sim1 :::"are_similar"::: ) ))) ;