:: TERMORD semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non trivial LoopStr ;
existence
not for b1 being LoopStr holds b1 is trivial
proof end;
end;

registration
cluster add-associative right_zeroed right_complementable non trivial LoopStr ;
existence
ex b1 being non trivial LoopStr st
( b1 is add-associative & b1 is right_complementable & b1 is right_zeroed )
proof end;
end;

definition
let X be set ;
let b be bag of X;
attr b is non-zero means :: TERMORD:def 1
b <> EmptyBag X;
end;

:: deftheorem defines non-zero TERMORD:def 1 :
for X being set
for b being bag of X holds
( b is non-zero iff b <> EmptyBag X );

theorem Th1: :: TERMORD:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for b1, b2 being bag of X holds
( b1 divides b2 iff ex b being bag of X st b2 = b1 + b )
proof end;

theorem Th2: :: TERMORD:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for p being Series of n,L holds (0_ n,L) *' p = 0_ n,L
proof end;

registration
let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let m1, m2 be Monomial of n,L;
cluster m1 *' m2 -> monomial-like ;
coherence
m1 *' m2 is monomial-like
proof end;
end;

registration
let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c1, c2 be ConstPoly of n,L;
cluster c1 *' c2 -> Constant ;
coherence
c1 *' c2 is Constant
proof end;
end;

theorem Th3: :: TERMORD:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b, b' being bag of n
for a, a' being non-zero Element of L holds Monom (a * a'),(b + b') = (Monom a,b) *' (Monom a',b')
proof end;

theorem :: TERMORD:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for a, a' being Element of L holds (a * a') | n,L = (a | n,L) *' (a' | n,L)
proof end;

Lm1: for n being Ordinal
for T being TermOrder of n
for b being set st b in field T holds
b is bag of n
proof end;

registration
let n be Ordinal;
cluster connected admissible Relation of Bags n, Bags n;
existence
ex b1 being TermOrder of n st
( b1 is admissible & b1 is connected )
proof end;
end;

registration
let n be Nat;
cluster admissible -> admissible well_founded Relation of Bags n, Bags n;
coherence
for b1 being admissible TermOrder of n holds b1 is well_founded
proof end;
end;

definition
let n be Ordinal;
let T be TermOrder of n;
let b, b' be bag of n;
pred b <= b',T means :Def2: :: TERMORD:def 2
[b,b'] in T;
end;

:: deftheorem Def2 defines <= TERMORD:def 2 :
for n being Ordinal
for T being TermOrder of n
for b, b' being bag of n holds
( b <= b',T iff [b,b'] in T );

definition
let n be Ordinal;
let T be TermOrder of n;
let b, b' be bag of n;
pred b < b',T means :Def3: :: TERMORD:def 3
( b <= b',T & b <> b' );
end;

