:: Term Orders
:: by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2016 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;