From: Simplane Simple Plane Simulate Plain Simple on
I'm specifying an operation on transitive relations for a
discrete-mathematics software library. Suppose I have a relation R =
(G, A,
A) which is transitive, i.e.:

for all x, y, z in A: xRy and yRz ==> xRz

Now suppose I have an operation on such transitive relation:

R' = R.transtivively_including (a, b) = (G', A', A') ==>
==> A' = A + {a, b} and
G' = G + {(a, b)} + ({(a, b)} o G) ==>
==> A' = A + {a, b} and
G' = G + {(a, b)} + {(x, b) | (x, a) in G)

xR'y <==> xRy or (x, y) = (a, b) or y = b and xRa
yR'z <==> yRz or (y, z) = (a, b) or z = b and yRa

From the above definitions I prove:

xR'y and yR'z ==> xR'z

I aim my proof:

initialize a list S to contain one element 0.
for each i from 1 to N do
let T be a list consisting of xi+y, for all y in S
let U be the union of T and S
sort U
make S empty
let y be the smallest element of U
add y to S
for each element z of U in increasing order do //trim the list by
eliminating numbers close one to another
if y<(1-c/N)z, set y=z and add z to S
if S contains a number between (1-c)s and s, output yes, otherwise no
O
From: In-Betweener on
Thanks for the help, but I simply didn't understand it. May it be clarified?
It seems more an algorithm than a mathematical, declarative proof.


"Simplane Simple Plane Simulate Plain Simple" <marty.musatov(a)gmail.com>
escreveu na mensagem
news:9d052cb9-8bb3-45b2-842f-1afbe9428917(a)n37g2000prc.googlegroups.com...
(...)
>
> I aim my proof:
>
> initialize a list S to contain one element 0.
> for each i from 1 to N do
> let T be a list consisting of xi+y, for all y in S
> let U be the union of T and S
> sort U
> make S empty
> let y be the smallest element of U
> add y to S
> for each element z of U in increasing order do //trim the list by
> eliminating numbers close one to another
> if y<(1-c/N)z, set y=z and add z to S
> if S contains a number between (1-c)s and s, output yes, otherwise no
> O