Nuprl Definition : dl-logical-eq-atomic
(a 
⇐⇒a b) ==  ∀p:ℕ. (|= <a> atm(p) 
⇒ <b> atm(p) ∧ |= <b> atm(p) 
⇒ <a> atm(p))
Definitions occuring in Statement : 
dl-valid: |= phi
, 
dl-diamond: <x1> x
, 
dl-implies: x1 
⇒ x
, 
dl-aprop: atm(x)
, 
nat: ℕ
, 
all: ∀x:A. B[x]
, 
and: P ∧ Q
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
nat: ℕ
, 
and: P ∧ Q
, 
dl-valid: |= phi
, 
dl-implies: x1 
⇒ x
, 
dl-diamond: <x1> x
, 
dl-aprop: atm(x)
FDL editor aliases : 
dl-logical-eq-atomic
Latex:
(a  \mLeftarrow{}{}\mRightarrow{}a  b)  ==    \mforall{}p:\mBbbN{}.  (|=  <a>  atm(p)  {}\mRightarrow{}  <b>  atm(p)  \mwedge{}  |=  <b>  atm(p)  {}\mRightarrow{}  <a>  atm(p))
Date html generated:
2019_10_15-AM-11_46_00
Last ObjectModification:
2019_03_26-PM-00_12_58
Theory : dynamic!logic
Home
Index