Nuprl Definition : sq-decider
sq-decider(eq) == ∀[x,y:Base]. ((∃z:Base. (eq x y ~ inl z)) ⇒ (x ~ y))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
inl: inl x,
base: Base,
sqequal: s ~ t
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
base: Base,
apply: f a,
inl: inl x,
sqequal: s ~ t
FDL editor aliases :
sq-decider
Latex:
sq-decider(eq) == \mforall{}[x,y:Base]. ((\mexists{}z:Base. (eq x y \msim{} inl z)) {}\mRightarrow{} (x \msim{} y))
Date html generated:
2016_05_14-AM-06_06_46
Last ObjectModification:
2015_09_22-PM-05_48_12
Theory : equality!deciders
Home
Index