The Dan-O-Matik translation has the "is" word
at the wrong position. He translates:

A number is even iff it is divisible into two equal parts.
ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]

But Euclid defines a composite terminology "even number",
ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]

So Euclid does the right thing compatible with Aristoteles:
https://en.wikipedia.org/wiki/Porphyrian_tree

If you find a concept away from the root towards the
leaves, these concepts do not accumulate dark elements,
outside of their parent concepts.

Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:14:44 UTC+2:
> What about:
>
> /* Dan-O-Matik Style */
> ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
> ALL(a):[Number(a) => [Odd(a) <=> ~EXIST(b):[Number(b) & a=2*b]]]
>
> Can you prove in DC Proof, both Even and Odd will have Dark Elements:
>
> ALL(a):[Even(a) => Odd(s(a))]
>
> Possibly no. But I guess it works with ordinary style:
>
> /* Ordinary Style = Euclid Style */
> ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> ALL(a):[Odd(a) <=> [Number(a) & ~EXIST(b):[Number(b) & a=2*b]]]
> Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:11:24 UTC+2:
> > Thats not how Euclid formulates it:
> >
> > 7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.
> >
> > He also uses the definition format with Even(_) in front:
> >
> > 6. An even number is that which is divisible into two equal parts.
> >
> > Which translates to:
> >
> > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> >
> > Even(a): An even number
> > <=>: is
> > Number(a): that which [number]
> > EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
> >
> > Very easy....
> > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> > > On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> > > > Wait, I am trying to make a better example with Even.
> > > > Ok, this is the better example, which corresponds
> > > > to the usual expectation we have about Even(_):
> > > >
> > > > ALL(a):[Even(a) => ~Even(next(a))]
> > > >
> > > You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

You can draw a little tree:

(Natural) Number
/ \
Even Number Odd Number

The requirement is of course:

Even ⊆ Number and Odd ⊆ Number

But Dan-O-Matik cannot prove it, because going down the
tree, from root to leaves, he introduces dark elements:

/* Not Provable from Dan-O-Matik Style */
ALL(a):[Even(a) => Number(a)] and ALL(a):[Odd(a) => Number(a)]

LMAO!

Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:19:40 UTC+2:
> The Dan-O-Matik translation has the "is" word
> at the wrong position. He translates:
>
> A number is even iff it is divisible into two equal parts.
> ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
>
> But Euclid defines a composite terminology "even number",
> ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
>
> So Euclid does the right thing compatible with Aristoteles:
> https://en.wikipedia.org/wiki/Porphyrian_tree
>
> If you find a concept away from the root towards the
> leaves, these concepts do not accumulate dark elements,
> outside of their parent concepts.
>
> Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:14:44 UTC+2:
> > What about:
> >
> > /* Dan-O-Matik Style */
> > ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
> > ALL(a):[Number(a) => [Odd(a) <=> ~EXIST(b):[Number(b) & a=2*b]]]
> >
> > Can you prove in DC Proof, both Even and Odd will have Dark Elements:
> >
> > ALL(a):[Even(a) => Odd(s(a))]
> >
> > Possibly no. But I guess it works with ordinary style:
> >
> > /* Ordinary Style = Euclid Style */
> > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> > ALL(a):[Odd(a) <=> [Number(a) & ~EXIST(b):[Number(b) & a=2*b]]]
> > Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:11:24 UTC+2:
> > > Thats not how Euclid formulates it:
> > >
> > > 7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.
> > >
> > > He also uses the definition format with Even(_) in front:
> > >
> > > 6. An even number is that which is divisible into two equal parts.
> > >
> > > Which translates to:
> > >
> > > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> > >
> > > Even(a): An even number
> > > <=>: is
> > > Number(a): that which [number]
> > > EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
> > >
> > > Very easy....
> > > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> > > > On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> > > > > Wait, I am trying to make a better example with Even.
> > > > > Ok, this is the better example, which corresponds
> > > > > to the usual expectation we have about Even(_):
> > > > >
> > > > > ALL(a):[Even(a) => ~Even(next(a))]
> > > > >
> > > > You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

Or maybe a little explanation of the subset axiom,
what it does and how it relates to definitions:

ALL(g):EXIST(s):ALL(x):[x e s <=> x e g & D(x)]

Porphyry suggests the Porphyrian tree in his introduction
(in Greek, "Isagoge") to Aristotle's Categories.

g : genera
s : species
D : differentiae

LoL

Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:25:40 UTC+2:
> You can draw a little tree:
>
> (Natural) Number
> / \
> Even Number Odd Number
>
> The requirement is of course:
>
> Even ⊆ Number and Odd ⊆ Number
>
> But Dan-O-Matik cannot prove it, because going down the
> tree, from root to leaves, he introduces dark elements:
>
> /* Not Provable from Dan-O-Matik Style */
> ALL(a):[Even(a) => Number(a)] and ALL(a):[Odd(a) => Number(a)]
>
> LMAO!
> Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:19:40 UTC+2:
> > The Dan-O-Matik translation has the "is" word
> > at the wrong position. He translates:
> >
> > A number is even iff it is divisible into two equal parts.
> > ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
> >
> > But Euclid defines a composite terminology "even number",
> > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> >
> > So Euclid does the right thing compatible with Aristoteles:
> > https://en.wikipedia.org/wiki/Porphyrian_tree
> >
> > If you find a concept away from the root towards the
> > leaves, these concepts do not accumulate dark elements,
> > outside of their parent concepts.
> >
> > Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:14:44 UTC+2:
> > > What about:
> > >
> > > /* Dan-O-Matik Style */
> > > ALL(a):[Number(a) => [Even(a) <=> EXIST(b):[Number(b) & a=2*b]]]
> > > ALL(a):[Number(a) => [Odd(a) <=> ~EXIST(b):[Number(b) & a=2*b]]]
> > >
> > > Can you prove in DC Proof, both Even and Odd will have Dark Elements:
> > >
> > > ALL(a):[Even(a) => Odd(s(a))]
> > >
> > > Possibly no. But I guess it works with ordinary style:
> > >
> > > /* Ordinary Style = Euclid Style */
> > > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> > > ALL(a):[Odd(a) <=> [Number(a) & ~EXIST(b):[Number(b) & a=2*b]]]
> > > Mostowski Collapse schrieb am Sonntag, 8. Mai 2022 um 22:11:24 UTC+2:
> > > > Thats not how Euclid formulates it:
> > > >
> > > > 7. An odd number is that which is not divisible into two equal parts, or that which differs by a unit from an even number.
> > > >
> > > > He also uses the definition format with Even(_) in front:
> > > >
> > > > 6. An even number is that which is divisible into two equal parts.
> > > >
> > > > Which translates to:
> > > >
> > > > ALL(a):[Even(a) <=> [Number(a) & EXIST(b):[Number(b) & a=2*b]]]
> > > >
> > > > Even(a): An even number
> > > > <=>: is
> > > > Number(a): that which [number]
> > > > EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
> > > >
> > > > Very easy....
> > > > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> > > > > On Sunday, May 8, 2022 at 2:45:06 PM UTC-4, Mostowski Collapse wrote:
> > > > > > Wait, I am trying to make a better example with Even.
> > > > > > Ok, this is the better example, which corresponds
> > > > > > to the usual expectation we have about Even(_):
> > > > > >
> > > > > > ALL(a):[Even(a) => ~Even(next(a))]
> > > > > >
> > > > > You would need to restrict the quantifier to N. Then, given the basic rules of arithmetic, you could then use a proof by contradiction.
> > > > > Dan
> > > > >
> > > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > > Visit my Math Blog at http://www.dcproof.wordpress.com

Mostowski Collapse wrote:

> Thats not how Euclid formulates it:
> Even(a): An even number <=>: is Number(a): that which [number]
> EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
> Very easy....
>
> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:

here we go, you two little nazi wankers.

Immortal Regiment. Rome, Italy
https://www.bitchute.com/video/E6dPfH2IEpo6/

On Sunday, May 8, 2022 at 5:07:43 PM UTC-4, Lupe Kaza wrote:
> Mostowski Collapse wrote:
>
> > Thats not how Euclid formulates it:
> > Even(a): An even number <=>: is Number(a): that which [number]
> > EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
> > Very easy....
> >
> > Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
> here we go, you two little nazi wankers.
>

How many times must I tell you, Nazi boy?

WAR OF AGRESSION = NAZI

So, it's off to the Ukrainian front next week? I wish I could say it was nice knowing you.

On 5/8/2022 3:25 PM, Dan Christensen wrote:
> On Sunday, May 8, 2022 at 5:07:43 PM UTC-4, Lupe Kaza wrote:
>> Mostowski Collapse wrote:
>>
>>> Thats not how Euclid formulates it:
>>> Even(a): An even number <=>: is Number(a): that which [number]
>>> EXIST(b):[Number(b) & a=2*b]: is divisible into two equal parts
>>> Very easy....
>>>
>>> Dan Christensen schrieb am Sonntag, 8. Mai 2022 um 21:59:28 UTC+2:
>> here we go, you two little nazi wankers.
>>
>
> How many times must I tell you, Nazi boy?
>
> WAR OF AGRESSION = NAZI
>
> So, it's off to the Ukrainian front next week? I wish I could say it was nice knowing you.
>

Should we help? If so, we have to be ready to fight a superpower.
Sending highly advanced weapons to the Ukrainian's, okay... Well, get
ready for a real war that extends well beyond the borders of that
country. WWIII. Are we all ready to fight it to the end? If not, then we
are not ready to win WWIII. Humm... Any thoughts?

