let R be Relation; :: thesis: for C being Completion of R
for a, b being object holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
let C be Completion of R; :: thesis: for a, b being object holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
let a, b be object ; :: thesis: ( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
nf (a,C) is_a_normal_form_of a,C by Th54;
then A1: C reduces a, nf (a,C) ;
( a,b are_convergent_wrt C implies a,b are_convertible_wrt C ) by Th37;
hence ( a,b are_convertible_wrt R implies nf (a,C) = nf (b,C) ) by Def28, Th55; :: thesis: ( nf (a,C) = nf (b,C) implies a,b are_convertible_wrt R )
nf (b,C) is_a_normal_form_of b,C by Th54;
then A2: C reduces b, nf (b,C) ;
( a,b are_convertible_wrt R iff a,b are_convergent_wrt C ) by Def28;
hence ( nf (a,C) = nf (b,C) implies a,b are_convertible_wrt R ) by A1, A2; :: thesis: verum