Nuprl Lemma : negated_spr_append_back_closed
g:
List 
. (spr(g) 
(a: List. (((g a) > 0) (b: List. ((g (a @ b)) > 0)))))
Proof
Definitions occuring in Statement :
append: as @ bs,
nat: ,
gt: i > j,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
natural_number: $n
Definitions :
all: x:A. B[x],
implies: P Q,
gt: i > j,
member: t 
T,
so_apply: x[s],
top: Top,
nat: ,
spr: spr(g),
uall: [x:A]. B[x],
guard: {T},
and: P 
Q,
prop: 
Lemmas :
Error :list_wf,
nat_wf,
gt_wf,
spr_wf,
last_induction,
append_wf,
append_back_nil,
append_assoc
\mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) > 0) {}\mRightarrow{} (\mforall{}b:\mBbbN{} List. ((g (a @ b)) > 0)))))
Date html generated:
2013_03_20-AM-10_32_29
Last ObjectModification:
2013_03_12-PM-04_17_12
Home
Index