The US southern border is wide open. If we are ready to go to real war,
we need to secure the borders.

Actually I have to retract what I said, mostly malicious
crank efforts by Dan Christensen. Now he hallucinates
an evenness concept, probably only to

summon more dark matter.

What one could do, is define a parameterized Even
that takes the additive structure <D,+> as a parameter,
here written in curried form:

ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]

We could then define different even on different structures:

Even(N,+N) = EvenN
Even(Z,+Z) = EvenZ
Even(Q,+Q) = EvenQ
Even(R,+R) = EvenR

But already EvenQ collapses:

EvenN =/= N
EvenZ =/= Z
EvenQ = Q
EvenR = R

Because every rational number can be represented as the
sum of two rational numbers. a/b = a/2b + a/2b. So
EvenQ does not anymore agree with EvenN on N.

So lump summing EvenN, EvenZ, EvenQ and EvenR
into one Even will not work. It already goes wrong inside
the domain D, nothing to do with outside domain D.

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 08:53:13 UTC+2:
> Actually I have to retract what I said, mostly malicious
> crank efforts by Dan Christensen. Now he hallucinates
> an evenness concept, probably only to
>
> summon more dark matter.

That rational numbers do not anymore have even/odd,
they have the dense property, i.e. that for two rational
numbers p < q, there is a third rational number p < r

and r < q, the rational numbers live in a dense order:

That is, for any two elements, one less than the other,
there is another element between them.
https://en.wikipedia.org/wiki/Dense_order

The rational numbers are even binarily dense, i.e.
if 0 < q then 0 < q/2 & q/2 < q. And if q < 0 then
q < q/2 and q/2 < 0.

Maybe they chose the name "dense" to honor
Dan Christensens dense stupidity?

LoL

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 09:26:23 UTC+2:
> What one could do, is define a parameterized Even
> that takes the additive structure <D,+> as a parameter,
> here written in curried form:
>
> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
>
> We could then define different even on different structures:
>
> Even(N,+N) = EvenN
> Even(Z,+Z) = EvenZ
> Even(Q,+Q) = EvenQ
> Even(R,+R) = EvenR
>
> But already EvenQ collapses:
>
> EvenN =/= N
> EvenZ =/= Z
> EvenQ = Q
> EvenR = R
>
> Because every rational number can be represented as the
> sum of two rational numbers. a/b = a/2b + a/2b. So
> EvenQ does not anymore agree with EvenN on N.
>
> So lump summing EvenN, EvenZ, EvenQ and EvenR
> into one Even will not work. It already goes wrong inside
> the domain D, nothing to do with outside domain D.
> Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 08:53:13 UTC+2:
> > Actually I have to retract what I said, mostly malicious
> > crank efforts by Dan Christensen. Now he hallucinates
> > an evenness concept, probably only to
> >
> > summon more dark matter.

On Wednesday, May 11, 2022 at 3:26:23 AM UTC-4, Mostowski Collapse wrote:
> What one could do, is define a parameterized Even
> that takes the additive structure <D,+> as a parameter,
> here written in curried form:
>
> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
>

Still plagued by wonky results. Why not the more conventional alternative:

ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

You can try both:

Case 1:
ALL(D):ALL(+):ALL(a):[a in D => [Even(D,+)(a) <=> EXIST(b):[b in D & a=2*b]]]

Case 2:
ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]

You will still see that EvenQ ∩ N =\= EvenN.

Proof:
EvenQ ∩ N = N. But 1 e N and ~(1 e EvenN)

Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 14:41:16 UTC+2:
> On Wednesday, May 11, 2022 at 3:26:23 AM UTC-4, Mostowski Collapse wrote:
> > What one could do, is define a parameterized Even
> > that takes the additive structure <D,+> as a parameter,
> > here written in curried form:
> >
> > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> >
> Still plagued by wonky results. Why not the more conventional alternative:
>
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

With your case 1 definition that is motivated by general
evenness, you only get Dan-O-Matiks meningeal paresis:

Case 1: Dan-O-Matiks Syphilis Brain
ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

You can even not prove:

/* Not Provable in Syphilis Brain World */
ALL(a):[~a e n => ~Even(a)]

So we don't know what Even is outside of n. Is it EvenN
or EvenQ? For EvenQ we have EvenQ(a) when ~a e n
and a e q. So EvenQ is indeed a counter example to

the above. But EvenQ is also a counter example to the
idea to make Even open, . Since EvenQ even starts to
disagree with EvenN, we have EvenQ ∩ N =\= EvenN. So I

