let X be ARS ; :: thesis: ( X is SN implies the reduction of X is strongly-normalizing )
set R = the reduction of X;
set A = the carrier of X;
A0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
assume A1: for f being Function of NAT, the carrier of X holds
not for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: the reduction of X is strongly-normalizing
let f be ManySortedSet of NAT ; :: according to REWRITE1:def 15 :: thesis: not for b1 being set holds [(f . b1),(f . (b1 + 1))] in the reduction of X
per cases ( f is the carrier of X -valued or not f is the carrier of X -valued ) ;
suppose f is the carrier of X -valued ; :: thesis: not for b1 being set holds [(f . b1),(f . (b1 + 1))] in the reduction of X
then ( rng f c= the carrier of X & dom f = NAT ) by ;
then reconsider g = f as Function of NAT, the carrier of X by FUNCT_2:2;
consider i being Nat such that
A2: not g . i ==> g . (i + 1) by A1;
take i ; :: thesis: not [(f . i),(f . (i + 1))] in the reduction of X
thus not [(f . i),(f . (i + 1))] in the reduction of X by A2; :: thesis: verum
end;
suppose not f is the carrier of X -valued ; :: thesis: not for b1 being set holds [(f . b1),(f . (b1 + 1))] in the reduction of X
then consider a being object such that
A3: ( a in rng f & not a in the carrier of X ) by ;
consider i being object such that
A4: ( i in dom f & a = f . i ) by ;
reconsider i = i as Element of NAT by A4;
take i ; :: thesis: not [(f . i),(f . (i + 1))] in the reduction of X
assume [(f . i),(f . (i + 1))] in the reduction of X ; :: thesis: contradiction
then a in field the reduction of X by ;
hence contradiction by A0, A3; :: thesis: verum
end;
end;