Mercurial > hg > Members > kono > Proof > automaton

changeset 308:2effd9a23299

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tra-04
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jan 2022 06:52:35 +0900
parents aeb805cd624a
children acb0214ea4d8
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 18 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sun Jan 02 06:04:32 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jan 02 06:52:35 2022 +0900
@@ -151,26 +151,27 @@
    ... | 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)
            ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = {!!} } where 
+           ; 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)) } 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)
-            → phase2 finq qd (tr→qs fa (y1 ++ z1) qd tr) ≡ true
-            → 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
-           tryz = tnext q tr 
-           tra-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2)
-           tra-05 = {!!}
-           tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
+        y1 = TA1.y ta
+        z1 = TA1.z ta
+        tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
+        tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
+        tryz : Trace fa (i ∷ y1 ++ z1) qd
+        tryz = tnext qd tryz0
+        tra-06 : equal? finq qd (δ fa q i) ≡ is0-bool (length y1)
+        tra-06 = TA1.q=qd ta 
+        tra-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2)
+        tra-05 y2 q tr = {!!}
+        tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-           tra-04 [] q tr 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 {!!} {!!}  )
-           tra-04 (y0 ∷ y2) q (tnext q tr) with equal? finq qd q | inspect (equal? finq qd) q
-           ... | true | record { eq = eq } = ⊥-elim ( ¬-bool {!!} {!!} ) -- y2 + z1 contains two qd
-           ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr )
+        tra-04 [] q tr 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-05 [] q tr) ) 
+        tra-04 (y0 ∷ y2) q (tnext q tr) with equal? finq qd q | inspect (equal? finq qd) q
+        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool (tra-05 (y0 ∷ y2) q (tnext q tr)) eq ) where -- y2 + z1 contains two qd
+        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr ) 
    ... | 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
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where