would say Dan Christensens problem is progressed neurosyphilis

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 15:02:20 UTC+2:
> You can try both:
>
> Case 1:
> ALL(D):ALL(+):ALL(a):[a in D => [Even(D,+)(a) <=> EXIST(b):[b in D & a=2*b]]]
>
> Case 2:
> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> You will still see that EvenQ ∩ N =\= EvenN.
>
> Proof:
> EvenQ ∩ N = N. But 1 e N and ~(1 e EvenN)
> Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 14:41:16 UTC+2:
> > On Wednesday, May 11, 2022 at 3:26:23 AM UTC-4, Mostowski Collapse wrote:
> > > What one could do, is define a parameterized Even
> > > that takes the additive structure <D,+> as a parameter,
> > > here written in curried form:
> > >
> > > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> > >
> > Still plagued by wonky results. Why not the more conventional alternative:
> >
> > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen, can you send us a picture of yourself?
Does it look like this here:

https://www.fazialis.de/de/gesichtslaehmung/#lightbox[4859]

This could improve the diagnosis of your mental
illness and progressed neurosyphilis.

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 15:22:42 UTC+2:
> With your case 1 definition that is motivated by general
> evenness, you only get Dan-O-Matiks meningeal paresis:
>
> Case 1: Dan-O-Matiks Syphilis Brain
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> You can even not prove:
>
> /* Not Provable in Syphilis Brain World */
> ALL(a):[~a e n => ~Even(a)]
>
> So we don't know what Even is outside of n. Is it EvenN
> or EvenQ? For EvenQ we have EvenQ(a) when ~a e n
> and a e q. So EvenQ is indeed a counter example to
>
> the above. But EvenQ is also a counter example to the
> idea to make Even open, . Since EvenQ even starts to
> disagree with EvenN, we have EvenQ ∩ N =\= EvenN. So I
>
> would say Dan Christensens problem is progressed neurosyphilis
> Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 15:02:20 UTC+2:
> > You can try both:
> >
> > Case 1:
> > ALL(D):ALL(+):ALL(a):[a in D => [Even(D,+)(a) <=> EXIST(b):[b in D & a=2*b]]]
> >
> > Case 2:
> > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> > You will still see that EvenQ ∩ N =\= EvenN.
> >
> > Proof:
> > EvenQ ∩ N = N. But 1 e N and ~(1 e EvenN)
> > Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 14:41:16 UTC+2:
> > > On Wednesday, May 11, 2022 at 3:26:23 AM UTC-4, Mostowski Collapse wrote:
> > > > What one could do, is define a parameterized Even
> > > > that takes the additive structure <D,+> as a parameter,
> > > > here written in curried form:
> > > >
> > > > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> > > >
> > > Still plagued by wonky results. Why not the more conventional alternative:
> > >
> > > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, May 11, 2022 at 9:22:42 AM UTC-4, Mostowski Collapse wrote:
> With your case 1 definition that is motivated by general
> evenness

Just evenness on the natural numbers.

>
> Case 1:
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> You can even not prove:
>
> /* Not Provable */
> ALL(a):[~a e n => ~Even(a)]
>

You mean: ALL(a):[~a e n => Odd(a)] is not provable. And that is GOOD thing!

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

No its both, no pink unicorns:

ALL(a):[~a e n => ~Even(a)]
ALL(a):[~a e n => ~Odd(a)]

Whats wrong with you?

The even and odd natural numbers are a disjoint
familiy of two sets that make up the set of the
natural numbers. In particular you can prove:

Challenge 1:
ALL(a):[a e n <=> [Even(a) v Odd(a)]]
Challenge 2:
ALL(a):[a e {} <=> [Even(a) & Odd(a)]]

