Nuprl Lemma : vr_test2
x:
. 
n:
. (x < n)
Proof not projected
Definitions occuring in Statement :
nat: ,
all: x:A. B[x],
exists: x:A. B[x],
rless: x < y,
real:
Definitions :
tactic: Error :tactic,
CollapseTHENA: Error :CollapseTHENA,
Auto: Error :Auto,
exists: x:A. B[x],
product: x:A 
B[x],
real: ,
all: x:A. B[x],
function: x:A 
B[x],
member: t 
T,
equal: s = t,
rleq: x 
y,
rabs: |x|,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
rminus: -(r),
uall: [x:A]. B[x],
nat: ,
qle: r s,
rnonneg: rnonneg(r),
isect: 
x:A. B[x],
subtype_rel: A 
r B,
uiff: uiff(P;Q),
and: P 
Q,
uimplies: b supposing a,
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A B,
strong-subtype: strong-subtype(A;B),
b-union: A 
B,
tunion: x:A.B[x],
reals: [],
rmax: rmax(r;s),
add: n + m,
D: Error :D,
MaAuto: Error :MaAuto,
natural_number: $n,
rless: x < y,
grp_leq: a b,
assert: 
b,
infix_ap: x f y,
apply: f a,
grp_le: 
,
qadd_grp: <
+>,
pair: <a, b>,
lambda: 
x.A[x],
ifthenelse: if b then t else f fi ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
nat_plus: 
,
prop: 
,
int: 
,
subtype: S T,
rationals: ,
set: {x:A| B[x]} ,
false: False,
implies: P 
Q,
void: Void,
universe: Type,
int_nzero: 
,
rpositive: rpositive(r),
qless: r < s,
iff: P 
Q,
rev_implies: P Q,
rsub: x - y,
qdiv: (r/s),
length: ||as||,
p-outcome: Outcome,
bool: 
,
quotient: x,y:A//B[x; y],
eclass: EClass(A[eo; e]),
es-E-interface: E(X),
fpf: a:A fp-> B[a],
btrue: tt,
union: left + right,
fpf-cap: f(x)?z,
true: True,
top: Top,
list: type List,
bag: bag(T),
isect2: T1 T2,
dataflow: dataflow(A;B),
fset: FSet{T},
record: record(x.T[x]),
record+: record+,
labeled-graph: LabeledGraph(T),
ldag: LabeledDAG(T),
or: P 
Q,
tag-by: zT,
spread: spread def,
infinitesmal: Infinitesmal,
sqequal: s ~ t,
valueall-type: valueall-type(T),
bfalse: ff,
so_lambda: 
x.t[x],
radd: r + s,
rmul: r * s,
req: x = y,
rev_uimplies: rev_uimplies(P;Q),
limited-type: LimitedType,
qeq: qeq(r;s),
sq_type: SQType(T),
qmul: r * s,
minus: -n,
reg-tolerance: 
(r;n),
reg-approx: r(n),
intensional-universe: IType,
qabs: |r|,
qsub: r - s,
qadd: r + s,
inf-apply: m(x),
grp_car: |g|,
subtract: n - m,
squash: 
T
Lemmas :
rabs_wf1,
rleq_transitivity,
true_wf,
squash_wf,
rev_implies_wf,
iff_wf,
vr_req_to_ieq,
vr_rsub_to_sub,
nat_inc_real,
int-equal-in-rationals,
rational-is-real,
intensional-universe_wf,
reg-approx_wf,
reg-tolerance_wf,
qmul_wf,
nat_plus_properties,
subtype_base_sq,
qdiv-self,
reals_wf,
radd_wf,
rsub_wf,
qeq_wf2,
assert-qeq,
uiff_wf,
not_functionality_wrt_uiff,
assert_wf,
int_inc,
rationals_inc,
qdiv_wf,
radd_wf1,
radd-rminus-assoc,
radd-comm,
radd_functionality,
req_weakening,
rleq_functionality,
uiff_transitivity,
radd-preserves-rleq,
tunion_wf,
bfalse_wf,
infinitesmal_wf,
ifthenelse_wf,
btrue_wf,
int-rational,
subtype_rel_wf,
rationals_wf,
bool_wf,
b-union_wf,
int_nzero_wf,
rleq-rational,
integer-bound,
not_wf,
false_wf,
member_wf,
le_wf,
rless-iff-rleq,
int_inc_real,
rless_wf,
rpositive_wf,
qless_wf,
nat_plus_wf,
rminus_wf1,
rleq-rmax,
nat_wf,
qle_wf,
rnonneg_wf,
rleq_wf,
real_wf
\mforall{}x:\mBbbR{}. \mexists{}n:\mBbbN{}. (x < n)
Date html generated:
2012_02_20-PM-03_32_40
Last ObjectModification:
2012_02_02-PM-01_55_07
Home
Index