RobertJasiek wrote:I'll edit Chris' proof (the second part only, which we are discussing here) later - may be tomorrow -, making the reference to local-1 and local-2\1 clearly visible.
Great!
Here it is:
***RED*** = deleted
BLUE = inserted
---(BLUE ITALIC)--- = comment
In a position, a string of a player is "two-eye-alive" if the opponent cannot force no intersection of the string with a two-eye-formation on.
...
For the implication two-eye-alive ->J2003-alive, imagine that a string is two-eye-alive.
***The string can either be uncapturable or not uncapturable*** The opponent can either force capture of the string or not. ---(This is what I mean with "primary")---(1)
***The string is uncapturable*** The opponent cannot force capture of the string ->
It is uncapturable. ---(This is what I mean with "secondary", the J2003-term follows from a "neutral" clause)--- -> It is J2003-alive
(2)
***It is not uncapturable -> The string is either capturable-1 or not capturable-1*** The opponent can force capture of the string. -> The opponent can force either no permanent stone on local-1 or not.(2a)
***It is capturable-1*** The opponent cannot force no permanent stone on local-1 ->
the string is capturable-1 -> It is J2003-alive
(2b)
***It is not capturable-1*** The opponent can force no permanent stone on local-1 -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach a two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the oponent reaches a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be capture by only moves of its opponent, it consists of permanent stones. In S(H) the two-eye-formation that is formed on the captured string
***has either a stone on local-1 of the string or it*** does not have a stone on local-1 of the string
---(this follows from the first sentence of (2b)-new)---***(2b1) If it has a stone on local-1 of the string, it is also on local-2.
(2b2) If it does not have a stone on local-1 of the string, then*** ---(superfluous now)--- local-1 of the string consists of the one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the the empty points of a two-eye-formation. This implies that this two-eye formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersection these adjacent intersections where empty or occupied by opposing stones. Hence, these intersections belong to local-2
\1 of the string.
***In both (2b1) and (2b2)*** we see that the two-eye-formation that is formed in S(H) has permanent stones on local-2
\1 of the string. Hence, if every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2
\1. Hence, the opponent cannot force
***both caputre of the string and*** no local-2
\1 permanent stone. Hence, the string is capturable-2
\1. Hence it is capturable-2. Hence, it is J2003-alive.
Hence, under the assumption that the string is two-eye-alive, we find that
it is J2003-alive . QED.
It will be just the contents of the table in prose.
We'll see:)
The table uses "two-eye-formation" as parameter, in Chris' proof this is a precondition. For the sake of comparision you can restrict yourself to the columns with "two-eye-formation" = "Y".
