# Re: [isabelle] Extensive case splits

```Hello,

first of all... Thanks for all the answers.

I did try that, but after several hours of no real life-sign of Isabelle
I got bored and stopped the process. I thought that it might be an idea,
to somehow break down the stuff to smaller steps, so that you can at
least see if anything is really happening, or if Isabelle is just doing
something stupid for hours. The main problem is that the proof goal is
very, very big (already considered in the number of involved
(in)-equations.

I have added a sample goal of the proof to this mail, to make the
description of this Isabelle problem less abstract.

Regards,
Dominik

On Wed, 2007-08-08 at 12:22 +0100, Lawrence Paulson wrote:
> This sort of case-splitting easily gives rise to huge numbers of
> goals, but this is best done internally. I assume you have already
> tried auto and force on them?
> Larry Paulson
>
> On 6 Aug 2007, at 17:27, Dominik Luecke wrote:
>
> > I am currently trying to prove a theorems that involve lots of case
> > splits in the proof process. I mean the single sub-goals a solvable by
> >
> >   apply (erule disjE)+
> >   apply (simp)
> >   apply (simp)
> >
> > ... Any speedup would help, especially since there are goals that
> > need to be
> > split up into about 23k cases to solve them.
>
--
Dominik Luecke                 Phone +49-421-218-64265
Dept. of Computer Science      Fax   +49-421-218-9864265
University of Bremen           luecke at tzi.de
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x2D82571B

```
```proof (prove): step 11

goal (theorem (DRA24_Composition1), 1 subgoal):
1. !!a b c.
[| ~ (0 = 0 & 0 = 1);
~ (xc(sp(b)) = xc(ep(b)) & yc(sp(b)) = yc(ep(b)));
~ (xc(sp(c)) = xc(ep(c)) & yc(sp(c)) = yc(ep(c)));
False | 0 = 0 & 0 = 0;
0 = 0 & 1 = 1 | 0 = 0 & 1 = 0;
False |
xc(sp(b)) = xc(sp(b)) & yc(sp(b)) = yc(sp(b));
xc(ep(b)) = xc(ep(b)) & yc(ep(b)) = yc(ep(b)) |
xc(ep(b)) = xc(sp(b)) & yc(ep(b)) = yc(sp(b));
False |
xc(sp(c)) = xc(sp(c)) & yc(sp(c)) = yc(sp(c));
xc(ep(c)) = xc(ep(c)) & yc(ep(c)) = yc(ep(c)) |
xc(ep(c)) = xc(sp(c)) & yc(ep(c)) = yc(sp(c));
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(0 + - yc(sp(c))) -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c)))
< 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
xc(sp(c)) = 0 & yc(sp(c)) = 1 -->
(yc(ep(c)) + - 1) * (0 + - 0) +
(0 + - xc(ep(c))) * (0 + - 1)
< 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
False |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
0 = 0 & 1 = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1;
xc(sp(c)) = 0 & yc(sp(c)) = 1 -->
0 < (yc(ep(c)) + - 1) * (0 + - 0) +
(0 + - xc(ep(c))) * (0 + - 1) -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
False |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
0 = 0 & 1 = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1;
xc(ep(c)) = 0 & yc(ep(c)) = 1 -->
0 < (1 + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - 0) * (0 + - yc(sp(c))) -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
False |
0 = 0 & 1 = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
xc(ep(c)) = 0 & yc(ep(c)) = 1 -->
(1 + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - 0) * (0 + - yc(sp(c)))
< 0 -->
0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
False |
0 = 0 & 1 = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 1;
0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) -->
xc(sp(c)) = 0 & yc(sp(c)) = 0 -->
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0)
< 0 -->
0 = 0 & 1 = 0 |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 | False;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
xc(sp(c)) = 0 & yc(sp(c)) = 0 -->
0 < (1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) -->
0 = 0 & 1 = 0 |
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c)) |
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(ep(c)) = 0 & yc(ep(c)) = 1 | False;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c)))
< 0 -->
xc(ep(c)) = 0 & yc(ep(c)) = 0 -->
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0)
< 0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c)) |
0 = 0 & 1 = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0 |
False | xc(sp(c)) = 0 & yc(sp(c)) = 1;
xc(ep(c)) = 0 & yc(ep(c)) = 1 -->
xc(sp(c)) = 0 & yc(sp(c)) = 0 -->
0 = 0 & 1 = 0 | False | 0 = 0 & 1 = 0 | False;
xc(sp(a)) = 0;
(1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) =
0 -->
0 = xc(sp(c)) & 1 = yc(sp(c)) |
0 = xc(sp(c)) & 0 = yc(sp(c));
0 < (1 + - 0) * (xc(sp(b)) + - 0) +
(0 + - 0) * (yc(sp(b)) + - 0);
0 < (1 + - 0) * (xc(ep(b)) + - 0) +
(0 + - 0) * (yc(ep(b)) + - 0);
0 < (yc(ep(b)) + - yc(sp(b))) * (0 + - xc(sp(b))) +
(xc(sp(b)) + - xc(ep(b))) * (0 + - yc(sp(b)));
0 < (yc(ep(b)) + - yc(sp(b))) * (0 + - xc(sp(b))) +
(xc(sp(b)) + - xc(ep(b))) * (1 + - yc(sp(b)));
0 < (yc(ep(b)) + - yc(sp(b))) *
(xc(sp(c)) + - xc(sp(b))) +
(xc(sp(b)) + - xc(ep(b))) *
(yc(sp(c)) + - yc(sp(b)));
0 < (yc(ep(b)) + - yc(sp(b))) *
(xc(ep(c)) + - xc(sp(b))) +
(xc(sp(b)) + - xc(ep(b))) *
(yc(ep(c)) + - yc(sp(b)));
0 < (yc(ep(c)) + - yc(sp(c))) *
(xc(sp(b)) + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(yc(sp(b)) + - yc(sp(c)));
0 < (yc(ep(c)) + - yc(sp(c))) *
(xc(ep(b)) + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(yc(ep(b)) + - yc(sp(c)));
yc(sp(a)) = 0;
(1 + - 0) * (xc(ep(c)) + - 0) +
(0 + - 0) * (yc(ep(c)) + - 0) =
0 -->
0 = xc(ep(c)) & 1 = yc(ep(c)) |
0 = xc(ep(c)) & 0 = yc(ep(c));
~ (0 = xc(sp(b)) & 1 = yc(sp(b)));
~ (0 = xc(sp(b)) & 0 = yc(sp(b)));
~ (0 = xc(ep(b)) & 1 = yc(ep(b)));
~ (0 = xc(ep(b)) & 0 = yc(ep(b)));
~ (xc(ep(b)) = 0 & yc(ep(b)) = 0);
~ (xc(sp(b)) = 0 & yc(sp(b)) = 0);
~ (xc(ep(b)) = 0 & yc(ep(b)) = 1);
~ (xc(sp(b)) = 0 & yc(sp(b)) = 1);
~ (xc(ep(b)) = xc(sp(c)) & yc(ep(b)) = yc(sp(c)));
~ (xc(sp(b)) = xc(sp(c)) & yc(sp(b)) = yc(sp(c)));
~ (xc(ep(b)) = xc(ep(c)) & yc(ep(b)) = yc(ep(c)));
~ (xc(sp(b)) = xc(ep(c)) & yc(sp(b)) = yc(ep(c)));
~ (xc(ep(c)) = xc(sp(b)) & yc(ep(c)) = yc(sp(b)));
~ (xc(sp(c)) = xc(sp(b)) & yc(sp(c)) = yc(sp(b)));
~ (xc(ep(c)) = xc(ep(b)) & yc(ep(c)) = yc(ep(b)));
~ (xc(sp(c)) = xc(ep(b)) & yc(sp(c)) = yc(ep(b)));
xc(ep(a)) = 0; yc(ep(a)) = 1;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) =
0 -->
xc(ep(c)) = 0 & yc(ep(c)) = 0 |
xc(sp(c)) = 0 & yc(sp(c)) = 0;
(yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) =
0 -->
xc(ep(c)) = 0 & yc(ep(c)) = 1 |
xc(sp(c)) = 0 & yc(sp(c)) = 1 |]
==> 0 < (1 + - 0) * (xc(sp(c)) + - 0) +
(0 + - 0) * (yc(sp(c)) + - 0) &
~ (0 = xc(sp(c)) & 1 = yc(sp(c))) &
~ (0 = xc(sp(c)) & 0 = yc(sp(c))) &
(0 = xc(ep(c)) & 0 = yc(ep(c))) &
~ (0 = xc(ep(c)) & 1 = yc(ep(c))) &
(xc(ep(c)) = 0 & yc(ep(c)) = 0) &
~ (xc(sp(c)) = 0 & yc(sp(c)) = 0) &
0 < (yc(ep(c)) + - yc(sp(c))) *
(0 + - xc(sp(c))) +
(xc(sp(c)) + - xc(ep(c))) *
(1 + - yc(sp(c))) &
~ (xc(ep(c)) = 0 & yc(ep(c)) = 1) &
~ (xc(sp(c)) = 0 & yc(sp(c)) = 1)
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.