Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/fin.agda @ 317:16e47a3c4eda

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 Mon, 03 Jan 2022 18:50:01 +0900
parents 248711134141
children 4a00e5f2b793
comparison
equal deleted inserted replaced
316:fd07e3205cea 317:16e47a3c4eda
129 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y 129 f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y
130 f≡→≡ refl = refl 130 f≡→≡ refl = refl
131 131
132 open import Data.List 132 open import Data.List
133 open import Relation.Binary.Definitions 133 open import Relation.Binary.Definitions
134
135 -- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ
136 -- fin-count q p[ = 0
137 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0
138 -- ... | tri-e = suc (fin-count q qs)
139 -- ... | false = fin-count q qs
140
141 -- fin-not-dup-in-list : { n : ℕ} (qs : List (Fin n) ) → Set
142 -- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
143
144 -- this is far easier
145 -- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
146 -- fin-not-dup-in-list→len<n = ?
134 147
135 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool 148 fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool
136 fin-phase2 q [] = false 149 fin-phase2 q [] = false
137 fin-phase2 q (x ∷ qs) with <-fcmp q x 150 fin-phase2 q (x ∷ qs) with <-fcmp q x
138 ... | tri< a ¬b ¬c = fin-phase2 q qs 151 ... | tri< a ¬b ¬c = fin-phase2 q qs