eq(f300(A),1,[f3(A,B,C),loop_cont_f3(C)],[B=0]).
eq(f300(A),1,[f3(A,B,C)],[B=1]).
eq(f3(A,B,C),1,[f3(-1+A,B,C)],[0>=A]).
eq(f3(A,B,C),1,[f3(-1+A,B,C)],[A>=1]).
eq(f3(A,B,A),0,[],[B=1]).