--- a/agda/logic.agda	Sun Nov 10 18:07:50 2019 +0900
+++ b/agda/logic.agda	Sun Nov 10 18:47:06 2019 +0900
@@ -110,6 +110,15 @@
 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
 bool-and-tt refl refl = refl
 
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
 bool-or-1 {false} {true} refl = refl
 bool-or-1 {false} {false} refl = refl

--- a/agda/regular-language.agda	Sun Nov 10 18:07:50 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 18:47:06 2019 +0900
@@ -285,11 +285,7 @@
     lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
           → (qa : states A ) → ( nq (case1 qa) ≡ true)
           → ( fa : List Σ → Bool ) → split fa (contain B) x ≡ true
-    lemma13 [] nq fn qa qat fa with found← finab fn
-    ... | S = {!!} where
-        lemma16 : nq (found-q S) /\ Concat-NFA.nend A B (found-q S) ≡ true
-        lemma16 = found-p S
-    -- = AB→split fa (contain B) [] [] {!!} {!!}
+    lemma13 [] nq fn qa qat fa = ?
     lemma13 (h ∷ t) nq fn qa qat fa with fa [] | accept (automaton B) (δ (automaton B) (astart B) h) t
     ... | true | true = refl
     ... | false | _ = subst (λ k → false \/ k ≡ true ) (sym lemma14 ) (bool-or-1 refl) where