Mercurial > hg > Members > kono > Proof > automaton

changeset 354:bc2cb1c6bc80

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 Tue, 18 Jul 2023 10:48:40 +0900
parents 5aae7a429f37
children e7a7cab74ca1
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 9 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:44:10 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 10:48:40 2023 +0900
@@ -645,8 +645,15 @@
     lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
         lem32 : (i : ℕ) → i ≡ toℕ (F←Q fa (f b)) → 0 < count-B i 
         lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
-        ... | yes isb = ?
-        ... | no nisb = ?
+        ... | yes isb = ≤-refl
+        ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
+            lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa )
+            lem33 = begin
+              f b ≡⟨ ? ⟩
+              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ ?)) ⟩
+              Q←F fa ( fromℕ< ? )  ≡⟨ ? ⟩
+              Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
+                open ≡-Reasoning
         lem32 (suc n) eq with <-cmp (finite fa) (suc n)
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a b ¬c = ?