Minimal Comprehensive Groebner Bases

Goals:

1. Decide if the transitivity of non-essentiality is necessary;
2. Prove the generated Groebner basis is minimal, faithful and comprehensive;
3. Extend it to general comprehensive Groebner systems;
4. Try to define the Canonical Minimal Comprehensive Groebner basis.


Done:

1. We do need the transitivity of non-essentiality to guarantee the comprehensiveness of the generated Groebner basis;

2. Faithfulness and comprehensiveness are trivial to prove; Minimality is able to be proved;

3. Extension: replace "LPP_X is x" by "LPP_X divides x".