Mercurial > hg > Members > kono > Proof > automaton

changeset 399:1cff8b68578a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Aug 2023 00:14:13 +0900
parents d7ea37e49f35
children 2c2fd5183a2b
files automaton-in-agda/src/derive.agda
diffstat 1 files changed, 11 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Sun Aug 06 00:03:48 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Aug 06 00:14:13 2023 +0900
@@ -294,15 +294,22 @@
 sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub } 
 ... | false = true
 ... | true = false
-sbderive (r & r₁) f s record { s = t ; is-sub = sub&2 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&2 r r₁ t is-sub } f 
+sbderive (r & r₁) f s record { s = t ; is-sub = sub&2 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&2 r r₁ t is-sub } 
 ... | false = true
 ... | true with derivative r s | derivative r₁ s
 ... | ε | φ = false
-... | ε | t = true
-... | φ | t = false
+... | ε | y = true
+... | φ | y = false
 ... | x1 | φ = false
 ... | x1 | y1 = false
-sbderive (r & r₁) f s record { s = .(z & r₁) ; is-sub = (sub&& .r .r₁ z x is-sub) } = ?
+sbderive (r & r₁) f s record { s = .(z & r₁) ; is-sub = (sub&& .r .r₁ z x is-sub) } with f record { s = z & r₁ ; is-sub = sub&& r r₁ z x is-sub } 
+... | false = true
+... | true with derivative r s | derivative r₁ s
+... | ε | φ = false
+... | ε | y = true
+... | φ | y = false
+... | x1 | φ = false
+... | x1 | y1 = false
 sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|1 is-sub) } = sbderive r sb00 s₁  record { s = s ; is-sub = is-sub } where
     sb00 : ISB r → Bool 
     sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|1 is-sub }