Nuprl Lemma : simple-loc-comb0-nlp
B:{B:
'| valueall-type(B)} . b:Id 
bag(B). NormalLProgrammable'(B;
v.b[v]| |) supposing l:Id. ((b l) = {})
Proof not projected
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
simple-loc-comb0: l.b[l]| |,
Id: Id,
uimplies: b supposing a,
so_apply: x[s],
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
all: x:A. B[x],
uimplies: b supposing a,
simple-loc-comb0: l.b[l]| |,
so_apply: x[s],
member: t 
T,
nat: 
,
implies: P 
Q,
prop: 
,
le: A 
B,
not: 
A,
false: False,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
int_seg: {i..j
},
lelt: i j < k,
and: P 
Q,
label: ...$L... t
Lemmas :
Id_wf,
simple-loc-comb-locally-programmable1,
Message_wf,
Message-inhabited,
squash_wf,
le_wf,
unit_wf2,
int_seg_wf,
select_wf,
eclass_wf2,
length_wf2,
bag_wf,
empty-bag_wf,
valueall-type_wf
\mforall{}B:\{B:\mBbbU{}'| valueall-type(B)\} . \mforall{}b:Id {}\mrightarrow{} bag(B).
NormalLProgrammable'(B;\mlambda{}v.b[v]| |) supposing \mforall{}l:Id. ((b l) = \{\})
Date html generated:
2011_10_20-PM-03_29_06
Last ObjectModification:
2011_08_19-PM-11_20_59
Home
Index