begin
definition
let X be
set ;
let b be
bag of
X;
end;
theorem Th1:
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 )
begin
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
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:
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:
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;
Lm2:
for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b <= b,T
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
Lm4:
for n being Ordinal
for T being TermOrder of n
for b being bag of n holds b in field T
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 )
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 )
begin
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) )
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))
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))
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)) = {}
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 )
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))} )
Lm13:
for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
Lm14:
for n being Ordinal
for O being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed 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)))
begin
Lm15:
for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
Lm16:
for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
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))
Lm17:
for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
Lm18:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (Red (p,T)) . (HT (p,T)) = 0. L
Lm19:
for n being Ordinal
for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
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