Nuprl Definition : reliable-env
reliable-env(env; r) == ∀t:ℕ. ∃t':ℕ. (t < t' ∧ ((fst((env t' r))) = 0 ∈ ℤ))
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
pi1: fst(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Latex:
reliable-env(env; r) == \mforall{}t:\mBbbN{}. \mexists{}t':\mBbbN{}. (t < t' \mwedge{} ((fst((env t' r))) = 0))
Date html generated:
2015_07_23-AM-11_17_04
Last ObjectModification:
2012_02_25-PM-03_45_12
Home
Index