--- a/automaton-in-agda/src/bijection.agda	Mon Jul 05 18:32:15 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Mon Jul 05 23:19:59 2021 +0900
@@ -336,12 +336,12 @@
      ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl
    } where
      lton1 : List Bool → ℕ
-     lton1 [] = 0
+     lton1 [] = 1
      lton1 (true ∷ t) = suc (lton1 t + lton1 t)
      lton1 (false ∷ t) = lton1 t + lton1 t
      lton : List Bool → ℕ
      lton [] = 0
-     lton x  = suc (lton1 x)
+     lton x  = pred (lton1 x)
 
      lb : (n : ℕ) → LB n lton
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = {!!} }
@@ -356,10 +356,12 @@
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
-           suc (lton (false ∷ t))  ≡⟨ cong (λ k → suc (lton k)) (sym eq)  ⟩ 
+           lton1 t + lton1 t   ≡⟨ {!!} ⟩ 
+           suc (pred (lton1 t + lton1 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 } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb05 lb03 ; isUnique = {!!}  } where
+     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = {!!}  } where
         lb05 :  1 < length (true ∷ t)
         lb05 = {!!}
         lb03 : lton (true ∷ t) ≡ n
@@ -373,36 +375,62 @@
         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
+        lb-1 : List Bool → List Bool
+        lb-1 [] =  []
+        lb-1 (true ∷ t) = false ∷ t 
+        lb-1 (false ∷ t) with lb-1 t
+        ... | [] = true ∷ []
+        ... | x ∷ t1 = true ∷ x ∷ t1
 
         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 ⟩ 
+        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t) 
+        lb04 [] = refl
+        lb04 (false ∷ t) = refl
+        lb04 (true ∷ []) = refl
+        lb04 (true ∷ t0 )  = begin
+           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ 
+           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩ 
+           lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
+              open ≡-Reasoning
+        tt1 : (t : List Bool) → Set
+        tt1 t = suc (lton1 t) ≡ lton1 (lb+1 t) 
+        tt2 = tt1 []
+        tt3 = tt1 (true ∷ [])
+        tt4 = tt1 (true ∷ true ∷ [])
+        tt6 : (n : ℕ) → List Bool
+        tt6 zero = []
+        tt6 (suc n) = lb+1 (tt6 n)
+        tt61 : (n : ℕ) → List (List Bool)
+        tt61 zero = []
+        tt61 (suc n) = lb+1 (tt6 n) ∷ tt61 n
+        tt7 : (n : ℕ) → Set
+        tt7 n = tt1 ( tt6 n )
+        tt9 : (n : ℕ) → List Bool → List Bool
+        tt9 zero x = x 
+        tt9 (suc n) x = lb-1 (tt9 n x)
+        tta : (n m : ℕ) →  List Bool
+        tta n m = tt9 m ( tt6 n)
+        ttb = Data.List.map lb-1 (tt61 10)
+        ttc = Data.List.map lb+1 (tt61 10)
+        ttd = Data.List.map lton (tt61 200)
+        ttf = tt61 128
+        tt5 = {!!}
+
+        lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n
+        lb02 [] refl = refl
+        lb02 (false ∷ t) eq = begin
+           lton (lb+1 (false ∷ t))  ≡⟨ {!!} ⟩ 
+           suc (suc (lton1 t + lton1 t))  ≡⟨ cong suc {!!} ⟩ 
            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 ⟩  
+        lb02 (true ∷ []) eq = ?
+        lb02 (true ∷ (t1 ∷ t2) ) eq1 =  begin
+           lton (lb+1 (true ∷ t0))  ≡⟨ {!!} ⟩ 
+           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)) ≡⟨ cong suc (add11 (lton1 t0) ) ⟩ 
+           suc (suc (suc (lton1 t0 + lton1 t0)))  ≡⟨ cong suc {!!} ⟩  
            suc n ∎  where
              open ≡-Reasoning
              t0 = t1 ∷ t2
@@ -411,7 +439,7 @@
      ntol : ℕ → List Bool 
      ntol 0 = []
      ntol 1 = false ∷ []
-     ntol (suc n) = ntol1 n
+     ntol (suc n) = {!!}
      xx :   (x : ℕ ) → List Bool ∧ ℕ
      xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
      add12 : (x1 x : ℕ ) → suc x1 + x ≡ x1 + suc x