Nuprl Lemma : rec-combined-class-locally-programmable1
[Info:{Info:Type| 
Info} ]
B:{B:Type| valueall-type(B)} . n:
.
[A:n 
Type]. [Xs:k:n EClass(A k)].
((k:n. NormalLProgrammable(A k;Xs k))
(F:k:n bag(A k) bag(B) bag(B)
NormalLProgrammable(B;F|Xs,(self)'|) supposing b:bag(B). ((F (
i.{}) b) = {})))
Proof not projected
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
rec-combined-class: f|X,(self)'|,
eclass: EClass(A[eo; e]),
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
natural_number: $n,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
prop: 
,
member: t 
T,
uimplies: b supposing a,
implies: P Q,
all: x:A. B[x],
uall: [x:A]. B[x],
primed-class-opt: Prior(X)?b,
primed-class: Prior(X),
rec-comb: rec-comb(X;f;init),
rec-combined-class: f|X,(self)'|,
true: True,
guard: {T},
or: P 
Q,
squash: T,
so_apply: x[s1;s2],
so_apply: x[s],
nat: ,
subtype: S 
T
Lemmas :
squash_wf,
valueall-type_wf,
nat_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
eclass_wf,
normal-locally-programmable_wf,
int_seg_wf,
empty-bag_wf,
equal_wf,
all_wf,
bag_wf,
exists_wf,
Id_wf,
rec-comb-locally-programmable1
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}B:\{B:Type| valueall-type(B)\} . \mforall{}n:\mBbbN{}.
\mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[Xs:k:\mBbbN{}n {}\mrightarrow{} EClass(A k)].
((\mforall{}k:\mBbbN{}n. NormalLProgrammable(A k;Xs k))
{}\mRightarrow{} (\mforall{}F:k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)
NormalLProgrammable(B;F|Xs,(self)'|) supposing \mforall{}b:bag(B). ((F (\mlambda{}i.\{\}) b) = \{\})))
Date html generated:
2012_01_23-PM-12_31_28
Last ObjectModification:
2011_12_14-PM-10_27_15
Home
Index