%%% Equivalence of ordinary and parallel reduction.
%%% Author: Frank Pfenning

% If M => N then M -->* N.

eq1 : M => N  ->  M -->* N  ->  type.
%mode eq1 +R -S*.

eq1_beta : eq1 (beta R1 R2) S*
         <- ({x:term} {eqx : x => x}
               eq1 eqx id1 -> eq1 (R1 x eqx) (S1* x))
         <- lm1* S1* S1*'
         <- apl1* S1*' S1*''
         <- eq1 R2 S2*
         <- apr1* S2* S2*'
         <- appd S2*' (step1 beta1 id1) S*'
         <- appd S1*'' S*' S*.

eq1_ap : eq1 (ap R1 R2) S*
       <- eq1 R1 S1*
       <- apl1* S1* S*'
       <- eq1 R2 S2*
       <- apr1* S2* S*''
       <- appd S*' S*'' S*.

eq1_lm : eq1 (lm R1) S*
       <- ({x:term} {eqx : x => x}
             eq1 eqx id1 -> eq1 (R1 x eqx) (S1* x))
       <- lm1* S1* S*.

%block leq1 : block {x:term} {eqx:x => x} {e:eq1 eqx id1}.
%worlds (leq1) (eq1 R S*).
%covers eq1 +R -S*.
%terminates R (eq1 R _).
%total R (eq1 R _).

% If M --> N then M => N.

eq2 : M --> N  ->  M => N  ->  type.
%mode eq2 +R -S.

eq2_beta1 : eq2 (beta1) (beta I1 I2)
          <- ({x:term} {eqx : x => x}
                identity x eqx -> identity (M1 x) (I1 x eqx))
          <- identity M2 I2.

% bug here in previous version
eq2_lm1   : eq2 (lm1 R1) (lm S1)
          <- ({x:term} {eqx : x => x}
		identity x eqx -> eq2 (R1 x) (S1 x eqx)).

eq2_apl1  : eq2 (apl1 R1) (ap S1 I2)
          <- eq2 R1 S1
          <- identity M2 I2.

eq2_apr1  : eq2 (apr1 R2) (ap I1 S2)
          <- eq2 R2 S2
          <- identity M1 I1.

%worlds (lid) (eq2 R S).
%covers eq2 +R -S.
%terminates R (eq2 R _).
%total R (eq2 R _).

% If M -->* N then M =>* N.

eq3 : M -->* N  ->  M =>* N  ->  type.
%mode eq3 +R* -S*.

eq3_id : eq3 id1 id.
eq3_step : eq3 (step1 R1 R2*) (S1 ; S2*)
         <- eq2 R1 S1
         <- eq3 R2* S2*.

%worlds () (eq3 R* S*).
%covers eq3 +R* -S*.
%terminates R* (eq3 R* _).
%total R* (eq3 R* _).

% If M =>* N then M -->* N.

eq4 : M =>* N  ->  M -->* N  ->  type.
%mode eq4 +R* -S*.

eq4_id : eq4 id id1.
eq4_step : eq4 (R1 ; R2*) S*
         <- eq1 R1 S1*
         <- eq4 R2* S2*
         <- appd S1* S2* S*.

%worlds () (eq4 R* S*).
%covers eq4 +R* -S*.
%terminates R* (eq4 R* _).
%total R* (eq4 R* _).

% If M <=> N then M <-> N.

eq5 : M <=> N  ->  M <-> N  ->  type.
%mode eq5 +C -C'.

eq5_red   : eq5 (reduce R*) (red S*)
          <- eq4 R* S*.
eq5_exp   : eq5 (expand R*) (sym (red S*))
          <- eq4 R* S*.
% bug here (trans C1' C2') instead of (trans C2' C1')
% Fri Dec 14 19:03:57 2001 -fp !!!
eq5_trans : eq5 (C1 ;; C2) (trans C2' C1')
          <- eq5 C1 C1'
          <- eq5 C2 C2'.

%worlds () (eq5 C C').
%covers eq5 +C -C'.
%terminates C (eq5 C _).
%total C (eq5 C _).

% If M <=> N then N <=> M.

sym_pconv : M <=> N  ->  N <=> M  ->  type.
%mode sym_pconv +C -C'.

spc_red   : sym_pconv (reduce R*) (expand R*).
spc_exp   : sym_pconv (expand R*) (reduce R*).
spc_trans : sym_pconv (C1 ;; C2) (C2' ;; C1')
          <- sym_pconv C1 C1'
          <- sym_pconv C2 C2'.

%worlds () (sym_pconv C C').
%covers sym_pconv +C -C'.
%terminates C (sym_pconv C _).
%total C (sym_pconv C _).

% The following is a bug not detected by term reconstruction
% spc_wrong : sym_pconv (C1 ;; C2) (C1' ;; C2')
%         <- sym_pconv C1 C1'
%         <- sym_pconv C2 C2'.

% If M <-> N then M <=> N.

eq6 : M <-> N  ->  M <=> N  ->  type.
%mode eq6 +C -C'.

eq6_refl  : eq6 refl (reduce id).
eq6_sym   : eq6 (sym C1) C'
          <- eq6 C1 C1'
          <- sym_pconv C1' C'.
% Bug here: (trans C1 C2)
% Fri Dec 14 18:50:34 2001 -fp !!!
eq6_trans : eq6 (trans C2 C1) (C1' ;; C2')
          <- eq6 C1 C1'
          <- eq6 C2 C2'.
eq6_red   : eq6 (red R*) (reduce S*)
          <- eq3 R* S*.

%worlds () (eq6 C C').
%covers eq6 +C -C'.
%terminates C (eq6 C _).
%total C (eq6 C _).