{ 
[Info:{Info:Type| 
Info} ]
A,B:{B:Type| valueall-type(B)} .
[X:EClass(A)]. [Y:EClass(B)].
(NormalLProgrammable(A;X)
NormalLProgrammable(B;Y)
NormalLProgrammable(A;(X until Y))) }
{ Proof }
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
until-class: (X until Y),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Lemmas :
primed-class-locally-programmable,
int_subtype_base,
decidable__equal_int,
empty-bag_wf,
bag-null_wf,
ge_wf,
set_subtype_base,
subtype_base_sq,
length_wf1,
non_neg_length,
length_cons,
length_nil,
length_wf_nat,
int_seg_wf,
nat_wf,
false_wf,
not_wf,
le_wf,
simple-comb-locally-programmable1,
select_wf,
sq_stable_from_decidable,
subtype_rel_wf,
top_wf,
subtype_rel_self,
es-base-E_wf,
es-interface-subtype_rel2,
es-interface-top,
member_wf,
until-class-simple-comb,
true_wf,
local-program-at_wf,
dataflow-program_wf,
Id_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
valueall-type_wf,
squash_wf,
iff_wf,
bag_wf,
ifthenelse_wf,
simple-comb2_wf,
until-class_wf,
normal-locally-programmable_wf,
rev_implies_wf,
primed-class_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A,B:\{B:Type| valueall-type(B)\} .
\mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)].
(NormalLProgrammable(A;X) {}\mRightarrow{} NormalLProgrammable(B;Y) {}\mRightarrow{} NormalLProgrammable(A;(X until Y)))
Date html generated:
2011_08_16-PM-06_19_59
Last ObjectModification:
2011_06_29-PM-12_43_19
Home
Index