[Agda] termination problem

[mechvel at scico.botik.ru]

Dear Agda developers,

There is a certain particular effect in termination check in Agda-2.6.1.

-- Sum of two monomial lists. For the same exponents the coefficients 
are summed by
-- _+_. If e > e', then the first head monomial is put ahead.
-- It is almost same as merging lists.

_+ms_ : Op₂ (List Mon)
[]                  +ms mons'                 =  mons'
mons                +ms []                    =  mons
((monᶜ a e) ∷ mons) +ms ((monᶜ b e') ∷ mons') =  with <-cmp e e'
...
     | tri> _ _ _ =  (monᶜ a e)  ∷ (mons +ms ((monᶜ b e') ∷ mons'))
... | tri< _ _ _ =  (monᶜ b e') ∷ (((monᶜ a e) ∷ mons) +ms mons')
... | tri≈ _ _ _ =  (monᶜ (a + b) e) ∷ (mons +ms mons')

On the right hand side, +ms is applied to the two lists, and at least 
one of these lists
is a tail of the corresponding argument on the left hand side.

Agda reports of unproved termination.
All right, this is a known effect. One has to introduce a counter as an 
additional argument.

Instead I try another version for the last sentence:

((monᶜ a e) ∷ mons) +ms ((monᶜ b e') ∷ mons') =
   with <-cmp e e' | (monᶜ b e') ∷ (((monᶜ a e) ∷ mons) +ms mons')   -- I
                   | (monᶜ (a + b) e) ∷ (mons +ms mons')             -- 
II
                   | (monᶜ a e) ∷ (mons +ms ((monᶜ b e') ∷ mons'))   -- 
III
... | tri< _ _ _ | xs | _  | _  = xs
... | tri≈ _ _ _ | _  | ys | _  = ys
... | tri> _ _ _ | _  | _  | zs = zs

And it is type-checked.

1) Can you, please, comment this?
2) For a good performance, only a single term among {I, II, II} needs to 
be computed.
    Will this be so?

Thanks,

------
Sergei