Mercurial > hg > Members > kono > Proof > automaton

changeset 349:9f3647718a9f

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:21:28 +0900
parents 8cd5bea05150
children ae38b5b3a6ec
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 16 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 22:34:17 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 23:21:28 2023 +0900
@@ -625,9 +625,15 @@
         lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
         ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le)
-        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = ? ; cb=n = trans eq1 (sym (trans eq2 eq))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?}
-        ... | case2 (s≤s lt) = ?
+        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq))
+                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
+             lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
+             lem10 = begin
+                0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩
+                toℕ (fromℕ< {0} 0<fa ) ≡⟨ cong toℕ (sym (finiso← fa _))  ⟩
+                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)
         ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq
         ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq
@@ -635,7 +641,13 @@
         ... | 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))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} 
+                ; 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 )) ⟩
+                ? ≡⟨ ? ⟩
+                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)
 
 -- end