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 27;
FinPoset RelStr(# (Bags n),T #) is well_founded
by BAGORDER:42;
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 let Y be
set ;
( Y c= field ((PolyRedRel P,T) ~ ) & Y <> {} implies ex p being set 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 set st
( p in Y & ((PolyRedRel P,T) ~ ) -Seg p misses Y )consider z being
Element of
Y;
z in Y
by A4;
then
z in field ((PolyRedRel P,T) ~ )
by A3;
then A5:
z in (dom ((PolyRedRel P,T) ~ )) \/ (rng ((PolyRedRel P,T) ~ ))
by RELAT_1:def 6;
then reconsider z9 =
z as
Polynomial of
n,
L by POLYNOM1:def 27;
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
set 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
consider b being
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 18;
assume A12:
(((PolyRedRel P,T) ~ ) -Seg p) /\ Y <> {}
;
contradiction
then
b in ((PolyRedRel P,T) ~ ) -Seg p
by XBOOLE_0:def 4;
then
[b,p] in (PolyRedRel P,T) ~
by WELLORD1:def 1;
then A13:
[p,b] in PolyRedRel P,
T
by RELAT_1:def 7;
then consider h9,
g9 being
set such that A14:
[p,b] = [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:6;
b =
[h9,g9] `2
by A14, MCART_1:def 2
.=
g9
by MCART_1:def 2
;
then reconsider b9 =
b as
Polynomial of
n,
L by A16, POLYNOM1:def 27;
A17:
p =
[h9,g9] `1
by A14, MCART_1:def 1
.=
h9
by MCART_1:def 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 2;
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 )
by Def7;
reconsider p =
p as
non-zero Polynomial of
n,
L ;
A19:
b9 < p,
T
by A18, Th43;
then A20:
Support b9 <> Support p
by Def3;
b in Y
by A12, XBOOLE_0:def 4;
then A21:
Support b9 in M
;
b9 <= p,
T
by A19, Def3;
then
[(Support b9),(Support p)] in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #))
by A11, Def2;
then
Support b9 in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #)) -Seg (Support p)
by A20, WELLORD1:def 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
set 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 set A = the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)};
set B = the
carrier of
(Polynom-Ring n,L);
let x be
set ;
( 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,Tthen 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 assume A24:
[x,x] in PolyRedRel P,
T
;
contradictionthen consider x1,
y1 being
set 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:6;
x =
[x1,y1] `1
by A25, MCART_1:def 1
.=
x1
by MCART_1:def 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 2;
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 )
by Def7;
then
x9 < x9,
T
by Th43;
then
Support x9 <> Support x9
by Def3;
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