Nuprl Lemma : aa_pc_3n_new
(
m:
. n:
. ((m ~ snd(aa_3n_plus_1_depth_pi(n))) 
(m 
0 )))
(d:. n:.
(((n > 0) 
(d ~ snd(aa_3n_plus_1_depth_pi(n)))) (
m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m) (n 
2^m)))))
Proof
Definitions occuring in Statement :
aa_3n_plus_1_depth_pi: aa_3n_plus_1_depth_pi(m),
nat: ,
pi1: fst(t),
pi2: snd(t),
gt: i > j,
ge: i j ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
natural_number: $n,
int: ,
sqequal: s ~ t,
exp: i^n
Definitions :
implies: P Q,
all: x:A. B[x],
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
gt: i > j,
le: A B,
not: 
A,
false: False,
ge: i j ,
uimplies: b supposing a,
nat: ,
and: P Q,
iff: P 
Q,
rev_implies: P Q,
exists: x:A. B[x],
aa_3n_plus_1_depth_pi: aa_3n_plus_1_depth_pi(m),
pi1: fst(t),
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
has-value: (a)
,
nat_plus: 
,
eq_int: (i =
j),
true: True,
squash: T,
uall: [x:A]. B[x],
so_apply: x[s],
or: P 
Q,
sq_type: SQType(T),
guard: {T},
uiff: uiff(P;Q),
pi2: snd(t),
bool: 
,
unit: Unit,
assert: 
b,
bnot: 
b,
it: 
Lemmas :
nat_wf,
all_wf,
nat_sq,
int_sq,
ge_wf,
nat_properties,
less_than_wf,
le_wf,
gt_wf,
eq_int_wf,
assert_wf,
bnot_wf,
not_wf,
equal_wf,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
exp_wf2,
set-value-type,
int-value-type,
divide_wf,
div_rem_sum,
bool_cases_sqequal,
Error :assert-bnot,
neg_assert_of_eq_int,
int_subtype_base,
squash_wf,
true_wf,
exp_add,
exp1
(\mforall{}m:\mBbbZ{}. \mforall{}n:\mBbbN{}. ((m \msim{} snd(aa\_3n\_plus\_1\_depth\_pi(n))) {}\mRightarrow{} (m \mgeq{} 0 )))
{}\mRightarrow{} (\mforall{}d:\mBbbN{}. \mforall{}n:\mBbbZ{}.
(((n > 0) \mwedge{} (d \msim{} snd(aa\_3n\_plus\_1\_depth\_pi(n))))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. ((fst(aa\_3n\_plus\_1\_depth\_pi(n)) \msim{} m) \mwedge{} (n \mleq{} 2\^{}m)))))
Date html generated:
2013_03_20-AM-09_57_12
Last ObjectModification:
2013_01_05-AM-11_20_11
Home
Index