You cannot prove the above with your demented
case 1 nonsense, which came directly from
your syphilis brain.

Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 17:04:01 UTC+2:
> On Wednesday, May 11, 2022 at 9:22:42 AM UTC-4, Mostowski Collapse wrote:
> > With your case 1 definition that is motivated by general
> > evenness
> Just evenness on the natural numbers.
>
> >
> > Case 1:
> > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > You can even not prove:
> >
> > /* Not Provable */
> > ALL(a):[~a e n => ~Even(a)]
> >
> You mean: ALL(a):[~a e n => Odd(a)] is not provable. And that is GOOD thing!
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, May 11, 2022 at 11:20:24 AM UTC-4, Mostowski Collapse (wrote:
> No its both, no pink unicorns:
> ALL(a):[~a e n => ~Even(a)]
> ALL(a):[~a e n => ~Odd(a)]
>

Not possible using the conventional definitions of Even and Odd. Maybe with one of your drug-induced, unconventional alternatives, Jan Burse?

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, May 11, 2022 at 12:26:23 AM UTC-7, Mostowski Collapse wrote:
> What one could do, is define a parameterized Even
> that takes the additive structure <D,+> as a parameter,
> here written in curried form:
>
> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
>
> We could then define different even on different structures:
>
> Even(N,+N) = EvenN
> Even(Z,+Z) = EvenZ
> Even(Q,+Q) = EvenQ
> Even(R,+R) = EvenR
>
> But already EvenQ collapses:
>
> EvenN =/= N
> EvenZ =/= Z
> EvenQ = Q
> EvenR = R
>
> Because every rational number can be represented as the
> sum of two rational numbers. a/b = a/2b + a/2b. So
> EvenQ does not anymore agree with EvenN on N.

Why should it?

You're playing a shell game. The respective parameters are Even(N,+N) and Even(Q,+Q). But when you do the lumping you are only considering N as a subset of Q, BUT NOT the relationship between +N and +Q. So all you've arrived at is that Even(N,+Q) is not the same as Even(N,+N). So what?

If your a/2b is not integral, then your a/2b + a/2b does not exist in N+

> So lump summing EvenN, EvenZ, EvenQ and EvenR
> into one Even will not work. It already goes wrong inside
> the domain D, nothing to do with outside domain D.

Consider the 'structure' of even and odd functions on the integers (rational numbers, real numbers, ...). We can identify an integer n with the constant function
f(x) = n for all x in our domain.

Then when we 'lump', all integers are even, and zero is both even and odd.

What does that prove? What does it say about your 'lumping'?

Obviously possible. You never heard of a congrence
relations such as for example:

n = m mod k ?

Its very easy:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

Obviously we have:

ALL(a):[~a e n => ~Even(a)]
ALL(a):[~a e n => ~Odd(a)]

Whats your counter example to the above two?

Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 17:50:34 UTC+2:
> On Wednesday, May 11, 2022 at 11:20:24 AM UTC-4, Mostowski Collapse (wrote:
> > No its both, no pink unicorns:
> > ALL(a):[~a e n => ~Even(a)]
> > ALL(a):[~a e n => ~Odd(a)]
> >
> Not possible using the conventional definitions of Even and Odd. Maybe with one of your drug-induced, unconventional alternatives, Jan Burse?
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

I am not advocating lumping. I try to understand what
Dan Christensen means by evenness and why he
oposes to these two definitions for even and

odd natural numbers:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

Which is a little crazy to oppose the two, to
say the least what this implies for the mental
state of Dan Christensen.

FredJeffries schrieb am Mittwoch, 11. Mai 2022 um 17:50:53 UTC+2:
> On Wednesday, May 11, 2022 at 12:26:23 AM UTC-7, Mostowski Collapse wrote:
> > What one could do, is define a parameterized Even
> > that takes the additive structure <D,+> as a parameter,
> > here written in curried form:
> >
> > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
> >
> > We could then define different even on different structures:
> >
> > Even(N,+N) = EvenN
> > Even(Z,+Z) = EvenZ
> > Even(Q,+Q) = EvenQ
> > Even(R,+R) = EvenR
> >
> > But already EvenQ collapses:
> >
> > EvenN =/= N
> > EvenZ =/= Z
> > EvenQ = Q
> > EvenR = R
> >
> > Because every rational number can be represented as the
> > sum of two rational numbers. a/b = a/2b + a/2b. So
> > EvenQ does not anymore agree with EvenN on N.
> Why should it?
>
> You're playing a shell game. The respective parameters are Even(N,+N) and Even(Q,+Q). But when you do the lumping you are only considering N as a subset of Q, BUT NOT the relationship between +N and +Q. So all you've arrived at is that Even(N,+Q) is not the same as Even(N,+N). So what?
>
> If your a/2b is not integral, then your a/2b + a/2b does not exist in N+
> > So lump summing EvenN, EvenZ, EvenQ and EvenR
> > into one Even will not work. It already goes wrong inside
> > the domain D, nothing to do with outside domain D.
> Consider the 'structure' of even and odd functions on the integers (rational numbers, real numbers, ...). We can identify an integer n with the constant function
> f(x) = n for all x in our domain.
>
> Then when we 'lump', all integers are even, and zero is both even and odd..
>
> What does that prove? What does it say about your 'lumping'?

The even/odd functions give a tri-partition of
a space (if you count also what is outside of
the space, you get a tetra-partition)

The even/odd numbers give a bi-partition of
a set (if you count also what is outside of
the set, you get a tri-partition).

The even and odd functions are not defined on the
basis of these two criteria, because even/odd
functions are a tri-partition, it will be

impossible to use these two criteria:

EXIST(b):[b e D & a=b+b]
~EXIST(b):[b e D & a=b+b]

Thats what I used here:

> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D &
EXIST(b):[b e D & b+b=a]] %%% here

And the corresponding Odd would be:

ALL(D):ALL(+):ALL(a):[Odd(D,+)(a) <=> a e D &
~EXIST(b):[b e D & b+b=a]] %%% here

There is now an other form of collapse:

OddN =\= {}
OddZ =\= {}
OddQ = {}
OddR = {}

The collapse has nothing todo that the
bi-partition would turn into a tri-partition.
Its just that the partitions get trivial,

i.e. the empty set {} or the full set of the
original numbers, i.e. D.

Mostowski Collapse schrieb:
> I am not advocating lumping. I try to understand what
> Dan Christensen means by evenness and why he
> oposes to these two definitions for even and
>
> odd natural numbers:
>
> Even = { a e n | a = 0 mod 2 }
> Odd = { a e n | a = 1 mod 2 }
>
> Which is a little crazy to oppose the two, to
> say the least what this implies for the mental
> state of Dan Christensen.
>
> FredJeffries schrieb am Mittwoch, 11. Mai 2022 um 17:50:53 UTC+2:
>> On Wednesday, May 11, 2022 at 12:26:23 AM UTC-7, Mostowski Collapse wrote:
>>> What one could do, is define a parameterized Even
>>> that takes the additive structure <D,+> as a parameter,
>>> here written in curried form:
>>>
>>> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]
>>>
>>> We could then define different even on different structures:
>>>
>>> Even(N,+N) = EvenN
>>> Even(Z,+Z) = EvenZ
>>> Even(Q,+Q) = EvenQ
>>> Even(R,+R) = EvenR
>>>
>>> But already EvenQ collapses:
>>>
>>> EvenN =/= N
>>> EvenZ =/= Z
>>> EvenQ = Q
>>> EvenR = R
>>>
>>> Because every rational number can be represented as the
>>> sum of two rational numbers. a/b = a/2b + a/2b. So
>>> EvenQ does not anymore agree with EvenN on N.
>> Why should it?
>>
>> You're playing a shell game. The respective parameters are Even(N,+N) and Even(Q,+Q). But when you do the lumping you are only considering N as a subset of Q, BUT NOT the relationship between +N and +Q. So all you've arrived at is that Even(N,+Q) is not the same as Even(N,+N). So what?
>>
>> If your a/2b is not integral, then your a/2b + a/2b does not exist in N+
>>> So lump summing EvenN, EvenZ, EvenQ and EvenR
>>> into one Even will not work. It already goes wrong inside
>>> the domain D, nothing to do with outside domain D.
>> Consider the 'structure' of even and odd functions on the integers (rational numbers, real numbers, ...). We can identify an integer n with the constant function
>> f(x) = n for all x in our domain.
>>
>> Then when we 'lump', all integers are even, and zero is both even and odd.
>>
>> What does that prove? What does it say about your 'lumping'?

