set R = PolyRedRel P,T;
now let x be
set ;
:: thesis: ( x in field (PolyRedRel P,T) implies not [x,x] in PolyRedRel P,T )assume
x in field (PolyRedRel P,T)
;
:: thesis: not [x,x] in PolyRedRel P,Tthen A2:
x in (dom (PolyRedRel P,T)) \/ (rng (PolyRedRel P,T))
by RELAT_1:def 6;
set A = the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)};
set B = the
carrier of
(Polynom-Ring n,L);
then reconsider x' =
x as
Polynomial of
n,
L ;
now assume A3:
[x,x] in PolyRedRel P,
T
;
:: thesis: contradictionthen consider x1,
y1 being
set such that A4:
(
[x,x] = [x1,y1] &
x1 in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
y1 in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
x =
[x1,y1] `1
by A4, MCART_1:def 1
.=
x1
by MCART_1:def 1
;
then
not
x' in {(0_ n,L)}
by A4, XBOOLE_0:def 5;
then
x' <> 0_ n,
L
by TARSKI:def 1;
then reconsider x' =
x' as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
x' reduces_to x',
P,
T
by A3, Def13;
then
ex
p being
Polynomial of
n,
L st
(
p in P &
x' reduces_to x',
p,
T )
by Def7;
then
x' < x',
T
by Th43;
then
Support x' <> Support x'
by Def3;
hence
contradiction
;
:: thesis: verum end; hence
not
[x,x] in PolyRedRel P,
T
;
:: thesis: verum end;
then
PolyRedRel P,T is_irreflexive_in field (PolyRedRel P,T)
by RELAT_2:def 2;
then A5:
PolyRedRel P,T is irreflexive
by RELAT_2:def 10;
set BT = RelStr(# (Bags n),T #);
set X = the InternalRel of (FinPoset RelStr(# (Bags n),T #));
FinPoset RelStr(# (Bags n),T #) is well_founded
by BAGORDER:42;
then A6:
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 ;
:: thesis: ( Y c= field ((PolyRedRel P,T) ~ ) & Y <> {} implies ex p being set st
( p in Y & ((PolyRedRel P,T) ~ ) -Seg p misses Y ) )assume A7:
(
Y c= field ((PolyRedRel P,T) ~ ) &
Y <> {} )
;
:: thesis: ex p being set st
( p in Y & ((PolyRedRel P,T) ~ ) -Seg p misses Y )set M =
{ (Support y') where y' is Polynomial of n,L : ex y being set st
( y in Y & y' = y ) } ;
consider z being
Element of
Y;
z in Y
by A7;
then
z in field ((PolyRedRel P,T) ~ )
by A7;
then A8:
z in (dom ((PolyRedRel P,T) ~ )) \/ (rng ((PolyRedRel P,T) ~ ))
by RELAT_1:def 6;
then reconsider z' =
z as
Polynomial of
n,
L by POLYNOM1:def 27;
Support z' in { (Support y') where y' is Polynomial of n,L : ex y being set st
( y in Y & y' = y ) }
by A7;
then reconsider M =
{ (Support y') where y' is Polynomial of n,L : ex y being set st
( y in Y & y' = 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 A10:
(
a in M & the
InternalRel of
(FinPoset RelStr(# (Bags n),T #)) -Seg a misses M )
by A6, WELLORD1:def 3;
consider p being
Polynomial of
n,
L such that A11:
(
Support p = a & ex
y being
set st
(
y in Y &
p = y ) )
by A10;
consider z being
set such that A12:
(
z in Y &
p = z )
by A11;
(((PolyRedRel P,T) ~ ) -Seg p) /\ Y = {}
proof
assume A13:
(((PolyRedRel P,T) ~ ) -Seg p) /\ Y <> {}
;
:: thesis: contradiction
consider b being
Element of
(((PolyRedRel P,T) ~ ) -Seg p) /\ Y;
A14:
(
b in ((PolyRedRel P,T) ~ ) -Seg p &
b in Y )
by A13, XBOOLE_0:def 4;
then
(
b <> p &
[b,p] in (PolyRedRel P,T) ~ )
by WELLORD1:def 1;
then A15:
[p,b] in PolyRedRel P,
T
by RELAT_1:def 7;
then consider h',
g' being
set such that A16:
(
[p,b] = [h',g'] &
h' in the
carrier of
(Polynom-Ring n,L) \ {(0_ n,L)} &
g' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
A17:
p =
[h',g'] `1
by A16, MCART_1:def 1
.=
h'
by MCART_1:def 1
;
not
h' in {(0_ n,L)}
by A16, XBOOLE_0:def 5;
then
h' <> 0_ n,
L
by TARSKI:def 1;
then reconsider p =
p as
non-zero Polynomial of
n,
L by A17, POLYNOM7:def 2;
b =
[h',g'] `2
by A16, MCART_1:def 2
.=
g'
by MCART_1:def 2
;
then reconsider b' =
b as
Polynomial of
n,
L by A16, POLYNOM1:def 27;
p reduces_to b',
P,
T
by A15, Def13;
then consider u being
Polynomial of
n,
L such that A18:
(
u in P &
p reduces_to b',
u,
T )
by Def7;
reconsider p =
p as
non-zero Polynomial of
n,
L ;
A19:
b' < p,
T
by A18, Th43;
then A20:
Support b' <> Support p
by Def3;
A21:
b' <= p,
T
by A19, Def3;
FinPoset RelStr(#
(Bags n),
T #)
= RelStr(#
(Fin the carrier of RelStr(# (Bags n),T #)),
(FinOrd RelStr(# (Bags n),T #)) #)
by BAGORDER:def 18;
then
[(Support b'),(Support p)] in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #))
by A21, Def2;
then A22:
Support b' in the
InternalRel of
(FinPoset RelStr(# (Bags n),T #)) -Seg (Support p)
by A20, WELLORD1:def 1;
Support b' in M
by A14;
then
Support b' in (the InternalRel of (FinPoset RelStr(# (Bags n),T #)) -Seg a) /\ M
by A11, A22, XBOOLE_0:def 4;
hence
contradiction
by A10, XBOOLE_0:def 7;
:: thesis: 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 A12;
:: thesis: verum end;
then
(PolyRedRel P,T) ~ is well_founded
by WELLORD1:def 2;
then
PolyRedRel P,T is co-well_founded
by REWRITE1:def 13;
hence
PolyRedRel P,T is strongly-normalizing
by A5; :: thesis: verum