inssort(X,v) = p(v,X) inssort(X,p(Y,Z)) = if(gt(X,Z),p(p(Y,Z),X),p(inssort(X,Y),Z)) if(true,X,Y) = X if(false,X,Y) = Y gt(s(X),0) = true gt(0,X) = false gt(s(X),s(Y)) = gt(X,Y)