:: VALUAT_1 semantic presentation begin definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; func :::"Valuations_in"::: "(" "Al" "," "A" ")" -> ($#m1_hidden :::"set"::: ) equals :: VALUAT_1:def 1 (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al" ")" ) "," "A" ")" ); end; :: deftheorem defines :::"Valuations_in"::: VALUAT_1:def 1 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) "," (Set (Var "A")) ")" )))); registrationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ) -> ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: VALUAT_1:1 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "Al")) ")" ) "," (Set (Var "A")))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Valuations_in"::: redefine func :::"Valuations_in"::: "(" "Al" "," "A" ")" -> ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "Al") "," "A"; end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "Al")); let "p" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ); func :::"FOR_ALL"::: "(" "x" "," "p" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) means :: VALUAT_1:def 2 (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k12_margrel1 :::"ALL"::: ) "{" (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "v9")) ")" ) where v9 "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ) : (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool (Bool "x" ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "v9")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ))); end; :: deftheorem defines :::"FOR_ALL"::: VALUAT_1:def 2 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "," (Set (Var "b5")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k12_margrel1 :::"ALL"::: ) "{" (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "v9")) ")" ) where v9 "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) : (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "v9")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ))) ")" ))))); theorem :: VALUAT_1:2 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "iff" (Bool "ex" (Set (Var "v1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) & (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "v1")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) ")" )) ")" )))))) ; theorem :: VALUAT_1:3 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "iff" (Bool "for" (Set (Var "v1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "v1")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" )))))) ; notationlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "ll" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); synonym "v" :::"*'"::: "ll" for "A" :::"*"::: "Al"; end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "ll" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); :: original: :::"*'"::: redefine func "v" :::"*'"::: "ll" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "A" means :: VALUAT_1:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) "k") & (Bool "(" "for" (Set (Var "i")) "being" ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "k")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "v" ($#k1_funct_1 :::"."::: ) (Set "(" "ll" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"*'"::: VALUAT_1:def 3 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "ll" be ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Const "k")) "," (Set (Const "Al")); let "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Const "A"))); func "ll" :::"'in'"::: "r" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) means :: VALUAT_1:def 4 (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) "ll") ($#r2_hidden :::"in"::: ) "r")) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) "ll") ($#r2_hidden :::"in"::: ) "r") ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) "ll") ($#r2_hidden :::"in"::: ) "r"))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" & "(" (Bool (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool "not" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) "ll") ($#r2_hidden :::"in"::: ) "r")) ")" ")" )); end; :: deftheorem defines :::"'in'"::: VALUAT_1:def 4 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b6")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "ll")) ($#k5_valuat_1 :::"'in'"::: ) (Set (Var "r")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r"))))) "implies" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool "not" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r")))) ")" ")" )) ")" ))))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ")" ); let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); :: original: :::"."::: redefine func "F" :::"."::: "p" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"interpretation"::: "of" "Al" "," "D" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) "Al" ")" ) "," (Set "(" ($#k3_margrel1 :::"relations_on"::: ) "D" ")" ) means :: VALUAT_1:def 5 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) "Al") (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) "D") "holds" (Bool "(" "not" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_margrel1 :::"="::: ) (Set (Var "r"))) "or" (Bool (Set (Var "r")) ($#r1_margrel1 :::"="::: ) (Set ($#k4_margrel1 :::"empty_rel"::: ) "D")) "or" (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k5_margrel1 :::"the_arity_of"::: ) (Set (Var "r")))) ")" ))); end; :: deftheorem defines :::"interpretation"::: VALUAT_1:def 5 : (Bool "for" (Set (Var "Al")) "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 "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "D"))) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))) "holds" (Bool "(" "not" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "P"))) ($#r1_margrel1 :::"="::: ) (Set (Var "r"))) "or" (Bool (Set (Var "r")) ($#r1_margrel1 :::"="::: ) (Set ($#k4_margrel1 :::"empty_rel"::: ) (Set (Var "D")))) "or" (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k5_margrel1 :::"the_arity_of"::: ) (Set (Var "r")))) ")" ))) ")" )))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "J" be ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Const "Al")) "," (Set (Const "A")); let "P" be ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "k")) "," (Set (Const "Al")); :: original: :::"."::: redefine func "J" :::"."::: "P" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) "A"); end; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Const "Al")) "," (Set (Const "A")); let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); func :::"Valid"::: "(" "p" "," "J" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) means :: VALUAT_1:def 6 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ")" ) "st" (Bool "(" (Bool it ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) "p")) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) "Al" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" (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")) "," "Al" (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "Al" "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "ll")) ($#k5_valuat_1 :::"'in'"::: ) (Set "(" "J" ($#k7_valuat_1 :::"."::: ) (Set (Var "P")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k15_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k16_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ) ")" )) ")" ))))) ")" ) ")" )); end; :: deftheorem defines :::"Valid"::: VALUAT_1:def 6 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "b5")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "ll")) ($#k5_valuat_1 :::"'in'"::: ) (Set "(" (Set (Var "J")) ($#k7_valuat_1 :::"."::: ) (Set (Var "P")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k15_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k16_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "F")) ($#k6_valuat_1 :::"."::: ) (Set (Var "p")) ")" ) ")" )) ")" ))))) ")" ) ")" )) ")" )))))); theorem :: VALUAT_1:4 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) ($#k1_margrel1 :::"-->"::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )))))) ; theorem :: VALUAT_1:5 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )))))) ; theorem :: VALUAT_1:6 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "ll")) ($#k5_valuat_1 :::"'in'"::: ) (Set "(" (Set (Var "J")) ($#k7_valuat_1 :::"."::: ) (Set (Var "P")) ")" ))))))))) ; theorem :: VALUAT_1:7 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) & (Bool (Set (Var "r")) ($#r1_margrel1 :::"="::: ) (Set (Set (Var "J")) ($#k7_valuat_1 :::"."::: ) (Set (Var "P"))))) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) "iff" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )))))))))) ; theorem :: VALUAT_1:8 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) & (Bool (Set (Var "r")) ($#r1_margrel1 :::"="::: ) (Set (Set (Var "J")) ($#k7_valuat_1 :::"."::: ) (Set (Var "P"))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Set (Var "v")) ($#k4_valuat_1 :::"*'"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "r")))) "iff" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" )))))))))) ; theorem :: VALUAT_1:9 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k15_margrel1 :::"'not'"::: ) (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ))))))) ; theorem :: VALUAT_1:10 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))))))) ; theorem :: VALUAT_1:11 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k16_margrel1 :::"'&'"::: ) (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "q")) "," (Set (Var "J")) ")" ")" ))))))) ; theorem :: VALUAT_1:12 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "q")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))))))) ; theorem :: VALUAT_1:13 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ")" ))))))) ; theorem :: VALUAT_1:14 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))))))) ; theorem :: VALUAT_1:15 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); let "J" be ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Const "Al")) "," (Set (Const "A")); let "v" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Const "Al")) "," (Set (Const "A")) ")" ); pred "J" "," "v" :::"|="::: "p" means :: VALUAT_1:def 7 (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" "p" "," "J" ")" ")" ) ($#k3_funct_2 :::"."::: ) "v") ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )); end; :: deftheorem defines :::"|="::: VALUAT_1:def 7 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )))))); theorem :: VALUAT_1:16 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "P")) ($#k4_cqc_lang :::"!"::: ) (Set (Var "ll")))) "iff" (Bool (Set (Set "(" (Set (Var "ll")) ($#k5_valuat_1 :::"'in'"::: ) (Set "(" (Set (Var "J")) ($#k7_valuat_1 :::"."::: ) (Set (Var "P")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )))))))) ; theorem :: VALUAT_1:17 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) "iff" (Bool (Bool "not" (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))) ")" )))))) ; theorem :: VALUAT_1:18 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) & (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) ")" ) ")" )))))) ; theorem :: VALUAT_1:19 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set (Set "(" ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ))))))) ; theorem :: VALUAT_1:20 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "v1")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "v1")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" ))))))) ; theorem :: VALUAT_1:21 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" )))))) ; theorem :: VALUAT_1:22 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "J")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" )))))) ; theorem :: VALUAT_1:23 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "or" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "q")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) ")" )))))) ; theorem :: VALUAT_1:24 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (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 "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) "iff" "(" (Bool (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))) "implies" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q"))) ")" ")" )))))) ; theorem :: VALUAT_1:25 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) "st" (Bool (Bool (Set (Set "(" ($#k3_valuat_1 :::"FOR_ALL"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Const "Al")) "," (Set (Const "A")); let "p" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al"))); pred "J" :::"|="::: "p" means :: VALUAT_1:def 8 (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" "Al" "," "A" ")" ) "holds" (Bool "J" "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) "p")); end; :: deftheorem defines :::"|="::: VALUAT_1:def 8 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool "(" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Var "p"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))) ")" ))))); theorem :: VALUAT_1:26 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "ex" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "V1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "V2")) ($#k3_funct_2 :::"."::: ) (Set (Var "Z")))) ")" )))))) ; theorem :: VALUAT_1:27 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "w")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "w")))))))))) ; theorem :: VALUAT_1:28 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "w")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))))))))) ; theorem :: VALUAT_1:29 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "w")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "w")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Var "J")) "," (Set (Var "w")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p")))) ")" ))))))) ; theorem :: VALUAT_1:30 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s9")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s9")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "p")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_valuat_1 :::"Valid"::: ) "(" (Set (Var "q")) "," (Set (Var "J")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))))))))) ; theorem :: VALUAT_1:31 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s9")))))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "s9")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")) ")" ))))))) ; theorem :: VALUAT_1:32 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))))))) ; theorem :: VALUAT_1:33 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: VALUAT_1:34 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))))))))) ; theorem :: VALUAT_1:35 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )))))))) ; theorem :: VALUAT_1:36 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "t")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "t")) ")" ) ")" ) ")" )))))))) ; theorem :: VALUAT_1:37 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "p"))) & (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Var "q")))))))) ; theorem :: VALUAT_1:38 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "v")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k2_valuat_1 :::"Valuations_in"::: ) "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) "," (Set (Var "v")) ($#r1_valuat_1 :::"|="::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")))))))))) ; theorem :: VALUAT_1:39 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al"))))))) ; theorem :: VALUAT_1:40 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: VALUAT_1:41 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")))))))) ; theorem :: VALUAT_1:42 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: VALUAT_1:43 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "t")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "t")) ")" ) ")" ) ")" ))))))) ; theorem :: VALUAT_1:44 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Var "q"))))))) ; theorem :: VALUAT_1:45 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))))))))) ; theorem :: VALUAT_1:46 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )))))))) ; theorem :: VALUAT_1:47 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "J")) "being" ($#m1_valuat_1 :::"interpretation"::: ) "of" (Set (Var "Al")) "," (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "J")) ($#r2_valuat_1 :::"|="::: ) (Set (Var "q"))))))))) ;