let X be ARS ; :: thesis: ( X is N.F. iff the reduction of X is with_NF_property )

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;

thus ( X is N.F. implies the reduction of X is with_NF_property ) :: thesis: ( the reduction of X is with_NF_property implies X is N.F. )

the reduction of X reduces b,a ; :: according to REWRITE1:def 20 :: thesis: X is N.F.

let x be Element of X; :: according to ABSRED_0:def 18 :: thesis: for y being Element of X st x is normform & x <=*=> y holds

y =*=> x

let y be Element of X; :: thesis: ( x is normform & x <=*=> y implies y =*=> x )

assume ( x is normform & x <=*=> y ) ; :: thesis: y =*=> x

hence the reduction of X reduces y,x by B1, Ch1; :: according to ABSRED_0:def 3 :: thesis: verum

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;

thus ( X is N.F. implies the reduction of X is with_NF_property ) :: thesis: ( the reduction of X is with_NF_property implies X is N.F. )

proof

assume B1:
for a, b being object st a is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X holds
assume A1:
for x, y being Element of X st x is normform & x <=*=> y holds

y =*=> x ; :: according to ABSRED_0:def 18 :: thesis: the reduction of X is with_NF_property

let a, b be object ; :: according to REWRITE1:def 20 :: thesis: ( not a is_a_normal_form_wrt the reduction of X or not a,b are_convertible_wrt the reduction of X or the reduction of X reduces b,a )

assume A2: ( a is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X ) ; :: thesis: the reduction of X reduces b,a

end;y =*=> x ; :: according to ABSRED_0:def 18 :: thesis: the reduction of X is with_NF_property

let a, b be object ; :: according to REWRITE1:def 20 :: thesis: ( not a is_a_normal_form_wrt the reduction of X or not a,b are_convertible_wrt the reduction of X or the reduction of X reduces b,a )

assume A2: ( a is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X ) ; :: thesis: the reduction of X reduces b,a

per cases
( ( a in the carrier of X & b in the carrier of X ) or not a in the carrier of X or not b in the carrier of X )
;

end;

suppose
( a in the carrier of X & b in the carrier of X )
; :: thesis: the reduction of X reduces b,a

then reconsider x = a, y = b as Element of X ;

( x is normform & x <=*=> y ) by A2, Ch1;

then y =*=> x by A1;

hence the reduction of X reduces b,a ; :: thesis: verum

end;( x is normform & x <=*=> y ) by A2, Ch1;

then y =*=> x by A1;

hence the reduction of X reduces b,a ; :: thesis: verum

suppose
( not a in the carrier of X or not b in the carrier of X )
; :: thesis: the reduction of X reduces b,a

then
( not a in field the reduction of X or not b in field the reduction of X )
by A0;

then a = b by A2, REWRITE1:28, REWRITE1:31;

hence the reduction of X reduces b,a by REWRITE1:12; :: thesis: verum

end;then a = b by A2, REWRITE1:28, REWRITE1:31;

hence the reduction of X reduces b,a by REWRITE1:12; :: thesis: verum

the reduction of X reduces b,a ; :: according to REWRITE1:def 20 :: thesis: X is N.F.

let x be Element of X; :: according to ABSRED_0:def 18 :: thesis: for y being Element of X st x is normform & x <=*=> y holds

y =*=> x

let y be Element of X; :: thesis: ( x is normform & x <=*=> y implies y =*=> x )

assume ( x is normform & x <=*=> y ) ; :: thesis: y =*=> x

hence the reduction of X reduces y,x by B1, Ch1; :: according to ABSRED_0:def 3 :: thesis: verum