# [Agda] strange termination check

Sergei Meshveliani mechvel at botik.ru
Thu Oct 10 19:57:36 CEST 2013

```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

```