# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640674608 -32400
# Node ID 24bcce90da91dc73d51aec1adfe655b8b19d2542
# Parent  c9802aa2a8c9540a6a5d24e0e2e56d9562dcba4d
...

diff -r c9802aa2a8c9 -r 24bcce90da91 automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Tue Dec 28 15:25:22 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Dec 28 15:56:48 2021 +0900
@@ -218,8 +218,35 @@
           f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true
               → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
               → fin-phase1 (fin+1 i) qs ≡ true
-          f1-phase1 (x ∷ qs) p (case1 q1) = {!!}
-          f1-phase1 (x ∷ qs) p (case2 q2) = {!!}
+          f1-phase1 (x ∷ qs) p (case1 q1) with  <-fcmp (fromℕ< a<sa) x
+          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
+          f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x
+          ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
+          ... | tri≈ ¬a₁ b₁ ¬c₁ = f1-phase2 qs {!!} (case2 q1) -- fin-phase1 i (list-less qs) ≡ true
+          ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
+          f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
+          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
+          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
+          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
+          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
+          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1)
+          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1)
+          f1-phase1 (x ∷ qs) p (case2 q1) with  <-fcmp (fromℕ< a<sa) x
+          ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
+          f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl )
+          f1-phase1 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
+          ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1)
+          ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
+          ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a ))
+          ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁  = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a ))
+          ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1)
+          ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
+          ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
      fdup-phase2 : (qs : List (Fin (suc n)) ) 
          → ( fin-phase2 (fromℕ< a<sa ) qs ≡ true )  ∨ NList n qs
      fdup-phase2 []  = case2  record { ls = [] ; lseq = refl ; ls< = case1 refl }