Mercurial > hg > Members > kono > Proof > automaton
changeset 392:23db567b4098
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 09:03:13 +0900 |
| parents | 0d8b093bc4e3 |
| children | 2ff6519fc270 |
| files | automaton-in-agda/src/non-regular.agda |
| diffstat | 1 files changed, 93 insertions(+), 80 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda Thu Jul 27 08:21:21 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Thu Jul 27 09:03:13 2023 +0900 @@ -10,7 +10,7 @@ open import automaton-ex open import finiteSetUtil open import finiteSet -open import Relation.Nullary +open import Relation.Nullary open import regular-language open import nat open import pumping @@ -25,17 +25,17 @@ list-eq (i0 ∷ s) (i0 ∷ s1) = false list-eq (i0 ∷ s) (i1 ∷ s1) = false list-eq (i1 ∷ s) (i0 ∷ s1) = false -list-eq (i1 ∷ s) (i1 ∷ s1) = list-eq s s1 +list-eq (i1 ∷ s) (i1 ∷ s1) = list-eq s s1 -input-addi0 : ( n : ℕ ) → List In2 → List In2 +input-addi0 : ( n : ℕ ) → List In2 → List In2 input-addi0 zero x = x input-addi0 (suc i) x = i0 ∷ input-addi0 i x -input-addi1 : ( n : ℕ ) → List In2 +input-addi1 : ( n : ℕ ) → List In2 input-addi1 zero = [] input-addi1 (suc i) = i1 ∷ input-addi1 i -inputnn0 : ( n : ℕ ) → List In2 +inputnn0 : ( n : ℕ ) → List In2 inputnn0 n = input-addi0 n (input-addi1 n) inputnn1-i1 : (i : ℕ) → List In2 → Bool @@ -49,7 +49,7 @@ inputnn1-i0 : (i : ℕ) → List In2 → ℕ ∧ List In2 inputnn1-i0 i [] = ⟪ i , [] ⟫ inputnn1-i0 i (i1 ∷ x) = ⟪ i , (i1 ∷ x) ⟫ -inputnn1-i0 i (i0 ∷ x) = inputnn1-i0 (suc i) x +inputnn1-i0 i (i0 ∷ x) = inputnn1-i0 (suc i) x open _∧_ @@ -97,7 +97,7 @@ nn08 zero () nn08 (suc i) () ... | i1 ∷ t | _ = +-comm 0 _ - nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) + nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) )) nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i nn09 zero with input-addi1 i | inspect input-addi1 i @@ -107,7 +107,7 @@ nn08 zero () nn08 (suc i) () ... | i1 ∷ t | _ = refl - nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) + nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true nn04 zero = refl nn04 (suc i) = nn04 i @@ -128,21 +128,21 @@ open import Data.List.Properties open import nat -lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) +lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) (TA.xyz=is TAnn) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) ) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyyz TAnn) ) where n : ℕ n = suc (finite (afin r)) - nn = inputnn0 n + nn = inputnn0 n nn03 : accept (automaton r) (astart r) nn ≡ true nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) nn09 : (n m : ℕ) → n ≤ n + m nn09 zero m = z≤n nn09 (suc n) m = s≤s (nn09 n m) nn04 : Trace (automaton r) nn (astart r) - nn04 = tr-accept← (automaton r) nn (astart r) nn03 + nn04 = tr-accept← (automaton r) nn (astart r) nn03 nntrace = tr→qs (automaton r) nn (astart r) nn04 - nn07 : (n : ℕ) → length (inputnn0 n ) ≡ n + n + nn07 : (n : ℕ) → length (inputnn0 n ) ≡ n + n nn07 i = nn19 i where nn17 : (i : ℕ) → length (input-addi1 i) ≡ i nn17 zero = refl @@ -154,7 +154,7 @@ nn19 i = begin length (input-addi0 i ( input-addi1 i )) ≡⟨ nn18 i i ⟩ i + length (input-addi1 i) ≡⟨ cong (λ k → i + k) ( nn17 i) ⟩ - i + i ∎ where open ≡-Reasoning + i + i ∎ where open ≡-Reasoning nn05 : length nntrace > finite (afin r) nn05 = begin suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ @@ -169,6 +169,8 @@ open import Tactic.MonoidSolver using (solve; solve-macro) + -- there is a counter example + -- tann : {x y z : List In2} → ¬ y ≡ [] → x ++ y ++ z ≡ nn → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) @@ -181,24 +183,28 @@ count1 [] = 0 count1 (i1 ∷ x) = suc (count1 x) count1 (i0 ∷ x) = count1 x + -- + -- prove some obvious fact + -- c0+1=n : (x : List In2 ) → count0 x + count1 x ≡ length x c0+1=n [] = refl c0+1=n (i0 ∷ t) = cong suc ( c0+1=n t ) c0+1=n (i1 ∷ t) = begin - count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ - (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ - suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t ) ⟩ + count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ + (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ + suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t ) ⟩ suc (length t) ∎ where open ≡-Reasoning + -- nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x nn15 x eq = nn18 where - nn17 : (x : List In2 ) → (count0 x ≡ proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))) + nn17 : (x : List In2 ) → (count0 x ≡ proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))) ∧ (count1 x ≡ 0 + count1 (proj2 (inputnn1-i0 0 x))) nn17 [] = ⟪ refl , refl ⟫ nn17 (i0 ∷ t ) with nn17 t ... | ⟪ eq1 , eq2 ⟫ = ⟪ begin suc (count0 t ) ≡⟨ cong suc eq1 ⟩ suc (proj1 (inputnn1-i0 0 t) + count0 (proj2 (inputnn1-i0 0 t))) ≡⟨ cong₂ _+_ (sym (nn31 t 0)) (cong count0 (sym (nn30 t 0))) ⟩ - proj1 (inputnn1-i0 1 t) + count0 (proj2 (inputnn1-i0 1 t)) ∎ + proj1 (inputnn1-i0 1 t) + count0 (proj2 (inputnn1-i0 1 t)) ∎ , trans eq2 (cong count1 (sym (nn30 t 0))) ⟫ where open ≡-Reasoning nn20 : proj2 (inputnn1-i0 1 t) ≡ proj2 (inputnn1-i0 0 t) @@ -208,109 +214,116 @@ nn19 zero [] eq = ⟪ refl , refl ⟫ nn19 zero (i0 ∷ y) () nn19 zero (i1 ∷ y) () - nn19 (suc i) (i1 ∷ y) eq with nn19 i y eq + nn19 (suc i) (i1 ∷ y) eq with nn19 i y eq ... | t = ⟪ proj1 t , cong suc (proj2 t ) ⟫ nn18 : count0 x ≡ count1 x nn18 = begin - count0 x ≡⟨ proj1 (nn17 x) ⟩ - proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x)) ≡⟨ cong (λ k → proj1 (inputnn1-i0 0 x) + k) - (proj1 (nn19 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) eq)) ⟩ - proj1 (inputnn1-i0 0 x) + 0 ≡⟨ +-comm _ 0 ⟩ - 0 + proj1 (inputnn1-i0 0 x) ≡⟨ cong (λ k → 0 + k) (sym (proj2 (nn19 _ _ eq))) ⟩ - 0 + count1 (proj2 (inputnn1-i0 0 x)) ≡⟨ sym (proj2 (nn17 x)) ⟩ + count0 x ≡⟨ proj1 (nn17 x) ⟩ + proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x)) ≡⟨ cong (λ k → proj1 (inputnn1-i0 0 x) + k) + (proj1 (nn19 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) eq)) ⟩ + proj1 (inputnn1-i0 0 x) + 0 ≡⟨ +-comm _ 0 ⟩ + 0 + proj1 (inputnn1-i0 0 x) ≡⟨ cong (λ k → 0 + k) (sym (proj2 (nn19 _ _ eq))) ⟩ + 0 + count1 (proj2 (inputnn1-i0 0 x)) ≡⟨ sym (proj2 (nn17 x)) ⟩ count1 x ∎ where open ≡-Reasoning - cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y - cong0 [] y = refl - cong0 (i0 ∷ x) y = cong suc (cong0 x y) - cong0 (i1 ∷ x) y = cong0 x y - cong1 : (x y : List In2 ) → count1 (x ++ y ) ≡ count1 x + count1 y - cong1 [] y = refl - cong1 (i1 ∷ x) y = cong suc (cong1 x y) - cong1 (i0 ∷ x) y = cong1 x y + distr0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y + distr0 [] y = refl + distr0 (i0 ∷ x) y = cong suc (distr0 x y) + distr0 (i1 ∷ x) y = distr0 x y + distr1 : (x y : List In2 ) → count1 (x ++ y ) ≡ count1 x + count1 y + distr1 [] y = refl + distr1 (i1 ∷ x) y = cong suc (distr1 x y) + distr1 (i0 ∷ x) y = distr1 x y + -- + -- i0 .. i0 ∷ i1 .. i1 sequece does not contains i1 → i0 transition + -- record i1i0 (z : List In2) : Set where field a b : List In2 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b ) nn12 : (x : List In2 ) → inputnn1 x ≡ true → ¬ i1i0 x nn12 x eq = nn17 x 0 eq where - nn17 : (x : List In2 ) → (i : ℕ) + nn17 : (x : List In2 ) → (i : ℕ) → inputnn1-i1 (proj1 (inputnn1-i0 i x)) (proj2 (inputnn1-i0 i x)) ≡ true → ¬ i1i0 x nn17 [] i eq li with i1i0.a li | i1i0.i10 li ... | [] | () ... | x ∷ s | () - nn17 (i0 ∷ x₁) i eq li = nn17 x₁ (suc i) eq record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li + nn17 (i0 ∷ x₁) i eq li = nn17 x₁ (suc i) eq record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li ; i10 = nn19 (i1i0.a li) (i1i0.i10 li) } where + -- first half nn18 : (a : List In2 ) → i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2 nn18 (i0 ∷ t) eq = t nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) ) → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li nn19 (i0 ∷ a) eq = cons-inject eq nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where + -- second half nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥ - nn20 [] zero eq li = nn21 (i1i0.a li) (i1i0.i10 li) where - nn21 : (a : List In2 ) → ¬ ( [] ≡ a ++ i1 ∷ i0 ∷ i1i0.b li ) - nn21 [] () - nn21 (x ∷ a) () - nn20 (i0 ∷ x₁) zero () li - nn20 (i0 ∷ x₁) (suc i) () li - nn20 (i1 ∷ x₁) (suc i) eqa li = nn20 x₁ i eqa record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li - ; i10 = nn19 (i1i0.a li) (i1i0.i10 li) } where - nn18 : (a : List In2 ) → i1 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2 - nn18 [] eqb = ? - nn18 (i1 ∷ t) eq = t - nn19 : (a : List In2 ) → (eq : i1 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) ) - → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li - nn19 (i1 ∷ a) eq = cons-inject eq - nn19 [] eqb = ? + nn20 x i eq li = nn21 (i1i0.a li) x i eq (i1i0.i10 li) where + nn21 : (a x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → x ≡ a ++ i1 ∷ i0 ∷ i1i0.b li → ⊥ + nn21 [] [] zero eq1 () + nn21 (i0 ∷ a) [] zero eq1 () + nn21 (i1 ∷ a) [] zero eq1 () + nn21 a (i0 ∷ x₁) zero () eq0 + nn21 [] (i0 ∷ x₁) (suc i) () eq0 + nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0 + nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0 + nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0 + nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject eq0) nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) - nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) + nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where + -- + -- we need simple calcuraion to obtain count0 y ≡ count1 y + -- nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z nn21 = begin (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩ - count0 x + (count0 y + (count0 y + count0 z)) ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (cong0 y _ )) ⟩ - count0 x + (count0 y + count0 (y ++ z)) ≡⟨ sym (cong (λ k → count0 x + k) (cong0 y _ )) ⟩ - count0 x + (count0 (y ++ y ++ z)) ≡⟨ sym (cong0 x _ ) ⟩ + count0 x + (count0 y + (count0 y + count0 z)) ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (distr0 y _ )) ⟩ + count0 x + (count0 y + count0 (y ++ z)) ≡⟨ sym (cong (λ k → count0 x + k) (distr0 y _ )) ⟩ + count0 x + (count0 (y ++ y ++ z)) ≡⟨ sym (distr0 x _ ) ⟩ count0 (x ++ y ++ y ++ z) ≡⟨ nn15 (x ++ y ++ y ++ z) xyyz ⟩ - count1 (x ++ y ++ y ++ z) ≡⟨ cong1 x _ ⟩ - count1 x + (count1 (y ++ y ++ z)) ≡⟨ cong (λ k → count1 x + k) (cong1 y _ ) ⟩ - count1 x + (count1 y + count1 (y ++ z)) ≡⟨ (cong (λ k → count1 x + (count1 y + k)) (cong1 y _ )) ⟩ + count1 (x ++ y ++ y ++ z) ≡⟨ distr1 x _ ⟩ + count1 x + (count1 (y ++ y ++ z)) ≡⟨ cong (λ k → count1 x + k) (distr1 y _ ) ⟩ + count1 x + (count1 y + count1 (y ++ z)) ≡⟨ (cong (λ k → count1 x + (count1 y + k)) (distr1 y _ )) ⟩ count1 x + (count1 y + (count1 y + count1 z)) ≡⟨ solve +-0-monoid ⟩ count1 x + count1 y + count1 y + count1 z ∎ where open ≡-Reasoning nn20 : count0 x + count0 y + count0 z ≡ count1 x + count1 y + count1 z nn20 = begin count0 x + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ - count0 x + (count0 y + count0 z) ≡⟨ cong (λ k → count0 x + k) (sym (cong0 y z)) ⟩ - count0 x + (count0 (y ++ z)) ≡⟨ sym (cong0 x _) ⟩ - count0 (x ++ (y ++ z)) ≡⟨ nn15 (x ++ y ++ z) xyz ⟩ - count1 (x ++ (y ++ z)) ≡⟨ cong1 x _ ⟩ - count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (cong1 y z) ⟩ + count0 x + (count0 y + count0 z) ≡⟨ cong (λ k → count0 x + k) (sym (distr0 y z)) ⟩ + count0 x + (count0 (y ++ z)) ≡⟨ sym (distr0 x _) ⟩ + count0 (x ++ (y ++ z)) ≡⟨ nn15 (x ++ y ++ z) xyz ⟩ + count1 (x ++ (y ++ z)) ≡⟨ distr1 x _ ⟩ + count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (distr1 y z) ⟩ count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ count1 x + count1 y + count1 z ∎ where open ≡-Reasoning -- this takes very long time to check and needs 10GB bb22 : count0 y ≡ count1 y - bb22 = ? -- begin --- count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( --- begin --- count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ --- (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ --- (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ --- (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ --- count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z --- ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ --- count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ --- count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z --- ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ --- count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ --- count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ --- count1 y ∎ where open ≡-Reasoning + bb22 = begin + count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( + begin + count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ + (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ + (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ + (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ + count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ + count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ + count1 y ∎ where open ≡-Reasoning + -- + -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y + -- bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where bb26 : 0 < count1 y bb26 with <-cmp 0 (count1 y) ... | tri< a ¬b ¬c = a ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (sym bb27 ) (0<ly y ny) ) where - 0<ly : (y : List In2) → ¬ y ≡ [] → 0 < length y + 0<ly : (y : List In2) → ¬ y ≡ [] → 0 < length y 0<ly [] ne = ⊥-elim ( ne refl ) 0<ly (x ∷ y) ne = s≤s z≤n bb27 : length y ≡ 0 @@ -324,7 +337,7 @@ ... | t = record { a = i0 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i0 ∷_) (i1i0.i10 t) } bb25 (i1 ∷ []) y 0<x 0<y = bb27 y 0<y where bb27 : (y : List In2 ) → 0 < count0 y → i1i0 (i1 ∷ y ) - bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } + bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } bb27 (i1 ∷ y) 0<y with bb27 y 0<y ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } bb25 (i1 ∷ i0 ∷ x₁) y 0<x 0<y = record { a = [] ; b = x₁ ++ y ; i10 = refl } @@ -340,7 +353,7 @@ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false - nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) + nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 ) ... | false | _ = refl