# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1690175861 -32400
# Node ID 374eb9b42d95ea105680c6376798bc522e0cf332
# Parent  a933c8531141fee9084ba940dadb8a83e6327a6f
...

diff -r a933c8531141 -r 374eb9b42d95 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 13:32:46 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 14:17:41 2023 +0900
@@ -165,7 +165,8 @@
     sub*   : {x y : Regex Σ} → SB x y  → SB (x *) y
     sub&1  : (x y z : Regex Σ) → SB x z → SB (x & y) z
     sub&2  : (x y z : Regex Σ) → SB y z → SB (x & y) z
-    sub&<  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB y (x & y) 
+    sub*&  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB (y *) (x & (y *)) 
+    sub&&  : (x y z : Regex Σ) → rank z < rank (x & z)  → SB (x & y) z → SB (x & y) (z & y) 
 
 record ISB (r : Regex Σ) : Set where
     field
@@ -174,7 +175,7 @@
 
 open import bijection using ( InjectiveF ; Is )  
 
-finISB2 : {r z : Regex Σ} → FiniteSet ( ISB z) → FiniteSet (SB r z)
+finISB2 : {r z : Regex Σ} → FiniteSet (ISB z) → FiniteSet (SB r z)
 finISB2 = ?
 
 finISB : (r : Regex Σ) → FiniteSet (ISB r)
@@ -188,24 +189,19 @@
      fb00 record { s = .(x || y) ; is-sub = sunit } = ?
      fb00 record { s = s ; is-sub = (sub|1 is-sub) } = ?
      fb00 record { s = s ; is-sub = (sub|2 is-sub) } = ?
-     fb00 record { s = (z & (x || y)) ; is-sub = (sub&< z (x || y) lt is-sub) } = ? where
-         fb01 : FiniteSet (ISB z)
-         fb01 = finISB z
-finISB (x & y) = ? where
+finISB (x & y) = iso-fin (fin-∨ (inject-fin (finISB y) ? ?) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) ? where
      fb00 : ISB (x & y) → ?
      fb00 record { s = .(x & y) ; is-sub = sunit } = ?
      fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = ?
      fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = ?
-     fb00 record { s = (z & (x & y)) ; is-sub = (sub&< z (x & y) lt is-sub) } = ? where
-         fb01 : FiniteSet (ISB z)
-         fb01 = finISB z
-finISB (x *) = ? where
+     fb00 record { s = (z & y) ; is-sub = (sub&& x y z lt is-sub) } = ?
+finISB (x *) = iso-fin (fin-∨ (inject-fin (finISB x) fi ? ) (fin-∨1 (finISB x) )) record { fun← = fb00 } where
+     fi : InjectiveF (ISB x) (ISB x)
+     fi = record { f = ? ; inject = ? }
      fb00 : ISB (x *) → ?
      fb00 record { s = .(x *) ; is-sub = sunit } = ?
      fb00 record { s = s ; is-sub = (sub* is-sub) } = ?
-     fb00 record { s = (z & (x *)) ; is-sub = (sub&< z (x *) lt is-sub) } = ? where
-         fb01 : FiniteSet (ISB z)
-         fb01 = finISB z
+     fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { s = z ; is-sub = is-sub }
 
 toSB : (r : Regex   Σ) →  ISB r → Bool
 toSB r cr = ?