# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609122929 -32400
# Node ID 3294dbcccfe8772671ed651fec597c7f7535f0e8
# Parent  b3f05cd08d24f20519c4d7008cbbffde05b43355
...

diff -r b3f05cd08d24 -r 3294dbcccfe8 agda/halt.agda
--- a/agda/halt.agda	Sun Dec 27 13:26:44 2020 +0900
+++ b/agda/halt.agda	Mon Dec 28 11:35:29 2020 +0900
@@ -2,12 +2,13 @@
 
 open import Level renaming ( zero to Zero ; suc to Suc )
 open import Data.Nat
+open import Data.Maybe
 open import Data.List hiding ([_])
 open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
 open import Data.Unit
-open import  Relation.Binary.Core
+open import  Relation.Binary.Core hiding (_⇔_)
 open import  Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 
@@ -69,7 +70,7 @@
 LBℕ = {!!}
 
 postulate
-   utm         : List Bool → List Bool → Bool
+   utm         : List Bool → List Bool → Maybe Bool
 
 open import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
@@ -77,12 +78,21 @@
 
 record TM : Set where
    field
-      tm : List Bool → Bool
+      tm : List Bool → Maybe Bool
       encode : List Bool
       is-tm : utm encode ≡ tm
 
 open TM
 
+record Halt : Set where
+   field
+      htm : TM
+      is-halt :          (t : TM ) → (x : List Bool ) → (tm htm  (encode t ++ x) ≡ just true) ⇔ ((tm t x ≡ just true) ∨ (tm t x ≡ just false)) 
+      nhtm : TM
+      nhtm-is-negation : (t : TM ) → (x : List Bool ) → (tm htm (encode t ++ x) ≡ just true) ⇔ (tm nhtm (encode t ++ x) ≡ nothing )
+
+open Halt
+
 tm-cong : {x y : TM} → tm x ≡ tm y → encode x ≡ encode y → is-tm x ≅ is-tm y → x ≡ y
 tm-cong refl refl refl  = refl
 
@@ -97,6 +107,8 @@
          tmb1 x with is-tm x | inspect is-tm x
          ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
-halting : (halt : TM → List Bool  → Bool ) → (z : TM) →  ¬ ((x : TM) → tm z ≡ (λ y → halt x y ) )
-halting halt z halting = {!!}
-
+halting : ¬ Halt
+halting h with tm (htm h) (encode (nhtm h) ++ encode (nhtm h))
+... | just true = ¬t=f {!!} {!!}
+... | nothing = {!!}
+... | just false = {!!}
diff -r b3f05cd08d24 -r 3294dbcccfe8 agda/root2.agda
--- a/agda/root2.agda	Sun Dec 27 13:26:44 2020 +0900
+++ b/agda/root2.agda	Mon Dec 28 11:35:29 2020 +0900
@@ -53,18 +53,24 @@
        2
     ∎ where open ≡-Reasoning
 
-gcd22 : { n m : ℕ} → gcd n 2 ≡ 2 → gcd m 2 ≡ 2 → ¬ ( gcd n m ≡ 1 )
-gcd22 {zero} {suc zero} gn () gnm
-gcd22 {zero} {suc (suc m)} refl gm ()
-gcd22 {suc zero} {zero} () gm gnm
-gcd22 {suc (suc n)} {zero} gn refl ()
-gcd22 {suc (suc n)} {suc (suc m)} gn gm gnm = gcd23 (suc n) (suc m) 0 {!!} gn gm gnm where
-   gcd12 : (n i : ℕ) →  gcd1 n (suc n) (suc i) 2 ≡ 2 →  gcd1 n (suc n) (suc i) 2 ≡ 2
-   gcd12 = ?
-   gcd23 : (n m i : ℕ ) → i ≤ 2  → (gn  : gcd1 n (suc n) (suc i) 2 ≡ 2) → (gm  : gcd1 m (suc m) (suc i) 2 ≡ 2) →
-       (gnm : gcd1 n (suc n) m (suc m) ≡ 1 ) → ⊥
-   gcd23 = {!!}
+open import nat
 
+gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
+gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
+   gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
+   gcd22 zero i0 zero o0 = refl
+   gcd22 zero i0 (suc o) o0 = refl
+   gcd22 (suc i) i0 zero o0 = refl
+   gcd22 (suc i) i0 (suc o) o0 = refl 
+   gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
+   gcd21 zero .1 zero j0 o o0 1<i 1<j 1<o gn gm refl = nat-<≡ 1<i
+   gcd21 zero i0 (suc zero) j0 o o0 1<i 1<j 1<o refl gm refl = {!!}
+   gcd21 zero i0 (suc (suc j)) j0 o o0 1<i 1<j 1<o refl gm gnm = {!!}
+   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn refl gnm = {!!}
+   gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
+   gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
+       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
+                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
 
 record Even (i : ℕ) : Set where
   field
@@ -135,8 +141,10 @@
     i j : ℕ
     coprime : gcd i j ≡ 1
 
-root2-irrational : ( n m : ℕ ) → n > 0 → m > 0  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
-root2-irrational n m n>0 m>0 2nm = gcd22 {n} {m}  (even→gcd=2 rot7 n>0 ) (even→gcd=2 ( even^2 {m} ( rot1)) m>0) where
+root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
+root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
+    rot5 : {n : ℕ} → n > 1 → n > 0
+    rot5 {n} lt = <-trans a<sa lt 
     rot1 : even ( m * m )
     rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
        rot4 : (n * n) * 2 ≡ m * m