Corr: Its a four partition, not a tri-partition.

Its null function, proper even function, proper
odd function and all the rest of the functions.
So the even/odd functions give a four-partition

of a space (if you count also what is outside of
the space, you get a five-partition). Also there is
a decomposition theorem as every function f,

can be represented as, and it is unique!

f(x) = f+(x) + f-(x)

Where f+ is a proper even function or the null
function, and f- is a proper odd function or the
null function.

What should be the decomposition theorem be
for natural numbers, based on odd and even
natural numbers? Its not a four-partition,

only a bi-partition?

Mostowski Collapse schrieb:
> The even/odd functions give a tri-partition of
> a space (if you count also what is outside of
> the space, you get a tetra-partition)
>
> The even/odd numbers give a bi-partition of
> a set (if you count also what is outside of
> the set, you get a tri-partition).
>
> The even and odd functions are not defined on the
> basis of these two criteria, because even/odd
> functions are a tri-partition, it will be
>
> impossible to use these two criteria:
>
> EXIST(b):[b e D & a=b+b]
> ~EXIST(b):[b e D & a=b+b]
>
> Thats what I used here:
>
> > ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D &
> EXIST(b):[b e D & b+b=a]]    %%% here
>
> And the corresponding Odd would be:
>
> ALL(D):ALL(+):ALL(a):[Odd(D,+)(a) <=> a e D &
> ~EXIST(b):[b e D & b+b=a]]   %%% here
>
> There is now an other form of collapse:
>
> OddN =\= {}
> OddZ =\= {}
> OddQ = {}
> OddR = {}
>
> The collapse has nothing todo that the
> bi-partition would turn into a tri-partition.
> Its just that the partitions get trivial,
>
> i.e. the empty set {} or the full set of the
> original numbers, i.e. D.
>
> Mostowski Collapse schrieb:
>> I am not advocating lumping. I try to understand what
>> Dan Christensen means by evenness and why he
>> oposes to these two definitions for even and
>>
>> odd natural numbers:
>>
>> Even = { a e n | a = 0 mod 2 }
>> Odd = { a e n | a = 1 mod 2 }
>>
>> Which is a little crazy to oppose the two, to
>> say the least what this implies for the mental
>> state of Dan Christensen.
>>
>> FredJeffries schrieb am Mittwoch, 11. Mai 2022 um 17:50:53 UTC+2:
>>> On Wednesday, May 11, 2022 at 12:26:23 AM UTC-7, Mostowski Collapse
>>> wrote:
>>>> What one could do, is define a parameterized Even
>>>> that takes the additive structure <D,+> as a parameter,
>>>> here written in curried form:
>>>>
>>>> ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D &
>>>> b+b=a]]
>>>>
>>>> We could then define different even on different structures:
>>>>
>>>> Even(N,+N) = EvenN
>>>> Even(Z,+Z) = EvenZ
>>>> Even(Q,+Q) = EvenQ
>>>> Even(R,+R) = EvenR
>>>>
>>>> But already EvenQ collapses:
>>>>
>>>> EvenN =/= N
>>>> EvenZ =/= Z
>>>> EvenQ = Q
>>>> EvenR = R
>>>>
>>>> Because every rational number can be represented as the
>>>> sum of two rational numbers. a/b = a/2b + a/2b. So
>>>> EvenQ does not anymore agree with EvenN on N.
>>> Why should it?
>>>
>>> You're playing a shell game. The respective parameters are Even(N,+N)
>>> and Even(Q,+Q). But when you do the lumping you are only considering
>>> N as a subset of Q, BUT NOT the relationship between +N and +Q. So
>>> all you've arrived at is that Even(N,+Q) is not the same as
>>> Even(N,+N). So what?
>>>
>>> If your a/2b is not integral, then your a/2b + a/2b does not exist in N+
>>>> So lump summing EvenN, EvenZ, EvenQ and EvenR
>>>> into one Even will not work. It already goes wrong inside
>>>> the domain D, nothing to do with outside domain D.
>>> Consider the 'structure' of even and odd functions on the integers
>>> (rational numbers, real numbers, ...). We can identify an integer n
>>> with the constant function
>>> f(x) = n for all x in our domain.
>>>
>>> Then when we 'lump', all integers are even, and zero is both even and
>>> odd.
>>>
>>> What does that prove? What does it say about your 'lumping'?
>

