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