# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1691629187 -32400
# Node ID 093e386c10a231382eea47d054ee8df633c0522e
# Parent  62a4d1a2c48d69fdfefb154931a066f4da4d19d4
...

diff -r 62a4d1a2c48d -r 093e386c10a2 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Thu Aug 10 09:29:03 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Thu Aug 10 09:59:47 2023 +0900
@@ -340,6 +340,29 @@
 derive-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ
 derive-ε r s refl = refl
 
+rg03-or : (x s : Σ) → {r r₁ : Regex Σ} → (derivative (r || r₁) s ≡ derivative r s ) ∨ (derivative (r || r₁) s ≡ derivative r₁ s ) 
+    ∨ (derivative (r || r₁) s ≡ derivative r s ||  derivative r₁ s )
+rg03-or x s {r} {r₁} with derivative r s | derivative r₁ s 
+... | φ | rr = case2 (case1 refl)
+... | ε | φ = case1 refl
+... | rr * | φ = case1 refl
+... | rr & rr₁ | φ = case1 refl
+... | rr || rr₁ | φ = case1 refl
+... | < x₁ > | φ = case1 refl
+... | ε | ε = case2 (case2 refl)
+... | rr * | ε = case2 (case2 refl)
+... | rr & rr₁ | ε = case2 (case2 refl)
+... | rr || rr₁ | ε = case2 (case2 refl)
+... | < x₁ > | ε = case2 (case2 refl)
+... | ε | rr₁ * = case2 (case2 refl)
+... | rr * | rr₁ * = case2 (case2 refl)
+... | rr & rr₂ | rr₁ * = case2 (case2 refl)
+... | rr || rr₂ | rr₁ * = case2 (case2 refl)
+... | < x₁ > | rr₁ * = case2 (case2 refl)
+... | rr | rr₁ & rr₂ = case2 (case2 ?)
+... | rr | rr₁ || rr₂ = case2 (case2 ?)
+... | rr | < x₁ > = case2 (case2 ?)
+
 derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match r x
 derive-is-regex-language ε [] = refl
 derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) 
@@ -353,7 +376,7 @@
     rg03 = ?
 derive-is-regex-language (r & r₁) x = ?
 derive-is-regex-language (r || r₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ []) 
-derive-is-regex-language (r || r₁) (x ∷ x₁) = ?
+derive-is-regex-language (r || r₁) (x ∷ x₁) = ? 
 derive-is-regex-language < x₁ > [] = refl
 derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
 ... | yes _  = refl
@@ -369,7 +392,7 @@
     ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε  _ _ eq )
 --    immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)
 
-derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x
+derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x
 derive=ISB ε [] = refl
 derive=ISB ε (x ∷ x₁) = ?
 derive=ISB φ [] = refl
@@ -383,8 +406,6 @@
 ... | no _ = refl
 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
 
-ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x
-ISB-is-regex-language r x = trans ( derive-is-regex-language r x ) (derive=ISB r x)