The abstract of the Mizar article:

Term Orders

by

Christoph Schwarzweller

Received December 20, 2002

MML identifier: TERMORD

[ Mizar article, MML identifier index ]

environ

 vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, TRIANG_1, FINSEQ_1, VECTSP_1,
      RLVECT_1, ORDINAL1, LATTICES, ALGSEQ_1, ANPROJ_1, CAT_3, GROUP_1,
      VECTSP_2, RELAT_1, RELAT_2, REALSET1, ALGSTR_1, CARD_1, ARYTM_1, MCART_1,
      FINSEQ_4, ARYTM_3, SQUARE_1, PBOOLE, ORDERS_1, ORDERS_2, FINSET_1,
      BAGORDER, WELLORD1, DICKSON, TERMORD;
 notation NUMBERS, XCMPLX_0, XREAL_0, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0,
      RELAT_1, MONOID_0, CARD_1, BAGORDER, RELSET_1, FUNCT_1, FINSET_1,
      ORDINAL1, NAT_1, ALGSTR_1, RLVECT_1, PBOOLE, FINSEQ_1, MCART_1, TRIANG_1,
      REALSET1, VECTSP_1, VECTSP_2, RELAT_2, POLYNOM1, BINARITH, ORDERS_1,
      ORDERS_2, FINSEQ_4, WELLORD1, POLYNOM7;
 constructors ALGSTR_2, POLYNOM7, MONOID_0, BINOM, BAGORDER, MCART_1, TRIANG_1,
      ORDERS_2, MEMBERED;
 clusters XREAL_0, STRUCT_0, FINSET_1, RELSET_1, FINSEQ_1, CARD_1, ALGSTR_1,
      POLYNOM1, POLYNOM2, POLYNOM7, BAGORDER, VECTSP_1, NAT_1, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

definition
cluster non trivial LoopStr;
end;

definition
cluster add-associative right_complementable right_zeroed
        (non trivial LoopStr);
end;

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

theorem :: TERMORD:1
for X being set,
    b1,b2 being bag of X
holds b1 divides b2 iff ex b being bag of X st b2 = b1 + b;

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

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

definition
let n be Ordinal,
    L be add-associative right_complementable
         right_zeroed distributive (non empty doubleLoopStr),
    c1,c2 be ConstPoly of n,L;
cluster c1 *' c2 -> Constant;
end;

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

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

begin

definition
let n be Ordinal;
cluster admissible connected TermOrder of n;
end;

definition
::: theorem 5.5 (ii), p. 190
let n be Nat;
cluster -> well_founded (admissible TermOrder of n);
end;

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

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

definition
let n be Ordinal,
    T be TermOrder of n,
    b1,b2 be bag of n;
func min(b1,b2,T) -> bag of n equals
:: TERMORD:def 4
 b1 if b1 <= b2,T otherwise b2;
func max(b1,b2,T) -> bag of n equals
:: TERMORD:def 5
 b1 if b2 <= b1,T otherwise b2;
end;

theorem :: TERMORD:5
for n being Ordinal,
    T being connected TermOrder of n,
    b1,b2 being bag of n
holds b1 <= b2,T iff not(b2 < b1,T);

theorem :: TERMORD:6
  for n being Ordinal,
    T being TermOrder of n,
    b being bag of n
holds b <= b,T;

theorem :: TERMORD:7
  for n being Ordinal,
    T being TermOrder of n,
    b1,b2 being bag of n
st b1 <= b2,T & b2 <= b1,T holds b1 = b2;

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

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

theorem :: TERMORD:10
  for n being Ordinal,
    T being admissible TermOrder of n,
    b1,b2 being bag of n
holds b1 divides b2 implies b1 <= b2,T;

theorem :: TERMORD:11
for n being Ordinal,
    T being TermOrder of n,
    b1,b2 being bag of n
holds min(b1,b2,T) = b1 or min(b1,b2,T) = b2;

theorem :: TERMORD:12
for n being Ordinal,
    T being TermOrder of n,
    b1,b2 being bag of n
holds max(b1,b2,T) = b1 or max(b1,b2,T) = b2;

theorem :: TERMORD:13
  for n being Ordinal,
    T being connected TermOrder of n,
    b1,b2 being bag of n
holds min(b1,b2,T) <= b1,T & min(b1,b2,T) <= b2,T;

theorem :: TERMORD:14
for n being Ordinal,
    T being connected TermOrder of n,
    b1,b2 being bag of n
holds b1 <= max(b1,b2,T),T & b2 <= max(b1,b2,T),T;

theorem :: TERMORD:15
for n being Ordinal,
    T being connected TermOrder of n,
    b1,b2 being bag of n
holds min(b1,b2,T) = min(b2,b1,T) & max(b1,b2,T) = max(b2,b1,T);

theorem :: TERMORD:16
  for n being Ordinal,
    T being connected TermOrder of n,
    b1,b2 being bag of n
holds min(b1,b2,T) = b1 iff max(b1,b2,T) = b2;

begin :: Headterms, Headmonomials and Headcoefficients

definition
::: definition 5.15, p. 194
let n be Ordinal,
    T be connected TermOrder of n,
    L be non empty ZeroStr,
    p be Polynomial of n,L;
func HT(p,T) -> Element of Bags n means
:: 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);
end;

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

definition
::: definition 5.15, p. 194
let n be Ordinal,
    T be connected TermOrder of n,
    L be non empty ZeroStr,
    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));
end;

definition
let n be Ordinal,
    T be connected TermOrder of n,
    L be non trivial ZeroStr,
    p be non-zero Polynomial of n,L;
cluster HM(p,T) -> non-zero;
cluster HC(p,T) -> non-zero;
end;

theorem :: TERMORD:17
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty ZeroStr,
    p being Polynomial of n,L
holds HC(p,T) = 0.L iff p = 0_(n,L);

theorem :: TERMORD:18
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds (HM(p,T)).(HT(p,T)) = p.(HT(p,T));

theorem :: TERMORD:19
for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L,
    b being bag of n st b <> HT(p,T)
holds HM(p,T).b = 0.L;

theorem :: TERMORD:20
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds Support(HM(p,T)) c= Support(p);

theorem :: TERMORD:21
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds Support(HM(p,T)) = {} or Support(HM(p,T)) = {HT(p,T)};

theorem :: TERMORD:22
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds term(HM(p,T)) = HT(p,T) & coefficient(HM(p,T)) = HC(p,T);

theorem :: TERMORD:23
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty ZeroStr,
    m being Monomial of n,L
holds HT(m,T) = term(m) & HC(m,T) = coefficient(m) & HM(m,T) = m;

theorem :: TERMORD:24
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty ZeroStr,
    c being ConstPoly of n,L
holds HT(c,T) = EmptyBag n & HC(c,T) = c.(EmptyBag n);

theorem :: TERMORD:25
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty ZeroStr,
    a being Element of L
holds HT(a _(n,L),T) = EmptyBag n & HC(a _(n,L),T) = a;

theorem :: TERMORD:26
for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds HT(HM(p,T),T) = HT(p,T);

theorem :: TERMORD:27
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non trivial ZeroStr,
    p being Polynomial of n,L
holds HC(HM(p,T),T) = HC(p,T);

theorem :: TERMORD:28
  for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty ZeroStr,
    p being Polynomial of n,L
holds HM(HM(p,T),T) = HM(p,T);

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

theorem :: TERMORD:30
for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            unital distributive (non empty doubleLoopStr),
    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};

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

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

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

theorem :: TERMORD:34
::: lemma 5.17 (iv), p. 195
  for n being Ordinal,
    T being admissible connected TermOrder of n,
    L being right_zeroed (non empty LoopStr),
    p,q being Polynomial of n,L
holds HT(p+q,T) <= max(HT(p,T),HT(q,T),T), T;

begin :: Reductum

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

theorem :: TERMORD:35
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    p being Polynomial of n,L
holds Support(Red(p,T)) c= Support(p);

theorem :: TERMORD:36
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    p being Polynomial of n,L
holds Support(Red(p,T)) = Support(p) \ {HT(p,T)};

theorem :: TERMORD:37
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    p being Polynomial of n,L
holds Support(HM(p,T) + Red(p,T)) = Support p;

theorem :: TERMORD:38
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    p being Polynomial of n,L
holds HM(p,T) + Red(p,T) = p;

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

theorem :: TERMORD:40
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    p being Polynomial of n,L,
    b being bag of n st b in Support p & b <> HT(p,T)
holds (Red(p,T)).b = p.b;