{ 
[Info:{Info:Type| 
Info} ]
A:{T:Type| valueall-type(T)}
[X:EClass(A)]
init:Id 
bag(A)
(NormalLProgrammable(A;X) 
NormalLProgrammable(A;Prior(X)?init)) }
{ Proof }
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
primed-class-opt: Prior(X)?b,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Lemmas :
seq-dataflow_wf,
buffer-dataflow_wf,
delay-program-meaning,
null-data-stream,
null-map,
not_assert_elim,
intensional-universe_wf,
append_is_nil,
band_wf,
bnot_of_lt_int,
null_wf,
null_append,
append-nil,
dataflow_subtype,
bag-subtype-list,
filter_append_sq,
last_append,
data-stream-cons,
subtype_rel_list,
iterate-dataflow_wf,
dataflow-ap_wf,
pi2_wf,
data-stream-append,
append_wf,
es-pred_wf,
filter_wf_top,
null_wf3,
es-loc-pred,
es-pred-causl,
bag-size_wf,
rev_implies_wf,
iff_wf,
l_member_wf,
assert_of_null,
not_functionality_wrt_uiff,
permutation_wf,
quotient_wf,
equiv_rel_wf,
trans_wf,
sym_wf,
refl_wf,
list-subtype,
filter_type,
ge_wf,
nat_properties,
es-causl-swellfnd,
es-causl_wf,
filter_wf,
guard_wf,
nat_ind_tp,
primed-class-opt-cases,
es-interface-top,
es-interface-subtype_rel2,
assert_of_bnot,
es-first_wf,
firstn_all,
firstn-append,
nat_wf,
non_neg_length,
length_wf_nat,
eqtt_to_assert,
assert_of_le_int,
le_wf,
uiff_transitivity,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_le_int,
bnot_wf,
le_int_wf,
firstn_wf,
list_subtype_base,
isect_subtype_base,
length-append,
map_append_sq,
es-before_wf3,
es-locl_wf,
es-before_wf,
map_wf,
sq_stable__subtype_rel,
es-le-before-not-null,
not_wf,
pos_length2,
top_wf,
non_null_iff_length,
assert_of_lt_int,
bool_wf,
bool_subtype_base,
bfalse_wf,
length_wf1,
assert_wf,
es-le-before_wf,
es-le_wf,
true_wf,
lt_int_wf,
ifthenelse_wf,
false_wf,
es-le-before_wf2,
es-base-E_wf,
es-le-loc,
es-info_wf,
map_wf_listp,
last-delay-data-stream1,
listp_wf,
dataflow_wf,
subtype_rel_self,
bag_wf,
subtype_rel_wf,
subtype_base_sq,
df-program-type_wf,
member_wf,
Id_wf,
squash_wf,
valueall-type_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
eclass_wf,
normal-locally-programmable_wf,
dataflow-program_wf,
local-program-at_wf,
primed-class-opt_wf,
delay-program_wf,
df-program-meaning_wf,
data-stream_wf,
last_wf,
es-loc_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A:\{T:Type| valueall-type(T)\}
\mforall{}[X:EClass(A)]
\mforall{}init:Id {}\mrightarrow{} bag(A). (NormalLProgrammable(A;X) {}\mRightarrow{} NormalLProgrammable(A;Prior(X)?init))
Date html generated:
2011_08_16-PM-06_19_30
Last ObjectModification:
2011_07_25-PM-05_14_59
Home
Index