let X be ARS ; :: thesis: ( X is WN iff the reduction of X is weakly-normalizing )
set R = the reduction of X;
A0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
thus ( X is WN implies the reduction of X is weakly-normalizing ) :: thesis: ( the reduction of X is weakly-normalizing implies X is WN )
proof
assume A1: for x being Element of X holds x is normalizable ; :: according to ABSRED_0:def 14 :: thesis: the reduction of X is weakly-normalizing
let a be object ; :: according to REWRITE1:def 14 :: thesis: ( not a in field the reduction of X or a has_a_normal_form_wrt the reduction of X )
assume a in field the reduction of X ; :: thesis: a has_a_normal_form_wrt the reduction of X
then reconsider a = a as Element of X by A0;
a is normalizable by A1;
hence a has_a_normal_form_wrt the reduction of X by Ch3; :: thesis: verum
end;
assume A2: for a being object st a in field the reduction of X holds
a has_a_normal_form_wrt the reduction of X ; :: according to REWRITE1:def 14 :: thesis: X is WN
let x be Element of X; :: according to ABSRED_0:def 14 :: thesis: x is normalizable
per cases ( x in field the reduction of X or not x in field the reduction of X ) ;
suppose x in field the reduction of X ; :: thesis: x is normalizable
hence x is normalizable by A2, Ch3; :: thesis: verum
end;
suppose A3: not x in field the reduction of X ; :: thesis: x is normalizable
take x ; :: according to ABSRED_0:def 13 :: thesis: x is_normform_of x
thus x is normform :: according to ABSRED_0:def 12 :: thesis: x =*=> x
proof
let y be Element of X; :: according to ABSRED_0:def 11 :: thesis: not x ==> y
thus not [x,y] in the reduction of X by A3, RELAT_1:15; :: according to ABSRED_0:def 1 :: thesis: verum
end;
thus x =*=> x ; :: thesis: verum
end;
end;