--- a/automaton-in-agda/src/fin.agda	Wed Dec 29 11:50:34 2021 +0900
+++ b/automaton-in-agda/src/fin.agda	Wed Dec 29 19:08:28 2021 +0900
@@ -173,9 +173,11 @@
 fin-dup-in-list>n {zero} (() ∷ qs) lt
 fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where
      open import Level using ( Level )
+     --  make a dup from one level below
      fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) →  fin-dup-in-list  (fromℕ< a<sa ) qs ≡ false
           → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs
      fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where
+          -- we have two loops on the max element and the current level. The disjuction means the phases may differ.
           f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true
               → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false)
               → fin-phase2 (fin+1 i) qs ≡ true
@@ -185,6 +187,7 @@
           ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1)
           ... | tri≈ ¬a₁ b₁ ¬c₁ = refl
           ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1)
+          -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required
           f1-phase2 (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-phase2 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 ))
@@ -249,6 +252,7 @@
      fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
      ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
      ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
+           -- if no dup in the max element, the list without the element is only one length shorter
            fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) 
            fless qs lt p = fl-phase1 n qs lt p where
                fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1  → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) 
@@ -267,5 +271,6 @@
                ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ )))
                ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p 
                ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
+           -- if the list without the max element is only one length shorter, we can recurse
            fdup : FDup-in-list n (list-less qs)
            fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)