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

diff -r 374eb9b42d95 -r 646ce1064288 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 14:17:41 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 14:29:12 2023 +0900
@@ -196,12 +196,19 @@
      fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = ?
      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 = ? }
+     record Z : Set where
+        field 
+          z : Regex Σ
+          lt : rank z < rank x
+          is-sub : SB x z
+     fi : InjectiveF Z (ISB x) 
+     fi = record { f = f ; inject = ? } where
+        f : Z → ISB x
+        f z = record { s = Z.z z ; is-sub = Z.is-sub z }
      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) } = case1 record { s = z ; is-sub = is-sub }
+     fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
 toSB : (r : Regex   Σ) →  ISB r → Bool
 toSB r cr = ?