Определение инварианта цикла для рекурсивной функции

Question

Предположим, у вас есть функция, которая возвращает разницу в длине между двумя массивами, однако она использует не обычные методы для определения длины, а рекурсивную функцию.
Можете ли вы помочь мне найти инвариант цикла? Я понимаю, что инвариант цикла - это то, что должно быть верно до условия и после условия. Однако я не могу этого понять. Вот код:

function func (int arr1_length, int arr2_length) {
   if (arr1_length == 0 && arr2_length == 0) return 0;
   if (arr1_length == 0) return arr2_length;
   if (arr2_length == 0) return arr1_length;
   return func (arr1_length-1, arr2_length-1);
}

Первый вызов - это func(arr1.length, arr2.length);