%%% Basic lemmas concerning parallel reductions
%%% Author: Frank Pfenning

% Every term reduces to itself (in parallel)

identity : {M:term} M => M  ->  type.
%mode identity +M -R.

id_lam : identity (lam M1) (lm R1)
       <- {x:term} {eqx: x => x} identity x eqx -> identity (M1 x) (R1 x eqx).

id_app : identity (app M1 M2) (ap R1 R2)
       <- identity M1 R1
       <- identity M2 R2.

%  Parallel multi-step reduction is transitive.

append : M =>* M'  ->  M' =>* M''  ->  M =>* M''  -> type.
%mode append +R* +S* -S*'.

append_id   : append id S* S*.
append_step : append (R1 ; R2*) S* (R1 ; S2*')
           <- append R2* S* S2*'.