:: FOMODEL0 semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); attr "f" is "X" :::"-one-to-one"::: means :: FOMODEL0:def 1 (Bool (Set "f" ($#k5_relat_1 :::"|"::: ) "X") "is" ($#v2_funct_1 :::"one-to-one"::: ) ); end; :: deftheorem defines :::"-one-to-one"::: FOMODEL0:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "X")) ($#v1_fomodel0 :::"-one-to-one"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is "f" :::"-unambiguous"::: means :: FOMODEL0:def 2 (Bool "f" "is" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "D" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v1_fomodel0 :::"-one-to-one"::: ) ); end; :: deftheorem defines :::"-unambiguous"::: FOMODEL0:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" (Set (Var "f")) ($#v2_fomodel0 :::"-unambiguous"::: ) ) "iff" (Bool (Set (Var "f")) "is" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#v1_fomodel0 :::"-one-to-one"::: ) ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is "D" :::"-prefix"::: means :: FOMODEL0:def 3 (Bool "X" "is" (Set "D" ($#k11_monoid_0 :::"-concatenation"::: ) ) ($#v2_fomodel0 :::"-unambiguous"::: ) ); end; :: deftheorem defines :::"-prefix"::: FOMODEL0:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) ) "iff" (Bool (Set (Var "X")) "is" (Set (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ) ($#v2_fomodel0 :::"-unambiguous"::: ) ) ")" ))); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func "D" :::"-pr1"::: -> ($#m1_subset_1 :::"BinOp":::) "of" "D" equals :: FOMODEL0:def 4 (Set ($#k9_funct_3 :::"pr1"::: ) "(" "D" "," "D" ")" ); end; :: deftheorem defines :::"-pr1"::: FOMODEL0:def 4 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k1_fomodel0 :::"-pr1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "D")) "," (Set (Var "D")) ")" ))); theorem :: FOMODEL0:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_finseq_2 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "B")) ")" ))))) ; theorem :: FOMODEL0:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_finseq_2 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ))))) ; theorem :: FOMODEL0:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "B")) ")" ))))) ; theorem :: FOMODEL0:4 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) "is" (Set (Var "U")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "y")) "is" (Set (Var "U")) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y")))))) ; theorem :: FOMODEL0:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ")" ))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "D" ($#k1_fomodel0 :::"-pr1"::: ) ) -> ($#v2_binop_1 :::"associative"::: ) for ($#m1_subset_1 :::"BinOp":::) "of" "D"; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "D" "," "D" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_binop_1 :::"associative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "D" "," "D" ($#k2_zfmisc_1 :::":]"::: ) ) "," "D" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"*"::: redefine func "Y" :::"*"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "D" ($#k11_monoid_0 :::"-concatenation"::: ) ) -> ($#v2_binop_1 :::"associative"::: ) for ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) "m" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is "X" :::"-one-to-one"::: means :: FOMODEL0:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ))) & (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"-one-to-one"::: FOMODEL0:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "X")) ($#v1_fomodel0 :::"-one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster "f" ($#v2_fomodel0 :::"-unambiguous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k5_relat_1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; registrationlet "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; identify ; identify ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_setfam_1 :::"empty-membered"::: ) for ($#m1_hidden :::"set"::: ) ; let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "e" ($#k1_tarski :::"}"::: ) ) -> ($#v2_setfam_1 :::"empty-membered"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "m1" ($#k4_finseq_2 :::"-tuples_on"::: ) "U") -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; registrationlet "X" be ($#v2_setfam_1 :::"empty-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_setfam_1 :::"empty-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "m0" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "m0" ($#k4_finseq_2 :::"-tuples_on"::: ) "A") -> ($#v2_setfam_1 :::"empty-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "m1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "m1" ($#k4_finseq_2 :::"-tuples_on"::: ) "e") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "e" ($#k3_xboole_0 :::"/\"::: ) "f") -> "f" ($#v2_fomodel0 :::"-unambiguous"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "e" ($#k3_xboole_0 :::"/\"::: ) "U") -> "U" ($#v3_fomodel0 :::"-prefix"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster "U" ($#v3_fomodel0 :::"-prefix"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"MultPlace"::: "(" "f" "," "x" ")" -> ($#m1_hidden :::"Function":::) means :: FOMODEL0:def 6 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "x" ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"MultPlace"::: FOMODEL0:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_fomodel0 :::"MultPlace"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) ")" ) ")" ) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "x" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); func :::"MultPlace"::: "(" "f" "," "x" ")" -> ($#m1_hidden :::"Function":::) equals :: FOMODEL0:def 7 (Set ($#k3_fomodel0 :::"MultPlace"::: ) "(" "f" "," "x" ")" ); end; :: deftheorem defines :::"MultPlace"::: FOMODEL0:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "holds" (Bool (Set ($#k4_fomodel0 :::"MultPlace"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_fomodel0 :::"MultPlace"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); func :::"MultPlace"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," "D" means :: FOMODEL0:def 8 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_fomodel0 :::"MultPlace"::: ) "(" "f" "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"MultPlace"::: FOMODEL0:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_fomodel0 :::"MultPlace"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )))) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "X" be ($#m1_hidden :::"set"::: ) ; redefine attr "X" is "f" :::"-unambiguous"::: means :: FOMODEL0:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k3_xboole_0 :::"/\"::: ) "D")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "X" ($#k3_xboole_0 :::"/\"::: ) "D")) & (Bool (Set (Var "d1")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set (Var "d2")) ($#r2_hidden :::"in"::: ) "D") & (Bool (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "d2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) ")" )); end; :: deftheorem defines :::"-unambiguous"::: FOMODEL0:def 9 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" (Set (Var "f")) ($#v2_fomodel0 :::"-unambiguous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "D")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "D")))) & (Bool (Set (Var "d1")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "d2")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "d2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) ")" )) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func "D" :::"-firstChar"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," "D" equals :: FOMODEL0:def 10 (Set ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" "D" ($#k1_fomodel0 :::"-pr1"::: ) ")" )); end; :: deftheorem defines :::"-firstChar"::: FOMODEL0:def 10 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k6_fomodel0 :::"-firstChar"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" (Set (Var "D")) ($#k1_fomodel0 :::"-pr1"::: ) ")" )))); theorem :: FOMODEL0:6 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" (Set (Var "U")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k6_fomodel0 :::"-firstChar"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func "D" :::"-multiCat"::: -> ($#m1_hidden :::"Function":::) equals :: FOMODEL0:def 11 (Set (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" "D" ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ")" )); end; :: deftheorem defines :::"-multiCat"::: FOMODEL0:def 11 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k7_fomodel0 :::"-multiCat"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"-multiCat"::: redefine func "D" :::"-multiCat"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "D" ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "e") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> "D" ($#v3_fomodel0 :::"-prefix"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) "D" ")" )); end; theorem :: FOMODEL0:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "D")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")) ")" )) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) )))) ; theorem :: FOMODEL0:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) )) "holds" (Bool (Set (Set (Var "D")) ($#k8_fomodel0 :::"-multiCat"::: ) ) "is" (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))) ($#v1_fomodel0 :::"-one-to-one"::: ) )))) ; theorem :: FOMODEL0:9 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "Y")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: FOMODEL0:10 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) "is" ($#v1_xboole_0 :::"zero"::: ) )) "holds" (Bool (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FOMODEL0:11 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set (Var "Y")) ")" )))) ; theorem :: FOMODEL0:12 (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "x")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A"))))) ; definitionlet "A", "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"chi"::: redefine func :::"chi"::: "(" "A" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: FOMODEL0:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_monoid_0 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "d")) ")" )) ")" ) ")" )))) ; theorem :: FOMODEL0:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "D")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))))) ; theorem :: FOMODEL0:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "D")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k1_monoid_0 :::"^"::: ) (Set (Var "d2")))))) ; registrationlet "f", "g" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "f", "g" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> "m" ($#v3_card_1 :::"-element"::: ) ; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> "X" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for(Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"X" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f" "," "g" ($#k13_funct_3 :::":>"::: ) ) -> (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) "m" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "p" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "p" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k3_relat_1 :::"*"::: ) "f") -> "m" ($#v3_card_1 :::"-element"::: ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "p", "q" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); func "f" :::"AppliedPairwiseTo"::: "(" "p" "," "q" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FOMODEL0:def 12 (Set "f" ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) "p" "," "q" ($#k13_funct_3 :::":>"::: ) )); end; :: deftheorem defines :::"AppliedPairwiseTo"::: FOMODEL0:def 12 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k10_fomodel0 :::"AppliedPairwiseTo"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k13_funct_3 :::":>"::: ) )))))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "m" be ($#m1_hidden :::"Nat":::); let "p", "q" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); cluster (Set "f" ($#k10_fomodel0 :::"AppliedPairwiseTo"::: ) "(" "p" "," "q" ")" ) -> "m" ($#v3_card_1 :::"-element"::: ) ; end; notationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "p", "q" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); synonym "f" :::"_\"::: "(" "p" "," "q" ")" for "f" :::"AppliedPairwiseTo"::: "(" "p" "," "q" ")" ; end; definitionredefine func :::"INT"::: equals :: FOMODEL0:def 13 (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )); end; :: deftheorem defines :::"INT"::: FOMODEL0:def 13 : (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))); theorem :: FOMODEL0:16 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" (Set (Var "Y")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "p")) "is" (Set (Var "m")) ($#v3_card_1 :::"-element"::: ) )) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))))))) ; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; func "A" :::"typed/\"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: FOMODEL0:def 14 (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B"); func "A" :::"/\typed"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "B" equals :: FOMODEL0:def 15 (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B"); end; :: deftheorem defines :::"typed/\"::: FOMODEL0:def 14 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k11_fomodel0 :::"typed/\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))))); :: deftheorem defines :::"/\typed"::: FOMODEL0:def 15 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k12_fomodel0 :::"/\typed"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; identify ; identify ; identify ; identify ; end; definitionlet "B", "A" be ($#m1_hidden :::"set"::: ) ; func "A" :::"null"::: "B" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL0:def 16 "A"; end; :: deftheorem defines :::"null"::: FOMODEL0:def 16 : (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k13_fomodel0 :::"null"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); identify ; identify ; end; registrationlet "A", "B", "C" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "B" ($#k6_subset_1 :::"\"::: ) "A" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "A" ($#k3_xboole_0 :::"/\"::: ) "C" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; func "A" :::"typed\"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: FOMODEL0:def 17 (Set "A" ($#k6_subset_1 :::"\"::: ) "B"); end; :: deftheorem defines :::"typed\"::: FOMODEL0:def 17 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k14_fomodel0 :::"typed\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B"))))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; identify ; identify ; end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; func "A" :::"\typed/"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "A" ($#k2_xboole_0 :::"\/"::: ) "B" ")" ) equals :: FOMODEL0:def 18 "A"; end; :: deftheorem defines :::"\typed/"::: FOMODEL0:def 18 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k15_fomodel0 :::"\typed/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; identify ; identify ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); identify ; identify ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k18_finseq_1 :::"[*]"::: ) ) -> ($#v8_relat_2 :::"transitive"::: ) for ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k18_finseq_1 :::"[*]"::: ) ) -> ($#v1_relat_2 :::"reflexive"::: ) for ($#m1_hidden :::"Relation":::); end; definitionfunc :::"plus"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: FOMODEL0:def 19 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))); end; :: deftheorem defines :::"plus"::: FOMODEL0:def 19 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_fomodel0 :::"plus"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) ")" )); theorem :: FOMODEL0:17 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k18_finseq_1 :::"[*]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "mm")) ")" ")" ) where mm "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ))) ; theorem :: FOMODEL0:18 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "f")) "," (Set (Var "m")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_funct_7 :::"iter"::: ) "(" (Set (Var "g")) "," (Set (Var "m")) ")" )))) ; registrationlet "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_tarski :::"union"::: ) "X") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; theorem :: FOMODEL0:19 (Bool "for" (Set (Var "Y")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "Y" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); cluster (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) "D" ")" ) ($#k3_funct_2 :::"."::: ) "d" ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) "d" ($#k6_domain_1 :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"FinSequence":::); let "q" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"FinSequence":::); identify ; identify ; identify ; identify ; end; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "Y")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); identify ; identify ; end; theorem :: FOMODEL0:20 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) "}" )) ; theorem :: FOMODEL0:21 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "Y"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ))))) ; theorem :: FOMODEL0:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: FOMODEL0:23 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Q")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Q")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; theorem :: FOMODEL0:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k9_fomodel0 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" ($#k9_fomodel0 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")))) ")" )) ; theorem :: FOMODEL0:25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; theorem :: FOMODEL0:26 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" (Set (Var "Y")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_finseq_1 :::"FinSequence-like"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Y"))))) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) -> "Y" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:27 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Q")) "being" ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "B")) "," (Set (Var "U1")) (Bool "for" (Set (Var "R")) "being" ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "B")) "," (Set (Var "U2")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_relset_1 :::"*"::: ) (Set (Var "Q")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "R"))) "is" ($#v1_funct_1 :::"Function-like"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_relset_1 :::"*"::: ) (Set (Var "Q")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "P")) ($#k4_relset_1 :::"*"::: ) (Set (Var "R"))))))))) ; theorem :: FOMODEL0:28 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)))) ; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p", "q" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> "U" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"FinSequence":::); end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; redefine attr "X" is "U" :::"-prefix"::: means :: FOMODEL0:def 20 (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "being" "U" ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2"))))) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" )); end; :: deftheorem defines :::"-prefix"::: FOMODEL0:def 20 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" (Set (Var "U")) ($#v3_fomodel0 :::"-prefix"::: ) ) "iff" (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "q2")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2"))))) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" )) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "X" ($#k3_finseq_2 :::"*"::: ) ); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); let "X" be (Set (Const "U")) ($#v3_fomodel0 :::"-prefix"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "U" ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" "m" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" )) -> "U" ($#v3_fomodel0 :::"-prefix"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:29 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" )) ; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) "y" ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) "x" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::)) & (Bool (Bool "not" (Set (Var "x")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" ))) ; theorem :: FOMODEL0:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "x")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Bool "not" (Set (Var "x")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "d")) ")" )) ")" ) ")" )))) ; registrationlet "p" be ($#m1_hidden :::"FinSequence":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k6_funct_4 :::"+~"::: ) "(" "x" "," "y" ")" ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); func "(" "x" "," "y" ")" :::"-SymbolSubstIn"::: "p" -> ($#m1_hidden :::"FinSequence":::) equals :: FOMODEL0:def 21 (Set "p" ($#k6_funct_4 :::"+~"::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"-SymbolSubstIn"::: FOMODEL0:def 21 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "(" "x" "," "y" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "p") -> "m" ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); let "p" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "(" "x" "," "u" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "p") -> "U" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"FinSequence":::); end; definitionlet "X", "x", "y" be ($#m1_hidden :::"set"::: ) ; let "p" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"-SymbolSubstIn"::: redefine func "(" "x" "," "y" ")" :::"-SymbolSubstIn"::: "p" -> ($#m1_hidden :::"FinSequence":::) equals :: FOMODEL0:def 22 (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) "X" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ")" ) ($#k3_relat_1 :::"*"::: ) "p"); end; :: deftheorem defines :::"-SymbolSubstIn"::: FOMODEL0:def 22 : (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k18_fomodel0 :::"-SymbolSubstIn"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")))))); definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); let "q" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"-SymbolSubstIn"::: redefine func "(" "x" "," "u" ")" :::"-SymbolSubstIn"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "U"; end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); func "x" :::"SubstWith"::: "u" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "U" ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" "U" ($#k3_finseq_2 :::"*"::: ) ")" ) means :: FOMODEL0:def 23 (Bool "for" (Set (Var "q")) "being" "U" ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set "(" "x" "," "u" ")" ($#k19_fomodel0 :::"-SymbolSubstIn"::: ) (Set (Var "q"))))); end; :: deftheorem defines :::"SubstWith"::: FOMODEL0:def 23 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "U")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set (Var "U")) ($#k3_finseq_2 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")))) "iff" (Bool "for" (Set (Var "q")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "u")) ")" ($#k19_fomodel0 :::"-SymbolSubstIn"::: ) (Set (Var "q"))))) ")" ))))); registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); cluster (Set "x" ($#k20_fomodel0 :::"SubstWith"::: ) "u") -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "F" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); let "m" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set "(" "x" ($#k20_fomodel0 :::"SubstWith"::: ) "u" ")" ) ($#k1_funct_1 :::"."::: ) "p") -> "m" ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "x" ($#k20_fomodel0 :::"SubstWith"::: ) "u" ")" ) ($#k1_funct_1 :::"."::: ) "e") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "U" ($#k7_fomodel0 :::"-multiCat"::: ) ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "U" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "n" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) (Set (Set (Const "m1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Const "n"))) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set ($#k1_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) "m1" ")" ) ($#k1_tarski :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) "U") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Set "(" (Set (Const "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Const "n"))) ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "U")) ($#k3_finseq_2 :::"*"::: ) ); cluster (Set (Set ($#k1_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) "U") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set ($#k9_finseq_1 :::"<*"::: ) "x" ($#k9_finseq_1 :::"*>"::: ) ) ($#k5_xboole_0 :::"\+\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Set (Const "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set "(" (Set "(" "p" ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) "p") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Set (Const "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Const "n"))) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" )) -> "m" ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#v5_relat_1 :::"-valued"::: ) -> ($#v3_relat_1 :::"empty-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_relat_1 :::"empty-yielding"::: ) -> (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:32 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fomodel0 :::"MultPlace"::: ) (Set "(" (Set (Var "U")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FOMODEL0:33 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" (Set (Set (Var "U")) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))))) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); let "R" be (Set (Const "Y")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"X" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); end; theorem :: FOMODEL0:34 (Bool "for" (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1")))) "implies" (Bool (Set "(" (Set (Var "u1")) "," (Set (Var "x2")) ")" ($#k18_fomodel0 :::"-SymbolSubstIn"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x2")) ($#k9_finseq_1 :::"*>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1")))) "implies" (Bool (Set "(" (Set (Var "u1")) "," (Set (Var "x2")) ")" ($#k18_fomodel0 :::"-SymbolSubstIn"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ")" )))) ; theorem :: FOMODEL0:35 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "u1")))) "implies" (Bool (Set (Set "(" (Set (Var "u1")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u2")) ($#k12_finseq_1 :::"*>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "u1")))) "implies" (Bool (Set (Set "(" (Set (Var "u1")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ")" ))) ; theorem :: FOMODEL0:36 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "q1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q1")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q2")) ")" ))))))) ; theorem :: FOMODEL0:37 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" (Set (Set (Var "U")) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k20_fomodel0 :::"SubstWith"::: ) (Set (Var "u")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: FOMODEL0:38 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "U")) ")" ) ")" )) ($#r1_hidden :::"="::: ) "{" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "u")) ($#k10_finseq_1 :::"*>"::: ) ) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) : (Bool verum) "}" )) ; registrationlet "f" be ($#m1_hidden :::"Function":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); cluster (Set (Set "(" (Set "(" "f" ($#k5_relat_1 :::"|"::: ) "U" ")" ) ($#k1_funct_1 :::"."::: ) "u" ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) "u" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"Function":::); let "U1", "U2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U1")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); cluster (Set (Set "(" (Set "(" "f" ($#k3_relat_1 :::"*"::: ) "g" ")" ) ($#k1_funct_1 :::"."::: ) "u" ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" "g" ($#k3_funct_2 :::"."::: ) "u" ")" ) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_int_1 :::"integer"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) -> ($#v7_ordinal1 :::"natural"::: ) ($#v1_int_1 :::"integer"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x", "y" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" "x" "," "y" ")" ")" ) ($#k6_xcmplx_0 :::"-"::: ) "x") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) for ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; end; theorem :: FOMODEL0:39 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_xboolean :::"boolean"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" )) ; registrationlet "Y" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) "Y") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) "x" "," "y" ($#k2_tarski :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) "x") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) "y") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "n" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"Nat":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) "n" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; registrationlet "m1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set "m1" ($#k2_xcmplx_0 :::"+"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k13_fomodel0 :::"null"::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v1_funct_1 :::"Function-like"::: ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k13_fomodel0 :::"null"::: ) "x") -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "p" be ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#m1_hidden :::"Relation":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k13_fomodel0 :::"null"::: ) "x") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "p" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k13_fomodel0 :::"null"::: ) "x") -> (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; registrationlet "p" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k1_card_1 :::"len"::: ) "p") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) for ($#m1_hidden :::"number"::: ) ; end; registrationlet "R" be ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "R" ($#k5_relat_1 :::"|"::: ) "X") -> "X" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "e" ($#k13_fomodel0 :::"null"::: ) "x") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "e" ($#k13_fomodel0 :::"null"::: ) "X") -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "X" "," (Set "(" "Y" ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); end; theorem :: FOMODEL0:40 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) )))) ; registrationlet "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k13_fomodel0 :::"null"::: ) "n") -> (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) "n" ")" )) ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); let "q" be (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> (Set "m" ($#k2_xcmplx_0 :::"+"::: ) "n") ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; theorem :: FOMODEL0:41 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) "is" (Set (Var "m")) ($#v3_card_1 :::"-element"::: ) ) & (Bool (Set (Var "q1")) "is" (Set (Var "m")) ($#v3_card_1 :::"-element"::: ) ) & (Bool "(" (Bool (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2")))) "or" (Bool (Set (Set (Var "p2")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q1")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" ))) ; theorem :: FOMODEL0:42 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "," (Set (Var "U1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set (Var "U1")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "U")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool (Set (Var "x")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "U1")) ($#k3_finseq_2 :::"*"::: ) )))) ; registrationlet "m" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set "m" ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "U")); cluster (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) "U" ")" ) ($#k3_funct_2 :::"."::: ) "u" ")" ) ($#k5_xboole_0 :::"\+\"::: ) "u") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set ($#k1_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k4_xboole_0 :::"\"::: ) "U") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:43 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "implies" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x1")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x2")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x2")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y2")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "implies" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x1")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x2")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x2")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x1")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y1")) ")" ))) ")" ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "U" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Relation":::); let "Q" be (Set (Const "U")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "P" ($#k3_relat_1 :::"*"::: ) "Q") -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"X" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); end; theorem :: FOMODEL0:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2"))) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p2")) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "p1")) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "p")) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) ) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k13_fomodel0 :::"null"::: ) "X") -> (Set "X" ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "R" ")" )) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "X", "Y" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v4_funct_1 :::"functional"::: ) ; end; registration cluster ($#v3_finseq_1 :::"FinSequence-membered"::: ) -> ($#v5_finset_1 :::"finite-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; func :::"SymbolsOf"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL0:def 24 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "X" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") "}" ); end; :: deftheorem defines :::"SymbolsOf"::: FOMODEL0:def 24 : (Bool "for" (Set (Var "X")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" ))); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v3_finseq_1 :::"FinSequence-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v4_funct_1 :::"functional"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) "X") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) "X") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FOMODEL0:45 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) ; registrationlet "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k16_complex1 :::"|."::: ) "z" ($#k16_complex1 :::".|"::: ) ) -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v2_xxreal_0 :::"positive"::: ) for ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; end; scheme :: FOMODEL0:sch 1 Sc1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "}" ) provided (Bool (Set F1 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) proof end; definitionlet "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; redefine func :::"SymbolsOf"::: "X" equals :: FOMODEL0:def 25 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") "}" ); end; :: deftheorem defines :::"SymbolsOf"::: FOMODEL0:def 25 : (Bool "for" (Set (Var "X")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" ))); theorem :: FOMODEL0:46 (Bool "for" (Set (Var "B")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "holds" (Bool (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "B")))))) ; theorem :: FOMODEL0:47 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "B")) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X")) ")" ); cluster (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) "F" ")" ) ($#k4_xboole_0 :::"\"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: FOMODEL0:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "m")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: FOMODEL0:50 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" (Set (Var "D")) ($#v3_fomodel0 :::"-prefix"::: ) ))) ; theorem :: FOMODEL0:51 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) ")" )) ; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) -> ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" "U" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ); end; registrationlet "e" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "e" ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: FOMODEL0:52 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set (Var "U1")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set (Var "U2")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "U1")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "U2")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "U1")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "U1")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "p")) "is" (Set (Set (Var "U1")) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "implies" (Bool (Set (Var "p")) "is" (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ) ")" ")" )))) ; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "U" ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "x") -> "U" ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func "x" :::"null"::: -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL0:def 26 "x"; end; :: deftheorem defines :::"null"::: FOMODEL0:def 26 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k22_fomodel0 :::"null"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))); registrationlet "Y" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) -> ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) "Y" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; registrationlet "X" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "U" ($#k13_finseq_1 :::"*"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "U" ($#k13_finseq_1 :::"*"::: ) ) -> ($#v2_setfam_1 :::"with_non-empty_element"::: ) ; end; registrationlet "X" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; theorem :: FOMODEL0:53 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "U1")) ($#r1_tarski :::"c="::: ) (Set (Var "U2"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "U1")) ($#k3_finseq_2 :::"*"::: ) )) & (Bool (Set (Var "p")) "is" (Set (Var "Y")) ($#v5_relat_1 :::"-valued"::: ) ) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "U1")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "U2")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))))) ; theorem :: FOMODEL0:54 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) "is" (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "U")) ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set (Var "X")) ($#v5_relat_1 :::"-valued"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_hidden :::"Nat":::); cluster (Set (Set "(" "m" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL0:55 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k3_finseq_2 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_finseq_2 :::"*"::: ) ")" )))) ; theorem :: FOMODEL0:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Q")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "Q")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k4_xboole_0 :::"\"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k13_fomodel0 :::"null"::: ) "X") -> (Set "X" ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "R" ")" )) ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Relation":::); end; theorem :: FOMODEL0:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); identify ; identify ; end; theorem :: FOMODEL0:58 (Bool "for" (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")))))) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X")))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func "X" :::"-freeCountableSet"::: -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL0:def 27 (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) "X" ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) "X" ")" )) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ); end; :: deftheorem defines :::"-freeCountableSet"::: FOMODEL0:def 27 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k23_fomodel0 :::"-freeCountableSet"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" )) ($#k6_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ))); theorem :: FOMODEL0:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "X")) ($#k23_fomodel0 :::"-freeCountableSet"::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "X")) ($#k23_fomodel0 :::"-freeCountableSet"::: ) ) "is" ($#v1_finset_1 :::"infinite"::: ) ) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k23_fomodel0 :::"-freeCountableSet"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "X" ($#k23_fomodel0 :::"-freeCountableSet"::: ) ")" ) ($#k3_xboole_0 :::"/\"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k23_fomodel0 :::"-freeCountableSet"::: ) ) -> ($#v4_card_3 :::"countable"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k4_numbers :::"INT"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); cluster (Set (Set "(" (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) "x" ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) "p" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k5_xboole_0 :::"\+\"::: ) "x") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "m0" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"number"::: ) ; let "p" be (Set (Const "m")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k13_fomodel0 :::"null"::: ) "m0") -> (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) "m0" ")" )) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for(Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) "m0" ")" )) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "q1", "q2" be (Set (Const "U")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set "(" (Set "(" "U" ($#k8_fomodel0 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "q1" "," "q2" ($#k10_finseq_1 :::"*>"::: ) ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" "q1" ($#k7_finseq_1 :::"^"::: ) "q2" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end;