**Discovery conditions**

We assume that our theorem is not algebraically true
__and__
that
Sat(
**I**
**,t,x**
) is zero (ie. theorem not generally true). This is normal....

Then we compute
**I_d=(**
**I**
**,t)**
(or
**I_d,x**
= Elim(
**y**
,
**I_d**
)).

Since
**t**
does not vanish over all
**I**
, we have that
**I_d**
gives a strictly smaller variety, where the theorem surely will be true...but trivially true!!

More interesting is to consider
**I_d,x**
.

__Proposition__

**I_d,x**
is zero ==>
**t**
vanishes over some privileged components of the hypotheses variety.

**I_d,x**
is zero <==
**t**
vanishes identically over some privileged components of the hypotheses variety.

Proof

==>

If for every privileged component
**t**
does not vanish, we take a

x
-polynomial g that vanishes over all remaining components. Then g vanishes

on the intersection of
*V*
**(**
**I**
**)**
and
**t**
=0, ie. g is in the radical of
**I_d**
, so
**I_d,x**
is not zero.

<==

Conversely, if
**I_d,x**
is not zero, take g in
**I_d,x**
. We have that g is a combination of
**I**
**, t**
, so it vanishes over any component where
**t**
vanishes. It follows that
**t**
can not vanish identically over privileged components.

==========================

**Notice**
: this result can be improved with further conditions on the privileged variables.

If
**I_d,x**
=(h'_1,...,h'_r) is not zero, we are in the
__generally false__
case. The thesis does not hold globally over any of the privileged components.

Then we may consider as new hypotheses variety (
**I**
**, I_d,x**
).

It is a proper subvariety, since the set of privileged variables
**x**
is now dependent.

We start all over again....considering a subset
**x'**
of independent variables. This time (
**I**
**, I_d,x, t**
) does not contain non zero
**x'**
polynomials, so we can hope :-) it is generally true ...

But see the next two examples: