eq(evalinsertsortstart(A,B,C,D),1,[evalinsertsortentryin(A,B,C,D)],[]).
eq(evalinsertsortreturnin(A,B,C,D),1,[evalinsertsortstop(A,B,C,D)],[]).
eq(evalinsertsortentryin(A,B,C,D),1,[evalinsertsortbb5in(1,B,C,D,E,F,G,H,I),loop_cont_evalinsertsortbb5in(F,G,H,I)],[E=0]).
eq(evalinsertsortentryin(A,B,C,D),1,[evalinsertsortbb5in(1,B,C,D,E,F,G,H,I)],[E=1]).
eq(loop_cont_evalinsertsortbb5in(A,B,C,D),0,[evalinsertsortreturnin(A,B,C,D)],[]).
eq(evalinsertsortbb5in(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbbin(A,B,C,D,E,F,G,H,I)],[B>=A+1]).
eq(evalinsertsortbb2in(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb3in(A,B,C,D,E,F,G,H,I)],[D>=0]).
eq(evalinsertsortbbin(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb2in(A,B,J,A-1,K,L,M,N,O),loop_cont_evalinsertsortbb2in(L,M,N,O,E,F,G,H,I)],[K=0]).
eq(evalinsertsortbbin(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb2in(A,B,J,A-1,K,L,M,N,O)],[E=1,K=1]).
eq(evalinsertsortbb3in(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb1in(A,B,C,D,E,F,G,H,I)],[J>=C+1]).
eq(loop_cont_evalinsertsortbb2in(A,B,C,D,E,F,G,H,I),0,[evalinsertsortbb4in(A,B,C,D,E,F,G,H,I)],[]).
eq(evalinsertsortbb1in(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb2in(A,B,C,D-1,E,F,G,H,I)],[]).
eq(evalinsertsortbb4in(A,B,C,D,E,F,G,H,I),1,[evalinsertsortbb5in(A+1,B,C,D,E,F,G,H,I)],[]).
eq(evalinsertsortbb5in(A,B,C,D,E,A,B,C,D),1,[],[E=0,A>=B]).
eq(evalinsertsortbb3in(A,B,C,D,E,A,B,C,D),1,[],[E=0,C>=F]).
eq(evalinsertsortbb3in(A,B,C,D,E,A,B,C,D),0,[],[E=1,F>=C]).
eq(evalinsertsortbb2in(A,B,C,D,E,A,B,C,D),1,[],[E=0,0>=D+1]).