reduction(if @ A @ B @ C, Y) :- !,
reduction(A, X),
(X == 0 ->
reduction(C, Y) ;
reduction(B, Y)).
reduction(A @ B, Y) :- !,
reduction(A, P),
reduction(B, Q),
reduction(z(X,Y), z(X,Y)) :- !.
reduction(A * B, C) :- !,
reduction(A, A2),
reduction(B, B2),
reduction(A - B, C) :- !,
reduction(A, A2),
reduction(B, B2),
reduction
(X
, X
) :- write('cannot reduction' :- X
), nl, halt.
?-
Y = z(F, z(X, F @ z(V, X @ X @ V)) @ z(X, F @ z(V, X @ X @ V))),
reduction(Y @ z(H, z(N, if @ N @ (H @ (N - 1) * N) @ 1)) @ 7, Result),
CjotIG9wKDEwMCwgeWZ4LCAnQCcpLgoKcmVkdWN0aW9uKGlmIEAgQSBAIEIgQCBDLCBZKSA6LSAhLAogICAgcmVkdWN0aW9uKEEsIFgpLAoJKFggPT0gMCAtPgoJCXJlZHVjdGlvbihDLCBZKSA7CgkJcmVkdWN0aW9uKEIsIFkpKS4KCnJlZHVjdGlvbihBIEAgQiwgWSkgOi0gISwKCXJlZHVjdGlvbihBLCBQKSwKCXJlZHVjdGlvbihCLCBRKSwKCWNvcHlfdGVybShQLCB6KFEsIFgpKSwgcmVkdWN0aW9uKFgsIFkpLgoKcmVkdWN0aW9uKHooWCxZKSwgeihYLFkpKSA6LSAhLgoKcmVkdWN0aW9uKEEgKiBCLCBDKSA6LSAhLAoJcmVkdWN0aW9uKEEsIEEyKSwKCXJlZHVjdGlvbihCLCBCMiksCglDIGlzIEEyICogQjIuCgpyZWR1Y3Rpb24oQSAtIEIsIEMpIDotICEsCglyZWR1Y3Rpb24oQSwgQTIpLAoJcmVkdWN0aW9uKEIsIEIyKSwKCUMgaXMgQTIgLSBCMi4KCnJlZHVjdGlvbihYLCBYKSA6LSBpbnRlZ2VyKFgpLCAhLgpyZWR1Y3Rpb24oWCwgWCkgOi0gd3JpdGUoJ2Nhbm5vdCByZWR1Y3Rpb24nIDotIFgpLCBubCwgaGFsdC4KCj8tCglZID0geihGLCB6KFgsIEYgQCB6KFYsIFggQCBYIEAgVikpIEAgeihYLCBGIEAgeihWLCBYIEAgWCBAIFYpKSksCglyZWR1Y3Rpb24oWSBAIHooSCwgeihOLCBpZiBAIE4gQCAoSCBAIChOIC0gMSkgKiBOKSBAIDEpKSBAIDcsIFJlc3VsdCksCgl3cml0ZShSZXN1bHQpLCBubCwKCWhhbHQuCgo=