:: MARGREL1 semantic presentation begin definitionlet "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "B")); :: original: :::"-->"::: redefine func "A" :::"-->"::: "b" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; definitionlet "IT" be ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine attr "IT" is :::"with_common_domain"::: means :: MARGREL1:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"with_common_domain"::: MARGREL1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_card_3 :::"with_common_domain"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))))) ")" )); registration cluster ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#v2_card_3 :::"with_common_domain"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode relation is ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#v2_card_3 :::"with_common_domain"::: ) ($#m1_hidden :::"set"::: ) ; end; theorem :: MARGREL1:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_hidden :::"relation":::)))) ; theorem :: MARGREL1:2 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"relation":::))) ; scheme :: MARGREL1:sch 1 relexist{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"FinSequence":::)] } : (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"relation":::) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "a"))]) ")" ) ")" ))) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P1[(Set (Var "b"))])) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))))) proof end; definitionlet "p", "r" be ($#m1_hidden :::"relation":::); redefine pred "p" :::"="::: "r" means :: MARGREL1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "p") "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "r") ")" )); end; :: deftheorem defines :::"="::: MARGREL1:def 2 : (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"relation":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) ")" )) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_card_3 :::"with_common_domain"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: MARGREL1:3 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "p")))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; definitionlet "p" be ($#m1_hidden :::"relation":::); assume (Bool (Set (Const "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"the_arity_of"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MARGREL1:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "p")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"the_arity_of"::: MARGREL1:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"relation":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_margrel1 :::"the_arity_of"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))))) ")" ))); definitionlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"relation_length"::: "of" "k" -> ($#m1_hidden :::"relation":::) means :: MARGREL1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "k")); end; :: deftheorem defines :::"relation_length"::: MARGREL1:def 4 : (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_margrel1 :::"relation_length"::: ) "of" (Set (Var "k"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"relation"::: "of" "X" -> ($#m1_hidden :::"relation":::) means :: MARGREL1:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) "X")); end; :: deftheorem defines :::"relation"::: MARGREL1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_margrel1 :::"relation"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ")" ))); theorem :: MARGREL1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m2_margrel1 :::"relation"::: ) "of" (Set (Var "X")))) ; theorem :: MARGREL1:5 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_margrel1 :::"relation_length"::: ) "of" (Set (Var "k")))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"relation"::: "of" "X" "," "k" -> ($#m1_hidden :::"relation":::) means :: MARGREL1:def 6 (Bool "(" (Bool it "is" ($#m2_margrel1 :::"relation"::: ) "of" "X") & (Bool it "is" ($#m1_margrel1 :::"relation_length"::: ) "of" "k") ")" ); end; :: deftheorem defines :::"relation"::: MARGREL1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_margrel1 :::"relation"::: ) "of" (Set (Var "X")) "," (Set (Var "k"))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_margrel1 :::"relation"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "b3")) "is" ($#m1_margrel1 :::"relation_length"::: ) "of" (Set (Var "k"))) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"relations_on"::: "D" -> ($#m1_hidden :::"set"::: ) means :: MARGREL1:def 7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set "D" ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b")))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"relations_on"::: MARGREL1:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b")))) ")" ) ")" ) ")" )) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_margrel1 :::"relations_on"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode relation of "D" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) "D"); end; theorem :: MARGREL1:6 (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"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))))))) ; theorem :: MARGREL1:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D")))))) ; theorem :: MARGREL1:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p", "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Const "D"))); :: original: :::"="::: redefine pred "p" :::"="::: "r" means :: MARGREL1:def 8 (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "p") "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "r") ")" )); end; :: deftheorem defines :::"="::: MARGREL1:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_margrel1 :::"="::: ) (Set (Var "r"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) ")" )) ")" ))); scheme :: MARGREL1:sch 2 relDexist{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" )] } : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set F1 "(" ")" )) "st" (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) "iff" (Bool P1[(Set (Var "a"))]) ")" ))) provided (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P1[(Set (Var "b"))])) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))))) proof end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"empty_rel"::: "D" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) "D") means :: MARGREL1:def 9 (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) it))); end; :: deftheorem defines :::"empty_rel"::: MARGREL1:def 9 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_margrel1 :::"empty_rel"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))))) ")" ))); theorem :: MARGREL1:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_margrel1 :::"empty_rel"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Const "D"))); assume (Bool (Set (Const "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_margrel1 :::"empty_rel"::: ) (Set (Const "D")))) ; func :::"the_arity_of"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MARGREL1:def 10 (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "p")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"the_arity_of"::: MARGREL1:def 10 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_margrel1 :::"empty_rel"::: ) (Set (Var "D"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_margrel1 :::"the_arity_of"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))))) ")" )))); scheme :: MARGREL1:sch 3 relDexist2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), P1[ ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" )] } : (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_margrel1 :::"relations_on"::: ) (Set F1 "(" ")" )) "st" (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) "iff" (Bool P1[(Set (Var "a"))]) ")" ))) proof end; definitionfunc :::"BOOLEAN"::: -> ($#m1_hidden :::"set"::: ) equals :: MARGREL1:def 11 (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ); end; :: deftheorem defines :::"BOOLEAN"::: MARGREL1:def 11 : (Bool (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )); registration cluster (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definition:: original: :::"FALSE"::: redefine func :::"FALSE"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"TRUE"::: redefine func :::"TRUE"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; redefine attr "x" is :::"boolean"::: means :: MARGREL1:def 12 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )); end; :: deftheorem defines :::"boolean"::: MARGREL1:def 12 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_xboolean :::"boolean"::: ) ) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ")" )); registration cluster -> ($#v1_xboolean :::"boolean"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "v" be ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) ; redefine func :::"'not'"::: "v" equals :: MARGREL1:def 13 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool "v" ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); let "w" be ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) ; redefine func "v" :::"'&'"::: "w" equals :: MARGREL1:def 14 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool "(" (Bool "v" ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool "w" ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); end; :: deftheorem defines :::"'not'"::: MARGREL1:def 13 : (Bool "for" (Set (Var "v")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )))) "implies" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); :: deftheorem defines :::"'&'"::: MARGREL1:def 14 : (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "or" "not" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) "implies" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); definitionlet "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'not'"::: redefine func :::"'not'"::: "v" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'&'"::: redefine func "v" :::"'&'"::: "w" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: MARGREL1:10 canceled; theorem :: MARGREL1:11 (Bool "for" (Set (Var "v")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ")" )) ; theorem :: MARGREL1:12 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) ")" & "(" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & (Bool "(" "not" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "or" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ) & "(" (Bool (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "or" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" )) "implies" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )) ; theorem :: MARGREL1:13 (Bool "for" (Set (Var "v")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#k4_xboolean :::"'&'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) ; theorem :: MARGREL1:14 (Bool "for" (Set (Var "v")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k4_xboolean :::"'&'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ; theorem :: MARGREL1:15 (Bool "for" (Set (Var "v")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) ; theorem :: MARGREL1:16 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "w")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "w")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set (Var "u"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"ALL"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: MARGREL1:def 15 (Set ($#k8_margrel1 :::"TRUE"::: ) ) if (Bool (Bool "not" (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) "X")) otherwise (Set ($#k7_margrel1 :::"FALSE"::: ) ); end; :: deftheorem defines :::"ALL"::: MARGREL1:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "implies" (Bool (Set ($#k11_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "implies" (Bool (Set ($#k11_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_margrel1 :::"ALL"::: ) "X") -> ($#v1_xboolean :::"boolean"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"ALL"::: redefine func :::"ALL"::: "X" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: MARGREL1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "implies" (Bool (Set ($#k12_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool (Set ($#k12_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool "not" (Bool (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "implies" (Bool (Set ($#k12_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" & "(" (Bool (Bool (Set ($#k12_margrel1 :::"ALL"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ")" )) ; begin definitionlet "f" be ($#m1_hidden :::"Relation":::); attr "f" is :::"boolean-valued"::: means :: MARGREL1:def 16 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )); end; :: deftheorem defines :::"boolean-valued"::: MARGREL1:def 16 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_margrel1 :::"boolean-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_margrel1 :::"boolean-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_xboolean :::"boolean"::: ) ; end; definitionlet "p" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); func :::"'not'"::: "p" -> ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) means :: MARGREL1:def 17 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (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 "b2"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1")))) & (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 "b1"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; let "q" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); func "p" :::"'&'"::: "q" -> ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) means :: MARGREL1:def 18 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "p" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "q" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (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 "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (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 "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; idempotence (Bool "for" (Set (Var "p")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (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 "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; end; :: deftheorem defines :::"'not'"::: MARGREL1:def 17 : (Bool "for" (Set (Var "p")) "," (Set (Var "b2")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_margrel1 :::"'not'"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (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 "p"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); :: deftheorem defines :::"'&'"::: MARGREL1:def 18 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b3")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k14_margrel1 :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (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 "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v1_margrel1 :::"boolean-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'not'"::: redefine func :::"'not'"::: "p" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: MARGREL1:def 19 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); let "q" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'&'"::: redefine func "p" :::"'&'"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: MARGREL1:def 20 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" "q" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"'not'"::: MARGREL1:def 19 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_margrel1 :::"'not'"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); :: deftheorem defines :::"'&'"::: MARGREL1:def 20 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k16_margrel1 :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); begin definitionlet "IT" be ($#m1_hidden :::"Relation":::); attr "IT" is :::"homogeneous"::: means :: MARGREL1:def 21 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "IT") "is" ($#v2_card_3 :::"with_common_domain"::: ) ); end; :: deftheorem defines :::"homogeneous"::: MARGREL1:def 21 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_margrel1 :::"homogeneous"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))) "is" ($#v2_card_3 :::"with_common_domain"::: ) ) ")" )); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Const "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Const "A")); attr "IT" is :::"quasi_total"::: means :: MARGREL1:def 22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "A" "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))); end; :: deftheorem defines :::"quasi_total"::: MARGREL1:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) ")" ))); registrationlet "f" be ($#m1_hidden :::"Relation":::); let "X" be ($#v2_card_3 :::"with_common_domain"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v2_margrel1 :::"homogeneous"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Const "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Const "A")); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "f") -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "A" ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "A" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "R") -> ($#v2_card_3 :::"with_common_domain"::: ) ; end; theorem :: MARGREL1:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "A")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "a"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A"))))) ; theorem :: MARGREL1:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "A")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A")) ")" )))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; mode PFuncFinSequence of "A" is ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" ")" ); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Const "A")); attr "IT" is :::"homogeneous"::: means :: MARGREL1:def 23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT")) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "h")) "is" ($#v2_margrel1 :::"homogeneous"::: ) ))); end; :: deftheorem defines :::"homogeneous"::: MARGREL1:def 23 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_margrel1 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "h")) "is" ($#v2_margrel1 :::"homogeneous"::: ) ))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Const "A")); attr "IT" is :::"quasi_total"::: means :: MARGREL1:def 24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "A" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "A" "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT")) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "h")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ))); end; :: deftheorem defines :::"quasi_total"::: MARGREL1:def 24 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_margrel1 :::"quasi_total"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "h")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" (Set (Const "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Const "A")) ")" ); :: original: :::"<*"::: redefine func :::"<*":::"x":::"*>"::: -> ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" "A"; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#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"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() 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; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_margrel1 :::"homogeneous"::: ) ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set (Const "A")); let "i" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "i") -> ($#v2_margrel1 :::"homogeneous"::: ) ; end; theorem :: MARGREL1:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "A")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set ($#k17_margrel1 :::"<*"::: ) (Set (Var "x")) ($#k17_margrel1 :::"*>"::: ) ) "is" ($#v4_margrel1 :::"homogeneous"::: ) ) & (Bool (Set ($#k17_margrel1 :::"<*"::: ) (Set (Var "x")) ($#k17_margrel1 :::"*>"::: ) ) "is" ($#v5_margrel1 :::"quasi_total"::: ) ) & (Bool (Set ($#k17_margrel1 :::"<*"::: ) (Set (Var "x")) ($#k17_margrel1 :::"*>"::: ) ) "is" ($#v2_relat_1 :::"non-empty"::: ) ) ")" )))) ; definitionlet "f" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::); func :::"arity"::: "f" -> ($#m1_hidden :::"Nat":::) means :: MARGREL1:def 25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))))) if (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"arity"::: MARGREL1:def 25 : (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_margrel1 :::"arity"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))))) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_margrel1 :::"arity"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); definitionlet "f" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); :: original: :::"arity"::: redefine func :::"arity"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; begin theorem :: MARGREL1:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D1"))))))) ; theorem :: MARGREL1:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "D")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "h")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"PFuncsDomHQN"::: "of" "D" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MARGREL1:def 26 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "D")); end; :: deftheorem defines :::"PFuncsDomHQN"::: MARGREL1:def 26 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m4_margrel1 :::"PFuncsDomHQN"::: ) "of" (Set (Var "D"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "b2")) "holds" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "D")))) ")" )); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m4_margrel1 :::"PFuncsDomHQN"::: ) "of" (Set (Const "D")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "P" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "D"; end;