Iterated inductive definitions and defunctionalization

% RUN-TIME %
%sort i %.
%term z i %.
%term s %pi i %-> i %.
%prec %prefix 10 s %.
%sort add {_ i} {_ i} {_ i} %.
%term add/z add z N N %.
%term add/s %pi (add (s M) N (s P)) %<- (add M N P) %.
%mode add %in %in %out %.
%worlds () (add M _ _) %.
%total (M) (add M _ _) %.
%unique add %in %in %out %.
%sort mult {_ i} {_ i} {_ i} %.
%term mult/z mult z N z %.
%term mult/s %pi (mult (s M) N P') %<- (mult M N P) %<- (add P N P') %.
%mode mult %in %in %out %.
%worlds () (mult M _ _) %.
%total (M) (mult M _ _) %.
%unique mult %in %in %out %.
%  SYNTAX  %
%sort tm %.
%sort binop %.
%term n %pi i %-> tm %.
%term let %pi tm %-> (%pi tm %-> tm) %-> tm %.
%term @ %pi binop %-> tm %-> tm %-> tm %.
%sort apply {_ binop} {_ i} {_ i} {_ i} %.
%mode apply %in %in %in %out %.
%worlds () (apply F M1 M2 _) %.
%total {F M1 M2} (apply F M1 M2 _) %.
%unique apply %in %in %in %out %.
% SEMANTICS %
%sort eval {_ tm} {_ i} %.
%mode eval %in %out %.
%term eval/n eval (n N) N %.
%term eval/let %pi (eval (let E E*) N) %<- (eval (E* E) N) %.
%term eval/@ %pi (eval (@ F E1 E2) N) %<- (eval E1 M1) %<- (eval E2 M2) %<- (apply F M1 M2 N) %.
%worlds () (eval E _) %.
%covers eval %in %out %.
%unique eval %in %out %.
% EXAMPLES %
%term plus binop %.
%term plus/_ %pi (apply plus M N P) %<- (add M N P) %.
%term times binop %.
%term times/_ %pi (apply times M N P) %<- (mult M N P) %.
%total (M1) (apply F M1 M2 _) %.
%unique apply %in %in %in %out %.
%worlds () (eval E _) %.
%covers eval %in %out %.
%unique eval %in %out %.
%query 1 _ _ eval (let (n (s s z)) ([two] let (n (s s s z)) ([three] @ plus two (@ times two three)))) N %.