Termination check failed on decreasing second arg with increasing first

[andrey-komarov]

The following code fails to termination check:

\static \function
plus' (x y : Nat) : Nat <= \elim y
  | zero => x
  | suc y' => plus' (suc x) y'

However, if we remove suc from first argument, or swap arguments, termination checker accepts the definitions:

\static \function
plus'' (x y : Nat) : Nat <= \elim y
  | zero => x
  | suc y' => suc (plus'' x y')

\static \function
plus''' (x y : Nat) : Nat <= \elim x
  | zero => y
  | suc x' => plus''' x' (suc y)

[valis]

This is expected behaviour. The current implementation of termination checker assumes that the first argument to recursive call that differs from the corresponding parameter of the function is decreasing.