Nuprl Lemma : listify-append-last
[T:Type]. [m:
]. [n:{n:| n 
m } ]. [f:{m..n + 1
} 
T]. (listify(f;m;n + 1) = (listify(f;m;n) @ [f n]))
Proof not projected
Definitions occuring in Statement :
listify: listify(f;m;n),
append: as @ bs,
int_seg: {i..j},
uall: [x:A]. B[x],
ge: i j ,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
add: n + m,
natural_number: $n,
int: ,
universe: Type,
equal: s = t
Definitions :
ge: i j ,
int_seg: {i..j},
listify: listify(f;m;n),
and: P 
Q,
le: A 
B,
member: t 
T,
not: 
A,
implies: P 
Q,
false: False,
prop: 
,
rev_implies: P 
Q,
iff: P Q,
all: x:A. B[x],
subtype: S 
T,
suptype: suptype(S; T),
lelt: i j < k,
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
uall: [x:A]. B[x],
bool: 
,
unit: Unit,
uimplies: b supposing a,
uiff: uiff(P;Q),
guard: {T},
it: 
Lemmas :
listify-append,
le_wf,
append_wf,
listify_wf,
int_seg_wf,
le_int_wf,
bool_wf,
assert_wf,
lt_int_wf,
bnot_wf,
ge_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_le_int,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_le_int,
assert_of_lt_int
\mforall{}[T:Type]. \mforall{}[m:\mBbbZ{}]. \mforall{}[n:\{n:\mBbbZ{}| n \mgeq{} m \} ]. \mforall{}[f:\{m..n + 1\msupminus{}\} {}\mrightarrow{} T].
(listify(f;m;n + 1) = (listify(f;m;n) @ [f n]))
Date html generated:
2012_02_20-PM-05_59_09
Last ObjectModification:
2012_02_02-PM-02_30_38
Home
Index