Nuprl Lemma : rec-combined-loc-class2-prc_wf
[Info:{Info:Type| 
Info} ]
B:{B:Type| valueall-type(B)} . n:
.
[A:n 
Type]. [Xs:k:n EClass(A k)].
Xprs:k:n. NormalLProgrammable(A k;Xs k). F:Id k:n bag(A k) bag(B) bag(B).
rec-combined-loc-class2-prc(B;n;Xprs;F) 
NormalLProgrammable(B;F|Loc, Xs, Prior(self)|)
supposing x:Id. b:bag(B). f:k:n bag(A k). ((
k:n. ((f k) = {})) 
((F x f b) = {}))
Proof not projected
Definitions occuring in Statement :
rec-combined-loc-class2-prc: rec-combined-loc-class2-prc(B;n;Xs;F),
normal-locally-programmable: NormalLProgrammable(A;X),
rec-combined-loc-class: f|Loc, X, Prior(self)|,
eclass: EClass(A[eo; e]),
Id: Id,
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
natural_number: $n,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
int_seg: {i..j},
bag: bag(T),
uimplies: b supposing a,
implies: P Q,
exists: x:A. B[x],
empty-bag: {},
member: t T,
rec-combined-loc-class2-prc: rec-combined-loc-class2-prc(B;n;Xs;F),
feedback-df-program-case2: feedback-df-program-case2(B;F;dfps;init),
upto: upto(n),
rec-combined-loc-class-locally-programmable2,
rec-comb-locally-programmable1,
feedback-prog: feedback-prog,
bl-exists: (xL.P[x])_b,
bnot: 
b,
isl: isl(x),
tuple-type: tuple-type(L),
df-program-statetype: df-program-statetype(dfp),
unit: Unit,
tuple: tuple(n;i.F[i]),
df-program-state: df-program-state(dfp),
select: l[i],
spreadn: spread4,
ifthenelse: if b then t else f fi ,
it: 
,
pi2: snd(t),
evalall: evalall(t),
pi1: fst(t),
null: null(as),
btrue: tt,
bfalse: ff,
permutation: permutation(T;L1;L2),
and: P 
Q,
inject: Inj(A;B;f),
permute_list: (L o f),
lelt: i 
j < k,
le: A B,
false: False,
not: A,
append: as @ bs,
mklist: mklist(n;f),
le_int: i z j,
lt_int: i <z j,
bor: p 
q,
reduce: reduce(f;k;as),
prop: 
,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
nat: ,
so_apply: x[s],
so_apply: x[s1;s2],
spreadn: spread3,
subtype: S 
T
Lemmas :
uall_wf,
squash_wf,
valueall-type_wf,
nat_wf,
int_seg_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
normal-locally-programmable_wf,
Id_wf,
bag_wf,
empty-bag_wf,
rec-combined-loc-class_wf,
nat_properties
\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{}Xprs:\mforall{}k:\mBbbN{}n. NormalLProgrammable(A k;Xs k). \mforall{}F:Id {}\mrightarrow{} k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B).
rec-combined-loc-class2-prc(B;n;Xprs;F) \mmember{} NormalLProgrammable(B;F|Loc, Xs, Prior(self)|)
supposing \mforall{}x:Id. \mforall{}b:bag(B). \mforall{}f:k:\mBbbN{}n {}\mrightarrow{} bag(A k).
((\mexists{}k:\mBbbN{}n. ((f k) = \{\})) {}\mRightarrow{} ((F x f b) = \{\}))
Date html generated:
2011_10_20-PM-03_26_58
Last ObjectModification:
2011_09_29-PM-11_10_54
Home
Index