let X be ARS ; :: thesis: for x being Element of X holds

( x is normalizable iff x has_a_normal_form_wrt the reduction of X )

let x be Element of X; :: thesis: ( x is normalizable iff x has_a_normal_form_wrt the reduction of X )

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 normalizable implies x has_a_normal_form_wrt the reduction of X ) :: thesis: ( x has_a_normal_form_wrt the reduction of X implies x is normalizable )

the reduction of X reduces x,a by A2, REWRITE1:def 6;

then ( x = a or a in field the reduction of X ) by REWRITE1:18;

then reconsider a = a as Element of X by A0;

take a ; :: according to ABSRED_0:def 13 :: thesis: a is_normform_of x

thus a is_normform_of x by A2, Ch2; :: thesis: verum

( x is normalizable iff x has_a_normal_form_wrt the reduction of X )

let x be Element of X; :: thesis: ( x is normalizable iff x has_a_normal_form_wrt the reduction of X )

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 normalizable implies x has_a_normal_form_wrt the reduction of X ) :: thesis: ( x has_a_normal_form_wrt the reduction of X implies x is normalizable )

proof

given a being object such that A2:
a is_a_normal_form_of x, the reduction of X
; :: according to REWRITE1:def 11 :: thesis: x is normalizable
given y being Element of X such that A1:
y is_normform_of x
; :: according to ABSRED_0:def 13 :: thesis: x has_a_normal_form_wrt the reduction of X

take y ; :: according to REWRITE1:def 11 :: thesis: y is_a_normal_form_of x, the reduction of X

thus y is_a_normal_form_of x, the reduction of X by A1, Ch2; :: thesis: verum

end;take y ; :: according to REWRITE1:def 11 :: thesis: y is_a_normal_form_of x, the reduction of X

thus y is_a_normal_form_of x, the reduction of X by A1, Ch2; :: thesis: verum

the reduction of X reduces x,a by A2, REWRITE1:def 6;

then ( x = a or a in field the reduction of X ) by REWRITE1:18;

then reconsider a = a as Element of X by A0;

take a ; :: according to ABSRED_0:def 13 :: thesis: a is_normform_of x

thus a is_normform_of x by A2, Ch2; :: thesis: verum