# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689671029 -32400
# Node ID 57d007e9c581a3160c61e7daf0f736df2424e36b
# Parent  168465a7b107b02d2f3004a8ef1ac5e5d8f63a18
...

diff -r 168465a7b107 -r 57d007e9c581 automaton-in-agda/src/finiteSetUtil.agda
--- 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