Nuprl Definition : dl-same-sem
dl-same-sem(x;K;r;s) ==
((dl-kind(x) = "prog" ∈ Atom)
⇒ (∀k,k':K. (r k k'
⇐⇒ s k k')))
∧ ((dl-kind(x) = "prop" ∈ Atom)
⇒ (∀k:K. (r k
⇐⇒ s k)))
Definitions occuring in Statement :
dl-kind: dl-kind(d)
,
all: ∀x:A. B[x]
,
iff: P
⇐⇒ Q
,
implies: P
⇒ Q
,
and: P ∧ Q
,
apply: f a
,
token: "$token"
,
atom: Atom
,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q
,
implies: P
⇒ Q
,
equal: s = t ∈ T
,
atom: Atom
,
dl-kind: dl-kind(d)
,
token: "$token"
,
all: ∀x:A. B[x]
,
iff: P
⇐⇒ Q
,
apply: f a
FDL editor aliases :
dl-same-sem
Latex:
dl-same-sem(x;K;r;s) ==
((dl-kind(x) = "prog") {}\mRightarrow{} (\mforall{}k,k':K. (r k k' \mLeftarrow{}{}\mRightarrow{} s k k')))
\mwedge{} ((dl-kind(x) = "prop") {}\mRightarrow{} (\mforall{}k:K. (r k \mLeftarrow{}{}\mRightarrow{} s k)))
Date html generated:
2019_10_15-AM-11_43_36
Last ObjectModification:
2019_03_26-AM-11_28_13
Theory : dynamic!logic
Home
Index