:: CGAMES_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"left-right"::: -> ; aggr :::"left-right":::(# :::"LeftOptions":::, :::"RightOptions"::: #) -> ($#l1_cgames_1 :::"left-right"::: ) ; sel :::"LeftOptions"::: "c1" -> ($#m1_hidden :::"set"::: ) ; sel :::"RightOptions"::: "c1" -> ($#m1_hidden :::"set"::: ) ; end; definitionfunc :::"ConwayZero"::: -> ($#m1_hidden :::"set"::: ) equals :: CGAMES_1:def 1 (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); end; :: deftheorem defines :::"ConwayZero"::: CGAMES_1:def 1 : (Bool (Set ($#k1_cgames_1 :::"ConwayZero"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" )); registration cluster ($#v1_cgames_1 :::"strict"::: ) for ($#l1_cgames_1 :::"left-right"::: ) ; end; definitionlet "alpha" be ($#m1_hidden :::"Ordinal":::); func :::"ConwayDay"::: "alpha" -> ($#m1_hidden :::"set"::: ) means :: CGAMES_1:def 2 (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool "alpha" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "alpha") ($#r1_hidden :::"="::: ) it) & (Bool "(" "for" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "beta"))) ($#r1_hidden :::"="::: ) "{" (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set (Var "x")) "," (Set (Var "y")) "#)" ) where x, y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "beta")) ")" ) ")" ) ")" ) : (Bool verum) "}" ) ")" ) ")" )); end; :: deftheorem defines :::"ConwayDay"::: CGAMES_1:def 2 : (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "alpha")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "alpha"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "beta"))) ($#r1_hidden :::"="::: ) "{" (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set (Var "x")) "," (Set (Var "y")) "#)" ) where x, y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "beta")) ")" ) ")" ) ")" ) : (Bool verum) "}" ) ")" ) ")" )) ")" ))); theorem :: CGAMES_1:1 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#v1_cgames_1 :::"strict"::: ) ($#l1_cgames_1 :::"left-right"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_cgames_1 :::"LeftOptions"::: ) "of" (Set (Var "w"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_cgames_1 :::"RightOptions"::: ) "of" (Set (Var "w")))))) "holds" (Bool "ex" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set (Var "alpha"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta")))) ")" )) ")" ) ")" )) ")" ))) ; theorem :: CGAMES_1:2 (Bool (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: CGAMES_1:3 (Bool "for" (Set (Var "alpha")) "," (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "alpha")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "beta")))) "holds" (Bool (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta"))))) ; registrationlet "alpha" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k2_cgames_1 :::"ConwayDay"::: ) "alpha") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"ConwayGame-like"::: means :: CGAMES_1:def 3 (Bool "ex" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))))); end; :: deftheorem defines :::"ConwayGame-like"::: CGAMES_1:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_cgames_1 :::"ConwayGame-like"::: ) ) "iff" (Bool "ex" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))))) ")" )); registrationlet "alpha" be ($#m1_hidden :::"Ordinal":::); cluster -> ($#v2_cgames_1 :::"ConwayGame-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_cgames_1 :::"ConwayDay"::: ) "alpha"); end; registration cluster (Set ($#k1_cgames_1 :::"ConwayZero"::: ) ) -> ($#v2_cgames_1 :::"ConwayGame-like"::: ) ; end; registration cluster ($#v1_cgames_1 :::"strict"::: ) ($#v2_cgames_1 :::"ConwayGame-like"::: ) for ($#l1_cgames_1 :::"left-right"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode ConwayGame is ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#m1_hidden :::"set"::: ) ; end; definition:: original: :::"ConwayZero"::: redefine func :::"ConwayZero"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )); end; definitionfunc :::"ConwayOne"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Num 1)) equals :: CGAMES_1:def 4 (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); func :::"ConwayStar"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Num 1)) equals :: CGAMES_1:def 5 (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "#)" ); end; :: deftheorem defines :::"ConwayOne"::: CGAMES_1:def 4 : (Bool (Set ($#k4_cgames_1 :::"ConwayOne"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" )); :: deftheorem defines :::"ConwayStar"::: CGAMES_1:def 5 : (Bool (Set ($#k5_cgames_1 :::"ConwayStar"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) ) "#)" )); theorem :: CGAMES_1:4 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set (Var "g")) "is" ($#v1_cgames_1 :::"strict"::: ) ($#l1_cgames_1 :::"left-right"::: ) )) ; registration cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) -> ($#v1_cgames_1 :::"strict"::: ) for ($#l1_cgames_1 :::"left-right"::: ) ; end; definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); func :::"the_LeftOptions_of"::: "g" -> ($#m1_hidden :::"set"::: ) means :: CGAMES_1:def 6 (Bool "ex" (Set (Var "w")) "being" ($#l1_cgames_1 :::"left-right"::: ) "st" (Bool "(" (Bool "g" ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool it ($#r1_hidden :::"="::: ) (Set "the" ($#u1_cgames_1 :::"LeftOptions"::: ) "of" (Set (Var "w")))) ")" )); func :::"the_RightOptions_of"::: "g" -> ($#m1_hidden :::"set"::: ) means :: CGAMES_1:def 7 (Bool "ex" (Set (Var "w")) "being" ($#l1_cgames_1 :::"left-right"::: ) "st" (Bool "(" (Bool "g" ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool it ($#r1_hidden :::"="::: ) (Set "the" ($#u2_cgames_1 :::"RightOptions"::: ) "of" (Set (Var "w")))) ")" )); end; :: deftheorem defines :::"the_LeftOptions_of"::: CGAMES_1:def 6 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#l1_cgames_1 :::"left-right"::: ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_cgames_1 :::"LeftOptions"::: ) "of" (Set (Var "w")))) ")" )) ")" ))); :: deftheorem defines :::"the_RightOptions_of"::: CGAMES_1:def 7 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "w")) "being" ($#l1_cgames_1 :::"left-right"::: ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_cgames_1 :::"RightOptions"::: ) "of" (Set (Var "w")))) ")" )) ")" ))); definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); func :::"the_Options_of"::: "g" -> ($#m1_hidden :::"set"::: ) equals :: CGAMES_1:def 8 (Set (Set "(" ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) "g" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_cgames_1 :::"the_RightOptions_of"::: ) "g" ")" )); end; :: deftheorem defines :::"the_Options_of"::: CGAMES_1:def 8 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")) ")" )))); theorem :: CGAMES_1:5 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))) "iff" (Bool "(" (Bool (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g2")))) & (Bool (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g2")))) ")" ) ")" )) ; registration cluster (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set ($#k4_cgames_1 :::"ConwayOne"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: CGAMES_1:6 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) "iff" (Bool (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: CGAMES_1:7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set ($#k4_cgames_1 :::"ConwayOne"::: ) ))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) ")" )) ; theorem :: CGAMES_1:8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) )))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) )))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) )))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set ($#k5_cgames_1 :::"ConwayStar"::: ) ))) ")" ")" )) ; theorem :: CGAMES_1:9 (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set (Var "alpha"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta")))) ")" ))) ")" ))) ; definitionlet "g" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "g")) "is" ($#m1_hidden :::"ConwayGame":::)) ; func :::"ConwayRank"::: "g" -> ($#m1_hidden :::"Ordinal":::) means :: CGAMES_1:def 9 (Bool "(" (Bool "g" ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) it)) & (Bool "(" "for" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "not" (Bool "g" ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta"))))) ")" ) ")" ); end; :: deftheorem defines :::"ConwayRank"::: CGAMES_1:def 9 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) "is" ($#m1_hidden :::"ConwayGame":::))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool "not" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta"))))) ")" ) ")" ) ")" ))); theorem :: CGAMES_1:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))))))) ; theorem :: CGAMES_1:11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) & (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))))))) ; theorem :: CGAMES_1:12 (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))) "iff" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))) ($#r1_ordinal1 :::"c="::: ) (Set (Var "alpha"))) ")" ))) ; theorem :: CGAMES_1:13 (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Var "alpha"))) "iff" (Bool "ex" (Set (Var "beta")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "beta")) ($#r2_hidden :::"in"::: ) (Set (Var "alpha"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "beta")))) ")" )) ")" ))) ; theorem :: CGAMES_1:14 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:15 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool "(" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:16 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Bool "not" (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g")))))) ; theorem :: CGAMES_1:17 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "x")) "is" ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#l1_cgames_1 :::"left-right"::: ) ))) ; theorem :: CGAMES_1:18 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "x")) "is" ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#l1_cgames_1 :::"left-right"::: ) ))) ; theorem :: CGAMES_1:19 (Bool "for" (Set (Var "w")) "being" ($#v1_cgames_1 :::"strict"::: ) ($#l1_cgames_1 :::"left-right"::: ) "holds" (Bool "(" (Bool (Set (Var "w")) "is" ($#m1_hidden :::"ConwayGame":::)) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_cgames_1 :::"LeftOptions"::: ) "of" (Set (Var "w"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_cgames_1 :::"RightOptions"::: ) "of" (Set (Var "w")))))) "holds" (Bool (Set (Var "z")) "is" ($#m1_hidden :::"ConwayGame":::))) ")" )) ; begin scheme :: CGAMES_1:sch 1 ConwayGameMinTot{ P1[ ($#m1_hidden :::"ConwayGame":::)] } : (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool P1[(Set (Var "g"))]) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g1"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))))) "holds" (Bool "not" (Bool P1[(Set (Var "g1"))])) ")" ) ")" )) provided (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool P1[(Set (Var "g"))])) proof end; scheme :: CGAMES_1:sch 2 ConwayGameMin{ P1[ ($#m1_hidden :::"ConwayGame":::)] } : (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool P1[(Set (Var "g"))]) & (Bool "(" "for" (Set (Var "gO")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool "not" (Bool P1[(Set (Var "gO"))])) ")" ) ")" )) provided (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool P1[(Set (Var "g"))])) proof end; scheme :: CGAMES_1:sch 3 ConwayGameInd{ P1[ ($#m1_hidden :::"ConwayGame":::)] } : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool P1[(Set (Var "g"))])) provided (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool "(" "for" (Set (Var "gO")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool P1[(Set (Var "gO"))]) ")" )) "holds" (Bool P1[(Set (Var "g"))])) proof end; begin definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"ConwayGame-valued"::: means :: CGAMES_1:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"ConwayGame":::))); end; :: deftheorem defines :::"ConwayGame-valued"::: CGAMES_1:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"ConwayGame":::))) ")" )); registrationlet "g" be ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "g" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set bbbadK5_NUMBERS()) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::); cluster -> ($#v7_ordinal1 :::"natural"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "f"); end; registrationlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "f"))); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v2_cgames_1 :::"ConwayGame-like"::: ) ; end; definitionlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ($#m1_hidden :::"FinSequence":::); attr "f" is :::"ConwayGameChain-like"::: means :: CGAMES_1:def 11 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "f") "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"ConwayGameChain-like"::: CGAMES_1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_cgames_1 :::"ConwayGameChain-like"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" )); theorem :: CGAMES_1:20 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))))) ; registrationlet "g" be ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "g" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v4_cgames_1 :::"ConwayGameChain-like"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set bbbadK5_NUMBERS()) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ($#v4_cgames_1 :::"ConwayGameChain-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode ConwayGameChain is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_cgames_1 :::"ConwayGame-valued"::: ) ($#v4_cgames_1 :::"ConwayGameChain-like"::: ) ($#m1_hidden :::"FinSequence":::); end; theorem :: CGAMES_1:21 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ))))) ; theorem :: CGAMES_1:22 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" ))))) ; theorem :: CGAMES_1:23 (Bool "for" (Set (Var "alpha")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Var "alpha")))))) ; definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); func :::"the_Tree_of"::: "g" -> ($#m1_hidden :::"set"::: ) means :: CGAMES_1:def 12 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) "g") ")" )) ")" )); end; :: deftheorem defines :::"the_Tree_of"::: CGAMES_1:def 12 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )) ")" )) ")" ))); registrationlet "g" be ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) "g") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); func :::"the_proper_Tree_of"::: "g" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_cgames_1 :::"the_Tree_of"::: ) "g" ")" ) equals :: CGAMES_1:def 13 (Set (Set "(" ($#k10_cgames_1 :::"the_Tree_of"::: ) "g" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "g" ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"the_proper_Tree_of"::: CGAMES_1:def 13 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) )))); theorem :: CGAMES_1:24 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g"))))) ; definitionlet "alpha" be ($#m1_hidden :::"Ordinal":::); let "g" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_cgames_1 :::"ConwayDay"::: ) (Set (Const "alpha"))); :: original: :::"the_Tree_of"::: redefine func :::"the_Tree_of"::: "g" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_cgames_1 :::"ConwayDay"::: ) "alpha" ")" ); end; registrationlet "g" be ($#m1_hidden :::"ConwayGame":::); cluster -> ($#v2_cgames_1 :::"ConwayGame-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) "g"); end; theorem :: CGAMES_1:25 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ConwayGameChain":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "n"))) "is" ($#m1_hidden :::"ConwayGameChain":::)))) ; theorem :: CGAMES_1:26 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"ConwayGameChain":::) "st" (Bool (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g")))) ")" ))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f2"))) "is" ($#m1_hidden :::"ConwayGameChain":::))) ; theorem :: CGAMES_1:27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "or" (Bool "ex" (Set (Var "gO")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "gO")))) ")" )) ")" ) ")" ))) ; theorem :: CGAMES_1:28 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gO")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "or" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g")))) ")" )) ; theorem :: CGAMES_1:29 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "gO"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k9_cgames_1 :::"ConwayRank"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:30 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) ")" )) "holds" (Bool (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "s"))))) ; theorem :: CGAMES_1:31 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g2"))))) "holds" (Bool (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g2"))))) ; theorem :: CGAMES_1:32 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g2"))))) "holds" (Bool (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g2"))))) ; theorem :: CGAMES_1:33 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:34 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:35 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g2"))))) "holds" (Bool (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g2"))))) ; theorem :: CGAMES_1:36 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k8_cgames_1 :::"the_Options_of"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "gO"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g"))))) ; theorem :: CGAMES_1:37 (Bool (Set ($#k12_cgames_1 :::"the_Tree_of"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: CGAMES_1:38 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k3_cgames_1 :::"ConwayZero"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g"))))) ; scheme :: CGAMES_1:sch 4 ConwayGameMin2{ P1[ ($#m1_hidden :::"ConwayGame":::)] } : (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool P1[(Set (Var "g"))]) & (Bool "(" "for" (Set (Var "gO")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g"))))) "holds" (Bool "not" (Bool P1[(Set (Var "gO"))])) ")" ) ")" )) provided (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool P1[(Set (Var "g"))])) proof end; begin scheme :: CGAMES_1:sch 5 Func1RecUniq{ F1( ($#m1_hidden :::"ConwayGame":::) "," ($#m1_hidden :::"Function":::)) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "g1")) "," (Set "(" (Set (Var "f1")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g1")) ")" ) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "g1")) "," (Set "(" (Set (Var "f2")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g1")) ")" ) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) proof end; scheme :: CGAMES_1:sch 6 Func1RecEx{ F1( ($#m1_hidden :::"ConwayGame":::) "," ($#m1_hidden :::"Function":::)) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "g1")) "," (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k11_cgames_1 :::"the_proper_Tree_of"::: ) (Set (Var "g1")) ")" ) ")" ) ")" )) ")" ) ")" ))) proof end; begin definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); func :::"-"::: "g" -> ($#m1_hidden :::"set"::: ) means :: CGAMES_1:def 14 (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) "g")) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) "g")) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "gR")) ")" ) where gR "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))) : (Bool (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" "," "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "gL")) ")" ) where gL "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g1"))) : (Bool (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" "#)" )) ")" ) ")" )); end; :: deftheorem defines :::"-"::: CGAMES_1:def 14 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cgames_1 :::"the_Tree_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cgames_1 :::"left-right"::: ) "(#" "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "gR")) ")" ) where gR "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))) : (Bool (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" "," "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "gL")) ")" ) where gL "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g1"))) : (Bool (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "}" "#)" )) ")" ) ")" )) ")" ))); registrationlet "g" be ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v2_cgames_1 :::"ConwayGame-like"::: ) ; end; theorem :: CGAMES_1:39 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) "iff" (Bool "ex" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gR")))) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) "iff" (Bool "ex" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gL")))) ")" )) ")" ) ")" ) ")" )) ; theorem :: CGAMES_1:40 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; theorem :: CGAMES_1:41 (Bool "for" (Set (Var "gO")) "," (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" )))) "implies" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g"))))) "implies" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g"))))) "implies" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) ")" & "(" (Bool (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" )))) "implies" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" )))) "implies" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g"))))) "implies" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g"))))) "implies" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" ))) ")" & "(" (Bool (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "gO"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set "(" ($#k13_cgames_1 :::"-"::: ) (Set (Var "g")) ")" )))) "implies" (Bool (Set (Var "gO")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) ")" ")" )) ; definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); attr "g" is :::"nonnegative"::: means :: CGAMES_1:def 15 (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "g" ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))))) "holds" (Bool "ex" (Set (Var "gRL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gRL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "gR")))) & (Bool (Set (Var "gRL")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"nonnegative"::: CGAMES_1:def 15 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g1"))))) "holds" (Bool "ex" (Set (Var "gRL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gRL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "gR")))) & (Bool (Set (Var "gRL")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" ))) ")" ) ")" )) ")" )); definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); attr "g" is :::"nonpositive"::: means :: CGAMES_1:def 16 (Bool (Set ($#k13_cgames_1 :::"-"::: ) "g") "is" ($#v5_cgames_1 :::"nonnegative"::: ) ); end; :: deftheorem defines :::"nonpositive"::: CGAMES_1:def 16 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) "iff" (Bool (Set ($#k13_cgames_1 :::"-"::: ) (Set (Var "g"))) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) ")" )); definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); attr "g" is :::"zero"::: means :: CGAMES_1:def 17 (Bool "(" (Bool "g" "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) & (Bool "g" "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" ); attr "g" is :::"fuzzy"::: means :: CGAMES_1:def 18 (Bool "(" (Bool (Bool "not" "g" "is" ($#v5_cgames_1 :::"nonnegative"::: ) )) & (Bool (Bool "not" "g" "is" ($#v6_cgames_1 :::"nonpositive"::: ) )) ")" ); end; :: deftheorem defines :::"zero"::: CGAMES_1:def 17 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v7_cgames_1 :::"zero"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" ) ")" )); :: deftheorem defines :::"fuzzy"::: CGAMES_1:def 18 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) )) ")" ) ")" )); definitionlet "g" be ($#m1_hidden :::"ConwayGame":::); attr "g" is :::"positive"::: means :: CGAMES_1:def 19 (Bool "(" (Bool "g" "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) & (Bool (Bool "not" "g" "is" ($#v7_cgames_1 :::"zero"::: ) )) ")" ); attr "g" is :::"negative"::: means :: CGAMES_1:def 20 (Bool "(" (Bool "g" "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) & (Bool (Bool "not" "g" "is" ($#v7_cgames_1 :::"zero"::: ) )) ")" ); end; :: deftheorem defines :::"positive"::: CGAMES_1:def 19 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v9_cgames_1 :::"positive"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v7_cgames_1 :::"zero"::: ) )) ")" ) ")" )); :: deftheorem defines :::"negative"::: CGAMES_1:def 20 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v10_cgames_1 :::"negative"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v7_cgames_1 :::"zero"::: ) )) ")" ) ")" )); registration cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v7_cgames_1 :::"zero"::: ) -> ($#v5_cgames_1 :::"nonnegative"::: ) ($#v6_cgames_1 :::"nonpositive"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v5_cgames_1 :::"nonnegative"::: ) ($#v6_cgames_1 :::"nonpositive"::: ) -> ($#v7_cgames_1 :::"zero"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v10_cgames_1 :::"negative"::: ) -> ($#v6_cgames_1 :::"nonpositive"::: ) ($#~v7_cgames_1 "non" ($#v7_cgames_1 :::"zero"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v6_cgames_1 :::"nonpositive"::: ) ($#~v7_cgames_1 "non" ($#v7_cgames_1 :::"zero"::: ) ) -> ($#v10_cgames_1 :::"negative"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v9_cgames_1 :::"positive"::: ) -> ($#v5_cgames_1 :::"nonnegative"::: ) ($#~v7_cgames_1 "non" ($#v7_cgames_1 :::"zero"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v5_cgames_1 :::"nonnegative"::: ) ($#~v7_cgames_1 "non" ($#v7_cgames_1 :::"zero"::: ) ) -> ($#v9_cgames_1 :::"positive"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v8_cgames_1 :::"fuzzy"::: ) -> ($#~v5_cgames_1 "non" ($#v5_cgames_1 :::"nonnegative"::: ) ) ($#~v6_cgames_1 "non" ($#v6_cgames_1 :::"nonpositive"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#~v5_cgames_1 "non" ($#v5_cgames_1 :::"nonnegative"::: ) ) ($#~v6_cgames_1 "non" ($#v6_cgames_1 :::"nonpositive"::: ) ) -> ($#v8_cgames_1 :::"fuzzy"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: CGAMES_1:42 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v7_cgames_1 :::"zero"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v9_cgames_1 :::"positive"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v10_cgames_1 :::"negative"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) ")" )) ; theorem :: CGAMES_1:43 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "gRL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gRL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "gR")))) & (Bool (Set (Var "gRL")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) ")" ))) ")" )) ; theorem :: CGAMES_1:44 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) "iff" (Bool "for" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "gLR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gLR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "gL")))) & (Bool (Set (Var "gLR")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" ))) ")" )) ; theorem :: CGAMES_1:45 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) )) "implies" (Bool "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gR")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gR")) "is" ($#v9_cgames_1 :::"positive"::: ) ) ")" )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gR")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gR")) "is" ($#v9_cgames_1 :::"positive"::: ) ) ")" ) ")" )) "implies" (Bool (Set (Var "g")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) )) "implies" (Bool "for" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gL")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gL")) "is" ($#v10_cgames_1 :::"negative"::: ) ) ")" )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gL")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gL")) "is" ($#v10_cgames_1 :::"negative"::: ) ) ")" ) ")" )) "implies" (Bool (Set (Var "g")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" ")" )) ; theorem :: CGAMES_1:46 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "iff" (Bool "(" (Bool "ex" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "gL")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) ")" )) & (Bool "ex" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "gR")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" )) ")" ) ")" )) ; theorem :: CGAMES_1:47 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v7_cgames_1 :::"zero"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gL")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gL")) "is" ($#v10_cgames_1 :::"negative"::: ) ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gR")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gR")) "is" ($#v9_cgames_1 :::"positive"::: ) ) ")" ) ")" ) ")" ) ")" )) ; theorem :: CGAMES_1:48 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v9_cgames_1 :::"positive"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gR")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gR")) "is" ($#v9_cgames_1 :::"positive"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "gL")) "is" ($#v5_cgames_1 :::"nonnegative"::: ) ) ")" )) ")" ) ")" )) ; theorem :: CGAMES_1:49 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v10_cgames_1 :::"negative"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "gL")) "being" ($#m1_hidden :::"ConwayGame":::) "holds" (Bool "(" "not" (Bool (Set (Var "gL")) ($#r2_hidden :::"in"::: ) (Set ($#k6_cgames_1 :::"the_LeftOptions_of"::: ) (Set (Var "g")))) "or" (Bool (Set (Var "gL")) "is" ($#v8_cgames_1 :::"fuzzy"::: ) ) "or" (Bool (Set (Var "gL")) "is" ($#v10_cgames_1 :::"negative"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "gR")) "being" ($#m1_hidden :::"ConwayGame":::) "st" (Bool "(" (Bool (Set (Var "gR")) ($#r2_hidden :::"in"::: ) (Set ($#k7_cgames_1 :::"the_RightOptions_of"::: ) (Set (Var "g")))) & (Bool (Set (Var "gR")) "is" ($#v6_cgames_1 :::"nonpositive"::: ) ) ")" )) ")" ) ")" )) ; registration cluster (Set ($#k1_cgames_1 :::"ConwayZero"::: ) ) -> ($#v7_cgames_1 :::"zero"::: ) ; end; registration cluster (Set ($#k4_cgames_1 :::"ConwayOne"::: ) ) -> ($#v9_cgames_1 :::"positive"::: ) ; cluster (Set ($#k5_cgames_1 :::"ConwayStar"::: ) ) -> ($#v8_cgames_1 :::"fuzzy"::: ) ; end; registration cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v7_cgames_1 :::"zero"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v9_cgames_1 :::"positive"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v8_cgames_1 :::"fuzzy"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "g" be ($#v6_cgames_1 :::"nonpositive"::: ) ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v5_cgames_1 :::"nonnegative"::: ) ; end; registrationlet "g" be ($#v5_cgames_1 :::"nonnegative"::: ) ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v6_cgames_1 :::"nonpositive"::: ) ; end; registrationlet "g" be ($#v9_cgames_1 :::"positive"::: ) ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v10_cgames_1 :::"negative"::: ) ; end; registration cluster ($#v2_cgames_1 :::"ConwayGame-like"::: ) ($#v10_cgames_1 :::"negative"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "g" be ($#v10_cgames_1 :::"negative"::: ) ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v9_cgames_1 :::"positive"::: ) ; end; registrationlet "g" be ($#v8_cgames_1 :::"fuzzy"::: ) ($#m1_hidden :::"ConwayGame":::); cluster (Set ($#k13_cgames_1 :::"-"::: ) "g") -> ($#v8_cgames_1 :::"fuzzy"::: ) ; end;