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 )

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

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 A2:
for a being object st a in field the reduction of X holds
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;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

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 )
;

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

end;thus x is normform :: according to ABSRED_0:def 12 :: thesis: x =*=> x

proof

thus
x =*=> x
; :: thesis: verum
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 not [x,y] in the reduction of X by A3, RELAT_1:15; :: according to ABSRED_0:def 1 :: thesis: verum