eq(f999(A,B),1,[f1(1,B-1,C,D,E),loop_cont_f1(D,E)],[C=0,B>=1,A=0]).
eq(f999(A,B),1,[f1(1,B-1,C,D,E)],[C=1,B>=1,A=0]).
eq(f1(A,B,C,D,E),1,[f1(A+1,B-1,C,D,E)],[B>=1]).
eq(f1(A,B,C,D,E),1,[f2(A-1,B,F,G,H),loop_cont_f2(G,H,C,D,E)],[F=0,A>=1]).
eq(f1(A,B,C,D,E),1,[f2(A-1,B,F,G,H)],[C=1,F=1,A>=1]).
eq(f2(A,B,C,D,E),1,[f2(A-1,B+1,C,D,E)],[A>=1]).
eq(loop_cont_f2(A,B,C,D,E),0,[f1(A,B,C,D,E)],[]).
eq(f1(A,B,C,A,B),0,[],[C=1]).
eq(f2(A,B,C,A+1,B-1),1,[],[C=0,B>=1]).
eq(f2(A,B,C,A,B),0,[],[C=1,1>=B+1]).