On Wednesday, May 11, 2022 at 12:07:22 PM UTC-4, Mostowski Collapse wrote:
> I am not advocating lumping. I try to understand what
> Dan Christensen means by evenness and why he
> oposes to these two definitions for even and
>
> odd natural numbers:
> Even = { a e n | a = 0 mod 2 }
> Odd = { a e n | a = 1 mod 2 }

Liar. Not my idea, and never wrote that, but at least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown. Don't you feel silly now?

As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:

1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)

Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).

I hope this helps.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

With the standard definition you can prove
everything, that you cannot prove with your Dan
Christensen nonsense. Examples that become provable

not using the Dan Christensen nonsense:

ALL(a):[~a in n => ~Even(a)]
ALL(a):[~a in n => ~Odd(a)]
ALL(a):[a e n <=> [Even(a) v Odd(a)]]
ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
Etc…

On the other hand with Dan Christensen syphilitic brain
definition one cannot prove these things, one is bugged with
dark elements. If you want you can be also

more specific and distinguish:

EvenN = { a e n | a = 0 mod 2 }
OddN = { a e n | a = 1 mod 2 }
EvenZ = { a e n | a = 0 mod 2 }
OddZ = { a e n | a = 1 mod 2 }

This is in case you have an application where you
also want to have a notion of odd/even integer.
Or some other EvenX/OddX. But to have a well

defined definition you need to be specific.

https://en.m.wikipedia.org/wiki/Well-defined

Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 20:47:36 UTC+2:
> On Wednesday, May 11, 2022 at 12:07:22 PM UTC-4, Mostowski Collapse wrote:
> > I am not advocating lumping. I try to understand what
> > Dan Christensen means by evenness and why he
> > oposes to these two definitions for even and
> >
> > odd natural numbers:
> > Even = { a e n | a = 0 mod 2 }
> > Odd = { a e n | a = 1 mod 2 }
> Liar. Not my idea, and never wrote that, but at least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown. Don't you feel silly now?
>
> As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:
>
> 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> 2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
>
> Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).
>
> I hope this helps.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Corr.: Typo

EvenN = { a e n | a = 0 mod 2 }
OddN = { a e n | a = 1 mod 2 }
EvenZ = { a e z | a = 0 mod 2 }
OddZ = { a e z | a = 1 mod 2 }

This is in case you have an application where you
also want to have a notion of odd/even integer.
Or some other EvenX/OddX. But to have a well

defined definition you need to be specific.

