Example

Example


Put on your computer the program 
% When permute(List,Permutation) is called with some list  List  one gets
% by backtracking all the permutations of  List
  
permute([],[]).
permute([X|Y],[U|V]) :- delete(U,[X|Y],W),permute(W,V).
delete(X,[X|Y],Y).
delete(U,[X|Y],[X|Z]) :- delete(U,Y,Z).

If you give TermiLog you'll get 
The results of TermiLog:

There may be non-termination ---
there is a circular variant without a forward positive cycle:
query(permute(b,f),[])
DOMAIN: [node(permute,*,1,b),node(permute,*,2,f)]
RANGE: [node(permute,+,1,b),node(permute,+,2,f)]
EDGES: []
ARCS: []

This means that TermiLog does not detect a decrease in argument size between recursive calls to permute.
Now if you perform the constraint inference you'll get 
The results of TermiLog:


Query terminates


All Q-M pairs are:
query(permute(b,f),[])
DOMAIN: [node(permute,*,1,b),node(permute,*,2,f)]
RANGE: [node(permute,+,1,b),node(permute,+,2,f)]
EDGES: []
ARCS: [arc(node(permute,*,1,b),node(permute,+,1,b))]
********************************************
query(delete(f,b,f),[])
DOMAIN: [node(delete,*,1,f),node(delete,*,2,b),node(delete,*,3,f)]
RANGE: [node(delete,+,1,f),node(delete,+,2,b),node(delete,+,3,f)]
EDGES: [edge(node(delete,*,1,f),node(delete,+,1,f))]
ARCS: [arc(node(delete,*,2,b),node(delete,+,2,b))]
********************************************

2 pairs in all.
Time for constructing Q-M pairs: 0.02 seconds
If you had used the List Size Norm instead of the Term Size Norm the results in this particular case would have been similar, but the meaning is different.
Proving termination of permute(b,f) with the Term Size Norm means that there is termination for queries where the first argument is ground (for example permute([1,2,3],P)).
Doing so with the List Size Norm means that there is termination for queries where the first argument is a list of fixed length (for example permute([X,f(X,Y),g(Z)],P)