:: Term Orders
:: by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

registration
cluster non trivial for addLoopStr ;
existence
 not for b1 being addLoopStr holds b1 is trivial
proofend;
end;

registration
cluster non empty non trivial right_complementable add-associative right_zeroed for addLoopStr ;
existence
 ex b1 being non trivial addLoopStr st
( b1 is add-associative & b1 is right_complementable & b1 is right_zeroed )
proofend;
end;

definition
let X be set ;
let b be bag of X;
attrb is zero  means :: TERMORD:def 1
b = EmptyBag X;
end;

:: deftheorem  defines zero TERMORD:def_1_:_
 for X being set
for b being bag of X holds
( b is zero iff b = EmptyBag X );

theorem Th1: :: TERMORD:1
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 )
proofend;

theorem Th2: :: TERMORD:2
for n being Ordinal
for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
proofend;

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

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

theorem Th3: :: TERMORD:3
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for b, b9 being bag of n
for a, a9 being non zero Element of L holds Monom ((a * a9),(b + b9)) = (Monom (a,b)) *' (Monom (a9,b9))
proofend;

theorem :: TERMORD:4
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for a, a9 being Element of L holds (a * a9) | (n,L) = (a | (n,L)) *' (a9 | (n,L))
proofend;

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
proofend;

registration
let n be Ordinal;
cluster Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric connected transitive admissible for Element of K19(K20((Bags n),(Bags n)));
existence
 ex b1 being TermOrder of n st
( b1 is admissible & b1 is connected )
proofend;
end;

:: theorem 5.5 (ii), p. 190
registration
let n be Nat;
cluster total reflexive antisymmetric transitive admissible  ->  well_founded admissible for Element of K19(K20((Bags n),(Bags n)));
coherence
 for b1 being admissible TermOrder of n holds b1 is well_founded
proofend;
end;

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

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

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

:: deftheorem Def3 defines < TERMORD:def_3_:_
 for n being Ordinal
for T being TermOrder of n
for b, b9 being bag of n holds
( b < b9,T iff ( b <= b9,T &amp; b <> b9 ) );

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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( 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
proofend;

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

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

theorem Th5: :: TERMORD:5
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 )
proofend;

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 )
proofend;

theorem :: TERMORD:6
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
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n st b1 <= b2,T &amp; b2 <= b1,T holds
b1 = b2 by Lm3;

theorem Th8: :: TERMORD:8
for n being Ordinal
for T being TermOrder of n
for b1, b2, b3 being bag of n st b1 <= b2,T &amp; b2 <= b3,T holds
b1 <= b3,T
proofend;

theorem Th9: :: TERMORD:9
for n being Ordinal
for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T
proofend;

theorem :: TERMORD:10
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
proofend;

theorem Th11: :: TERMORD:11
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 )
proofend;

theorem Th12: :: TERMORD:12
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 )
proofend;

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

theorem :: TERMORD:13
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 &amp; min (b1,b2,T) <= b2,T )
proofend;

theorem Th14: :: TERMORD:14
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 &amp; b2 <= max (b1,b2,T),T )
proofend;

theorem Th15: :: TERMORD:15
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) &amp; max (b1,b2,T) = max (b2,b1,T) )
proofend;

theorem :: TERMORD:16
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 )
proofend;

begin

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 = {} &amp; it = EmptyBag n ) or ( it in Support p &amp; ( 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 = {} &amp; b1 = EmptyBag n ) or ( b1 in Support p &amp; ( for b being bag of n st b in Support p holds
b <= b1,T ) ) )
proofend;
uniqueness
 for b1, b2 being Element of Bags n st ( ( Support p = {} &amp; b1 = EmptyBag n ) or ( b1 in Support p &amp; ( for b being bag of n st b in Support p holds
b <= b1,T ) ) ) &amp; ( ( Support p = {} &amp; b2 = EmptyBag n ) or ( b2 in Support p &amp; ( for b being bag of n st b in Support p holds
b <= b2,T ) ) ) holds
b1 = b2
proofend;
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 = {} &amp; b5 = EmptyBag n ) or ( b5 in Support p &amp; ( 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) )
proofend;

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))
proofend;

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))
proofend;

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)) = {}
proofend;

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
proofend;
cluster HC (p,T) ->  non zero ;
coherence
 not HC (p,T) is zero
proofend;
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 &amp; HC (m,O) = coefficient m &amp; HM (m,O) = m )
proofend;

theorem :: TERMORD:17
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
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
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
proofend;

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))} )
proofend;

theorem :: TERMORD:20
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
proofend;

theorem :: TERMORD:21
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
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) &amp; coefficient (HM (p,T)) = HC (p,T) )
proofend;

theorem :: TERMORD:23
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 &amp; HC (m,T) = coefficient m &amp; HM (m,T) = m ) by Lm11;

theorem :: TERMORD:24
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 &amp; HC (c,T) = c . (EmptyBag n) )
proofend;

theorem :: TERMORD:25
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 &amp; HC ((a | (n,L)),T) = a )
proofend;

theorem Th26: :: TERMORD:26
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)
proofend;

theorem :: TERMORD:27
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)
proofend;

theorem :: TERMORD:28
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 being_linear-order holds
R linearly_orders S
proofend;

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)))
proofend;

theorem Th29: :: TERMORD:29
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT (p,T)) + (HT (q,T)) in Support (p *' q)
proofend;

theorem Th30: :: TERMORD:30
for n being Ordinal
for L being non empty right_complementable well-unital distributive add-associative right_zeroed 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 &amp; t in Support q )  }
proofend;

theorem Th31: :: TERMORD:31
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T))
proofend;

theorem Th32: :: TERMORD:32
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HC ((p *' q),T) = (HC (p,T)) * (HC (q,T))
proofend;

theorem :: TERMORD:33
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HM ((p *' q),T) = (HM (p,T)) *' (HM (q,T))
proofend;

theorem :: TERMORD:34
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
proofend;

begin

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
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 right_complementable add-associative right_zeroed addLoopStr
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 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))
proofend;

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 &amp; b <> HT (p,O) holds
b in Support (Red (p,O))
proofend;

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))}
proofend;

theorem :: TERMORD:35
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 Support (Red (p,T)) c= Support p
proofend;

theorem :: TERMORD:36
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 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 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
proofend;

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
proofend;

theorem :: TERMORD:37
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 Support ((HM (p,T)) + (Red (p,T))) = Support p
proofend;

theorem :: TERMORD:38
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 (HM (p,T)) + (Red (p,T)) = p
proofend;

theorem :: TERMORD:39
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 by Lm18;

theorem :: TERMORD:40
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
for b being bag of n st b in Support p &amp; b <> HT (p,T) holds
(Red (p,T)) . b = p . b by Lm19;