environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, POLYNOM1, NAT_1, RLVECT_1, VECTSP_2, POLYNOM7, POLYNOM2, NAT_2, RELAT_2, CARD_1, CARD_2, MATRLIN, XBOOLE_0, XBOOLE_1, ORDERS_1, BAGORDER, WELLORD1, XREAL_1, PARTFUN1, VALUED_0, STRUCT_0, XREAL_0, PRE_POLY, XTUPLE_0;
schemes NAT_1;
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;
constructors HIDDEN, VECTSP_2, ALGSTR_1, TRIANG_1, POLYNOM7, BAGORDER, WELLORD2, RELSET_1, POLYNOM1, BINOP_2, VFUNCT_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;
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 )
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 )
by Def4, Def5;
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)))
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