Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/non-regular.agda @ 396:f26444eb0275

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... look bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 03 Aug 2023 17:32:50 +0900
parents cd81e0869fac
children 2e22a1f3a55a
comparison
equal deleted inserted replaced
395:cd81e0869fac 396:f26444eb0275
159 length (i0 ∷ i0 ∷ x ∷ z) ≡⟨ refl ⟩ 159 length (i0 ∷ i0 ∷ x ∷ z) ≡⟨ refl ⟩
160 suc (length (i0 ∷ i0 ∷ z)) ≡⟨ cong suc (nn16 z) ⟩ 160 suc (length (i0 ∷ i0 ∷ z)) ≡⟨ cong suc (nn16 z) ⟩
161 suc (suc (suc (length (y (i0 ∷ z))))) ≡⟨ cong suc (cong suc ( cong suc (nn17 z))) ⟩ 161 suc (suc (suc (length (y (i0 ∷ z))))) ≡⟨ cong suc (cong suc ( cong suc (nn17 z))) ⟩
162 suc (suc (suc (length (y (x ∷ z))))) ≡⟨ refl ⟩ 162 suc (suc (suc (length (y (x ∷ z))))) ≡⟨ refl ⟩
163 suc (suc (length (i0 ∷ y (x ∷ z)))) ∎ where open ≡-Reasoning 163 suc (suc (length (i0 ∷ y (x ∷ z)))) ∎ where open ≡-Reasoning
164 nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 1 t)) (proj2 (inputnn1-i0 1 t)) ≡ true 164 nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 0 t)) (proj2 (inputnn1-i0 0 t)) ≡ true
165 → t ++ (i1 ∷ []) ≡ y t 165 → top-is-i0 t ≡ true
166 nn11 t eq = ? 166 → y t ++ (i1 ∷ []) ≡ t
167 nn11 [] eq ne = ?
168 nn11 (i0 ∷ t) eq ne = ?
169 nn11 (i1 ∷ []) eq ne = ?
170 nn11 (i1 ∷ i0 ∷ t) eq ne = ?
171 nn11 (i1 ∷ i1 ∷ t) eq ne = cong (i1 ∷_ ) (nn11 (i1 ∷ t) eq ? )
167 nn10 : (y : List In2 ) 172 nn10 : (y : List In2 )
168 → inputnn1-i1 (proj1 (inputnn1-i0 0 y)) (proj2 (inputnn1-i0 0 y)) ≡ true 173 → inputnn1-i1 (proj1 (inputnn1-i0 0 y)) (proj2 (inputnn1-i0 0 y)) ≡ true
169 → y ≡ input-addi0 (half y) (input-addi1 (half y)) 174 → y ≡ input-addi0 (half y) (input-addi1 (half y))
170 nn10 y eq = nn08 y eq 175 nn10 y eq = nn08 y eq
171 nn14 : inputnn1-i1 (proj1 (inputnn1-i0 0 (y t))) (proj2 (inputnn1-i0 0 (y t))) ≡ true 176 nn14 : inputnn1-i1 (proj1 (inputnn1-i0 0 (y t))) (proj2 (inputnn1-i0 0 (y t))) ≡ true