[Agda] strange termination check

[Sergei Meshveliani]

Please, why the below  powerToPos  is not checked as terminating ?


{-# OPTIONS --termination-depth=3 #-}
module Report where
open import Level    using () renaming (zero to 0ℓ)
open import Function using (case_of_)
open import Relation.Binary 
            using (module Setoid; module IsEquivalence;_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Algebra    using (Semigroup; module Semigroup)
open import Data.Empty using (⊥)
open import Data.List  using ([]; _∷_)
open import Data.Fin   using (Fin) renaming (zero to 0b; suc to sucB)
open import Data.Digit using (Bit)
open import Data.Bin   using (Bin⁺)
          
1b : Bit
1b = sucB 0b

postulate H : Semigroup 0ℓ 0ℓ

open Semigroup H using (setoid; _≈_; _∙_)
                       renaming (Carrier to C; isEquivalence to ≈equiv)
open IsEquivalence ≈equiv using ()
                 renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)

HasLast1 : Bin⁺ → Set       -- "is the bit list of a non-zero binary"
HasLast1 []           =  ⊥
HasLast1 (b ∷ [])     =  b ≡ 1b
HasLast1 (_ ∷ b ∷ bs) =  HasLast1 (b ∷ bs)

powerToPos : C → (bs : Bin⁺) → HasLast1 bs → C
powerToPos _ []            ()
powerToPos x (1b ∷ [])     _             =  x
powerToPos x (b ∷ b' ∷ bs) last1-b:b':bs =
                           case b of \ { 0b              → p ∙ p
                                       ; (sucB 0b)       → x ∙ (p ∙ p)
                                       ; (sucB (sucB ()))
                                       }
                           where
                           last1-b':bs : HasLast1 (b' ∷ bs)
                           last1-b':bs = last1-b:b':bs

                           p = powerToPos x (b' ∷ bs) last1-b':bs
----------------------------------------------------------------------------

The recursion     (b ∷ b' ∷ bs)  -->  (b' ∷ bs)  

by the second argument is well-founded. Why does not the checker see the
termination proof? 

Thanks,

------
Sergei