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.