Mercurial > hg > Members > kono > Proof > automaton

changeset 301:30033f273f1d

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 Fri, 31 Dec 2021 23:06:08 +0900
parents 67d8e42b7782
children 55f8031e4214
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 4 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Fri Dec 31 20:02:54 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Dec 31 23:06:08 2021 +0900
@@ -141,14 +141,15 @@
           | 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 (tra-02 ? ? ? (TA1.trace-yz ta) ? ? ) } where
+           ; trace-xyyz = tnext q ( tra-02 (TA1.y ta) (δ fa q i) (sym (equal→refl finq eq)) {!!} {!!} {!!} ) } where
+              -- Trace fa ([] ++ (i ∷ TA1.y ta) ++ (i ∷ TA1.y ta) ++ TA1.z ta) q
               -- tra-02 (i ∷  TA1.y ta) q (sym (equal→refl finq eq)) (tnext q (TA1.trace-yz ta)) {!!} {!!} } where
         ta : TA1 fa (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
-        tra-02 : (y1 : List Σ) → (q0 : Q) → q ≡ qd  → (tr : Trace fa (y1 ++ TA1.z ta) (δ fa q i))
+        tra-02 : (y1 : List Σ) → (q0 : Q) → q ≡ qd  → (tr : Trace fa (y1 ++ TA1.z ta) q0)
             → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ true
             → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ false
-            → Trace fa (y1 ++ i ∷ TA1.y ta ++ TA1.z ta) (δ fa q0 i)
+            → Trace fa (y1 ++ i ∷ TA1.y ta ++ TA1.z ta) q0
         tra-02 [] q0 q=qd tr p np with equal? finq qd q0 | inspect ( equal? finq qd) q0
         ... | true  | record { eq = eq } = subst (λ k →  Trace fa (i ∷ TA1.y ta ++ TA1.z ta) k  ) {!!} (tnext q (TA1.trace-yz ta)  ) where
             tra-03 : q ≡ q0