%%% The Church-Rosser theorem for ordinary reduction
%%% Author: Frank Pfenning

cr_ord : M <-> M'  ->  M -->* N  ->  M' -->* N  ->  type.
% %mode +{M} +{M'} +{C:M <-> M'}
%       -{N} -{S*:M -->* N} -{S*':M' -->* N} cr_ord C S* S*'.
%mode cr_ord +C -S* -S*'.

cr_all : cr_ord C S* S*'
       <- eq6 C C'
       <- cr C' R* R*'
       <- eq4 R* S*
       <- eq4 R*' S*'.

%worlds () (cr_ord C S* S*').
%covers cr_ord +C -S* -S*'.
%terminates C (cr_ord C _ _).
%total C (cr_ord C _ _).