Consider the code (this is attempt to formalize base-2 arithmetics)
data Bit : Set₀
where
bit'0 :
Bit
bit'1 :
Bit
data BitList : Set₀
where
bleaf :
BitList
bbranch : Bit → BitList →
BitList
data ℕ : Set₀
where
bzero :
ℕ
btop : BitList →
ℕ
private
_+'_ : BitList → BitList →
BitList
bleaf +' bleaf = bbranch bit'0
bleaf
bleaf +' bbranch bit'0 y' = bbranch bit'1
y'
bleaf +' bbranch bit'1 y' = bbranch bit'0 ( bleaf +' y'
)
bbranch bit'0 y' +' bleaf = bbranch bit'1
y'
bbranch bit'1 y' +' bleaf = bbranch bit'0 ( y' +'
bleaf)
bbranch bit'0 y1 +' bbranch bit'0 y2 = bbranch bit'0 ( y1 +' y2
)
bbranch bit'0 y1 +' bbranch bit'1 y2 = bbranch bit'1 ( y1 +' y2
)
bbranch bit'1 y1 +' bbranch bit'0 y2 = bbranch bit'1 ( y1 +' y2
)
bbranch bit'1 y1 +' bbranch bit'1 y2 = bbranch bit'0 ( ( bleaf +' y1 )
+' y2 ) -- termination checker fails here.
_+_ : ℕ → ℕ →
ℕ
bzero + bzero =
bzero
bzero + btop y = btop
y
btop y + bzero = btop
y
btop y + btop y' = btop ( y +' y'
)
How to prove, that it WILL terminate?