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