--- a/agda/halt.agda	Sun Mar 14 21:33:23 2021 +0900
+++ b/agda/halt.agda	Tue Mar 16 14:02:45 2021 +0900
@@ -45,70 +45,56 @@
            diag b n 
         ∎ ) where open ≡-Reasoning
 
-postulate
-   utm         : List Bool → List Bool → Maybe Bool
-
 record TM : Set where
    field
       tm : List Bool → Maybe Bool
-      encode : List Bool
-      is-tm : utm encode ≡ tm
 
 open TM
 
-Halt1 : TM → List Bool  → Bool -- ℕ → ( ℕ → Bool )
-Halt1 = {!!}
-
-record Halt1-is-tm : Set where
+record UTM : Set where
    field
-       htm : TM
-       htm-is-Halt1 : (t : TM ) → (x : List Bool) → (Halt1 t x ≡ true) ⇔ ((tm htm (encode t ++ x)) ≡ just true)
+      utm : TM
+      encode : TM → List Bool
+      is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x
 
-Halt2 : (tm : TM ) →  List Bool -- ( ℕ → Bool ) → ℕ  
-Halt2 tm = encode tm
-
-not-halt : {!!}
-not-halt = {!!}
+open UTM 
 
 open _∧_
-
 open ≡-Reasoning
 
-
 open import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 
 
 record Halt : Set where
    field
+      halt :  (t : TM ) → (x : List Bool ) → Bool
+      -- is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
+      -- is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
+
+record HaltIsTM (ha : Halt) (utm : UTM) : 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 )
+      htm-is-halt : (t : TM ) → (x : List Bool ) → (Halt.halt ha t x ≡ true ) ⇔ ( just true ≡ tm htm (encode utm t ++ x) )
 
 open Halt
 
-TNℕ : Halt → HBijection (TM → Bool) TM
-TNℕ = {!!}
-
-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
+TNL : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (List Bool → Bool) (List Bool)
+TNL halt utm halt-is-tm = record {
+       fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
+     ; fun→  = λ h  → encode utm record { tm = λ x → just (h x) } 
+     ; fiso← = TN1
+  } where
+     TN1 :  (h : List Bool → Bool) → (λ y → Halt.halt halt (UTM.utm utm) (encode utm (record { tm = λ x → just (h x) }) ++ y)) ≡ h
+     TN1 h =  f-extensionality (λ y →
+        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → just (h x) }) ++ y) ≡⟨ {!!} ⟩
+        h y ∎ ) where open ≡-Reasoning
 
-tm-bij :  HBijection TM (List Bool)
-tm-bij = record {
-       fun←  = λ x → record { tm = utm x ; encode = x ; is-tm = refl }
-     ; fun→  = λ tm → encode tm
-     ; fiso← = tmb1
-    }  where
-         tmb1 : (x : TM ) →  record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x
-         tmb1 x with is-tm x | inspect is-tm x
-         ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
---  Halt1 (Halt2 x) ≡ x
---  Halt2 (Halt2 y) ≡ y
+-- TNℕ : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (TM → Bool) TM
+-- TNℕ halt utm halt-is-tm = record {
+--        fun←  = λ tm tm1 → Halt.halt halt tm (encode utm tm1)
+--      ; fun→  = λ h  → record { tm = λ x → just (h {!!} ) } --  TM → Bool → TM
+--      ; fiso← = {!!}
+--   }
 
-halting : ¬ Halt
-halting h with tm (htm h) (encode (nhtm h) ++ encode (nhtm h))
-... | just true = ¬t=f {!!} {!!}
-... | nothing = {!!}
-... | just false = {!!}