Nuprl Lemma : simple-loc-comb-0-nlp
B:{B:
'| valueall-type(B)} . b:Id 
bag(B).
NormalLProgrammable'(B;simple-loc-comb-0(b)) supposing l:Id. ((b l) = {})
Proof not projected
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
simple-loc-comb-0: simple-loc-comb-0(b),
Id: Id,
uimplies: b supposing a,
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 :
simple-loc-comb-0: simple-loc-comb-0(b),
so_apply: x[s],
simple-loc-comb0: 
l.b[l]| |
Lemmas :
simple-loc-comb0-nlp
\mforall{}B:\{B:\mBbbU{}'| valueall-type(B)\} . \mforall{}b:Id {}\mrightarrow{} bag(B).
NormalLProgrammable'(B;simple-loc-comb-0(b)) supposing \mforall{}l:Id. ((b l) = \{\})
Date html generated:
2011_10_20-PM-03_29_14
Last ObjectModification:
2011_08_19-PM-10_59_48
Home
Index