Mercurial > hg > Members > kono > Proof > automaton

changeset 174:0e87089e5de4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
..`
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Mar 2021 15:31:56 +0900
parents 6835096cfa3a
children bf50676c77af
files agda/halt.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/agda/halt.agda	Sun Mar 14 08:27:05 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 15:31:56 2021 +0900
@@ -42,12 +42,12 @@
 
 --  ¬ A = A → ⊥ 
 
-diag :  (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ → Bool
+diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
-diagonal : ¬ Bijection  ( ℕ → Bool ) ℕ
-diagonal b = diagn1 (fun→ b (diag b) ) refl where
-    diagn1 : (n : ℕ ) → ¬ (fun→ b (diag b) ≡ n ) 
+diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
+diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
+    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
@@ -172,8 +172,8 @@
      lbisor [] = refl
      lbisor (false ∷ []) = refl
      lbisor (true ∷ []) = refl
-     lbisor (false ∷ true ∷ t) = ?
-     lbisor (false ∷ false ∷ t) = ?
+     lbisor (false ∷ true ∷ t) = {!!}
+     lbisor (false ∷ false ∷ t) = {!!}
      lbisor (true ∷ x ∷ t) = {!!}
 
 
@@ -204,7 +204,7 @@
          tmb1 x with is-tm x | inspect is-tm x
          ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
-TNℕ : Bijection  TM ℕ
+TNℕ : Halt → Bijection (TM → Bool) TM
 TNℕ = {!!}
 
 --  Halt1 (Halt2 x) ≡ x