eq(f0(A,B,C,D),1,[f1(A,B,2,D,E,F,G,H,I),loop_cont_f1(F,G,H,I)],[E=0,A>=0,3>=A,3>=B,B>=0]).
eq(f0(A,B,C,D),1,[f1(A,B,2,D,E,F,G,H,I)],[E=1,A>=0,3>=A,3>=B,B>=0]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B+1,C,B+1,E,F,G,H,I)],[C+A>=2*B+1,0>=2]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B+1,C,B+1,E,F,G,H,I)],[C+A>=2*B+1]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B-1,C,B-1,E,F,G,H,I)],[2*B>=2+C+A]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B-1,C,B-1,E,F,G,H,I)],[2*B>=2+C+A,0>=2]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B,C,B,E,F,G,H,I)],[0>=1,2*B>=C+A,C+A+1>=2*B]).
eq(f1(A,B,C,D,E,A,B,C,D),0,[],[E=1]).