Mercurial > hg > Members > kono > Proof > automaton

changeset 352:34426fe27745

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:16:53 +0900
parents c9a8d586695c
children 5aae7a429f37
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 29 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 08:24:31 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:16:53 2023 +0900
@@ -619,8 +619,36 @@
     maxb : ℕ
     maxb = count-B (finite fa)
 
+    count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j
+    count-B-mono {i} {j} i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    ... | case2 i<j = lem00 _ _ i<j where
+         lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j
+         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
+             lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
+             lem01 zero with <-cmp (finite fa) 1 
+             lem01 zero | tri< a ¬b ¬c = ≤-refl
+             lem01 zero | tri≈ ¬a b ¬c = ≤-refl
+             lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) | inspect count-B 0
+             ... | yes isb1 | yes isb0  | record { eq = eq0 } = s≤s z≤n
+             ... | yes isb1 | no  nisb0 | record { eq = eq0 } = z≤n
+             ... | no nisb1 | yes isb0  | record { eq = eq0 } = refl-≤≡ (sym eq0)
+             ... | no nisb1 | no  nisb0 | record { eq = eq0 } = z≤n
+             lem01 (suc n) with <-cmp (finite fa) (suc n) | inspect count-B (suc n)
+             ... | tri< a ¬b ¬c | record { eq = eq1 } = ?
+             ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ?
+             ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))
+             ... | yes isb = ? -- refl-≤s
+             ... | no nisb = ? -- ≤-refl
+
+
     cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
-    cb<mb = ?
+    cb<mb b = sx≤y→x<y (begin
+        ? ≤⟨ ? ⟩ 
+        ? ∎ 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))})) 
 
     cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
     cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where