Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/temporal-logic.agda @ 330:407684f806e4

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 Wed, 16 Nov 2022 17:43:10 +0900
parents cd73fe566291
children 6f3636fbc481
comparison
equal deleted inserted replaced
329:ba0ae5de62d1 330:407684f806e4
99 q-exists : V → QPTL V → QPTL V 99 q-exists : V → QPTL V → QPTL V
100 q-not : QPTL V → QPTL V 100 q-not : QPTL V → QPTL V
101 _q\/_ : QPTL V → QPTL V → QPTL V 101 _q\/_ : QPTL V → QPTL V → QPTL V
102 _q/\_ : QPTL V → QPTL V → QPTL V 102 _q/\_ : QPTL V → QPTL V → QPTL V
103 103
104 --
105 -- ∃ p ( <> p → ? )
106 --
107
108
104 {-# TERMINATING #-} 109 {-# TERMINATING #-}
105 SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y)) → QPTL V → V → Bool → QPTL V 110 SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y)) → QPTL V → V → Bool → QPTL V
106 SQP1 {V} dec (qt x) v t = qt x 111 SQP1 {V} dec (qt x) v t = qt x
107 SQP1 {V} dec (qs x) v t with dec x v 112 SQP1 {V} dec (qs x) v t with dec x v
108 ... | yes _ = qt t 113 ... | yes _ = qt t