Nuprl Lemma : empty_spr
g:
List 
. (spr(g) 
((g []) > 0) (a: List. ((g a) > 0)))
Proof
Definitions occuring in Statement :
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,
nil: Error :nil,
append: as @ bs,
list_ind: Error :list_ind,
it: 
,
nat: ,
uall: [x:A]. B[x],
prop: 
Lemmas :
Error :list_wf,
nat_wf,
gt_wf,
Error :nil_wf,
spr_wf,
negated_spr_append_back_closed
\mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} ((g []) > 0) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. ((g a) > 0)))
Date html generated:
2013_03_20-AM-10_32_33
Last ObjectModification:
2013_03_12-PM-04_24_09
Home
Index