--- a/automaton-in-agda/src/bijection.agda	Mon Jul 05 15:35:48 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Mon Jul 05 18:32:15 2021 +0900
@@ -326,15 +326,14 @@
   field
      nlist : List Bool
      isBin : lton nlist ≡ n
+     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x 
 
---
-{-# TERMINATING #-}
 LBℕ : Bijection ℕ ( List Bool ) 
 LBℕ = record {
        fun←  = λ x → lton x 
-     ; fun→  = λ n → ntol n 
-     ; fiso← = lbiso0 
-     ; fiso→ = lbisor
+     ; fun→  = λ n → LB.nlist (lb n) 
+     ; fiso← = λ n → LB.isBin (lb n)
+     ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl
    } where
      lton1 : List Bool → ℕ
      lton1 [] = 0
@@ -345,53 +344,76 @@
      lton x  = suc (lton1 x)
 
      lb : (n : ℕ) → LB n lton
-     lb zero = record { nlist = [] ; isBin = refl }
+     lb zero = record { nlist = [] ; isBin = refl ; isUnique = {!!} }
      lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
-     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isBin = begin
+     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = {!!} ; isBin = begin
        lton (false ∷ []) ≡⟨ refl ⟩ 
        suc 0  ≡⟨ refl ⟩ 
        suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
        suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 
        suc n ∎ }  where open ≡-Reasoning
-     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 } where
+     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = {!!}  } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
            suc (lton (false ∷ t))  ≡⟨ cong (λ k → suc (lton k)) (sym eq)  ⟩ 
            suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩ 
            suc n ∎  where open ≡-Reasoning
-     ... | true ∷ t | record { eq = eq } = n-induction {_} {_} {ℕ} {λ x → LB x lton } (λ x → x) LBN ( suc n )  where
-         div3 : ℕ → ℕ
-         div3 x with div2 x
-         ... | ⟪ n , true ⟫ = n 
-         ... | ⟪ n , false ⟫ = 0
-         lb02 : {n : ℕ} → div3 n ≡ zero → LB n lton
-         lb02 {n} eq with div2 n | inspect div2 n
-         ... | ⟪ x , true ⟫ | record { eq = eq1 } = {!!}
-         ... | ⟪ x , false ⟫ | record { eq = eq1 } = {!!}
-         LBN : Ninduction ℕ (λ x → LB x lton ) ( λ x → x )
-         LBN = record {
-             pnext = div3 
-           ; fzero = {!!}
-           ; decline = {!!} 
-           ; ind = {!!} 
-          }
+     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb05 lb03 ; isUnique = {!!}  } where
+        lb05 :  1 < length (true ∷ t)
+        lb05 = {!!}
+        lb03 : lton (true ∷ t) ≡ n
+        lb03 = begin
+           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ 
+           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ 
+           n ∎  where open ≡-Reasoning
+
+        lb+1 : List Bool → List Bool
+        lb+1 [] =  false ∷ [] 
+        lb+1 (false ∷ t) = true ∷ t 
+        lb+1 (true ∷ t) =  false ∷ lb+1 t
+
+        lb04 : (t : List Bool) → 1 < length t →  suc (lton1 t) ≡ lton1 (lb+1 t) 
+        lb04 [] ()
+        lb04 (false ∷ t) ne = refl
+        lb04 (true ∷ []) (s≤s ())
+        lb04 (true ∷ t1 ∷ t2 ) (s≤s ne) = begin
+           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ refl ⟩ 
+           suc ((1 + lton1 t0) + lton1 t0) ≡⟨ cong (λ k → suc (k + lton1 t0)) (+-comm 1 (lton1 t0)) ⟩ 
+           suc ((lton1 t0 + 1) + lton1 t0) ≡⟨ cong suc (+-assoc (lton1 t0) 1 (lton1 t0)) ⟩ 
+           suc (lton1 t0 + (1 + lton1 t0)) ≡⟨ refl ⟩ 
+           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0 ({!!}) ) ⟩ 
+           lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
+              open ≡-Reasoning
+              t0 = t1 ∷ t2
+
+        add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
+        add11 zero = refl
+        add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
+
+        lb02 : (t : List Bool) → 1 < length t → lton t ≡ n → lton (lb+1 t) ≡ suc n
+        lb02 [] lt refl = refl
+        lb02 (false ∷ t) lt eq = begin
+           lton (lb+1 (false ∷ t))  ≡⟨ refl ⟩ 
+           suc (suc (lton1 t + lton1 t))  ≡⟨ cong suc eq ⟩ 
+           suc n ∎  where open ≡-Reasoning
+        lb02 (true ∷ []) (s≤s ()) eq1
+        lb02 (true ∷ (t1 ∷ t2) ) lt eq1 =  begin
+           lton (lb+1 (true ∷ t0))  ≡⟨ refl ⟩ 
+           suc (lton1 (lb+1 t0) + lton1 (lb+1 t0)) ≡⟨ cong (λ k → suc (k + k )) (sym (lb04 t0 {!!}))  ⟩  -- suc (suc (lton1 t + lton1 t)) ≡ n
+           suc (suc (lton1 t0) + suc (lton1 t0)) ≡⟨ {!!} ⟩ 
+           suc (suc (suc (lton1 t0 + lton1 t0)))  ≡⟨ cong suc eq1 ⟩  
+           suc n ∎  where
+             open ≡-Reasoning
+             t0 = t1 ∷ t2
 
 
-     ntol1 : ℕ → List Bool 
-     ntol1 0 = []
-     ntol1 (suc x) with div2 (suc x)
-     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1 -- non terminating
-     ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
      ntol : ℕ → List Bool 
      ntol 0 = []
      ntol 1 = false ∷ []
      ntol (suc n) = ntol1 n
      xx :   (x : ℕ ) → List Bool ∧ ℕ
      xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
