set BT = RelStr(# (Bags n),T #);
set X = the InternalRel of (FinPoset RelStr(# (Bags n),T #));
set R = PolyRedRel (P,T);
A1:
0_ (n,L) = 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
FinPoset RelStr(# (Bags n),T #) is well_founded
by BAGORDER:41;
then A2:
the InternalRel of (FinPoset RelStr(# (Bags n),T #)) is_well_founded_in the carrier of (FinPoset RelStr(# (Bags n),T #))
by WELLFND1:def 2;
now for Y being set st Y c= field ((PolyRedRel (P,T)) ~) & Y <> {} holds
ex p being object st
( p in Y & ((PolyRedRel (P,T)) ~) -Seg p misses Y )let Y be
set ;
( Y c= field ((PolyRedRel (P,T)) ~) & Y <> {} implies ex p being object st
( p in Y & ((PolyRedRel (P,T)) ~) -Seg p misses Y ) )assume that A3:
Y c= field ((PolyRedRel (P,T)) ~)
and A4:
Y <> {}
;
ex p being object st
( p in Y & ((PolyRedRel (P,T)) ~) -Seg p misses Y )set z = the
Element of
Y;
the
Element of
Y in Y
by A4;
then
the
Element of
Y in field ((PolyRedRel (P,T)) ~)
by A3;
then A5:
the
Element of
Y in (dom ((PolyRedRel (P,T)) ~)) \/ (rng ((PolyRedRel (P,T)) ~))
by RELAT_1:def 6;
then reconsider z9 = the
Element of
Y as
Polynomial of
n,
L by POLYNOM1:def 11;
set M =
{ (Support y9) where y9 is Polynomial of n,L : ex y being set st
( y in Y & y9 = y ) } ;
Support z9 in { (Support y9) where y9 is Polynomial of n,L : ex y being set st
( y in Y & y9 = y ) }
by A4;
then reconsider M =
{ (Support y9) where y9 is Polynomial of n,L : ex y being set st
( y in Y & y9 = y ) } as non
empty set ;
then
M c= the
carrier of
(FinPoset RelStr(# (Bags n),T #))
by TARSKI:def 3;
then consider a being
object such that A7:
a in M
and A8:
the
InternalRel of
(FinPoset RelStr(# (Bags n),T #)) -Seg a misses M
by A2, WELLORD1:def 3;
consider p being
Polynomial of
n,
L such that A9:
Support p = a
and A10:
ex
y being
set st
(
y in Y &
p = y )
by A7;
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y = {}
proof
set b = the
Element of
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y;
A11:
FinPoset RelStr(#
(Bags n),
T #)
= RelStr(#
(Fin the carrier of RelStr(# (Bags n),T #)),
(FinOrd RelStr(# (Bags n),T #)) #)
by BAGORDER:def 16;
assume A12:
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y <> {}
;
contradiction
then
the
Element of
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y in ((PolyRedRel (P,T)) ~) -Seg p
by XBOOLE_0:def 4;
then
[ the Element of (((PolyRedRel (P,T)) ~) -Seg p) /\ Y,p] in (PolyRedRel (P,T)) ~
by WELLORD1:1;
then A13:
[p, the Element of (((PolyRedRel (P,T)) ~) -Seg p) /\ Y] in PolyRedRel (
P,
T)
by RELAT_1:def 7;
then consider h9,
g9 being
object such that A14:
[p, the Element of (((PolyRedRel (P,T)) ~) -Seg p) /\ Y] = [h9,g9]
and A15:
h9 in NonZero (Polynom-Ring (n,L))
and A16:
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
the
Element of
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y = g9
by A14, XTUPLE_0:1;
then reconsider b9 = the
Element of
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y as
Polynomial of
n,
L by A16, POLYNOM1:def 11;
A17:
p = h9
by A14, XTUPLE_0:1;
not
h9 in {(0_ (n,L))}
by A1, A15, XBOOLE_0:def 5;
then
h9 <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider p =
p as
non-zero Polynomial of
n,
L by A17, POLYNOM7:def 1;
p reduces_to b9,
P,
T
by A13, Def13;
then A18:
ex
u being
Polynomial of
n,
L st
(
u in P &
p reduces_to b9,
u,
T )
;
reconsider p =
p as
non-zero Polynomial of
n,
L ;
A19:
b9 < p,
T
by A18, Th43;
then A20:
Support b9 <> Support p
;
the
Element of
(((PolyRedRel (P,T)) ~) -Seg p) /\ Y in Y
by A12, XBOOLE_0:def 4;
then A21:
Support b9 in M
;
b9 <= p,
T
by A19;
then
[(Support b9),(Support p)] in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #))
by A11;
then
Support b9 in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #)) -Seg (Support p)
by A20, WELLORD1:1;
then
Support b9 in ( the InternalRel of (FinPoset RelStr(# (Bags n),T #)) -Seg a) /\ M
by A9, A21, XBOOLE_0:def 4;
hence
contradiction
by A8, XBOOLE_0:def 7;
verum
end; then
((PolyRedRel (P,T)) ~) -Seg p misses Y
by XBOOLE_0:def 7;
hence
ex
p being
object st
(
p in Y &
((PolyRedRel (P,T)) ~) -Seg p misses Y )
by A10;
verum end;
then
(PolyRedRel (P,T)) ~ is well_founded
by WELLORD1:def 2;
then A22:
PolyRedRel (P,T) is co-well_founded
by REWRITE1:def 13;
now for x being object st x in field (PolyRedRel (P,T)) holds
not [x,x] in PolyRedRel (P,T)set A = the
carrier of
(Polynom-Ring (n,L)) \ {(0_ (n,L))};
set B = the
carrier of
(Polynom-Ring (n,L));
let x be
object ;
( x in field (PolyRedRel (P,T)) implies not [x,x] in PolyRedRel (P,T) )assume
x in field (PolyRedRel (P,T))
;
not [x,x] in PolyRedRel (P,T)then A23:
x in (dom (PolyRedRel (P,T))) \/ (rng (PolyRedRel (P,T)))
by RELAT_1:def 6;
then reconsider x9 =
x as
Polynomial of
n,
L ;
now not [x,x] in PolyRedRel (P,T)assume A24:
[x,x] in PolyRedRel (
P,
T)
;
contradictionthen consider x1,
y1 being
object such that A25:
[x,x] = [x1,y1]
and A26:
x1 in the
carrier of
(Polynom-Ring (n,L)) \ {(0_ (n,L))}
and
y1 in the
carrier of
(Polynom-Ring (n,L))
by A1, RELSET_1:2;
x = x1
by A25, XTUPLE_0:1;
then
not
x9 in {(0_ (n,L))}
by A26, XBOOLE_0:def 5;
then
x9 <> 0_ (
n,
L)
by TARSKI:def 1;
then reconsider x9 =
x9 as
non-zero Polynomial of
n,
L by POLYNOM7:def 1;
x9 reduces_to x9,
P,
T
by A24, Def13;
then
ex
p being
Polynomial of
n,
L st
(
p in P &
x9 reduces_to x9,
p,
T )
;
then
x9 < x9,
T
by Th43;
then
Support x9 <> Support x9
;
hence
contradiction
;
verum end; hence
not
[x,x] in PolyRedRel (
P,
T)
;
verum end;
then
PolyRedRel (P,T) is_irreflexive_in field (PolyRedRel (P,T))
by RELAT_2:def 2;
then
PolyRedRel (P,T) is irreflexive
by RELAT_2:def 10;
hence
PolyRedRel (P,T) is strongly-normalizing
by A22; verum