The domain predicate captures a call--by--value order of computation, so the entire computation system must be adjusted slightly to reflect this. In particular, computing the value of a function application (total or partial) dictates that function and argument are normalized before beta reduction, both subterms in pairs are normalized, and for injections into disjoint sums the subterm is normalized. In this extension direct computation rules are not present.
To add 
> types to the logic we add terms
fix(f,x.b)where f and x range over variables and a,b,t,A and B range over terms. When closed, the first two kinds of terms are canonical, and the last two are noncanonical.
A>B
dom(t)
t[a]
Let 
stand for fix(f,x.b) henceforth.
Each closed term 
[a]\
is a redex with contractum
,
and each closed term
dom(
)\
is a redex with contractum
where\x. rec(,x.
b
;
;x),
is defined below.
The rule for binding variables is as follows.
