# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615656731 -32400
# Node ID 684f53fb9b2cdbbc2ccd0342c8d5f4a62152b391
# Parent  70beed7c4e300098a879e0a22db9e2a7c54b1ee7
...

diff -r 70beed7c4e30 -r 684f53fb9b2c agda/halt.agda
--- a/agda/halt.agda	Sat Mar 13 17:33:26 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 02:32:11 2021 +0900
@@ -113,12 +113,49 @@
 
 open _∧_
 
---   []     case1
---   0    → case2 10   
---   0111 → case2 10111
+open import nat
+
+--   []     0
+--   0    → 1
+--   1    → 2
+--   01   → 3
+--   11   → 4
+--   ...
 --
-LBℕ : Bijection  ( List Bool ) ℕ
-LBℕ = {!!}
+{-# TERMINATING #-}
+LBℕ : Bijection ℕ ( List Bool ) 
+LBℕ = record {
+       fun←  = λ x → lton x 
+     ; fun→  = λ n → ntol n 
+     ; fiso← = lbiso0 
+     ; fiso→ = {!!}
+   } where
+     lton1 : List Bool → ℕ
+     lton1 [] = 0
+     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)
+     ntol1 : ℕ → List Bool 
+     ntol1 0 = []
+     ntol1 (suc x) with div2 (suc x)
+     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1
+     ... | ⟪ 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))  ⟫
+     lbiso1 :  (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
+     lbiso1 = {!!}
+     lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
+     lbiso0 zero = refl
+     lbiso0 (suc zero) = refl
+     lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) {!!} ( lbiso1 (suc x)) where
+        hh : suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
+        hh = ?
 
 
 open import Axiom.Extensionality.Propositional
diff -r 70beed7c4e30 -r 684f53fb9b2c agda/nat.agda
--- a/agda/nat.agda	Sat Mar 13 17:33:26 2021 +0900
+++ b/agda/nat.agda	Sun Mar 14 02:32:11 2021 +0900
@@ -55,10 +55,17 @@
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )
 
+-- x ^ y
 exp : ℕ → ℕ → ℕ
 exp _ zero = 1
 exp n (suc m) = n * ( exp n m )
 
+div2 : ℕ → (ℕ ∧ Bool )
+div2 zero =  ⟪ 0 , false ⟫
+div2 (suc zero) =  ⟪ 0 , true ⟫
+div2 (suc (suc n)) =  ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where
+    open _∧_
+
 minus : (a b : ℕ ) →  ℕ
 minus a zero = a
 minus zero (suc b) = zero
diff -r 70beed7c4e30 -r 684f53fb9b2c agda/prime.agda
--- a/agda/prime.agda	Sat Mar 13 17:33:26 2021 +0900
+++ b/agda/prime.agda	Sun Mar 14 02:32:11 2021 +0900
@@ -23,6 +23,9 @@
       prime : Prime factor
       dividable : Dividable factor n
 
+isPrime : ( n : ℕ ) → Dec ( Prime n )
+isPrime = ?
+
 nonPrime : ( n : ℕ ) → ¬ Prime n → NonPrime n
 nonPrime n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
     np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
@@ -43,18 +46,6 @@
   factm : (n m : ℕ ) → n < (suc m) →  Dividable n (factorial m )
   factm = {!!}
   fact : (n : ℕ ) → n < (suc (factorial (suc m))) →   gcd (suc (factorial (suc m))) n ≡ 1
-  fact n lt = fact12  (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) ? )) where
-       fact10 : Dividable n (factorial (suc m)) → gcd (suc (factorial (suc m))) n ≡ 1
-       fact10 d = begin
-            gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd (suc k) n) (sym (Dividable.is-factor d )) ⟩
-            gcd (suc (Dividable.factor d * n + 0))   n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) {!!} ⟩
-            gcd ( (Dividable.factor d * n + 0) + 1)  n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (Dividable.factor d * n) 0) ⟩
-            gcd ( Dividable.factor d * n + 1)  n   ≡⟨  gcdmul+1 (Dividable.factor d)  n  ⟩
-            1 ∎  
+  fact n lt = fact12  (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) {!!} )) where
        fact12 : NonPrime (factorial (suc m)) → gcd (suc (factorial (suc m))) n ≡ 1
        fact12 np = {!!}
-       fact11 : gcd (suc (factorial (suc m))) n ≡ 1
-       fact11 with <-cmp n (suc m)
-       ... | tri< a ¬b ¬c = fact10 ( factm n (suc m) {!!} ) 
-       ... | tri≈ ¬a b ¬c = fact10 ( factm n (suc m) {!!} ) 
-       ... | tri> ¬a ¬b c = fact12 (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) {!!} ))