% Church Rosser for products
% Carsten Schuermann

term : type.
pair : term -> term -> term.
let  : term -> (term -> term -> term) -> term.
0 : term.

=> : term -> term -> type. %infix none 10 =>.
                            %name => R.


ppair : M1 => M1' -> M2 => M2'
	-> (pair M1 M2) => (pair M1' M2').
plet  : M1 => M1'
	 -> ({x:term} x => x -> {y:term} y => y -> M2 x y => M2' x y)
	 -> (let M1 M2) => (let M1' M2').
pbeta : M1 => M1' -> M2 => M2' 
	 -> ({x:term} x => x -> {y:term} y => y -> M3 x y => M3' x y)
	 -> (let (pair M1 M2) M3) => (M3' M1' M2'). 
subst : ({x:term} x => x -> {y:term} y => y -> M2 x y => M2' x y)
	 -> ({x:term} {x':term} x => x'
	       -> {y:term}{y':term} y => y' -> M2 x y => M2' x' y')
	    -> type.


p0 : 0 => 0.

%mode subst +R -R'.
sub-1 : subst ([x][u][y][v] u) ([x][x'][u][y][y'][v] u).
sub-2 : subst ([x][u][y][v] v) ([x][x'][u][y][y'][v] v).
sub-3 : subst ([x][u][y][v] ppair (R1 x u y v ) (R2 x u y v))
	      ([x][x'][u][y][y'][v] ppair (S1 x x' u y y' v ) (S2 x x' u y y' v))
	 <- subst R1 S1
	 <- subst R2 S2.
sub-4 : subst ([x][u][y][v] plet (R1 x u y v ) (R2 x u y v))
	      ([x][x'][u][y][y'][v] plet (S1 x x' u y y' v ) (S2 x x' u y y' v))
	 <- subst R1 S1
	 <- ({a}{b}{c}{d} subst ([x][u][y][v] R2 x u y v a b c d)
	                     ([x][x'][u][y][y'][v] S2 x x' u y y' v a b c d)).
sub-4 : subst ([x][u][y][v] pbeta (R1 x u y v ) (R2 x u y v) (R3 x u y v))
	      ([x][x'][u][y][y'][v] pbeta (S1 x x' u y y' v ) (S2 x x' u y y' v) (S3 x x' u y y' v))
	 <- subst R1 S1
	 <- subst R2 S2
	 <- ({a}{b}{c}{d} subst ([x][u][y][v] R3 x u y v a b c d)
	                     ([x][x'][u][y][y'][v] S3 x x' u y y' v a b c d)).
sub-5 : subst ([x][u][y][v] R) ([x][x'][u][y][y'][v] R).

%block l:  block {x:term} {idx: x => x}.
%worlds (l) (subst R R').
%covers subst +R -R'.
%terminates R (subst R _).
%total R (subst R _).


dia : E => E' -> E => E'' -> E' => E''' -> E'' => E''' -> type.
%mode dia +R +S -U -V.
dia-1 : dia (ppair R1 R2) (ppair S1 S2) (ppair U1 U2) (ppair V1 V2)
	 <- dia R1 S1 U1 V1
	 <- dia R2 S2 U2 V2.
	    
dia-2 : dia (plet R1 R2) (plet S1 S2) (plet U1 U2) (plet V1 V2)
	 <- dia R1 S1 U1 V1
	 <- ({x}{u} dia u u u u 
	       -> {y}{v} dia v v v v 
	       -> dia (R2 x u y v) (S2 x u y v) (U2 x u y v) (V2 x u y v)).
 
dia-3 : dia (pbeta R1 R2 R3) (pbeta S1 S2 S3) (U3' _ _ U1 _ _ U2) (V3' _ _ V1 _ _ V2) 
	 <- dia R1 S1 U1 V1
	 <- dia R2 S2 U2 V2
	 <- ({x}{u} dia u u u u 
	       -> {y}{v} dia v v v v 
	       -> dia (R3 x u y v) (S3 x u y v) (U3 x u y v) (V3 x u y v))
	 <- subst U3 U3'
	 <- subst V3 V3'.

dia-4 : dia (pbeta R1 R2 R3) (plet (ppair S1 S2) S3) (U3' _ _ U1 _ _ U2) (pbeta V1 V2 V3)	
	 <- dia R1 S1 U1 V1
	 <- dia R2 S2 U2 V2
	 <- ({x}{u} dia u u u u 
	       -> {y}{v} dia v v v v 
	       -> dia (R3 x u y v) (S3 x u y v) (U3 x u y v) (V3 x u y v))
	 <- subst U3 U3'.

dia-5 : dia (plet (ppair R1 R2) R3) (pbeta S1 S2 S3) (pbeta U1 U2 U3) (V3' _ _ V1 _ _ V2)
	 <- dia R1 S1 U1 V1
	 <- dia R2 S2 U2 V2
	 <- ({x}{u} dia u u u u 
	       -> {y}{v}dia v v v v 
	       -> dia (R3 x u y v) (S3 x u y v) (U3 x u y v) (V3 x u y v))
	 <- subst V3 V3'.

dia-6 : dia p0 p0 p0 p0.

%block l2 : block {x:term} {idx:x => x}
	     {hd: dia idx idx idx idx}.
%worlds (l2) (dia _ _ _ _).
%covers dia +R' +R'' -S' -S''.
%terminates [R' R''] (dia R' R'' _ _).
%total [R' R''] (dia R' R'' _ _).