--- a/automaton-in-agda/src/bijection.agda	Tue Jul 06 01:40:18 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Tue Jul 06 11:07:11 2021 +0900
@@ -372,16 +372,50 @@
      lton x  = pred (lton1 x)
 
      lton1>0 : (x : List Bool ) → 0 < lton1 x 
-     lton1>0 x = {!!}
+     lton1>0 [] = a<sa
+     lton1>0 (true ∷ x₁) = 0<s
+     lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y
+
+     2lton1>0 : (t : List Bool ) →  0 < lton1 t + lton1 t
+     2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y
+
+     lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y)
+     lton-cons>0 {true} {[]} = refl-≤s
+     lton-cons>0 {true} {x ∷ y} =  {!!}
+     lton-cons>0 {false} {[]} = refl-≤
+     lton-cons>0 {false} {x ∷ y} = {!!}
+
+     lb=0 : {x y : ℕ } → pred x  < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1)
+     lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s)
+     lb=0 {suc x} {suc y} lt = begin
+            suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl  ⟩
+            suc (suc x) + suc x ≡⟨ refl ⟩
+            suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩
+            suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩
+            suc y + suc y ≡⟨ refl ⟩
+            suc ((suc y + suc y) ∸ 1) ∎  where open ≤-Reasoning
+     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y 
+     lb=1 {x} {y} {true} eq = {!!}
+     lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y)
+     ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a))
+     ... | tri≈ ¬a b ¬c = b
+     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c))
+
+     lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y
+     lb=b [] [] eq = refl
+     lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} ))
+     lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} ))
+     lb=b (true ∷ x) (false ∷ y) eq = {!!}
+     lb=b (false ∷ x) (true ∷ y) eq = {!!}
+     lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) 
+     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) 
 
      lb : (n : ℕ) → LB n lton
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
-         lb05 [] refl = refl
-         lb05 (true ∷ t) eq = {!!}
-         lb05 (false ∷ t) eq = {!!}
+         lb05 x eq = lb=b [] x (sym eq)
      lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
-     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = {!!} ; isBin = begin
+     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = begin
        lton (false ∷ []) ≡⟨ refl ⟩ 
        suc 0  ≡⟨ refl ⟩ 
        suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
@@ -396,17 +430,23 @@
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
-           lton1 t + lton1 t   ≡⟨ sym ( sucprd {!!} ) ⟩ 
+           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 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) lb03 ; isUnique = {!!}  } where
+     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
         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
+        -- eq : LB.nlist (lb n) ≡ true ∷ t ,  eq1 : pred (suc (lton1 t1 + lton1 t1)) ≡ suc n
+        lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
+        lb07 (true ∷ t1) eq1 = ⊥-elim (nat-≡< eq1  (begin
+           lton1 (true ∷ t1) ≤⟨ {!!} ⟩
+           suc n ∎ )) where open ≤-Reasoning  -- lton1 (true ∷ t) ∸ 1 ≡ n, lton1 t1 + lton1 t1 ≡ suc n
+        lb07 (false ∷ t1) eq1 = {!!}
 
         add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
         add11 zero = refl
@@ -427,7 +467,7 @@
         lb02 t eq1 = begin
             lton (lb+1 t) ≡⟨ refl ⟩
             pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩
-            pred (suc (lton1 t))  ≡⟨ sym (sucprd {!!} ) ⟩
+            pred (suc (lton1 t))  ≡⟨ sym (sucprd (lton1>0 t)) ⟩
             suc (pred (lton1 t)) ≡⟨ refl ⟩
             suc (lton t) ≡⟨ cong suc eq1  ⟩
             suc n ∎  where open ≡-Reasoning