%% s(X,X) :- X=error.
%% s(X,Xf) :- not X=error, p(X)=1, Xf=X.
%% s(X,Xf) :- not X=error, p(X)=0, s(h(X),Y), s(Y,Xf).

unfold(s(X,Xf),
	[
         body([], [eq(X,error),eq(X,Xf)]),
	 body([], [neq(X,error),eq(p(X),1),eq(X,Xf)]),
	 body([s(h(X),Y),s(Y,Xf)], [neq(X,error),eq(p(X),0)])
        ]).

% To Prove:
%
% s(X,Y), s(Y,Xf) |= s(X,Xf)

run :-
	set_counter(assertionnumber, 0),
 	addunfoldlevel(0, [s(X,Y), s(Y,Xf)],
 	               UnfoldableGAtoms),
        addunfoldlevel(0, [s(X,Xf)],
 		       UnfoldableHAtoms),
	lprove(0, 0, [], UnfoldableGAtoms, [],
		     [], UnfoldableHAtoms, [], []),
        printf("PROOF FAILED.\n", []).
run :-
	counter_value(assertionnumber, X),
	printf("Proof succeed\n", []),
	printf("Number of assertions: %\n", [X]).


:- consult('datastruct.clpr').