eq(f2(A,B,C,D),1,[f300(A,B,C,D,E,F,G,H,I),loop_cont_f300(F,G,H,I)],[E=0]).
eq(f2(A,B,C,D),1,[f300(A,B,C,D,E,F,G,H,I)],[E=1]).
eq(f300(A,B,C,D,E,F,G,H,I),1,[f300(1+A,B,J,D,E,F,G,H,I)],[J>=1,B>=1+A]).
eq(f300(A,B,C,D,E,F,G,H,I),1,[f300(1+A,B,J,D,E,F,G,H,I)],[0>=J+1,B>=1+A]).
eq(f300(A,B,C,D,E,F,G,H,I),1,[f300(A,-1+B,0,D,E,F,G,H,I)],[B>=1+A]).
eq(f300(A,B,C,D,E,A,B,C,F),1,[],[E=1,A>=B]).