--- a/agda/logic.agda	Sat Nov 09 10:04:34 2019 +0900
+++ b/agda/logic.agda	Sat Nov 09 14:44:38 2019 +0900
@@ -107,6 +107,9 @@
 lemma-∧-1 {false} {true} ()
 lemma-∧-1 {false} {false} ()
 
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
 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
@@ -118,10 +121,17 @@
 bool-or-3 {true} = refl
 bool-or-3 {false} = refl
 
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
 bool-or-4 {true} = refl
 bool-or-4 {false} = refl
 
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
 bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
 bool-and-1 {false} {b} refl = refl
 bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false

--- a/agda/regular-language.agda	Sat Nov 09 10:04:34 2019 +0900
+++ b/agda/regular-language.agda	Sat Nov 09 14:44:38 2019 +0900
@@ -103,7 +103,7 @@
 open import nfa
 open import sbconst2
 open FiniteSet
-open import Data.Nat.Properties
+open import Data.Nat.Properties hiding ( _≟_ )
 open import Relation.Binary as B hiding (Decidable)
 
 postulate 
@@ -111,7 +111,8 @@
    fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
 
 Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
-Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } where
+Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } 
+   module Concat-NFA where
        δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
        δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
        δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (astart B) )
@@ -232,7 +233,7 @@
       true
      ∎  where open ≡-Reasoning
 
-postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) already in finiteSet
 
 open NAutomaton
 
@@ -245,17 +246,30 @@
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        exists finav (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
-    nmove = {!!}
+    nmove (case1 q) nq nqt h = found finav {_} {(case1 q)} ( bool-and-tt nqt lemma-nmove-a )  where
+        lemma-nmove-a : Nδ NFA (case1 q) h (abmove (case1 q) h) ≡ true
+        lemma-nmove-a with F←Q (afin A) (δ (automaton A) q h) ≟ F←Q (afin A) (δ (automaton A) q h)
+        lemma-nmove-a | yes refl = refl
+        lemma-nmove-a | no ne = ⊥-elim (ne refl)
+    nmove (case2 q) nq nqt h = found finav {_} {(case2 q)} ( bool-and-tt nqt lemma-nmove ) where
+        lemma-nmove : Nδ NFA (case2 q) h (abmove (case2 q) h) ≡ true
+        lemma-nmove with F←Q (afin B) (δ (automaton B) q h) ≟ F←Q (afin B) (δ (automaton B) q h)
+        lemma-nmove | yes refl = refl
+        lemma-nmove | no ne = ⊥-elim (ne refl)
     lemma6 : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
         → Naccept NFA finav nq z  ≡ true
-    lemma6 [] q nq _ fb = lemma8 where
+    lemma6 [] q nq nqt fb = lemma8 where
         lemma8 : exists finav ( λ q → nq q /\ Nend NFA q ) ≡ true
-        lemma8 = {!!}
+        lemma8 = found finav {_} {case2 q} ( bool-and-tt nqt fb )
     lemma6 (h ∷ t ) q nq nq=q fb = lemma6 t (δ (automaton B) q h) (Nmoves NFA finav nq h) (nmove (case2 q) nq nq=q h) fb 
     lemma7 : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
         → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
         → Naccept NFA finav nq (y ++ z)  ≡ true
-    lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq {!!} fb
+    lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq lemma71 fb where
+         lemma71 : nq (case2 (astart B)) ≡ true
+         lemma71 = {!!}
+         lemma-nq=q : (nq (case1 q) ≡ true)
+         lemma-nq=q = nq=q
     lemma7 (h ∷ t) z q nq nq=q fa fb = lemma7 t z (δ (automaton A) q h) (Nmoves NFA finav nq h) (nmove (case1 q) nq nq=q h)  fa fb where
     lemma9 : equal? finav (case1 (astart A)) (case1 (astart A)) ≡ true
     lemma9 with Data.Fin._≟_ (F←Q finav (case1 (astart A))) ( F←Q finav (case1 (astart A)) )