:: PUA2MSS1 semantic presentation begin registrationlet "X" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_relat_1 :::"non-empty"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "X"; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" ")" ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v4_margrel1 :::"homogeneous"::: ) ($#v5_margrel1 :::"quasi_total"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" ")" ); end; registration cluster ($#v4_unialg_1 :::"non-empty"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_unialg_1 :::"UAStr"::: ) ; end; theorem :: PUA2MSS1:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (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 (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ; theorem :: PUA2MSS1:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Const "A")); :: original: :::"proj2"::: redefine func :::"rng"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" ")" ")" ); end; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "S" -> ($#m1_subset_1 :::"PartFunc":::) "of" "A" "," "B"; end; definitionlet "A" be ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; mode OperSymbol of "A" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A")); mode operation of "A" is ($#m1_pua2mss1 :::"Element"::: ) "of" (Set ($#k1_pua2mss1 :::"rng"::: ) (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A")); end; definitionlet "A" be ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "o" be ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Const "A")); func :::"Den"::: "(" "o" "," "A" ")" -> ($#m1_pua2mss1 :::"operation":::) "of" "A" equals :: PUA2MSS1:def 1 (Set (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) "o"); end; :: deftheorem defines :::"Den"::: PUA2MSS1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))))); begin theorem :: PUA2MSS1:3 canceled; theorem :: PUA2MSS1:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set (Var "Y")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Y")) "st" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "q"))))))) ; theorem :: PUA2MSS1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "q")))) "iff" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) ($#r2_relset_1 :::"="::: ) (Set (Var "q"))) ")" )))))) ; theorem :: PUA2MSS1:6 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p")))) ")" )))) ; theorem :: PUA2MSS1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p")))))))) ; theorem :: PUA2MSS1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Q")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "{" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k8_mcart_1 :::":]"::: ) ) where p "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "P")), q "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Q")) : (Bool verum) "}" "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: PUA2MSS1:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "{" (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" ) where p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "P")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool verum) "}" "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) )))) ; theorem :: PUA2MSS1:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "{" (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" ) where p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "P"))) : (Bool verum) "}" "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X"))))))) ; theorem :: PUA2MSS1:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "{" (Set "(" (Set (Var "a")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "Y")) ")" ) where a "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "P")) : (Bool (Set (Var "a")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y"))) "}" "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")))))) ; theorem :: PUA2MSS1:12 (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "holds" (Bool "{" (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "a")) ")" ) where a "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "P")) : (Bool verum) "}" "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "f"))))) ; theorem :: PUA2MSS1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "st" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "q")) ($#k1_tarski :::"}"::: ) ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"IndexedPartition"::: "of" "X" -> ($#m1_hidden :::"Function":::) means :: PUA2MSS1:def 2 (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) it) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X") & (Bool it "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ); end; :: deftheorem defines :::"IndexedPartition"::: PUA2MSS1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "b2"))) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "b2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Const "X")); :: original: :::"proj2"::: redefine func :::"rng"::: "P" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_relat_1 :::"non-empty"::: ) ($#v2_funct_1 :::"one-to-one"::: ) for ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" "X"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); :: original: :::"id"::: redefine func :::"id"::: "P" -> ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Const "X")); let "x" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set (Const "X"))) ; func "P" :::"-index_of"::: "x" -> ($#m1_hidden :::"set"::: ) means :: PUA2MSS1:def 3 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "P")) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set "P" ($#k1_funct_1 :::"."::: ) it)) ")" ); end; :: deftheorem defines :::"-index_of"::: PUA2MSS1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k5_pua2mss1 :::"-index_of"::: ) (Set (Var "x")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "b4")))) ")" ) ")" ))))); theorem :: PUA2MSS1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" )) "holds" (Bool (Set (Var "P")) "is" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "X"))))) ; theorem :: PUA2MSS1:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "P")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "Y")))))) ; begin scheme :: PUA2MSS1:sch 1 IndRelationEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4() -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "R")) "," (Set (Var "i")) ")" ))) ")" ) ")" ))) proof end; scheme :: PUA2MSS1:sch 2 RelationUniq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) "iff" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )) ")" )) "holds" (Bool (Set (Var "R1")) ($#r2_relset_1 :::"="::: ) (Set (Var "R2")))) proof end; scheme :: PUA2MSS1:sch 3 IndRelationUniq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4() -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) } : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "R")) "," (Set (Var "i")) ")" ))) ")" ) ")" )) & (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "R2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set F3 "(" ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "R")) "," (Set (Var "i")) ")" ))) ")" ) ")" ))) "holds" (Bool (Set (Var "R1")) ($#r2_relset_1 :::"="::: ) (Set (Var "R2")))) proof end; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; func :::"DomRel"::: "A" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" "A" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ))) ")" )); end; :: deftheorem defines :::"DomRel"::: PUA2MSS1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_pua2mss1 :::"DomRel"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ))) ")" )) ")" ))); registrationlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; cluster (Set ($#k6_pua2mss1 :::"DomRel"::: ) "A") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A"))); func "R" :::"|^"::: "A" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" "A" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"|^"::: PUA2MSS1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ) ")" ) ")" )) ")" ))); definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A"))); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "R" :::"|^"::: "(" "A" "," "i" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 6 (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) "i")) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "R") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) "A"))) ")" ) ")" )); end; :: deftheorem defines :::"|^"::: PUA2MSS1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))))) ")" ) ")" )) ")" ))))); theorem :: PUA2MSS1:16 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A")))) ")" ))) ; theorem :: PUA2MSS1:17 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))))))) ; theorem :: PUA2MSS1:18 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "j")) ")" ))))) ; theorem :: PUA2MSS1:19 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_pua2mss1 :::"DomRel"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))) "is" ($#v3_relat_2 :::"symmetric"::: ) ) & (Bool (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))) "is" ($#v8_relat_2 :::"transitive"::: ) ) ")" ))) ; theorem :: PUA2MSS1:20 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool (Set (Set (Var "R")) ($#k7_pua2mss1 :::"|^"::: ) (Set (Var "A"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "R"))))) ; theorem :: PUA2MSS1:21 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_pua2mss1 :::"DomRel"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) "is" ($#v3_relat_2 :::"symmetric"::: ) ) & (Bool (Set (Set (Var "R")) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) "is" ($#v8_relat_2 :::"transitive"::: ) ) ")" )))) ; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; func :::"LimDomRel"::: "A" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k6_pua2mss1 :::"DomRel"::: ) "A" ")" ) ($#k8_pua2mss1 :::"|^"::: ) "(" "A" "," (Set (Var "i")) ")" ))) ")" )); end; :: deftheorem defines :::"LimDomRel"::: PUA2MSS1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k6_pua2mss1 :::"DomRel"::: ) (Set (Var "A")) ")" ) ($#k8_pua2mss1 :::"|^"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ))) ")" )) ")" ))); theorem :: PUA2MSS1:22 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) "holds" (Bool (Set ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A"))) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_pua2mss1 :::"DomRel"::: ) (Set (Var "A"))))) ; registrationlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; cluster (Set ($#k9_pua2mss1 :::"LimDomRel"::: ) "A") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Const "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Const "X")); let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); pred "f" :::"is_partitable_wrt"::: "P" means :: PUA2MSS1:def 8 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "P" (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "P" "st" (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"is_partitable_wrt"::: PUA2MSS1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_pua2mss1 :::"is_partitable_wrt"::: ) (Set (Var "P"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "a"))))) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Const "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Const "X")); let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); pred "f" :::"is_exactly_partitable_wrt"::: "P" means :: PUA2MSS1:def 9 (Bool "(" (Bool "f" ($#r1_pua2mss1 :::"is_partitable_wrt"::: ) "P") & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "P" "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" ) ")" ); end; :: deftheorem defines :::"is_exactly_partitable_wrt"::: PUA2MSS1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_pua2mss1 :::"is_exactly_partitable_wrt"::: ) (Set (Var "P"))) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r1_pua2mss1 :::"is_partitable_wrt"::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ) ")" )))); theorem :: PUA2MSS1:23 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "f")) ($#r2_pua2mss1 :::"is_exactly_partitable_wrt"::: ) (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))))))) ; scheme :: PUA2MSS1:sch 4 FiniteTransitivity{ F1() -> ($#m1_hidden :::"FinSequence":::), F2() -> ($#m1_hidden :::"FinSequence":::), P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool P1[(Set F1 "(" ")" )]) and (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set F1 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "z1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))]) & (Bool P2[(Set (Var "z1")) "," (Set (Var "z2"))])) "holds" (Bool P1[(Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "z2")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))]))) and (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F1 "(" ")" )))) "holds" (Bool P2[(Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))])) proof end; theorem :: PUA2MSS1:24 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "f")) ($#r2_pua2mss1 :::"is_exactly_partitable_wrt"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A")) ")" ))))) ; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; mode :::"a_partition"::: "of" "A" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 10 (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" "A" "holds" (Bool (Set (Var "f")) ($#r2_pua2mss1 :::"is_exactly_partitable_wrt"::: ) it)); end; :: deftheorem defines :::"a_partition"::: PUA2MSS1:def 10 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A"))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_pua2mss1 :::"operation":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "f")) ($#r2_pua2mss1 :::"is_exactly_partitable_wrt"::: ) (Set (Var "b2")))) ")" ))); definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; mode :::"IndexedPartition"::: "of" "A" -> ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: PUA2MSS1:def 11 (Bool (Set ($#k3_pua2mss1 :::"rng"::: ) it) "is" ($#m3_pua2mss1 :::"a_partition"::: ) "of" "A"); end; :: deftheorem defines :::"IndexedPartition"::: PUA2MSS1:def 11 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m4_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set ($#k3_pua2mss1 :::"rng"::: ) (Set (Var "b2"))) "is" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A"))) ")" ))); definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "P" be ($#m4_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Const "A")); :: original: :::"proj2"::: redefine func :::"rng"::: "P" -> ($#m3_pua2mss1 :::"a_partition"::: ) "of" "A"; end; theorem :: PUA2MSS1:25 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A")) ")" )) "is" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A")))) ; theorem :: PUA2MSS1:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set "(" (Set (Var "q1")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p")))) & (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "P")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "q1")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))))))))) ; theorem :: PUA2MSS1:27 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "P")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A")) ")" ))))) ; begin definitionlet "S1", "S2" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "f", "g" be ($#m1_hidden :::"Function":::); pred "f" "," "g" :::"form_morphism_between"::: "S1" "," "S2" means :: PUA2MSS1:def 12 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1")) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "g") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S1")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S2")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "g") ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S2")) & (Bool (Set "f" ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S2") ($#k3_relat_1 :::"*"::: ) "g")) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S1")) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S1") ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set "f" ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S2") ($#k1_funct_1 :::"."::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"form_morphism_between"::: PUA2MSS1:def 12 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2")))) & (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1")))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S2"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S2"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" )))) ")" ) ")" ) ")" ))); theorem :: PUA2MSS1:28 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S")) "," (Set (Var "S")))) ; theorem :: PUA2MSS1:29 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "," (Set (Var "g1")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) & (Bool (Set (Var "f2")) "," (Set (Var "g2")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S2")) "," (Set (Var "S3")))) "holds" (Bool (Set (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1"))) "," (Set (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1"))) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S3"))))) ; definitionlet "S1", "S2" be ($#l1_msualg_1 :::"ManySortedSign"::: ) ; pred "S1" :::"is_rougher_than"::: "S2" means :: PUA2MSS1:def 13 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) "S2" "," "S1") & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S1")) ")" )); end; :: deftheorem defines :::"is_rougher_than"::: PUA2MSS1:def 13 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S1")) ($#r4_pua2mss1 :::"is_rougher_than"::: ) (Set (Var "S2"))) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S2")) "," (Set (Var "S1"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1")))) ")" )) ")" )); definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; :: original: :::"is_rougher_than"::: redefine pred "S1" :::"is_rougher_than"::: "S2"; reflexivity (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool ((Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: PUA2MSS1:30 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r4_pua2mss1 :::"is_rougher_than"::: ) (Set (Var "S2"))) & (Bool (Set (Var "S2")) ($#r4_pua2mss1 :::"is_rougher_than"::: ) (Set (Var "S3")))) "holds" (Bool (Set (Var "S1")) ($#r4_pua2mss1 :::"is_rougher_than"::: ) (Set (Var "S3")))) ; begin definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "P" be ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Const "A")); func :::"MSSign"::: "(" "A" "," "P" ")" -> ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) means :: PUA2MSS1:def 14 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "P") & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ) where o "is" ($#m2_subset_1 :::"OperSymbol":::) "of" "A", p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "P" ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r2_subset_1 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," "A" ")" ")" ))) "}" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" "A" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "P" ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r2_subset_1 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," "A" ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," "A" ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"MSSign"::: PUA2MSS1:def 14 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_pua2mss1 :::"MSSign"::: ) "(" (Set (Var "A")) "," (Set (Var "P")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ) where o "is" ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Var "A")), p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "P")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r2_subset_1 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ))) "}" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "P")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "p"))) ($#r2_subset_1 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) ))) ")" )) ")" ) ")" ) ")" )))); registrationlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "P" be ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Const "A")); cluster (Set ($#k11_pua2mss1 :::"MSSign"::: ) "(" "A" "," "P" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "P" be ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" ($#k11_pua2mss1 :::"MSSign"::: ) "(" (Set (Const "A")) "," (Set (Const "P")) ")" ")" ); :: original: :::"`1"::: redefine func "o" :::"`1"::: -> ($#m2_subset_1 :::"OperSymbol":::) "of" "A"; :: original: :::"`2"::: redefine func "o" :::"`2"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "P" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "G" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "P" be ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "S"))); pred "A" :::"can_be_characterized_by"::: "S" "," "G" "," "P" means :: PUA2MSS1:def 15 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "G") "is" ($#m4_pua2mss1 :::"IndexedPartition"::: ) "of" "A") & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "P") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" "A"))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" "A" "holds" (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "G") ($#k5_relat_1 :::"|"::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" )) "is" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," "A" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"can_be_characterized_by"::: PUA2MSS1:def 15 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r6_pua2mss1 :::"can_be_characterized_by"::: ) (Set (Var "S")) "," (Set (Var "G")) "," (Set (Var "P"))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "G"))) "is" ($#m4_pua2mss1 :::"IndexedPartition"::: ) "of" (Set (Var "A"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "the" ($#u1_unialg_1 :::"charact"::: ) "of" (Set (Var "A"))))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "G"))) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" )) "is" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" )) ")" ) ")" ) ")" ))))); definitionlet "A" be ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; pred "A" :::"can_be_characterized_by"::: "S" means :: PUA2MSS1:def 16 (Bool "ex" (Set (Var "G")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"(Bool "ex" (Set (Var "P")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "st" (Bool "A" ($#r6_pua2mss1 :::"can_be_characterized_by"::: ) "S" "," (Set (Var "G")) "," (Set (Var "P"))))); end; :: deftheorem defines :::"can_be_characterized_by"::: PUA2MSS1:def 16 : (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r7_pua2mss1 :::"can_be_characterized_by"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "G")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S"))(Bool "ex" (Set (Var "P")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "st" (Bool (Set (Var "A")) ($#r6_pua2mss1 :::"can_be_characterized_by"::: ) (Set (Var "S")) "," (Set (Var "G")) "," (Set (Var "P"))))) ")" ))); theorem :: PUA2MSS1:31 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "A")) ($#r7_pua2mss1 :::"can_be_characterized_by"::: ) (Set ($#k11_pua2mss1 :::"MSSign"::: ) "(" (Set (Var "A")) "," (Set (Var "P")) ")" )))) ; theorem :: PUA2MSS1:32 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "Q")) "being" ($#m2_pua2mss1 :::"IndexedPartition"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "st" (Bool (Bool (Set (Var "A")) ($#r6_pua2mss1 :::"can_be_characterized_by"::: ) (Set (Var "S")) "," (Set (Var "G")) "," (Set (Var "Q")))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"OperSymbol":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "G")))) "st" (Bool (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_pua2mss1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "G"))) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" )))))))) ; theorem :: PUA2MSS1:33 (Bool "for" (Set (Var "A")) "being" ($#v2_unialg_1 :::"partial"::: ) ($#v4_unialg_1 :::"non-empty"::: ) ($#l1_unialg_1 :::"UAStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m3_pua2mss1 :::"a_partition"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_pua2mss1 :::"LimDomRel"::: ) (Set (Var "A")) ")" )))) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r7_pua2mss1 :::"can_be_characterized_by"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k11_pua2mss1 :::"MSSign"::: ) "(" (Set (Var "A")) "," (Set (Var "P")) ")" ) ($#r5_pua2mss1 :::"is_rougher_than"::: ) (Set (Var "S")))))) ;