Nuprl Definition : dl-sem-eq
a ≡ b == ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k1,k2:K. ([|a|] k1 k2 ⇐⇒ [|b|] k1 k2)
Definitions occuring in Statement :
dl-prog-sem: [|alpha|],
nat: ℕ,
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
universe: Type,
nat: ℕ,
function: x:A ⟶ B[x],
prop: ℙ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
dl-prog-sem: [|alpha|],
so_apply: x[s]
FDL editor aliases :
dl-sem-eq
Latex:
a \mequiv{} b == \mforall{}K:Type. \mforall{}R:\mBbbN{} {}\mrightarrow{} K {}\mrightarrow{} K {}\mrightarrow{} \mBbbP{}. \mforall{}P:\mBbbN{} {}\mrightarrow{} K {}\mrightarrow{} \mBbbP{}. \mforall{}k1,k2:K. ([|a|] k1 k2 \mLeftarrow{}{}\mRightarrow{} [|b|] k1 k2)
Date html generated:
2019_10_15-AM-11_45_49
Last ObjectModification:
2019_03_26-PM-00_01_31
Theory : dynamic!logic
Home
Index