Mercurial > hg > Members > kono > Proof > automaton

changeset 353:5aae7a429f37

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 09:44:10 +0900
parents 34426fe27745
children bc2cb1c6bc80
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 17 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:16:53 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:44:10 2023 +0900
@@ -641,11 +641,24 @@
              ... | yes isb = ? -- refl-≤s
              ... | no nisb = ? -- ≤-refl
 
+    lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
+    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 = ?
+        lem32 (suc n) eq with <-cmp (finite fa) (suc n)
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
+        ... | yes isb = ?
+        ... | no nisb = ?
 
     cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
-    cb<mb b = sx≤y→x<y (begin
-        ? ≤⟨ ? ⟩ 
-        ? ∎ where
+    cb<mb b = sx≤y→x<y ( begin
+        suc ( pred (count-B (toℕ (F←Q fa (f b)))))  ≡⟨ sucprd (lem31 b) ⟩ 
+        count-B (toℕ (F←Q fa (f b)))  ≤⟨ lem02 ⟩ 
+        count-B (finite fa)   ∎ ) where
           open ≤-Reasoning
           lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa)
           lem02 = count-B-mono (<to≤ (fin<n {_} {(F←Q fa (f b))})) 
@@ -707,13 +720,11 @@
              CB = cb00 (toℕ (fromℕ< (cb<mb b))) fin<n
              isb : Is B A f (Q←F fa (fromℕ< fin<n))
              isb = ?
-             lem31 : 0 < count-B (toℕ (F←Q fa (f b)))
-             lem31 = ?
              lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b)))
              lem30 = begin
                  count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩
                  suc (toℕ (fromℕ< (cb<mb b)))  ≡⟨ cong suc (toℕ-fromℕ< (cb<mb b)) ⟩
-                 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd lem31 ⟩
+                 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩
                  count-B (toℕ (F←Q fa (f b))) ∎