[Hol-info] defining mutually recursive functions that use two categories of variables

[<w_...@en...>]

I am trying to define mutually recursive functions that use two  
categories of variables: time and space coordinates. HOL did not  
distinguish between arguments when trying to prove termination. Is it  
possible to specify the set of arguments that need to be considered  
for proofing termination.

In the following simple example, The time argument of the calling  
function is always strictly greater than those of the called functions.
This should be enough for the functions to terminate.
  To define them using HOL, we have to prove that the summation of the  
arguments  of each of the called functions is strictly less than the  
summation of the arguments of the calling function, which is not true  
here.

val defn = Hol_defn "fn1fn2"
`(fn1 t x y =
      if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
    (fn1 (t - 1) x y ) + (fn2 (t - 1) x (y+1)))
/\
(fn2 t x y  =
      if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
	(fn2 (t - 1) x y) + (fn1 (t - 1) x (y+1)))
`;

-  e (WF_REL_TAC `^R`);
OK..
1 subgoal:
> val it =
     (!y x t. ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==> 0 < t) /\
     (!y x t.
        ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==>
        t - 1 + (x + (y + 1)) < t + (x + y)) /\
     (!y x t. ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==> 0 < t) /\
     !y x t.
       ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==>
       t - 1 + (x + (y + 1)) < t + (x + y)

      : goalstack
-

Walid