--- a/agda/halt.agda	Thu Mar 18 00:16:42 2021 +0900
+++ b/agda/halt.agda	Thu Mar 18 07:47:39 2021 +0900
@@ -60,7 +60,6 @@
 open UTM 
 
 open _∧_
-open ≡-Reasoning
 
 open import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
@@ -71,50 +70,45 @@
       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
-      htm-is-halt : (t : TM ) → (x : List Bool ) → (Halt.halt ha t x ≡ true ) ⇔ ( just true ≡ tm htm (encode utm t ++ x) )
-
 open Halt
 
-TNL : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (List Bool → Bool) (List Bool)
-TNL halt utm halt-is-tm = record {
+TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
+TNL halt utm = record {
        fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
      ; fun→  = λ h  → encode utm record { tm = h1 h } 
      ; fiso← = λ h →  f-extensionality (λ y → TN1 h y )
   } where
+     open ≡-Reasoning
      h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
      h1 h x with h x
      ... | true =  just true
      ... | false = nothing
+     tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool
+     tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y
      h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing
      h-nothing h y eq with h y
      h-nothing h y refl | false = refl
      h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
      h-just h y eq with h y
      h-just h y refl | true = refl
-     TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (encode utm (record { tm = h1 h }) ++ y) ≡ h y
+     TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
      TN1 h y with h y | inspect h y
      ... | true  | record { eq = eq1 } = begin
-        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) y1 ) (case1 (sym tm-y1)) ⟩
+        Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
         true ∎  where
-          open ≡-Reasoning
-          y1 : List Bool
-          y1 = encode utm (record { tm = λ x → h1 h x }) ++ y
-          tm-y1 = begin
-              tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y)  ≡⟨  is-tm utm _ y ⟩
+          tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ just true
+          tm-tenc = begin
+              tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
               h1 h y ≡⟨ h-just h y eq1  ⟩
-              just true  ∎  where
+              just true  ∎  
      ... | false | record { eq = eq1 } = begin
-        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) y1 ) (sym tm-y1) ⟩
+        Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
         false ∎  where
-          open ≡-Reasoning
-          y1 : List Bool
-          y1 = encode utm (record { tm = λ x → h1 h x }) ++ y
-          tm-y1 :  tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡ nothing
-          tm-y1 = begin
-              tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y)  ≡⟨  is-tm utm _ y ⟩
+          tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ nothing
+          tm-tenc = begin
+              tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
               h1 h y ≡⟨  h-nothing h y eq1 ⟩
-              nothing  ∎  where
+              nothing  ∎  
+     -- the rest of bijection means encoding is unique
+     -- fiso→ :  (y : List Bool ) → encode utm record { tm = λ x →  h1 (λ tm → Halt.halt halt (UTM.utm utm) tm  ) x } ≡ y