# Executable Specification

[View sred.sig]
[View sred.mod]
sig sred.
kind tm type.
type app tm -> tm -> tm.
type abs (tm -> tm) -> tm.
type tm tm -> o.
type beta, betas, wh, sred tm -> tm -> o.

module sred.
tm (app M N) :- tm M, tm N.
tm (abs R) :- pi x\ tm x => tm (R x).
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).
betas M M.
betas M N :- betas M P, beta P N.
wh (app (abs R) M) (R M).
wh (app M N) (app M' N) :- wh M M'.
sred M1 M3 :- wh M1 M2, sred M2 M3.
sred (app M1 N1) (app M2 N2) :- sred M1 M2, sred N1 N2.
sred (abs R1) (abs R2) :- pi x\ sred x x => sred (R1 x) (R2 x).