--- a/automaton-in-agda/src/bijection.agda	Mon Jul 05 11:10:15 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Mon Jul 05 15:35:48 2021 +0900
@@ -314,7 +314,6 @@
 
 open import nat
 
-open ≡-Reasoning
 
 --   []     0
 --   0    → 1
@@ -322,6 +321,12 @@
 --   01   → 3
 --   11   → 4
 --   ...
+
+record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where
+  field
+     nlist : List Bool
+     isBin : lton nlist ≡ n
+
 --
 {-# TERMINATING #-}
 LBℕ : Bijection ℕ ( List Bool ) 
@@ -338,6 +343,41 @@
      lton : List Bool → ℕ
      lton [] = 0
      lton x  = suc (lton1 x)
+
+     lb : (n : ℕ) → LB n lton
+     lb zero = record { nlist = [] ; isBin = refl }
+     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
+     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; 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
+        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 = {!!} 
+          }
+
+
      ntol1 : ℕ → List Bool 
      ntol1 0 = []
      ntol1 (suc x) with div2 (suc x)
@@ -360,12 +400,12 @@
      div20 x x1 eq = begin
          x1 + x1 ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
          div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
-         suc x ∎ 
+         suc x ∎ where open ≡-Reasoning
      div21 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , true ⟫  → suc  (x1 + x1) ≡ suc x
      div21 x x1 eq = begin
          suc  (x1 + x1) ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
          div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
-         suc x ∎ 
+         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)
@@ -374,14 +414,14 @@
          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) ∎ 
+         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) ∎ 
+         suc (suc x) ∎ where open ≡-Reasoning
      lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
      lbiso0 zero = refl
      lbiso0 (suc zero) = refl