Mercurial > hg > Members > kono > Proof > automaton

changeset 312:025c05355024

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, 02 Jan 2022 23:18:15 +0900
parents 59e2d48950e8
children ae33e1504f2b
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 9 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sun Jan 02 19:28:01 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jan 02 23:18:15 2022 +0900
@@ -165,7 +165,7 @@
            ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
            ; trace-xyyz = tra-04 (i ∷ TA1.y ta) q (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i) ) (equal→refl finq eq) tryz0))
-              tra-052 } where 
+              (tra-052 (TA1.q=qd ta)) }  where 
         ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
         y1 = TA1.y ta
@@ -176,18 +176,17 @@
         tryz = tnext qd tryz0
         tra-06 : QDSEQ finq qd (TA1.z ta) (TA1.trace-yz ta)
         tra-06 = TA1.q=qd ta 
-        tra-052 : QDSEQ finq qd z1 (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i)) (equal→refl finq eq) tryz0))
-        tra-052 = ?
-        tra-051 : QDSEQ finq qd z1 {!!}
-        tra-051 = TA1.q=qd ta
+        tra-052 : QDSEQ finq qd z1 (TA1.trace-yz ta)
+               →  QDSEQ finq qd z1 (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i)) (equal→refl finq eq) tryz0))
+        tra-052 drs = {!!} -- qd-next ? ? ? ? (subst (λ k → Trace fa k (δ fa q i) ) ? drs)
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
-               →  QDSEQ finq qd z1 {q} {y2} tr
+               →  QDSEQ finq qd z1 {q} {y2} tr -- should be y ++ z1
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-        tra-04 [] q tr (qd-nil .q .tr x₁) with equal? finq qd q | inspect (equal? finq qd) q
+        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
         ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
-        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  ne {!!} ) 
-        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next y2 .q tr x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool {!!} eq ) where -- y2 + z1 contains two qd
+        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ ) 
+        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
+        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) -- y2 + z1 contains two qd
         ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
    ... | true | record { eq = eq } | true | record { eq = np} = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
            ; non-nil-y = non-nil-y ta