eq(f2(A,B,C,D),1,[f1(A,B,C,D,E,F,G,H,I),loop_cont_f1(F,G,H,I)],[E=0]).
eq(f2(A,B,C,D),1,[f1(A,B,C,D,E,F,G,H,I)],[E=1]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(1+A,B,J,D,E,F,G,H,I)],[J>=1,B>=1+A]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(1+A,B,J,D,E,F,G,H,I)],[0>=J+1,B>=1+A]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,B,0,D,E,F,G,H,I)],[B>=1+A]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(1+A,A,J,D,E,F,G,H,I)],[J>=1,B>=K,A=B]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(1+A,A,J,D,E,F,G,H,I)],[0>=J+1,B>=K,A=B]).
eq(f1(A,B,C,D,E,F,G,H,I),1,[f1(A,A,0,D,E,F,G,H,I)],[B>=J,A=B]).
eq(f1(A,B,C,D,E,A,B,C,F),1,[],[E=1,A>=B,A>=B+1]).
eq(f1(A,B,C,D,E,A,B,C,F),1,[],[E=1,A>=B,B>=A+1]).