{ 
[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). init:Id bag(B).
F:Id k:n bag(A k) bag(B) bag(B).
strictness:(i:Id. b:bag(B). f:k:n bag(A k).
((
k:n. ((f k) = {})) 
((F i f b) = {})))
(i:Id. b:bag(B). ((F i (
i.{}) b) = {})).
(rec-comb-prc(B;n;Xprs;init;F;strictness)
NormalLProgrammable(B;rec-comb(Xs;F;init))) }
{ Proof }
Definitions occuring in Statement :
rec-comb-prc: rec-comb-prc(B;n;Xprs;init;F;strictness),
normal-locally-programmable: NormalLProgrammable(A;X),
rec-comb: rec-comb(X;f;init),
eclass: EClass(A[eo; e]),
Id: Id,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
or: P Q,
member: t T,
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 :
uall: [x:A]. B[x],
all: x:A. B[x],
int_seg: {i..j},
bag: bag(T),
or: P Q,
implies: P Q,
exists: x:A. B[x],
empty-bag: {},
member: t T,
rec-comb-prc: rec-comb-prc(B;n;Xprs;init;F;strictness),
feedback-df-program-case2: feedback-df-program-case2(B;F;dfps;init),
upto: upto(n),
feedback-df-program-case1: feedback-df-program-case1(B;F;dfps;init),
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),
bl-all: (xL.P[x])_b,
band: p q,
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-comb_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{}init:Id {}\mrightarrow{} bag(B). \mforall{}F:Id
{}\mrightarrow{} k:\mBbbN{}n {}\mrightarrow{} bag(A k)
{}\mrightarrow{} bag(B)
{}\mrightarrow{} bag(B).
\mforall{}strictness:(\mdownarrow{}\mforall{}i:Id. \mforall{}b:bag(B). \mforall{}f:k:\mBbbN{}n {}\mrightarrow{} bag(A k).
((\mexists{}k:\mBbbN{}n. ((f k) = \{\})) {}\mRightarrow{} ((F i f b) = \{\})))
\mvee{} (\mdownarrow{}\mforall{}i:Id. \mforall{}b:bag(B). ((F i (\mlambda{}i.\{\}) b) = \{\})).
(rec-comb-prc(B;n;Xprs;init;F;strictness) \mmember{} NormalLProgrammable(B;rec-comb(Xs;F;init)))
Date html generated:
2011_08_16-PM-06_35_09
Last ObjectModification:
2011_08_13-PM-10_04_10
Home
Index