https://en.m.wikipedia.org/wiki/Well-defined

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 20:53:31 UTC+2:
> With the standard definition you can prove
> everything, that you cannot prove with your Dan
> Christensen nonsense. Examples that become provable
>
> not using the Dan Christensen nonsense:
>
> ALL(a):[~a in n => ~Even(a)]
> ALL(a):[~a in n => ~Odd(a)]
> ALL(a):[a e n <=> [Even(a) v Odd(a)]]
> ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
> Etc…
>
> On the other hand with Dan Christensen syphilitic brain
> definition one cannot prove these things, one is bugged with
> dark elements. If you want you can be also
>
> more specific and distinguish:
>
> EvenN = { a e n | a = 0 mod 2 }
> OddN = { a e n | a = 1 mod 2 }
> EvenZ = { a e n | a = 0 mod 2 }
> OddZ = { a e n | a = 1 mod 2 }
>
> This is in case you have an application where you
> also want to have a notion of odd/even integer.
> Or some other EvenX/OddX. But to have a well
>
> defined definition you need to be specific.
>
> https://en.m.wikipedia.org/wiki/Well-defined
> Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 20:47:36 UTC+2:
> > On Wednesday, May 11, 2022 at 12:07:22 PM UTC-4, Mostowski Collapse wrote:
> > > I am not advocating lumping. I try to understand what
> > > Dan Christensen means by evenness and why he
> > > oposes to these two definitions for even and
> > >
> > > odd natural numbers:
> > > Even = { a e n | a = 0 mod 2 }
> > > Odd = { a e n | a = 1 mod 2 }
> > Liar. Not my idea, and never wrote that, but at least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown. Don't you feel silly now?
> >
> > As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:
> >
> > 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > 2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> >
> > Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).
> >
> > I hope this helps.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

ALL(a):[a e {} <=> [Even(a) & Odd(a)]] is provable with
your definition, but the others are not:

Counter Models to Dans Definition:

ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)

Via https://www.umsu.de/trees:

Counter Model 1: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧
(∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.
Domain: { 0, 1, 2}
N: { 0,1 }
E: { 0,2 }
O: { 1 }
D: { 0 }

Counter Model 2: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Oa) is invalid.
Countermodel:
Domain: { 0, 1, 2 }
N: { 0,1 }
E: { 0 }
O: { 1,2 }
D: { 0 }

Counter Model 3: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(Na ↔ (Oa ∨ Ea)) is invalid.
Domain: { 0, 1, 2 }
N: { 0,1 }
E: { 0,2 }
O: { 1 }
D: { 0 }

Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 20:55:29 UTC+2:
> Corr.: Typo
> EvenN = { a e n | a = 0 mod 2 }
> OddN = { a e n | a = 1 mod 2 }
> EvenZ = { a e z | a = 0 mod 2 }
> OddZ = { a e z | a = 1 mod 2 }
> This is in case you have an application where you
> also want to have a notion of odd/even integer.
> Or some other EvenX/OddX. But to have a well
>
> defined definition you need to be specific.
>
> https://en.m.wikipedia.org/wiki/Well-defined
> Mostowski Collapse schrieb am Mittwoch, 11. Mai 2022 um 20:53:31 UTC+2:
> > With the standard definition you can prove
> > everything, that you cannot prove with your Dan
> > Christensen nonsense. Examples that become provable
> >
> > not using the Dan Christensen nonsense:
> >
> > ALL(a):[~a in n => ~Even(a)]
> > ALL(a):[~a in n => ~Odd(a)]
> > ALL(a):[a e n <=> [Even(a) v Odd(a)]]
> > ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
> > Etc…
> >
> > On the other hand with Dan Christensen syphilitic brain
> > definition one cannot prove these things, one is bugged with
> > dark elements. If you want you can be also
> >
> > more specific and distinguish:
> >
> > EvenN = { a e n | a = 0 mod 2 }
> > OddN = { a e n | a = 1 mod 2 }
> > EvenZ = { a e n | a = 0 mod 2 }
> > OddZ = { a e n | a = 1 mod 2 }
> >
> > This is in case you have an application where you
> > also want to have a notion of odd/even integer.
> > Or some other EvenX/OddX. But to have a well
> >
> > defined definition you need to be specific.
> >
> > https://en.m.wikipedia.org/wiki/Well-defined
> > Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 20:47:36 UTC+2:
> > > On Wednesday, May 11, 2022 at 12:07:22 PM UTC-4, Mostowski Collapse wrote:
> > > > I am not advocating lumping. I try to understand what
> > > > Dan Christensen means by evenness and why he
> > > > oposes to these two definitions for even and
> > > >
> > > > odd natural numbers:
> > > > Even = { a e n | a = 0 mod 2 }
> > > > Odd = { a e n | a = 1 mod 2 }
> > > Liar. Not my idea, and never wrote that, but at least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown. Don't you feel silly now?
> > >
> > > As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:
> > >
> > > 1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > > 2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> > >
> > > Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).
> > >
> > > I hope this helps.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com