:: deftheorem Def3 defines < TERMORD:def 3 :
for n being Ordinal
for T being TermOrder of n
for b, b' being bag of n holds
( b < b',T iff ( b <= b',T & b <> b' ) );

definition
let n be Ordinal;
let T be TermOrder of n;
let b1, b2 be bag of n;
func min b1,b2,T -> bag of n equals :Def4: :: TERMORD:def 4
b1 if b1 <= b2,T
otherwise b2;
correctness
coherence
( ( b1 <= b2,T implies b1 is bag of n ) & ( not b1 <= b2,T implies b2 is bag of n ) );
consistency
for b1 being bag of n holds verum;
;
func max b1,b2,T -> bag of n equals :Def5: :: TERMORD:def 5
b1 if b2 <= b1,T
otherwise b2;
correctness
coherence
( ( b2 <= b1,T implies b1 is bag of n ) & ( not b2 <= b1,T implies b2 is bag of n ) );
consistency
for b1 being bag of n holds verum;
;
end;

:: deftheorem Def4 defines min TERMORD:def 4 :
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( ( b1 <= b2,T implies min b1,b2,T = b1 ) & ( not b1 <= b2,T implies min b1,b2,T = b2 ) );

:: deftheorem Def5 defines max TERMORD:def 5 :
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( ( b2 <= b1,T implies max b1,b2,T = b1 ) & ( not b2 <= b1,T implies max b1,b2,T = b2 ) );

Lm2: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T
proof end;

Lm3: for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2
proof end;

Lm4: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b in field T
proof end;

theorem Th5: :: TERMORD:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
proof end;

Lm5: for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
proof end;

theorem :: TERMORD:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T by Lm2;

theorem :: TERMORD:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T & b2 <= b1,T holds
b1 = b2 by Lm3;

theorem Th8: :: TERMORD:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T & b2 <= b3,T holds
b1 <= b3,T
proof end;

theorem Th9: :: TERMORD:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T
proof end;

theorem :: TERMORD:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being admissible TermOrder of n
for b1, b2 being bag of n st b1 divides b2 holds
b1 <= b2,T
proof end;

theorem Th11: :: TERMORD:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( min b1,b2,T = b1 or min b1,b2,T = b2 )
proof end;

theorem Th12: :: TERMORD:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( max b1,b2,T = b1 or max b1,b2,T = b2 )
proof end;

Lm6: for n being Ordinal
for T being TermOrder of n
for b being bag of n holds
( min b,b,T = b & max b,b,T = b )
proof end;

theorem :: TERMORD:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min b1,b2,T <= b1,T & min b1,b2,T <= b2,T )
proof end;

theorem Th14: :: TERMORD:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= max b1,b2,T,T & b2 <= max b1,b2,T,T )
proof end;

theorem Th15: :: TERMORD:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min b1,b2,T = min b2,b1,T & max b1,b2,T = max b2,b1,T )
proof end;

theorem :: TERMORD:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( min b1,b2,T = b1 iff max b1,b2,T = b2 )
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HT p,T -> Element of Bags n means :Def6: :: TERMORD:def 6
( ( Support p = {} & it = EmptyBag n ) or ( it in Support p & ( for b being bag of n st b in Support p holds
b <= it,T ) ) );
existence
ex b1 being Element of Bags n st
( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) )
proof end;
uniqueness
for b1, b2 being Element of Bags n st ( ( Support p = {} & b1 = EmptyBag n ) or ( b1 in Support p & ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) & ( ( Support p = {} & b2 = EmptyBag n ) or ( b2 in Support p & ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines HT TERMORD:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b5 being Element of Bags n holds
( b5 = HT p,T iff ( ( Support p = {} & b5 = EmptyBag n ) or ( b5 in Support p & ( for b being bag of n st b in Support p holds
b <= b5,T ) ) ) );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HC p,T -> Element of L equals :: TERMORD:def 7
p . (HT p,T);
correctness
coherence
p . (HT p,T) is Element of L;
;
end;

:: deftheorem defines HC TERMORD:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HC p,T = p . (HT p,T);

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func HM p,T -> Monomial of n,L equals :: TERMORD:def 8
 Monom (HC p,T),(HT p,T);
correctness
coherence
Monom (HC p,T),(HT p,T) is Monomial of n,L;
;
end;

:: deftheorem defines HM TERMORD:def 8 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HM p,T = Monom (HC p,T),(HT p,T);

Lm7: for n being Ordinal
for O being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC p,O = 0. L iff p = 0_ n,L )
proof end;

Lm8: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM p,O) . (HT p,O) = p . (HT p,O)
proof end;

Lm9: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC p,O <> 0. L holds
HT p,O in Support (HM p,O)
proof end;

Lm10: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC p,O = 0. L holds
Support (HM p,O) = {}
proof end;

registration
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial ZeroStr ;
let p be non-zero Polynomial of n,L;
cluster HM p,T -> non-zero ;
coherence
HM p,T is non-zero
proof end;
cluster HC p,T -> non-zero ;
coherence
HC p,T is non-zero
proof end;
end;

Lm11: for n being Ordinal
for O being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT m,O = term m & HC m,O = coefficient m & HM m,O = m )
proof end;

theorem :: TERMORD:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC p,T = 0. L iff p = 0_ n,L ) by Lm7;

