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