Mercurial > hg > Members > kono > Proof > automaton

changeset 359:57d007e9c581

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 18:03:49 +0900
parents 168465a7b107
children 6ba2836177b4
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 10 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 17:20:37 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 18:03:49 2023 +0900
@@ -634,12 +634,16 @@
              ... | 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
+             lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | inspect count-B (suc i) | inspect count-B (suc (suc i))
+             ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | record { eq = eq0 } | record { eq = eq1 } = refl-≤≡ (sym eq0)
+             ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | _ | _ = ⊥-elim (nat-≡< b (<-trans a a<sa))
+             ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c | _ | _ = ⊥-elim (nat-<> a (<-trans a<sa c) )
+             ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | record { eq = eq0 }  | _ = refl-≤≡ (sym eq0)
+             ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) )
+             ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c))
+             ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ  c a<sa ) )
+             ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 }  = ?
+             ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | _ | _ = ?
 
     lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
     lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where