eq(0,0,true).
eq(0,s(X),false).
eq(s(X),0,false).
eq(s(X),s(Y),Z):- eq(X,Y,Z).
le(0,Y,true).
le(s(X),0,false).
le(s(X),s(Y),Z):- le(X,Y,Z).
app(nil,Y,Y).
app(add(N,X),Y,add(N,add(X,Y))).
min(add(N,nil),N).
min(add(N,add(M,X)),Y):- le(N,M,Z),ifmin(Z,add(N,add(M,X)),Y).
ifmin(true,add(N,add(M,X)),Z):- min(add(N,X),Z).
ifmin(false,add(N,add(M,X)),Z):- min(add(M,X),Z).
rm(N,nil,nil).
rm(N,add(M,X),Z):- ifrm(eq(N,M),N,add(M,X),Z).
ifrm(true,N,add(M,X),Z):- rm(N,X,Z).
ifrm(false,N,add(M,X),add(M,Z)):- rm(N,X,Z).
minsort(nil,nil,nil).
minsort(add(N,X),Y, U):- min(add(N,X),Z), eq(N,Z,T), ifminsort(T, add(N,X), Y, U).
ifminsort(true,add(N,X),Y, add(N,V)):- rm(N,X,U), app(U,Y,T), minsort(T,nill,V).
ifminsort(false,add(N,X),Y,V):- minsort(X,add(N,Y),V).