let R be Relation; :: thesis: for C being Completion of R
for a, b being set 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 set holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )
let a, b be set ; :: 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 Th55;
then A1: C reduces a, nf (a,C) by Def6;
( a,b are_convergent_wrt C implies a,b are_convertible_wrt C ) by Th38;
hence ( a,b are_convertible_wrt R implies nf (a,C) = nf (b,C) ) by Def28, Th56; :: 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 Th55;
then A2: C reduces b, nf (b,C) by Def6;
( 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, Def7; :: thesis: verum