# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1700124042 -32400
# Node ID 4e4acdc43dee2730731662fa6489d7642eaa0ec8
# Parent  3d0aa205edf9fc82c822a2887ac8c3e1e7087838
...

diff -r 3d0aa205edf9 -r 4e4acdc43dee automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Wed Nov 15 16:24:07 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Thu Nov 16 17:40:42 2023 +0900
@@ -207,28 +207,7 @@
       true ∎  where open ≡-Reasoning
 
 
--- plit→AB1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x →  split A B x ≡ true 
--- plit→AB1 {Σ} A B [] S = begin
---      split A B [] ≡⟨⟩
---      A [] /\ B [] ≡⟨ cong₂ _/\_ a=t b=t  ⟩ 
---      true  /\ true  ≡⟨ bool-and-tt refl refl ⟩
---      true ∎  where 
---         open ≡-Reasoning
---         a=t : A [] ≡ true
---         a=t = begin
---            A [] ≡⟨ cong (λ k → A k) (sym (proj1 (list-empty++ (sp0 S) (sp1 S) (sp-concat S))))  ⟩
---            A (sp0 S) ≡⟨ prop0 S ⟩
---            true ∎  where open ≡-Reasoning
---         b=t : B [] ≡ true
---         b=t = begin
---            B [] ≡⟨ cong (λ k → B k) (sym (proj2 (list-empty++ (sp0 S) (sp1 S) (sp-concat S))))  ⟩
---            B (sp1 S) ≡⟨ prop1 S ⟩
---            true ∎  where open ≡-Reasoning
--- plit→AB1 {Σ} A B (h ∷ t ) S = begin
---      split A B (h ∷ t ) ≡⟨⟩
---      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t ≡⟨ cong (λ k → A [] /\ B (h ∷ t) \/ k ) 
---         (split→AB1 {Σ} (λ t1 → A (h ∷ t1)) B t ? ) ⟩
---      A [] /\ B (h ∷ t) \/ true ≡⟨ bool-or-3 ⟩
---      true ∎  where open ≡-Reasoning
--- 
+split→AB1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x →  split A B x ≡ true 
+split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S)  )
+