Mercurial > hg > Members > kono > Proof > automaton

changeset 350:ae38b5b3a6ec

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 Mon, 17 Jul 2023 23:59:32 +0900
parents 9f3647718a9f
children c9a8d586695c
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 23:21:28 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 23:59:32 2023 +0900
@@ -597,7 +597,7 @@
     count-B zero with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
     ... | yes isb = 1
     ... | no nisb = 0
-    count-B (suc n) with <-cmp (finite fa) n
+    count-B (suc n) with <-cmp (finite fa) (suc n)
     ... | tri< a ¬b ¬c = count-B n
     ... | tri≈ ¬a b ¬c = count-B n
     ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
@@ -634,18 +634,18 @@
                 toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa )))  ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
                 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt)  ))
-        lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) i | inspect count-B (suc i)
+        lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i)
         ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq
         ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq
         ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))
         ... | no nisb = lem09 i (suc j) (s≤s le) eq
         ... | yes isb with ≤-∨ (s≤s le)
-        ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = ?  ; cb=n = trans eq1 (sym (trans eq2 eq))
+        ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq ))
                 ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
-              lem10 :  suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
-              lem10 = begin
-                suc i ≡⟨ cong suc (sym ( toℕ-fromℕ< c )) ⟩
-                ? ≡⟨ ? ⟩
+              lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
+              lem11 = begin
+                suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩
+                toℕ (fromℕ< c)  ≡⟨ cong toℕ (sym (finiso← fa _)) ⟩
                 toℕ (F←Q fa (Q←F fa (fromℕ< c )))  ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
                 toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq)