RobertJasiek wrote:Because I do not see that the proof would remain unaffected and a new proof for a changed local-2 definition is not available.
Here you are, Robert.
I think you will also be able to recognise that there is some superflous text in Chris' original proof.
---------------------------------------------
From: Chris Dams <chr...@wn5.nospamplease.nl>
Newsgroups: rec.games.go
Subject: Re: Model for the World Amateur Go Championship Rules
Date: Wed, 12 Apr 2006 20:56:06 +0000 (UTC)
Message-ID: <e1jph6$13q$1@wnnews.sci.kun.nl>
References: <p67q32p0mo82bm1c2h5gpolhs93hncpu52@4ax.com> <e1j9jn$pla$1@wnnews.sci.kun.nl> <27gq32p0vhdvn6j0e5o1fneud7erkaas4a@4ax.com>
Dear Robert,
Robert Jasiek <jas...@snafu.de> writes:
>On Wed, 12 Apr 2006 16:24:23 +0000 (UTC), Chris Dams
><chr...@wn5.nospamplease.nl> wrote:
>>> 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.
>>
>>> _J2003-alive_ is defined like in J2003 as either uncapturable,
>>>capturable-1, or capturable-2.
>>
>>> In a position, a string is _WAGC-alive-in-seki_ if it is
>>>J2003-alive and not two-eye-alive.
>>
>>> In a position, a string is _WAGC-alive_ if it is either
>>>two-eye-alive or WAGC-alive-in-seki.
>>
>>From these definitions it follows that WAGC-alive is identical to
>>J2003-alive.
>I doubt this. If you claim it, then please present a formal proof!
I have to admit that I, at first, interpreted "either" as "or" in the
definition of WAGC-alive. However, I think the identity of J2003-alive
and WAGC-alive is still provable. Proof is given below.
Let us denote
> In a position, a string is _WAGC-alive-in-seki_ if it is
> J2003-alive and not two-eye-alive.
as
WAGC-alive-in-seki == J2003-alive && (!two-eye-alive )
In the same notation we also have from
> In a position, a string is _WAGC-alive_ if it is either
> two-eye-alive or WAGC-alive-in-seki.
WAGC-alive == two-eye-alive ^^ WAGC-alive-in-seki.
Substituting the former into the latter expression, we find
WAGC-alive == two-eye-alive ^^ (J2003-alive && (!two-eye-alive)).
In propositional calculus this reduces to
WAGC-alive == J2003-alive || two-eye-alive.
If we now also have the implication two-eye-alive -> J2003-alive if follows
that
WAGC-alive == J2003-alive.
*** insert >>> For the following it is assumed that "local-2" is understood without its points, which belong to "local-1" <<< insert
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.
(1) The string is uncapturable -> It is J2003-alive
(2) It is not uncapturable -> The string is either capturable-1 or
not capturable-1
(2a) It is capturable-1 -> It is J2003-alive
(2b) It is not capturable-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 *** could be deleted, see below >>> has either a
stone on local-1 of the string or it <<< could be deleted, see below *** does not have a stone on local-1
of the string
(2b1) If it has a stone on local-1 of the string, *** delete >>> it is also on
local-2 <<< delete *** *** insert >>> it would be capturable-1, what contradicts the assumption that the string is not capturable-1. So the string cannot have a stone on local-1. <<< insert *** *** (2b1) can be deleted completely !!! ***.
(2b2) *** delete >>> If <<< delete *** *** insert >>> Because <<< insert *** it does not have a stone on local-1 of the string,
then 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 intersections these adjacent intersections where empty or
occupied by opposing stones. Hence, these intersections belong to
local-2 of the string.
In *** delete >>> both (2b1) and <<< delete *** (2b2) we see that the two-eye-formation that is
formed in S(H) has permanent stones on local-2 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. Hence, the opponent cannot force both caputre of the string
and no local-2 permanent stone. Hence, the string 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.
Best,
Chris
