:: MMLQUERY semantic presentation begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode List of "X" is ($#m1_subset_1 :::"Subset":::) "of" "X"; mode Operation of "X" is ($#m1_subset_1 :::"Relation":::) "of" "X"; end; definitionlet "x", "y", "R" be ($#m1_hidden :::"set"::: ) ; pred "x" "," "y" :::"in"::: "R" means :: MMLQUERY:def 1 (Bool (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R"); end; :: deftheorem defines :::"in"::: MMLQUERY:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "R")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_mmlquery :::"in"::: ) (Set (Var "R"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )); notationlet "x", "y", "R" be ($#m1_hidden :::"set"::: ) ; antonym "x" "," "y" :::"nin"::: "R" for "x" "," "y" :::"in"::: "R"; end; theorem :: MMLQUERY:1 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R1")) ($#r1_tarski :::"c="::: ) (Set (Var "R2"))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R1")) "," (Set (Var "z")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R2")) "," (Set (Var "z")) ")" ))) ")" )) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); synonym "x" :::"."::: "O" for :::"Im"::: "(" "X" "," "O" ")" ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"."::: redefine func "x" :::"."::: "O" -> ($#m1_subset_1 :::"List":::) "of" "X"; end; theorem :: MMLQUERY:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_mmlquery :::"in"::: ) (Set (Var "O"))) "iff" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")))) ")" ))))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "L" be ($#m1_subset_1 :::"List":::) "of" (Set (Const "X")); synonym "L" :::"|"::: "O" for "X" :::".:"::: "O"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "L" be ($#m1_subset_1 :::"List":::) "of" (Set (Const "X")); :: original: :::"|"::: redefine func "L" :::"|"::: "O" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 2 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") "}" ); func "L" :::"\&"::: "O" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 3 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") "}" ); func "L" :::"WHERE"::: "O" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 4 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_mmlquery :::"in"::: ) "O") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" )) "}" ; let "O2" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); func "L" :::"WHEREeq"::: "(" "O" "," "O2" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 5 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREle"::: "(" "O" "," "O2" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 6 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREge"::: "(" "O" "," "O2" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 7 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHERElt"::: "(" "O" "," "O2" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 8 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREgt"::: "(" "O" "," "O2" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 9 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; end; :: deftheorem defines :::"|"::: MMLQUERY:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))))); :: deftheorem defines :::"\&"::: MMLQUERY:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))))); :: deftheorem defines :::"WHERE"::: MMLQUERY:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_mmlquery :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" )) "}" )))); :: deftheorem defines :::"WHEREeq"::: MMLQUERY:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k5_mmlquery :::"WHEREeq"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREle"::: MMLQUERY:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k6_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREge"::: MMLQUERY:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k7_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHERElt"::: MMLQUERY:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k8_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREgt"::: MMLQUERY:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k9_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#m1_subset_1 :::"List":::) "of" (Set (Const "X")); let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); func "L" :::"WHEREeq"::: "(" "O" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 10 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r1_hidden :::"="::: ) "n") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREle"::: "(" "O" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 11 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r1_ordinal1 :::"c="::: ) "n") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREge"::: "(" "O" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 12 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool "n" ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHERElt"::: "(" "O" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 13 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" )) ($#r2_hidden :::"in"::: ) "n") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; func "L" :::"WHEREgt"::: "(" "O" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 14 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool "n" ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "L") ")" ) "}" ; end; :: deftheorem defines :::"WHEREeq"::: MMLQUERY:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k10_mmlquery :::"WHEREeq"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREle"::: MMLQUERY:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k11_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREge"::: MMLQUERY:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "n")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHERElt"::: MMLQUERY:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k13_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); :: deftheorem defines :::"WHEREgt"::: MMLQUERY:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" ) "}" ))))); theorem :: MMLQUERY:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))))) ; theorem :: MMLQUERY:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))) ($#r1_tarski :::"c="::: ) (Set (Var "L")))))) ; theorem :: MMLQUERY:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O"))))) "holds" (Bool (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Var "L")))))) ; theorem :: MMLQUERY:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O")))))))) ; theorem :: MMLQUERY:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))))))) ; theorem :: MMLQUERY:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O")))))))) ; theorem :: MMLQUERY:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))))))) ; theorem :: MMLQUERY:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k10_mmlquery :::"WHEREeq"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O")))))))) ; theorem :: MMLQUERY:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" )))))) ; theorem :: MMLQUERY:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k11_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k13_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: MMLQUERY:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O1")) "," (Set (Var "m")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k12_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O2")) "," (Set (Var "n")) ")" )))))) ; theorem :: MMLQUERY:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O1")) "," (Set (Var "m")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k14_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O2")) "," (Set (Var "n")) ")" )))))) ; theorem :: MMLQUERY:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k11_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O2")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k11_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O1")) "," (Set (Var "m")) ")" )))))) ; theorem :: MMLQUERY:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k13_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O2")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k13_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O1")) "," (Set (Var "m")) ")" )))))) ; theorem :: MMLQUERY:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O3")))) "holds" (Bool (Set (Set (Var "L1")) ($#k7_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k7_mmlquery :::"WHEREge"::: ) "(" (Set (Var "O3")) "," (Set (Var "O1")) ")" ))))) ; theorem :: MMLQUERY:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O3")))) "holds" (Bool (Set (Set (Var "L1")) ($#k9_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k9_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O3")) "," (Set (Var "O1")) ")" ))))) ; theorem :: MMLQUERY:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O3")))) "holds" (Bool (Set (Set (Var "L1")) ($#k6_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O3")) "," (Set (Var "O1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k6_mmlquery :::"WHEREle"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ))))) ; theorem :: MMLQUERY:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O")) "," (Set (Var "O3")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O3")))) "holds" (Bool (Set (Set (Var "L1")) ($#k8_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O3")) "," (Set (Var "O1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k8_mmlquery :::"WHERElt"::: ) "(" (Set (Var "O")) "," (Set (Var "O2")) ")" ))))) ; theorem :: MMLQUERY:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "," (Set (Var "O1")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k9_mmlquery :::"WHEREgt"::: ) "(" (Set (Var "O")) "," (Set (Var "O1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))))))) ; theorem :: MMLQUERY:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O2"))))))) ; theorem :: MMLQUERY:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O")))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) ")" )) ")" ))))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"List":::) "of" (Set (Const "X")); synonym "A" :::"AND"::: "B" for "X" :::"/\"::: "A"; synonym "A" :::"OR"::: "B" for "X" :::"\/"::: "A"; synonym "A" :::"BUTNOT"::: "B" for "X" :::"\"::: "A"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"List":::) "of" (Set (Const "X")); :: original: :::"AND"::: redefine func "A" :::"AND"::: "B" -> ($#m1_subset_1 :::"List":::) "of" "X"; :: original: :::"OR"::: redefine func "A" :::"OR"::: "B" -> ($#m1_subset_1 :::"List":::) "of" "X"; :: original: :::"BUTNOT"::: redefine func "A" :::"BUTNOT"::: "B" -> ($#m1_subset_1 :::"List":::) "of" "X"; end; theorem :: MMLQUERY:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "L2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "L1")) ($#k16_mmlquery :::"OR"::: ) (Set (Var "L2")) ")" ) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O")) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "L2")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O")) ")" )))))) ; theorem :: MMLQUERY:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2"))) & (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L1")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L2")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O2"))))))) ; theorem :: MMLQUERY:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O2"))))))) ; theorem :: MMLQUERY:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set "(" (Set (Var "O1")) ($#k15_mmlquery :::"AND"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O1")) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "L")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O2")) ")" )))))) ; theorem :: MMLQUERY:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "L1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "L1")) ($#r1_tarski :::"c="::: ) (Set (Var "L2")))) "holds" (Bool (Set (Set (Var "L2")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "L1")) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O"))))))) ; begin theorem :: MMLQUERY:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")))) ")" )) "holds" (Bool (Set (Var "O1")) ($#r2_relset_1 :::"="::: ) (Set (Var "O2"))))) ; theorem :: MMLQUERY:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O2")))) ")" )) "holds" (Bool (Set (Var "O1")) ($#r2_relset_1 :::"="::: ) (Set (Var "O2"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); func :::"NOT"::: "O" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 15 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O" ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))); end; :: deftheorem defines :::"NOT"::: MMLQUERY:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O")) ")" ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O1", "O2" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); synonym "O1" :::"AND"::: "O2" for "X" :::"/\"::: "O1"; synonym "O1" :::"OR"::: "O2" for "X" :::"\/"::: "O1"; synonym "O1" :::"BUTNOT"::: "O2" for "X" :::"\"::: "O1"; synonym "O1" :::"|"::: "O2" for "X" :::"*"::: "O1"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "O1", "O2" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); :: original: :::"AND"::: redefine func "O1" :::"AND"::: "O2" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 16 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O1" ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))); :: original: :::"OR"::: redefine func "O1" :::"OR"::: "O2" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 17 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O1" ")" ) ($#k16_mmlquery :::"OR"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))); :: original: :::"BUTNOT"::: redefine func "O1" :::"BUTNOT"::: "O2" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 18 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O1" ")" ) ($#k17_mmlquery :::"BUTNOT"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O2" ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))); :: original: :::"|"::: redefine func "O1" :::"|"::: "O2" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 19 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) "O1" ")" ) ($#k2_mmlquery :::"|"::: ) "O2"))); func "O1" :::"\&"::: "O2" -> ($#m1_subset_1 :::"Operation":::) "of" "X" means :: MMLQUERY:def 20 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" "X" "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) "O1" ")" ) ($#k3_mmlquery :::"\&"::: ) "O2" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))); end; :: deftheorem defines :::"AND"::: MMLQUERY:def 16 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "O1")) ($#k19_mmlquery :::"AND"::: ) (Set (Var "O2")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))) ")" ))); :: deftheorem defines :::"OR"::: MMLQUERY:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "O1")) ($#k20_mmlquery :::"OR"::: ) (Set (Var "O2")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k16_mmlquery :::"OR"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))) ")" ))); :: deftheorem defines :::"BUTNOT"::: MMLQUERY:def 18 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "O1")) ($#k21_mmlquery :::"BUTNOT"::: ) (Set (Var "O2")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k17_mmlquery :::"BUTNOT"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))) ")" ))); :: deftheorem defines :::"|"::: MMLQUERY:def 19 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "O1")) ($#k22_mmlquery :::"|"::: ) (Set (Var "O2")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "O1")) ")" ) ($#k2_mmlquery :::"|"::: ) (Set (Var "O2"))))) ")" ))); :: deftheorem defines :::"\&"::: MMLQUERY:def 20 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "O1")) ($#k23_mmlquery :::"\&"::: ) (Set (Var "O2")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O2")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) "}" ))) ")" ))); theorem :: MMLQUERY:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set (Var "O1")) ($#k19_mmlquery :::"AND"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" )))))) ; theorem :: MMLQUERY:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set (Var "O1")) ($#k20_mmlquery :::"OR"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k16_mmlquery :::"OR"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" )))))) ; theorem :: MMLQUERY:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set (Var "O1")) ($#k21_mmlquery :::"BUTNOT"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k17_mmlquery :::"BUTNOT"::: ) (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O2")) ")" )))))) ; theorem :: MMLQUERY:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set (Var "O1")) ($#k22_mmlquery :::"|"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k2_mmlquery :::"|"::: ) (Set (Var "O2"))))))) ; theorem :: MMLQUERY:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set (Var "O1")) ($#k23_mmlquery :::"\&"::: ) (Set (Var "O2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "O1")) ")" ) ($#k3_mmlquery :::"\&"::: ) (Set (Var "O2"))))))) ; theorem :: MMLQUERY:36 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"nin"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O")))) ")" ) ")" ))) ; theorem :: MMLQUERY:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "O")) ")" ) ")" ))))) ; theorem :: MMLQUERY:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O")))))) ; theorem :: MMLQUERY:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "O"))))))) ; theorem :: MMLQUERY:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k10_mmlquery :::"WHEREeq"::: ) "(" (Set (Var "O")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" )))))) ; theorem :: MMLQUERY:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_mmlquery :::"NOT"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")))))) ; theorem :: MMLQUERY:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O1")) ")" ) ($#k20_mmlquery :::"OR"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O2")) ")" )) ($#r1_relset_1 :::"c="::: ) (Set ($#k18_mmlquery :::"NOT"::: ) (Set "(" (Set (Var "O1")) ($#k19_mmlquery :::"AND"::: ) (Set (Var "O2")) ")" ))))) ; theorem :: MMLQUERY:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_mmlquery :::"NOT"::: ) (Set "(" (Set (Var "O1")) ($#k20_mmlquery :::"OR"::: ) (Set (Var "O2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O1")) ")" ) ($#k19_mmlquery :::"AND"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O2")) ")" ))))) ; theorem :: MMLQUERY:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O1"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "O2"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "O1")) ($#k20_mmlquery :::"OR"::: ) (Set (Var "O2")) ")" ) ($#k23_mmlquery :::"\&"::: ) (Set (Var "O"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "O1")) ($#k23_mmlquery :::"\&"::: ) (Set (Var "O")) ")" ) ($#k19_mmlquery :::"AND"::: ) (Set "(" (Set (Var "O2")) ($#k23_mmlquery :::"\&"::: ) (Set (Var "O")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); attr "O" is :::"filtering"::: means :: MMLQUERY:def 21 (Bool "O" ($#r1_relset_1 :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) "X")); end; :: deftheorem defines :::"filtering"::: MMLQUERY:def 21 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_mmlquery :::"filtering"::: ) ) "iff" (Bool (Set (Var "O")) ($#r1_relset_1 :::"c="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) ")" ))); theorem :: MMLQUERY:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_mmlquery :::"filtering"::: ) ) "iff" (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "O")) ")" ))) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); cluster (Set ($#k18_mmlquery :::"NOT"::: ) "O") -> ($#v1_mmlquery :::"filtering"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_mmlquery :::"filtering"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); let "O" be ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); cluster (Set "O" ($#k3_xboole_0 :::"AND"::: ) ) -> ($#v1_mmlquery :::"filtering"::: ) for ($#m1_subset_1 :::"Operation":::) "of" "X"; cluster (Set "F" ($#k3_xboole_0 :::"AND"::: ) ) -> ($#v1_mmlquery :::"filtering"::: ) for ($#m1_subset_1 :::"Operation":::) "of" "X"; cluster (Set "O" ($#k4_xboole_0 :::"BUTNOT"::: ) ) -> ($#v1_mmlquery :::"filtering"::: ) for ($#m1_subset_1 :::"Operation":::) "of" "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F1", "F2" be ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Const "X")); cluster (Set "F2" ($#k2_xboole_0 :::"OR"::: ) ) -> ($#v1_mmlquery :::"filtering"::: ) for ($#m1_subset_1 :::"Operation":::) "of" "X"; end; theorem :: MMLQUERY:46 (Bool "for" (Set (Var "X")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_mmlquery :::"."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: MMLQUERY:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "L")) ($#k2_mmlquery :::"|"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k4_mmlquery :::"WHERE"::: ) (Set (Var "F"))))))) ; theorem :: MMLQUERY:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_mmlquery :::"NOT"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "F")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "F"))))) ; theorem :: MMLQUERY:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_mmlquery :::"NOT"::: ) (Set "(" (Set (Var "F1")) ($#k19_mmlquery :::"AND"::: ) (Set (Var "F2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "F1")) ")" ) ($#k20_mmlquery :::"OR"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: MMLQUERY:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "O")) ($#k20_mmlquery :::"OR"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: MMLQUERY:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mmlquery :::"filtering"::: ) ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k20_mmlquery :::"OR"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: MMLQUERY:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "O")) ($#k19_mmlquery :::"AND"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: MMLQUERY:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_subset_1 :::"Operation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "O1")) ($#k20_mmlquery :::"OR"::: ) (Set (Var "O2")) ")" ) ($#k19_mmlquery :::"AND"::: ) (Set "(" ($#k18_mmlquery :::"NOT"::: ) (Set (Var "O1")) ")" )) ($#r1_relset_1 :::"c="::: ) (Set (Var "O2"))))) ; begin definitionlet "A" be ($#m1_hidden :::"FinSequence":::); let "a" be ($#m1_hidden :::"set"::: ) ; func :::"#occurrences"::: "(" "a" "," "A" ")" -> ($#m1_hidden :::"Nat":::) equals :: MMLQUERY:def 22 (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "A")) & (Bool "a" ($#r2_hidden :::"in"::: ) (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) "}" ); end; :: deftheorem defines :::"#occurrences"::: MMLQUERY:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) "}" )))); theorem :: MMLQUERY:54 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))))) ; theorem :: MMLQUERY:55 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) ")" ) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "A")) ")" ))) ")" ))) ; definitionlet "A" be ($#m1_hidden :::"FinSequence":::); func :::"max#"::: "A" -> ($#m1_hidden :::"Nat":::) means :: MMLQUERY:def 23 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," "A" ")" ) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," "A" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ); end; :: deftheorem defines :::"max#"::: MMLQUERY:def 23 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k25_mmlquery :::"max#"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) ")" ))); theorem :: MMLQUERY:56 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k25_mmlquery :::"max#"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))))) ; theorem :: MMLQUERY:57 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "a")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k25_mmlquery :::"max#"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); let "n" be ($#m1_hidden :::"Nat":::); func :::"ROUGH"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 24 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," "A" ")" )) "}" if (Bool "X" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "m" be ($#m1_hidden :::"Nat":::); func :::"ROUGH"::: "(" "A" "," "n" "," "m" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 25 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "X" : (Bool "(" (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," "A" ")" )) & (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," "A" ")" ) ($#r1_xxreal_0 :::"<="::: ) "m") ")" ) "}" if (Bool "X" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; end; :: deftheorem defines :::"ROUGH"::: MMLQUERY:def 24 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" )) "}" )))); :: deftheorem defines :::"ROUGH"::: MMLQUERY:def 25 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k27_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" )) & (Bool (Set ($#k24_mmlquery :::"#occurrences"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) "}" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); func :::"ROUGH"::: "A" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 26 (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" "A" "," (Set "(" ($#k25_mmlquery :::"max#"::: ) "A" ")" ) ")" ); end; :: deftheorem defines :::"ROUGH"::: MMLQUERY:def 26 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k28_mmlquery :::"ROUGH"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k25_mmlquery :::"max#"::: ) (Set (Var "A")) ")" ) ")" )))); theorem :: MMLQUERY:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k27_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: MMLQUERY:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "m")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: MMLQUERY:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m1"))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m2")))) "holds" (Bool (Set ($#k27_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "m1")) "," (Set (Var "n2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k27_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n1")) "," (Set (Var "m2")) ")" ))))) ; theorem :: MMLQUERY:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k27_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: MMLQUERY:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MMLQUERY:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_prob_3 :::"Union"::: ) (Set (Var "A")))))) ; theorem :: MMLQUERY:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k15_mmlquery :::"AND"::: ) (Set (Var "L2")))))) ; theorem :: MMLQUERY:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_subset_1 :::"List":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k26_mmlquery :::"ROUGH"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k16_mmlquery :::"OR"::: ) (Set (Var "L2")))))) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"ConstructorDB"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"ConstructorDB":::(# :::"carrier":::, :::"Constrs":::, :::"ref-operation"::: #) -> ($#l1_mmlquery :::"ConstructorDB"::: ) ; sel :::"Constrs"::: "c1" -> ($#m1_subset_1 :::"List":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"ref-operation"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" "c1"); end; definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode List of "X" is ($#m1_subset_1 :::"List":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); mode Operation of "X" is ($#m1_subset_1 :::"Operation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "S")); func :::"@"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" "X" equals :: MMLQUERY:def 27 "R"; end; :: deftheorem defines :::"@"::: MMLQUERY:def 27 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "S")) "holds" (Bool (Set ($#k29_mmlquery :::"@"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))))); definitionlet "X" be ($#l1_mmlquery :::"ConstructorDB"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "a" :::"ref"::: -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 28 (Set "a" ($#k1_mmlquery :::"."::: ) (Set "(" ($#k29_mmlquery :::"@"::: ) (Set "the" ($#u2_mmlquery :::"ref-operation"::: ) "of" "X") ")" )); func "a" :::"occur"::: -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 29 (Set "a" ($#k1_mmlquery :::"."::: ) (Set "(" (Set "(" ($#k29_mmlquery :::"@"::: ) (Set "the" ($#u2_mmlquery :::"ref-operation"::: ) "of" "X") ")" ) ($#k3_relset_1 :::"~"::: ) ")" )); end; :: deftheorem defines :::"ref"::: MMLQUERY:def 28 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k30_mmlquery :::"ref"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_mmlquery :::"."::: ) (Set "(" ($#k29_mmlquery :::"@"::: ) (Set "the" ($#u2_mmlquery :::"ref-operation"::: ) "of" (Set (Var "X"))) ")" ))))); :: deftheorem defines :::"occur"::: MMLQUERY:def 29 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k31_mmlquery :::"occur"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_mmlquery :::"."::: ) (Set "(" (Set "(" ($#k29_mmlquery :::"@"::: ) (Set "the" ($#u2_mmlquery :::"ref-operation"::: ) "of" (Set (Var "X"))) ")" ) ($#k3_relset_1 :::"~"::: ) ")" ))))); theorem :: MMLQUERY:66 (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "y")) ($#k30_mmlquery :::"ref"::: ) )) "iff" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k31_mmlquery :::"occur"::: ) )) ")" ))) ; definitionlet "X" be ($#l1_mmlquery :::"ConstructorDB"::: ) ; attr "X" is :::"ref-finite"::: means :: MMLQUERY:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"ref-finite"::: MMLQUERY:def 30 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_mmlquery :::"ref-finite"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v3_mmlquery :::"ref-finite"::: ) for ($#l1_mmlquery :::"ConstructorDB"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) for ($#l1_mmlquery :::"ConstructorDB"::: ) ; end; registrationlet "X" be ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); cluster (Set "x" ($#k30_mmlquery :::"ref"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "X" be ($#l1_mmlquery :::"ConstructorDB"::: ) ; let "A" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Const "X"))); func :::"ATLEAST"::: "A" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 31 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set ($#k2_relset_1 :::"rng"::: ) "A") ($#r1_tarski :::"c="::: ) (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) )) "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"ATMOST"::: "A" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 32 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) "A")) "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"EXACTLY"::: "A" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 33 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) "A")) "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "n" be ($#m1_hidden :::"Nat":::); func :::"ATLEAST-"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 34 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) "A" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) "n") "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; end; :: deftheorem defines :::"ATLEAST"::: MMLQUERY:def 31 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) )) "}" ))); :: deftheorem defines :::"ATMOST"::: MMLQUERY:def 32 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k33_mmlquery :::"ATMOST"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")))) "}" ))); :: deftheorem defines :::"EXACTLY"::: MMLQUERY:def 33 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k34_mmlquery :::"EXACTLY"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")))) "}" ))); :: deftheorem defines :::"ATLEAST-"::: MMLQUERY:def 34 : (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )))); definitionlet "X" be ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) ; let "A" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Const "X"))); let "n" be ($#m1_hidden :::"Nat":::); func :::"ATMOST+"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 35 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "A" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) "n") "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "m" be ($#m1_hidden :::"Nat":::); func :::"EXACTLY+-"::: "(" "A" "," "n" "," "m" ")" -> ($#m1_subset_1 :::"List":::) "of" "X" equals :: MMLQUERY:def 36 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "A" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) "A" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) "m") ")" ) "}" if (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; end; :: deftheorem defines :::"ATMOST+"::: MMLQUERY:def 35 : (Bool "for" (Set (Var "X")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )))); :: deftheorem defines :::"EXACTLY+-"::: MMLQUERY:def 36 : (Bool "for" (Set (Var "X")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k30_mmlquery :::"ref"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) "}" )))); theorem :: MMLQUERY:67 (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "holds" (Bool (Set ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A")))))) ; theorem :: MMLQUERY:68 (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "holds" (Bool (Set ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "B")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k33_mmlquery :::"ATMOST"::: ) (Set (Var "B")))))) ; theorem :: MMLQUERY:69 (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "holds" (Bool (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "B")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k34_mmlquery :::"EXACTLY"::: ) (Set (Var "B")))))) ; theorem :: MMLQUERY:70 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "A")) "," (Set (Var "m")) ")" ))))) ; theorem :: MMLQUERY:71 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "B")) "," (Set (Var "m")) ")" ))))) ; theorem :: MMLQUERY:72 (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m1"))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m2")))) "holds" (Bool (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "B")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "B")) "," (Set (Var "m1")) "," (Set (Var "m2")) ")" ))))) ; theorem :: MMLQUERY:73 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "holds" (Bool (Set ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: MMLQUERY:74 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "holds" (Bool (Set ($#k33_mmlquery :::"ATMOST"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ))))) ; theorem :: MMLQUERY:75 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "holds" (Bool (Set ($#k34_mmlquery :::"EXACTLY"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ))))) ; theorem :: MMLQUERY:76 (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "holds" (Bool (Set ($#k34_mmlquery :::"EXACTLY"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A")) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" ($#k33_mmlquery :::"ATMOST"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MMLQUERY:77 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Y")) "being" ($#v3_mmlquery :::"ref-finite"::: ) ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "Y"))) "holds" (Bool (Set ($#k37_mmlquery :::"EXACTLY+-"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k35_mmlquery :::"ATLEAST-"::: ) "(" (Set (Var "B")) "," (Set (Var "m")) ")" ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" ($#k36_mmlquery :::"ATMOST+"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: MMLQUERY:78 (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "x")) ($#k31_mmlquery :::"occur"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A")))) "}" )))) ; theorem :: MMLQUERY:79 (Bool "for" (Set (Var "X")) "being" ($#l1_mmlquery :::"ConstructorDB"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_mmlquery :::"Constrs"::: ) "of" (Set (Var "X"))) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k32_mmlquery :::"ATLEAST"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k31_mmlquery :::"occur"::: ) ")" ) ($#k15_mmlquery :::"AND"::: ) (Set "(" (Set (Var "c2")) ($#k31_mmlquery :::"occur"::: ) ")" )))))) ;