Nuprl Lemma : gammaFIM_fun
g,h:
List 
.
(spr(g)
(a: List. (((g a) = 0) ((g (a @ [h a])) = 0)))
((g []) = 0)
(f: . x:. (gammaFIM(mklist(x;f);g;h) = mklist(x;
n.gammaFIM(mklist(n + 1;f);g;h)[n]))))
Proof
Definitions occuring in Statement :
gammaFIM: gammaFIM(a;g;h),
select: l[i],
append: as @ bs,
nat: ,
all: x:A. B[x],
implies: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
add: n + m,
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
Definitions :
ge: i 
j ,
primrec: primrec(n;b;c),
so_lambda: 
x.t[x],
false: False,
not: 
A,
le: A 
B,
prop: 
,
member: t 
T,
mklist: mklist(n;f),
implies: P Q,
nat: ,
all: x:A. B[x],
list_ind: Error :list_ind,
length: ||as||,
bfalse: ff,
btrue: tt,
it: 
,
eq_int: (i =
j),
ifthenelse: if b then t else f fi ,
gammaFIM: gammaFIM(a;g;h),
nil: Error :nil,
exists: 
x:A. B[x],
true: True,
squash: 
T,
int_seg: {i..j
},
top: Top,
and: P 
Q,
lelt: i j < k,
iff: P 
Q,
rev_implies: P Q,
cand: A c B,
hd: hd(l),
so_apply: x[s],
uall: [x:A]. B[x],
unit: Unit,
bool: 
,
uimplies: b supposing a,
sq_type: SQType(T),
or: P 
Q,
bnot: 
b,
uiff: uiff(P;Q),
assert: 
b,
guard: {T},
nequal: a 
b T
Lemmas :
ge_wf,
nat_properties,
spr_wf,
Error :cons_wf,
append_wf,
Error :list_wf,
all_wf,
le_wf,
Error :nil_wf,
equal_wf,
nat_wf,
Error :list_ind_reverse_unfold1,
bool_wf,
eq_int_wf,
gammaFIM_equi_length_mklist,
gammaFIM_equi_length,
gammaFIM_true,
gammaFIM_id,
base_sq,
ext-eq_weakening,
subtype_rel_weakening,
lelt_wf,
subtype_rel_sets,
int_seg_wf,
subtype_rel_dep_function,
subtype_rel_set_simple,
mklist_wf,
gammaFIM_wf,
select_wf,
gammaFIM_unfold,
mklist_length,
neg_assert_of_eq_int,
Error :assert-bnot,
bool_subtype_base,
subtype_base_sq,
bool_cases_sqequal,
eqff_to_assert,
assert_of_eq_int,
eqtt_to_assert,
Error :firstn-mklist1,
subtype_top,
top_wf,
subtype_rel_list,
Error :non_null_iff_length,
last_wf,
int_subtype_base,
mklist-add1,
true_wf,
squash_wf,
length_wf_nat,
length_cons,
length_wf_nil,
non_neg_length,
length_nil,
length_wf,
select_append_back,
select0,
and_wf
\mforall{}g,h:\mBbbN{} List {}\mrightarrow{} \mBbbN{}.
(spr(g)
{}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} ((g (a @ [h a])) = 0)))
{}\mRightarrow{} ((g []) = 0)
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}x:\mBbbN{}.
(gammaFIM(mklist(x;f);g;h) = mklist(x;\mlambda{}n.gammaFIM(mklist(n + 1;f);g;h)[n]))))
Date html generated:
2013_03_20-AM-10_33_41
Last ObjectModification:
2013_03_11-PM-04_55_21
Home
Index