open import Relation.Binary.PropositionalEquality
open import Data.Sum
open import Data.Product
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable
open import Relation.Binary.Core
open import Relation.Nullary
open import Data.Nat using (ℕ) renaming (_+_ to _⊹_)

data Digit : Set where
  zero : Digit
  one : Digit
  two : Digit

data Digits : Set
last : Digits → Digit

infixl 3 [_] _⟨_⟩∷_
data Digits where
  [_] : Digit → Digits
  _⟨_⟩∷_ : (ds : Digits) → (nice : last ds ≢ zero) → (d : Digit) → Digits

last [ x ] = x
last (ds ⟨ nice ⟩∷ d) = last ds


suc' : Digits → (∃ λ ds → last ds ≢ zero)
suc' [ zero ] = [ one ] , λ ()
suc' [ one ] = [ two ] , λ ()
suc' [ two ] = ([ one ] ⟨ (λ ()) ⟩∷ zero) , λ ()
suc' (ds ⟨ nice ⟩∷ zero) = (ds ⟨ nice ⟩∷ one) , nice
suc' (ds ⟨ nice ⟩∷ one) = (ds ⟨ nice ⟩∷ two) , nice
suc' (ds ⟨ nice ⟩∷ two) = ((proj₁ deeper) ⟨ proj₂ deeper ⟩∷ zero) , proj₂ deeper
  where
  deeper = suc' ds


suc : Digits → Digits
suc ds = proj₁ (suc' ds)


infixl 4 _+_
_+_ : (a b : Digits) → Digits
help : (a b : Digits) → last a ≢ zero → last b ≢ zero → last (a + b) ≢ zero

[ zero ] + x = x
[ one ] + x = suc x
[ two ] + x = suc (suc x)
x + [ zero ] = x
x + [ one ] = suc x
x + [ two ] = suc (suc x)
(a ⟨ nice ⟩∷ zero) + (b ⟨ nice₁ ⟩∷ d) = ((a + b) ⟨ help a b nice nice₁ ⟩∷ d)
(a ⟨ nice ⟩∷ d) + (b ⟨ nice₁ ⟩∷ zero) = ((a + b) ⟨ help a b nice nice₁ ⟩∷ d)
(a ⟨ nice ⟩∷ one) + (b ⟨ nice₁ ⟩∷ one) = ((a + b) ⟨ help a b nice nice₁ ⟩∷ two)
(a ⟨ nice ⟩∷ one) + (b ⟨ nice₁ ⟩∷ two) = (proj₁ deeper ⟨ proj₂ deeper ⟩∷ zero)
  where
  deeper = suc' (a + b)
(a ⟨ nice ⟩∷ two) + (b ⟨ nice₁ ⟩∷ one) = (proj₁ deeper ⟨ proj₂ deeper ⟩∷ zero)
  where
  deeper = suc' (a + b)
(a ⟨ nice ⟩∷ two) + (b ⟨ nice₁ ⟩∷ two) = (proj₁ deeper ⟨ proj₂ deeper ⟩∷ one)
  where
  deeper = suc' (suc (a + b))


help [ zero ] b x y = y
help [ one ] b x y = proj₂ (suc' b)
help [ two ] b x y = proj₂ (suc' (suc b))
help (a ⟨ nice ⟩∷ d) [ zero ] x y = x
help (a ⟨ nice ⟩∷ d) [ one ] x y = proj₂ (suc' (a ⟨ nice ⟩∷ d))
help (a ⟨ nice ⟩∷ d) [ two ] x y = proj₂ (suc' (suc (a ⟨ nice ⟩∷ d)))
help (a ⟨ nice ⟩∷ zero) (b ⟨ nice₁ ⟩∷ d) x y = help a b x y
help (a ⟨ nice ⟩∷ one) (b ⟨ nice₁ ⟩∷ zero) x y = help a b x y
help (a ⟨ nice ⟩∷ one) (b ⟨ nice₁ ⟩∷ one) x y = help a b x y
help (a ⟨ nice ⟩∷ one) (b ⟨ nice₁ ⟩∷ two) x y = proj₂ (suc' (a + b))
help (a ⟨ nice ⟩∷ two) (b ⟨ nice₁ ⟩∷ zero) x y = help a b x y
help (a ⟨ nice ⟩∷ two) (b ⟨ nice₁ ⟩∷ one) x y = proj₂ (suc' (a + b))
help (a ⟨ nice ⟩∷ two) (b ⟨ nice₁ ⟩∷ two) x y = proj₂ (suc' (suc (a + b)))


infixl 5 _|*_
_|*_ : Digit → Digits → Digits
zero |* b = [ zero ]
one |* b = b
two |* b = b + b


step' : Digits → Digits → Digits
step' xs [ x ] = x |* xs
step' xs (ys ⟨ nice ⟩∷ x) = step' (x |* xs) ys

step : Digits → Digits
step = step' [ one ]



contains0 :