{ 
[Info:{Info:Type| 
Info} ]. [A:{A:Type| valueall-type(A)} ]. [X:EClass(A)].
(NormalLProgrammable(A;X) 
LocBounded(A;X) Programmable(A;X)) }
{ Proof }
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],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Lemmas :
pi2_wf,
rev_implies_wf,
programmable-iff-bounded-locally-programmable,
uall_wf,
subtype_base_sq,
pi1_wf,
class-loc-bound_wf,
set_subtype_base,
bool_wf,
iff_wf,
assert_wf,
deq_wf,
squash_wf,
valueall-type_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
loc-bounded-class_wf,
normal-locally-programmable_wf,
member_wf,
programmable_wf,
bag-map_wf,
id-deq_wf,
bag-remove-repeats_wf,
df-program-meaning_wf,
Id_wf,
df-program-type_wf,
bag_wf,
dataflow_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]. \mforall{}[A:\{A:Type| valueall-type(A)\} ]. \mforall{}[X:EClass(A)].
(NormalLProgrammable(A;X) {}\mRightarrow{} LocBounded(A;X) {}\mRightarrow{} Programmable(A;X))
Date html generated:
2011_08_16-PM-06_15_50
Last ObjectModification:
2011_07_19-PM-03_45_33
Home
Index