Nuprl Lemma : programmable-iff-bounded-locally-programmable
Info:{Info:Type| 
Info} . A:{A:Type| valueall-type(A)} .
[X:EClass(A)]. (Programmable(A;X) 
NormalLProgrammable(A;X) 
LocBounded(A;X))
Proof not projected
Definitions occuring in Statement :
programmable: Programmable(A;X),
normal-locally-programmable: NormalLProgrammable(A;X),
loc-bounded-class: LocBounded(T;X),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
squash: T,
and: P Q,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Definitions :
rev_implies: P Q,
implies: P Q,
prop: 
,
so_lambda: 
x y.t[x; y],
member: t 
T,
and: P Q,
iff: P Q,
uall: [x:A]. B[x],
all: x:A. B[x],
true: True,
guard: {T},
so_lambda: x.t[x],
bag-member: x bs,
subtype: S 
T,
top: Top,
class-loc-bound: class-loc-bound{i:l}(Info;T;X;L),
exists: 
x:A. B[x],
loc-bounded-class: LocBounded(T;X),
squash: T,
false: False,
not: 
A,
so_apply: x[s1;s2],
ycomb: Y,
uiff: uiff(P;Q),
empty-bag: {},
uimplies: b supposing a,
or: P 
Q,
so_apply: x[s],
decidable: Dec(P),
map: map(f;as),
dataflow-history-val: dataflow-history-val(es;e;x.P[x]),
classrel: v X(e),
bag-map: bag-map(f;bs),
bag-mapfilter: bag-mapfilter(f;P;bs),
dataflow-set-class: dataflow-set-class(x.P[x]),
sq_exists: x:{A| B[x]},
programmable: Programmable(A;X),
rev_uimplies: rev_uimplies(P;Q)
Lemmas :
locally-programmable-iff,
and_functionality_wrt_iff,
iff_functionality_wrt_iff,
locally-programmable_wf,
loc-bounded-class_wf,
normal-locally-programmable_wf,
and_wf,
programmable_wf,
squash_wf,
valueall-type_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
eclass_wf,
class-loc-bound_wf,
empty-bag_wf,
equal_wf,
not_functionality_wrt_uiff,
bag-member-empty,
es-le-before_wf,
es-info_wf,
map_wf,
last-data-stream-dataflow-union-empty,
equal-empty-bag,
assert-bag-null,
bag-filter_wf,
es-loc_wf,
eq_id_wf,
assert_wf,
bag-null_wf,
decidable__assert,
classrel_wf,
pi1_wf_top,
bag_wf,
dataflow_wf,
Id_wf,
bag-map_wf,
bag-member_wf,
bag-member-map,
assert-eq-id,
bag-member-filter-set,
empty-bag-iff-no-member,
decidable__equal_Id,
decidable__bag-member2
\mforall{}Info:\{Info:Type| \mdownarrow{}Info\} . \mforall{}A:\{A:Type| valueall-type(A)\} .
\mforall{}[X:EClass(A)]. (Programmable(A;X) \mLeftarrow{}{}\mRightarrow{} NormalLProgrammable(A;X) \mwedge{} LocBounded(A;X))
Date html generated:
2012_01_23-PM-12_30_16
Last ObjectModification:
2011_12_13-PM-05_44_24
Home
Index