:: XTUPLE_0 semantic presentation begin definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"pair"::: means :: XTUPLE_0:def 1 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"pair"::: XTUPLE_0:def 1 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ))) ")" )); registrationlet "x1", "x2" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_tarski :::"["::: ) "x1" "," "x2" ($#k4_tarski :::"]"::: ) ) -> ($#v1_xtuple_0 :::"pair"::: ) ; end; theorem :: XTUPLE_0:1 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" )) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "x")) "is" ($#v1_xtuple_0 :::"pair"::: ) ) ; func "x" :::"`1"::: -> ($#m1_hidden :::"set"::: ) means :: XTUPLE_0:def 2 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y1")))); func "x" :::"`2"::: -> ($#m1_hidden :::"set"::: ) means :: XTUPLE_0:def 3 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y2")))); end; :: deftheorem defines :::"`1"::: XTUPLE_0:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_xtuple_0 :::"pair"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) ")" ))); :: deftheorem defines :::"`2"::: XTUPLE_0:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_xtuple_0 :::"pair"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) ")" ))); registrationlet "x1", "x2" be ($#m1_hidden :::"set"::: ) ; reduce ; reduce ; end; registration cluster ($#v1_xtuple_0 :::"pair"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "x" be ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) ; reduce ; end; theorem :: XTUPLE_0:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xtuple_0 :::"pair"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_xtuple_0 :::"`2"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; begin definitionlet "x1", "x2", "x3" be ($#m1_hidden :::"set"::: ) ; func :::"[":::"x1" "," "x2" "," "x3":::"]"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 4 (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) "x1" "," "x2" ($#k4_tarski :::"]"::: ) ) "," "x3" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"["::: XTUPLE_0:def 4 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "x3")) ($#k4_tarski :::"]"::: ) ))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"triple"::: means :: XTUPLE_0:def 5 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))); end; :: deftheorem defines :::"triple"::: XTUPLE_0:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_xtuple_0 :::"triple"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ))) ")" )); registrationlet "x1", "x2", "x3" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_xtuple_0 :::"["::: ) "x1" "," "x2" "," "x3" ($#k3_xtuple_0 :::"]"::: ) ) -> ($#v2_xtuple_0 :::"triple"::: ) ; end; theorem :: XTUPLE_0:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"="::: ) (Set (Var "y3"))) ")" )) ; registration cluster ($#v2_xtuple_0 :::"triple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_xtuple_0 :::"triple"::: ) -> ($#v1_xtuple_0 :::"pair"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func "x" :::"`1_3"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 6 (Set (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func "x" :::"`2_3"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 7 (Set (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"`1_3"::: XTUPLE_0:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))); :: deftheorem defines :::"`2_3"::: XTUPLE_0:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))); notationlet "x" be ($#m1_hidden :::"set"::: ) ; synonym "x" :::"`3_3"::: for "x" :::"`2"::: ; end; registrationlet "x1", "x2", "x3" be ($#m1_hidden :::"set"::: ) ; reduce ; reduce ; reduce ; end; registrationlet "x" be ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) ; reduce ; end; theorem :: XTUPLE_0:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_xtuple_0 :::"`1_3"::: ) )) & (Bool (Set (Set (Var "a")) ($#k5_xtuple_0 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_xtuple_0 :::"`3_3"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; begin definitionlet "x1", "x2", "x3", "x4" be ($#m1_hidden :::"set"::: ) ; func :::"[":::"x1" "," "x2" "," "x3" "," "x4":::"]"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 8 (Set ($#k4_tarski :::"["::: ) (Set ($#k3_xtuple_0 :::"["::: ) "x1" "," "x2" "," "x3" ($#k3_xtuple_0 :::"]"::: ) ) "," "x4" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"["::: XTUPLE_0:def 8 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set (Var "x4")) ($#k4_tarski :::"]"::: ) ))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"quadruple"::: means :: XTUPLE_0:def 9 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))); end; :: deftheorem defines :::"quadruple"::: XTUPLE_0:def 9 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_xtuple_0 :::"quadruple"::: ) ) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ))) ")" )); registrationlet "x1", "x2", "x3", "x4" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_xtuple_0 :::"["::: ) "x1" "," "x2" "," "x3" "," "x4" ($#k6_xtuple_0 :::"]"::: ) ) -> ($#v3_xtuple_0 :::"quadruple"::: ) ; end; theorem :: XTUPLE_0:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"="::: ) (Set (Var "y3"))) & (Bool (Set (Var "x4")) ($#r1_hidden :::"="::: ) (Set (Var "y4"))) ")" )) ; registration cluster ($#v3_xtuple_0 :::"quadruple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_xtuple_0 :::"quadruple"::: ) -> ($#v2_xtuple_0 :::"triple"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func "x" :::"`1_4"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 10 (Set (Set "(" (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); func "x" :::"`2_4"::: -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 11 (Set (Set "(" (Set "(" "x" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ); end; :: deftheorem defines :::"`1_4"::: XTUPLE_0:def 10 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k7_xtuple_0 :::"`1_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))); :: deftheorem defines :::"`2_4"::: XTUPLE_0:def 11 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k8_xtuple_0 :::"`2_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))); notationlet "x" be ($#m1_hidden :::"set"::: ) ; synonym "x" :::"`3_4"::: for "x" :::"`2_3"::: ; synonym "x" :::"`4_4"::: for "x" :::"`2"::: ; end; registrationlet "x1", "x2", "x3", "x4" be ($#m1_hidden :::"set"::: ) ; reduce ; reduce ; reduce ; reduce ; end; registrationlet "x" be ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) ; reduce ; end; theorem :: XTUPLE_0:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" )))) ; theorem :: XTUPLE_0:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"proj1"::: "X" -> ($#m1_hidden :::"set"::: ) means :: XTUPLE_0:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")) ")" )); func :::"proj2"::: "X" -> ($#m1_hidden :::"set"::: ) means :: XTUPLE_0:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X")) ")" )); end; :: deftheorem defines :::"proj1"::: XTUPLE_0:def 12 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )) ")" )); :: deftheorem defines :::"proj2"::: XTUPLE_0:def 13 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )) ")" )); theorem :: XTUPLE_0:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Y"))))) ; theorem :: XTUPLE_0:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Y"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"proj1_3"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 14 (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) "X" ")" )); func :::"proj2_3"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 15 (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) "X" ")" )); end; :: deftheorem defines :::"proj1_3"::: XTUPLE_0:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" )))); :: deftheorem defines :::"proj2_3"::: XTUPLE_0:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" )))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"proj3_3"::: "X" for :::"proj2"::: "X"; end; theorem :: XTUPLE_0:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "Y"))))) ; theorem :: XTUPLE_0:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "Y"))))) ; theorem :: XTUPLE_0:12 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:14 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"proj1_4"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 16 (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) "X" ")" )); func :::"proj2_4"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: XTUPLE_0:def 17 (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) "X" ")" )); end; :: deftheorem defines :::"proj1_4"::: XTUPLE_0:def 16 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" )))); :: deftheorem defines :::"proj2_4"::: XTUPLE_0:def 17 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" )))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"proj3_4"::: "X" for :::"proj2_3"::: "X"; synonym :::"proj4_4"::: "X" for :::"proj2"::: "X"; end; theorem :: XTUPLE_0:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "Y"))))) ; theorem :: XTUPLE_0:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "Y"))))) ; theorem :: XTUPLE_0:18 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:19 (Bool "for" (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:20 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X"))))) ; theorem :: XTUPLE_0:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k7_xtuple_0 :::"`1_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k7_xtuple_0 :::"`1_4"::: ) )) & (Bool (Set (Set (Var "a")) ($#k8_xtuple_0 :::"`2_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k8_xtuple_0 :::"`2_4"::: ) )) & (Bool (Set (Set (Var "a")) ($#k5_xtuple_0 :::"`3_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_xtuple_0 :::"`3_4"::: ) )) & (Bool (Set (Set (Var "a")) ($#k2_xtuple_0 :::"`4_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_xtuple_0 :::"`4_4"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; begin registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_xtuple_0 :::"proj1"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_xtuple_0 :::"proj1_3"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_xtuple_0 :::"proj2_3"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k13_xtuple_0 :::"proj1_4"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_xtuple_0 :::"proj2_4"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: XTUPLE_0:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:24 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:25 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:26 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:28 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:30 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:31 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:32 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:33 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:34 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:35 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:36 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:37 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k12_xtuple_0 :::"proj2_3"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k12_xtuple_0 :::"proj2_3"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:39 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:40 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:42 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k13_xtuple_0 :::"proj1_4"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k13_xtuple_0 :::"proj1_4"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:43 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:44 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" )))) ; theorem :: XTUPLE_0:46 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "X")) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k14_xtuple_0 :::"proj2_4"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k14_xtuple_0 :::"proj2_4"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )))) ;