[Agda] Size change of higher order arguments

[Shin-Cheng Mu]

Hi,

The proposition Acc _<_ x states that x is "accessible" -- that is,
every element smaller than x is accessible. The following definition
is similar to the one in Logic.Induction.WellFounded:

   data Acc {a : Set}(_<_ : a -> a -> Set) : a -> Set where
     acc : (x : a) -> (forall y -> y < x -> Acc _<_ y) -> Acc _<_ x

We can define a fold for acc:

   acc-fold : {a : Set} (_<_ : a -> a -> Set) {P : a -> Set} ->
     ((x : a) -> (forall y -> y < x -> P y) -> P x) ->
       (z : a) -> Acc _<_ z -> P z
   acc-fold _<_ =A3X z (acc h) =3D
     =A3X z (\y y<z -> acc-fold _<_ =A3X y (h y y<z))

The definition passes the termination check, as I had wished.
However, I am curious why. In the recursive call:

    acc-fold _<_ =A3X y (h y y<z)

the third argument "h y y<z" does not seem structurally
"smaller" than "acc h", in the same way "n" is smaller than
"suc n", for example.

I had an impression that Agda uses a kind of size-change termination.
How is size-change of higher order arguments defined?
Is the termination checker of Agda documented somewhere?

Thanks.

best regards,
Shin