Nuprl Lemma : aa_3n_plus_1_depth_wf_comp_ind_pi_full
((
p:
. a,b:Base. ((p ~ a + b) 
((
a1:. (a1 ~ a)) 
(b1:. (b1 ~ b)))))
(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,
add: n + m,
natural_number: $n,
int: ,
base: Base,
sqequal: s ~ t,
exp: i^n
Definitions :
nat: ,
uimplies: b supposing a,
false: False,
not: 
A,
le: A B,
gt: i > j,
implies: P Q,
and: P Q,
all: x:A. B[x],
exists: x:A. B[x],
ge: i j ,
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
rev_implies: P 
Q,
iff: P Q,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
pi1: fst(t),
aa_3n_plus_1_depth_pi: aa_3n_plus_1_depth_pi(m),
nat_plus: 
,
eq_int: (i =
j),
true: True,
squash: 
T,
uall: [x:A]. B[x],
so_apply: x[s],
uiff: uiff(P;Q),
guard: {T},
sq_type: SQType(T),
or: P 
Q,
pi2: snd(t),
bool: 
,
unit: Unit,
it: 
Lemmas :
le_wf,
less_than_wf,
nat_properties,
nat_wf,
all_wf,
base_wf,
base_sq,
int_sq,
exists_wf,
nat_sq,
ge_wf,
gt_wf,
assert_of_bnot,
iff_weakening_uiff,
iff_transitivity,
eqff_to_assert,
assert_of_eq_int,
eqtt_to_assert,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bool_cases,
equal_wf,
not_wf,
bnot_wf,
assert_wf,
eq_int_wf,
exp_wf2,
subtype_rel_self,
int_subtype_base,
divide_wf,
div_rem_sum,
uiff_transitivity,
squash_wf,
true_wf,
exp_add,
exp1
((\mforall{}p:\mBbbZ{}. \mforall{}a,b:Base. ((p \msim{} a + b) {}\mRightarrow{} ((\mexists{}a1:\mBbbZ{}. (a1 \msim{} a)) \mwedge{} (\mexists{}b1:\mBbbZ{}. (b1 \msim{} b)))))
\mwedge{} (\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_56_35
Last ObjectModification:
2012_11_27-AM-10_33_39
Home
Index