:: QC_LANG1 semantic presentation begin theorem :: QC_LANG1:1 (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "k")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: QC_LANG1:2 (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "k3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "k3")) ($#k1_enumset1 :::"}"::: ) ) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; definitionmode :::"QC-alphabet"::: -> ($#m1_hidden :::"set"::: ) means :: QC_LANG1:def 1 (Bool "(" (Bool it "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ) & (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ")" ); end; :: deftheorem defines :::"QC-alphabet"::: QC_LANG1:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) "is" ($#m1_qc_lang1 :::"QC-alphabet"::: ) ) "iff" (Bool "(" (Bool (Set (Var "b1")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ) & (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ")" ) ")" )); registration cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"QC-symbols"::: "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: QC_LANG1:def 2 (Set ($#k10_xtuple_0 :::"rng"::: ) "A"); end; :: deftheorem defines :::"QC-symbols"::: QC_LANG1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "A"))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode QC-symbol of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_qc_lang1 :::"QC-symbols"::: ) "A"); end; theorem :: QC_LANG1:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool "(" (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")))) ")" )) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k1_qc_lang1 :::"QC-symbols"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"QC-variables"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: QC_LANG1:def 3 (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 6) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 4) "," (Num 5) ($#k2_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"QC-variables"::: QC_LANG1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 6) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 4) "," (Num 5) ($#k2_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: QC_LANG1:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode QC-variable of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A"); func :::"bound_QC-variables"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) "A" ")" ) equals :: QC_LANG1:def 4 (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 4) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"fixed_QC-variables"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) "A" ")" ) equals :: QC_LANG1:def 5 (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 5) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"free_QC-variables"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) "A" ")" ) equals :: QC_LANG1:def 6 (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 6) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"QC-pred_symbols"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: QC_LANG1:def 7 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), x "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" : (Bool (Num 7) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" ; end; :: deftheorem defines :::"bound_QC-variables"::: QC_LANG1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 4) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))); :: deftheorem defines :::"fixed_QC-variables"::: QC_LANG1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 5) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))); :: deftheorem defines :::"free_QC-variables"::: QC_LANG1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Num 6) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))); :: deftheorem defines :::"QC-pred_symbols"::: QC_LANG1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), x "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) : (Bool (Num 7) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )); registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: QC_LANG1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: QC_LANG1:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode QC-pred_symbol of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "P" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (Set (Const "A"))); func :::"the_arity_of"::: "P" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: QC_LANG1:def 8 (Bool (Set "P" ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 7) ($#k2_nat_1 :::"+"::: ) it)); end; :: deftheorem defines :::"the_arity_of"::: QC_LANG1:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) (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_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P")))) "iff" (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 7) ($#k2_nat_1 :::"+"::: ) (Set (Var "b3")))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "k" :::"-ary_QC-pred_symbols"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_qc_lang1 :::"QC-pred_symbols"::: ) "A" ")" ) equals :: QC_LANG1:def 9 "{" (Set (Var "P")) where P "is" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" "A" : (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) "k") "}" ; end; :: deftheorem defines :::"-ary_QC-pred_symbols"::: QC_LANG1:def 9 : (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"::: ) ) "holds" (Bool (Set (Set (Var "k")) ($#k8_qc_lang1 :::"-ary_QC-pred_symbols"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "P")) where P "is" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "A")) : (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) "}" ))); registrationlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster (Set "k" ($#k8_qc_lang1 :::"-ary_QC-pred_symbols"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode bound_QC-variable of "A" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A"); mode fixed_QC-variable of "A" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) "A"); mode free_QC-variable of "A" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) "A"); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode QC-pred_symbol of "k" "," "A" is ($#m2_subset_1 :::"Element"::: ) "of" (Set "k" ($#k8_qc_lang1 :::"-ary_QC-pred_symbols"::: ) "A"); end; registrationlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() "k" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A"); end; definitionlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode QC-variable_list of "k" "," "A" is "k" ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; attr "D" is "A" :::"-closed"::: means :: QC_LANG1:def 10 (Bool "(" (Bool "D" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A" (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A" "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) "D"))) ")" ) & (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) "D") & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "D") ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "D") ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "D")) "holds" (Bool (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "D")) ")" ) ")" ); end; :: deftheorem defines :::"-closed"::: QC_LANG1:def 10 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "D")) "is" (Set (Var "A")) ($#v1_qc_lang1 :::"-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "D")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))))) ")" ) & (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" ) ")" ) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"QC-WFF"::: "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: QC_LANG1:def 11 (Bool "(" (Bool it "is" "A" ($#v1_qc_lang1 :::"-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" "A" ($#v1_qc_lang1 :::"-closed"::: ) )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"QC-WFF"::: QC_LANG1:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" (Set (Var "A")) ($#v1_qc_lang1 :::"-closed"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) "is" (Set (Var "A")) ($#v1_qc_lang1 :::"-closed"::: ) )) "holds" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))); theorem :: QC_LANG1:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "is" (Set (Var "A")) ($#v1_qc_lang1 :::"-closed"::: ) )) ; registrationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) "A" ($#v1_qc_lang1 :::"-closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode QC-formula of "A" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A"); end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "P" be ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Const "A")); let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); assume (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Const "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "l")))) ; func "P" :::"!"::: "l" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") equals :: QC_LANG1:def 12 (Set (Set ($#k12_finseq_1 :::"<*"::: ) "P" ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "l"); end; :: deftheorem defines :::"!"::: QC_LANG1:def 12 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "P")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "l"))))))); theorem :: QC_LANG1:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set (Set (Var "p")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "ll")))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"@"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: QC_LANG1:def 13 "p"; end; :: deftheorem defines :::"@"::: QC_LANG1:def 13 : (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 ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"VERUM"::: "A" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG1:def 14 (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"'not'"::: "p" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG1:def 15 (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) "p" ")" )); let "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func "p" :::"'&'"::: "q" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG1:def 16 (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) "p" ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) "q" ")" )); end; :: deftheorem defines :::"VERUM"::: QC_LANG1:def 14 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ))); :: deftheorem defines :::"'not'"::: QC_LANG1:def 15 : (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 ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ))))); :: deftheorem defines :::"'&'"::: QC_LANG1:def 16 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "q")) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"All"::: "(" "x" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG1:def 17 (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) "x" ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) "p" ")" )); end; :: deftheorem defines :::"All"::: QC_LANG1:def 17 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k4_tarski :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" )))))); scheme :: QC_LANG1:sch 1 QCInd{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))] } : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "F"))])) provided (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")))])))) and (Bool P1[(Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "p"))])) "holds" (Bool P1[(Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")))])) and (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "p"))]) & (Bool P1[(Set (Var "q"))])) "holds" (Bool P1[(Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")))])) and (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "p"))])) "holds" (Bool P1[(Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )]))) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); attr "F" is :::"atomic"::: means :: QC_LANG1:def 18 (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A" "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll"))))))); attr "F" is :::"negative"::: means :: QC_LANG1:def 19 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p"))))); attr "F" is :::"conjunctive"::: means :: QC_LANG1:def 20 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))))); attr "F" is :::"universal"::: means :: QC_LANG1:def 21 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A"(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )))); end; :: deftheorem defines :::"atomic"::: QC_LANG1:def 18 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll"))))))) ")" ))); :: deftheorem defines :::"negative"::: QC_LANG1:def 19 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p"))))) ")" ))); :: deftheorem defines :::"conjunctive"::: QC_LANG1:def 20 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))))) ")" ))); :: deftheorem defines :::"universal"::: QC_LANG1:def 21 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )))) ")" ))); theorem :: QC_LANG1:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) "or" (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ")" ))) ; theorem :: QC_LANG1:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG1:11 (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")) "holds" (Bool (Set ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))))) ; theorem :: QC_LANG1:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" & "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Var "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) "implies" (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ")" & "(" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))))) "implies" (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ")" ")" ))) ; theorem :: QC_LANG1:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "G")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k11_qc_lang1 :::"@"::: ) (Set (Var "G"))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ; func :::"the_pred_symbol_of"::: "F" -> ($#m1_subset_1 :::"QC-pred_symbol":::) "of" "A" means :: QC_LANG1:def 22 (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")))) ")" )))); end; :: deftheorem defines :::"the_pred_symbol_of"::: QC_LANG1:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_qc_lang1 :::"the_pred_symbol_of"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")))) ")" )))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ; func :::"the_arguments_of"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) "A") means :: QC_LANG1:def 23 (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," "A"(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," "A" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "ll"))) & (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")))) ")" )))); end; :: deftheorem defines :::"the_arguments_of"::: QC_LANG1:def 23 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A"))(Bool "ex" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "ll"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "ll")))) ")" )))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ; func :::"the_argument_of"::: "F" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" means :: QC_LANG1:def 24 (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) it)); end; :: deftheorem defines :::"the_argument_of"::: QC_LANG1:def 24 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "b3")))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) ; func :::"the_left_argument_of"::: "F" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" means :: QC_LANG1:def 25 (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set it ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))))); end; :: deftheorem defines :::"the_left_argument_of"::: QC_LANG1:def 25 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) ; func :::"the_right_argument_of"::: "F" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" means :: QC_LANG1:def 26 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) it))); end; :: deftheorem defines :::"the_right_argument_of"::: QC_LANG1:def 26 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "b3"))))) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); assume (Bool (Set (Const "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ; func :::"bound_in"::: "F" -> ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" means :: QC_LANG1:def 27 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" it "," (Set (Var "p")) ")" ))); func :::"the_scope_of"::: "F" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" means :: QC_LANG1:def 28 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," it ")" ))); end; :: deftheorem defines :::"bound_in"::: QC_LANG1:def 27 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "b3")) "," (Set (Var "p")) ")" ))) ")" )))); :: deftheorem defines :::"the_scope_of"::: QC_LANG1:def 28 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "b3")) ")" ))) ")" )))); theorem :: QC_LANG1:14 (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"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ))))) ; theorem :: QC_LANG1:15 (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"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ))) ")" ))) ; theorem :: QC_LANG1:16 (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"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "p")) ")" ))))) ; scheme :: QC_LANG1:sch 2 QCInd2{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))] } : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "p"))])) provided (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 P1[(Set (Var "p"))]) ")" & (Bool P1[(Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" ))]) & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool P1[(Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")))])) "implies" (Bool P1[(Set (Var "p"))]) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool P1[(Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")))]) & (Bool P1[(Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")))])) "implies" (Bool P1[(Set (Var "p"))]) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool P1[(Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")))])) "implies" (Bool P1[(Set (Var "p"))]) ")" ")" )) proof end; theorem :: QC_LANG1:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 2)) & (Bool (Set (Set (Var "P")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 3)) ")" )))) ; theorem :: QC_LANG1:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & "(" (Bool (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")))) ")" & "(" (Bool (Bool (Set (Var "F")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "F")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) ")" & "(" (Bool (Bool (Set (Var "F")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "implies" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) ")" ")" ))) ; theorem :: QC_LANG1:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 2)) & (Bool (Set (Set "(" (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Num 3)) ")" ))) ; theorem :: QC_LANG1:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) & (Bool (Bool "not" (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#v3_qc_lang1 :::"negative"::: ) )) & (Bool (Bool "not" (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) & (Bool (Bool "not" (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#v5_qc_lang1 :::"universal"::: ) )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) & (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) & (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) & (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) ")" )) ")" ) ")" ) ")" )) ; scheme :: QC_LANG1:sch 3 QCFuncEx{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k12_qc_lang1 :::"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")) ")" ) ")" ) ")" )) ")" & "(" (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")) ")" ) ")" ) ")" )) ")" & "(" (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 (Var "p")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) ")" )) ")" ")" ) ")" ) ")" )) proof end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "ll" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); func :::"still_not-bound_in"::: "ll" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) equals :: QC_LANG1:def 29 "{" (Set "(" "ll" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "ll")) & (Bool (Set "ll" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A")) ")" ) "}" ; end; :: deftheorem defines :::"still_not-bound_in"::: QC_LANG1:def 29 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "ll")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "ll"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "ll")))) & (Bool (Set (Set (Var "ll")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); func :::"still_not-bound_in"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) means :: QC_LANG1:def 30 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A" ")" ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "p")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & "(" (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 "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) "A")) ")" ) "}" ) ")" & "(" (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 (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (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 (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (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 (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"still_not-bound_in"::: QC_LANG1:def 30 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & "(" (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 "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ) ")" & "(" (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 (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (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 (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (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 (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" ")" ) ")" ) ")" )) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "A")); attr "p" is :::"closed"::: means :: QC_LANG1:def 31 (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"closed"::: QC_LANG1:def 31 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) "iff" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; mode :::"Relation"::: "of" "A" -> ($#m1_hidden :::"Relation":::) means :: QC_LANG1:def 32 (Bool it ($#r2_wellord1 :::"well_orders"::: ) (Set (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))); end; :: deftheorem defines :::"Relation"::: QC_LANG1:def 32 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_qc_lang1 :::"Relation"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set (Var "b2")) ($#r2_wellord1 :::"well_orders"::: ) (Set (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s", "t" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); pred "s" :::"<="::: "t" means :: QC_LANG1:def 33 (Bool "ex" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) "s") & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) "t") & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" )) if (Bool "(" (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "t" ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) (Bool (Set ($#k4_tarski :::"["::: ) "s" "," "t" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "the" ($#m2_qc_lang1 :::"Relation"::: ) "of" "A") if (Bool "(" (Bool (Bool "not" "s" ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Bool "not" "t" ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ) otherwise (Bool "t" ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"<="::: QC_LANG1:def 33 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) "iff" (Bool "ex" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Bool "not" (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "the" ($#m2_qc_lang1 :::"Relation"::: ) "of" (Set (Var "A"))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "or" "not" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "or" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) "iff" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) ")" ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s", "t" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); pred "s" :::"<"::: "t" means :: QC_LANG1:def 34 (Bool "(" (Bool "s" ($#r1_qc_lang1 :::"<="::: ) "t") & (Bool "s" ($#r1_hidden :::"<>"::: ) "t") ")" ); end; :: deftheorem defines :::"<"::: QC_LANG1:def 34 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) "iff" (Bool "(" (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) ")" ) ")" ))); theorem :: QC_LANG1:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u")))) "holds" (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u"))))) ; theorem :: QC_LANG1:22 (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")) "holds" (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))))) ; theorem :: QC_LANG1:23 (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")) "st" (Bool (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u"))) & (Bool (Set (Var "u")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t")))) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "t"))))) ; theorem :: QC_LANG1:24 (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")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "u"))) "or" (Bool (Set (Var "u")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) ")" ))) ; theorem :: QC_LANG1:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) "iff" (Bool (Bool "not" (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "s")))) ")" ))) ; theorem :: QC_LANG1:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) "or" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) "or" (Bool (Set (Var "t")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "s"))) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Const "A")) ")" ); func :::"min"::: "Y" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" means :: QC_LANG1:def 35 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "Y") & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "Y")) "holds" (Bool it ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) ")" ) ")" ); end; :: deftheorem defines :::"min"::: QC_LANG1:def 35 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (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 ($#k25_qc_lang1 :::"min"::: ) (Set (Var "Y")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "b3")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) ")" ) ")" ) ")" )))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"0"::: "A" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" means :: QC_LANG1:def 36 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" "holds" (Bool it ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t")))); end; :: deftheorem defines :::"0"::: QC_LANG1:def 36 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k26_qc_lang1 :::"0"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "b2")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t")))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); func :::"Seg"::: "s" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) equals :: QC_LANG1:def 37 "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A" : (Bool "s" ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) "}" ; end; :: deftheorem defines :::"Seg"::: QC_LANG1:def 37 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k27_qc_lang1 :::"Seg"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) : (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) "}" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); func "s" :::"++"::: -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" equals :: QC_LANG1:def 38 (Set ($#k25_qc_lang1 :::"min"::: ) (Set "(" ($#k27_qc_lang1 :::"Seg"::: ) "s" ")" )); end; :: deftheorem defines :::"++"::: QC_LANG1:def 38 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "s")) ($#k28_qc_lang1 :::"++"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k25_qc_lang1 :::"min"::: ) (Set "(" ($#k27_qc_lang1 :::"Seg"::: ) (Set (Var "s")) ")" ))))); theorem :: QC_LANG1:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Set (Var "s")) ($#k28_qc_lang1 :::"++"::: ) )))) ; theorem :: QC_LANG1:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set ($#k25_qc_lang1 :::"min"::: ) (Set (Var "Y2"))) ($#r1_qc_lang1 :::"<="::: ) (Set ($#k25_qc_lang1 :::"min"::: ) (Set (Var "Y1")))))) ; theorem :: QC_LANG1:29 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "v"))))) ; theorem :: QC_LANG1:30 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "s")) ($#r2_qc_lang1 :::"<"::: ) (Set (Var "v"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_hidden :::"set"::: ) ; func "s" :::"@"::: "A" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" equals :: QC_LANG1:def 39 "s" if (Bool "s" "is" ($#m1_subset_1 :::"QC-symbol":::) "of" "A") otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"@"::: QC_LANG1:def 39 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "s")) "is" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")))) "implies" (Bool (Set (Set (Var "s")) ($#k29_qc_lang1 :::"@"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" & "(" (Bool (Bool (Set (Var "s")) "is" (Bool "not" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A"))))) "implies" (Bool (Set (Set (Var "s")) ($#k29_qc_lang1 :::"@"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "t" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "t" :::"+"::: "n" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" means :: QC_LANG1:def 40 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "t") & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) ($#k28_qc_lang1 :::"++"::: ) )) ")" ) ")" )); end; :: deftheorem defines :::"+"::: QC_LANG1:def 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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) ($#k28_qc_lang1 :::"++"::: ) )) ")" ) ")" )) ")" ))))); theorem :: QC_LANG1:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "t")) ($#r1_qc_lang1 :::"<="::: ) (Set (Set (Var "t")) ($#k30_qc_lang1 :::"+"::: ) (Set (Var "n"))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; func "A" :::"-one_in"::: "Y" -> ($#m1_subset_1 :::"QC-symbol":::) "of" "A" equals :: QC_LANG1:def 41 "the" ($#m1_subset_1 :::"Element"::: ) "of" "Y" if (Bool "Y" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) "A" ")" )) otherwise (Set ($#k26_qc_lang1 :::"0"::: ) "A"); end; :: deftheorem defines :::"-one_in"::: QC_LANG1:def 41 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" ))) "implies" (Bool (Set (Set (Var "A")) ($#k31_qc_lang1 :::"-one_in"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y"))) ")" & "(" (Bool (Bool (Set (Var "Y")) "is" (Bool "not" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_qc_lang1 :::"QC-symbols"::: ) (Set (Var "A")) ")" )))) "implies" (Bool (Set (Set (Var "A")) ($#k31_qc_lang1 :::"-one_in"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k26_qc_lang1 :::"0"::: ) (Set (Var "A")))) ")" ")" )));