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