-     add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
-     add11 zero = refl
-     add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
      add12 : (x1 x : ℕ ) → suc x1 + x ≡ x1 + suc x
      add12 zero x = refl
      add12 (suc x1) x = cong suc (add12 x1 x)
@@ -406,39 +428,3 @@
          suc  (x1 + x1) ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
          div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
          suc x ∎ where open ≡-Reasoning
-     lbiso1 :  (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
-     lbiso1 zero = refl
-     lbiso1 (suc x) with div2 (suc x) | inspect div2 (suc x)
-     ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin
-         suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ sym (add11 _) ⟩
-         suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
-         suc x1 + suc x1 ≡⟨ add11 x1 ⟩
-         suc (suc  (x1 + x1)) ≡⟨ cong suc (div21 x x1 eq1) ⟩
-         suc (suc x) ∎ where open ≡-Reasoning
-     ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
-         suc (lton1 (ntol1 x1) + lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + lton1 (ntol1 x1) ) (lbiso1 x1) ⟩
-         suc x1 + lton1 (ntol1 x1) ≡⟨ add12 _ _ ⟩
-         x1 + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → x1 + k )  (lbiso1 x1) ⟩
-         x1 + suc x1 ≡⟨ +-comm x1 _ ⟩
-         suc (x1 + x1) ≡⟨ cong suc (div20 x x1 eq1) ⟩
-         suc (suc x) ∎ where open ≡-Reasoning
-     lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
-     lbiso0 zero = refl
-     lbiso0 (suc zero) = refl
-     lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) (hh x) ( lbiso1 (suc x)) where
-        hh : (x : ℕ ) → suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
-        hh x with div2 (suc x)
-        ... | ⟪ _ , true ⟫ = refl
-        ... | ⟪ _ , false ⟫ = refl
-     lbisor0 :  (x : List Bool) → ntol1 (lton1 (true ∷ x))  ≡ true ∷ x
-     lbisor0 = {!!}
-     lbisor1 :  (x : List Bool) → ntol1 (lton1 (false ∷ x))  ≡ false ∷ x
-     lbisor1 = {!!}
-     lbisor :  (x : List Bool) → ntol (lton x)  ≡ x
-     lbisor [] = refl
-     lbisor (false ∷ []) = refl
-     lbisor (true ∷ []) = refl
-     lbisor (false ∷ t) = trans {!!} ( lbisor1 t ) 
-     lbisor (true ∷  t) = trans {!!} ( lbisor0 t ) 
-
-