theorem :: TERMORD:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds (HM p,T) . (HT p,T) = p . (HT p,T) by Lm8;

theorem Th19: :: TERMORD:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT p,T holds
(HM p,T) . b = 0. L
proof end;

Lm12: for n being Ordinal
for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM p,O) = {} or Support (HM p,O) = {(HT p,O)} )
proof end;

theorem :: TERMORD:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds Support (HM p,T) c= Support p
proof end;

theorem :: TERMORD:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM p,T) = {} or Support (HM p,T) = {(HT p,T)} ) by Lm12;

theorem :: TERMORD:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM p,T) = HT p,T & coefficient (HM p,T) = HC p,T )
proof end;

theorem :: TERMORD:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT m,T = term m & HC m,T = coefficient m & HM m,T = m ) by Lm11;

theorem :: TERMORD:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT c,T = EmptyBag n & HC c,T = c . (EmptyBag n) )
proof end;

theorem :: TERMORD:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for a being Element of L holds
( HT (a | n,L),T = EmptyBag n & HC (a | n,L),T = a )
proof end;

theorem Th26: :: TERMORD:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HT (HM p,T),T = HT p,T
proof end;

theorem :: TERMORD:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC (HM p,T),T = HC p,T
proof end;

theorem :: TERMORD:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HM (HM p,T),T = HM p,T by Lm11;

Lm13: for X being set
for S being Subset of X
for R being Order of X st R is_linear-order holds
R linearly_orders S
proof end;

Lm14: for n being Ordinal
for O being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable unital distributive left_zeroed non trivial doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT p,O) + (HT q,O)) = (p . (HT p,O)) * (q . (HT q,O))
proof end;

theorem Th29: :: TERMORD:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable unital distributive left_zeroed non trivial domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT p,T) + (HT q,T) in Support (p *' q)
proof end;

theorem Th30: :: TERMORD:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
proof end;

theorem Th31: :: TERMORD:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT (p *' q),T = (HT p,T) + (HT q,T)
proof end;

theorem Th32: :: TERMORD:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HC (p *' q),T = (HC p,T) * (HC q,T)
proof end;

theorem :: TERMORD:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HM (p *' q),T = (HM p,T) *' (HM q,T)
proof end;

theorem :: TERMORD:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_zeroed LoopStr
for p, q being Polynomial of n,L holds HT (p + q),T <= max (HT p,T),(HT q,T),T,T
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p be Polynomial of n,L;
func Red p,T -> Polynomial of n,L equals :: TERMORD:def 9
p - (HM p,T);
coherence
p - (HM p,T) is Polynomial of n,L ;
end;

:: deftheorem defines Red TERMORD:def 9 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of n,L holds Red p,T = p - (HM p,T);

Lm15: for n being Ordinal
for O being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds not HT p,O in Support (Red p,O)
proof end;

Lm16: for n being Ordinal
for O being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT p,O holds
b in Support (Red p,O)
proof end;

Lm17: for n being Ordinal
for O being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds Support (Red p,O) = (Support p) \ {(HT p,O)}
proof end;

theorem :: TERMORD:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds Support (Red p,T) c= Support p
proof end;

theorem :: TERMORD:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds Support (Red p,T) = (Support p) \ {(HT p,T)} by Lm17;

Lm18: for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds (Red p,T) . (HT p,T) = 0. L
proof end;

Lm19: for n being Ordinal
for O being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for b being bag of n st b <> HT p,O holds
(Red p,O) . b = p . b
proof end;

theorem :: TERMORD:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds Support ((HM p,T) + (Red p,T)) = Support p
proof end;

theorem :: TERMORD:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds (HM p,T) + (Red p,T) = p
proof end;

theorem :: TERMORD:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L holds (Red p,T) . (HT p,T) = 0. L by Lm18;

theorem :: TERMORD:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for T being connected TermOrder of n
for L being add-associative right_zeroed right_complementable non trivial LoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT p,T holds
(Red p,T) . b = p . b by Lm19;