:: Term Orders
::  by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ZFMISC_1, ALGSTR_0, VECTSP_1, RLVECT_1, PRE_POLY,
      XCMPLX_0, ARYTM_3, FUNCT_1, XXREAL_0, ARYTM_1, CARD_1, XBOOLE_0,
      SUBSET_1, RELAT_1, PBOOLE, TARSKI, ORDINAL1, LATTICES, POLYNOM1,
      FINSEQ_1, CARD_3, PARTFUN1, NAT_1, SUPINF_2, POLYNOM7, STRUCT_0,
      VECTSP_2, CAT_3, BAGORDER, RELAT_2, WELLORD1, FINSET_1, BROUWER,
      VALUED_0, ORDERS_1, ALGSTR_1, TERMORD;
 notations ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1, ORDERS_1,
      RELAT_1, CARD_1, BAGORDER, RELSET_1, FUNCT_1, PARTFUN1, FINSET_1,
      XXREAL_0, ALGSTR_1, PBOOLE, FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_0,
      RLVECT_1, VFUNCT_1, XTUPLE_0, MCART_1, VECTSP_1, VECTSP_2, RELAT_2,
      POLYNOM1, NAT_D, WELLORD1, POLYNOM7;
 constructors VECTSP_2, ALGSTR_1, TRIANG_1, POLYNOM7, BAGORDER, WELLORD2,
      RELSET_1, POLYNOM1, BINOP_2, VFUNCT_1, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, NAT_1, CARD_1,
      FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, POLYNOM7,
      BAGORDER, VALUED_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

registration
  cluster non trivial for addLoopStr;
end;

registration
  cluster add-associative right_complementable right_zeroed for non trivial
    addLoopStr;
end;

definition
  let X be set, b be bag of X;
  attr b is 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 well-unital distributive non empty doubleLoopStr, p being Series
  of n, L holds 0_(n,L) *' p = 0_(n,L);

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

registration
  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 well-unital distributive domRing-like non trivial doubleLoopStr,
b,b9 being bag of n, a,a9 being non zero Element of L holds Monom(a * a9,b + b9
  ) = Monom(a,b) *' Monom(a9,b9);

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

begin

registration
  let n be Ordinal;
  cluster admissible connected for TermOrder of n;
end;

:: theorem 5.5 (ii), p. 190

registration
  let n be Nat;
  cluster -> well_founded for admissible TermOrder of n;
end;

definition
  let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
  pred b <= b9,T means
:: TERMORD:def 2

  [b,b9] in T;
end;

definition
  let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
  pred b < b9,T means
:: TERMORD:def 3

  b <= b9,T & b <> b9;
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
  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;

registration
  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
  well-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 well-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 well-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 well-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 well-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 addLoopStr, p,q being Polynomial of n,L holds HT
  (p+q,T) <= max(HT(p,T),HT(q,T),T), T;

begin :: Reductum

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