Mercurial > hg > Members > kono > Proof > automaton

changeset 28:950d08ec1885

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exits done but not so goot
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 14:14:40 +0900
parents caf9b6aebd24
children 2887577a3d63
files agda/nfa.agda
diffstat 1 files changed, 15 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/agda/nfa.agda	Mon Nov 05 11:16:29 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 14:14:40 2018 +0900
@@ -44,10 +44,21 @@
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
      exists : ( Q → Bool ) → Bool
-     exists p = exists1 fin p where
-         exists1 : {n : ℕ} → Fin n → ( Q → Bool ) → Bool
-         exists1 ( zero ) _ = false
-         exists1 ( suc f ) p = p (Q←F {!!}) ∧ exists1 f p
+     exists p = exists1 fin (s≤s (lt0 n)) p where
+         lt0 : (n : ℕ) →  n Data.Nat.≤ n
+         lt0 zero = z≤n
+         lt0 (suc n) = s≤s (lt0 n)
+         lt1 : {m n : ℕ} → suc m  < suc n →  m Data.Nat.≤ n
+         lt1 {zero} _ = z≤n
+         lt1 {suc m} {zero} (s≤s ()) 
+         lt1 {suc m} {suc n} (s≤s lt) = s≤s (lt1 lt) 
+         lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
+         lt2 {zero} lt = z≤n
+         lt2 {suc m} {zero} ()
+         lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
+         exists1 : {m : ℕ} → Fin m → m < suc n  → ( Q → Bool ) → Bool
+         exists1 ( zero ) _ _ = false
+         exists1 ( suc f ) lt p = p (Q←F (inject≤ f (lt1 lt))) ∧ exists1 f (lt2 lt)  p
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n