% X is a decision algorithm for the HP
%da(X) == (a(X) and all(Y,c(Y) => all(Z,d(X,Y,Z)))).

% X is a program that decides the HP
%dp(X) == (c(X) and all(Y,c(Y) => all(Z,d(X,Y,Z)))).






% halting is outputing something

h(X,Y) -> o(X,Y,out(X,Y)).
o(X,Y,O) -> h(X,Y).





% correctness criterion for the decision procedure
dp(W) ->
 c(W) and
 all(Y,all(Z, c(Y) => ( h(Y,Z) <=> o(W,(Y,Z),1)) and 
                      (~h(Y,Z) <=> o(W,(Y,Z),0)))).