Mercurial > hg > Members > kono > Proof > automaton

changeset 303:5261402429f9

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 Sat, 01 Jan 2022 11:00:41 +0900
parents 55f8031e4214
children b0a88e024188
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sat Jan 01 10:36:52 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Jan 01 11:00:41 2022 +0900
@@ -141,7 +141,8 @@
           | phase1 finq qd (tr→qs fa is (δ fa q i) tr) | inspect ( phase1 finq qd)  (tr→qs fa is (δ fa q i) tr) 
    ... | true | record { eq = eq } | false | record { eq = np} = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = tnext q {!!} } where
+           ; trace-xyyz = tra-02 (i ∷ TA1.y ta) (TA1.z ta) q
+                    (tnext q (TA1.trace-yz ta)) (subst (λ k → Trace fa (TA1.z ta)  k) {!!} (TA1.trace-z ta)) {!!} {!!}  } where
         ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
         tra-02 : (y1 z1 : List Σ) → (qd : Q) → (tr : Trace fa (y1 ++ z1) qd) → (trz : Trace fa z1 qd)
@@ -149,7 +150,7 @@
             → phase1 finq qd (tr→qs fa (y1 ++ z1) qd tr) ≡ false
             → Trace fa (y1 ++ y1 ++ z1) qd
         tra-02 [] z1 qd tryz trz p1 np1 = trz
-        tra-02 (i ∷ y1) z1 qd (tnext q tr) trz p1 np1 = {!!} where
+        tra-02 (i ∷ y1) z1 qd (tnext q tr) trz p1 np1 = tnext q (tra-04 y1 (δ fa q i) tr {!!} ( qd ∷ tr→qs fa (y1 ++ z1) (δ fa qd i) tr) {!!} np1 p1 )  where
            tryz = tnext q tr 
            tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
                → (qs zqs : List Q)