# Executable Specification

[View cr.sig]
[View cr.mod]
sig cr.
kind tm type.
type app tm -> tm -> tm.
type abs (tm -> tm) -> tm.
type trm, notabs tm -> o.
type pr1, cd1 tm -> tm -> o.
type beta, betan tm -> tm -> o.

module cr.
trm (app M N) :- trm M, trm N.
trm (abs R) :- pi x\ trm x => trm (R x).
pr1 (app T1 S1) (app T2 S2) :- pr1 T1 T2, pr1 S1 S2.
pr1 (abs S1) (abs S2) :- pi x\ pr1 x x => pr1 (S1 x) (S2 x).
pr1 (app (abs T1) S1) (T2 S2) :- pr1 (abs T1) (abs T2), pr1 S1 S2.
notabs (app M N).
cd1 (app T1 S1) (app T2 S2) :- notabs T1, cd1 T1 T2, cd1 S1 S2.
cd1 (abs S1) (abs S2) :- pi x\ notabs x => cd1 x x => cd1 (S1 x) (S2 x).
cd1 (app (abs T1) S1) (T2 S2) :- cd1 (abs T1) (abs T2), cd1 S1 S2.
beta (app M N) (app M' N) :- beta M M'.
beta (app M N) (app M N') :- beta N N'.
beta (abs S1) (abs S2) :- pi x\ beta (S1 x) (S2 x).
beta (app (abs R) M) (R M).
betan M M.
betan M N :- beta M P, betan P N.