Mercurial > hg > Members > kono > Proof > automaton
changeset 380:646ce1064288
... !
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Jul 2023 14:29:12 +0900 |
| parents | 374eb9b42d95 |
| children | 113330c6e896 |
| files | automaton-in-agda/src/derive.agda |
| diffstat | 1 files changed, 10 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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 = ?