Nuprl Lemma : defined-by-bind-comb-program
[Info:Type]. [B:{B:Type| valueall-type(B)} ]. [P:eclass-program{i:l}(Info)].
[Q:x:eclass-program-type(P) 
eclass-program{i:l}(Info)].
defined-class(bind-comb-program(B;P;Q)) = defined-class(P) >x> defined-class(Q x)
supposing x:eclass-program-type(P). (eclass-program-type(Q x) = B)
Proof not projected
Definitions occuring in Statement :
bind-comb-program: bind-comb-program(B;PX;PY),
defined-class: defined-class(prg),
eclass-program-type: eclass-program-type(prg),
eclass-program: eclass-program{i:l}(Info),
bind-class: X >x> Y[x],
eclass: EClass(A[eo; e]),
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t 
T,
so_lambda: 
x.t[x],
rev_implies: P 
Q,
iff: P 
Q,
so_lambda: x y.t[x; y],
squash: 
T,
true: True,
and: P 
Q,
implies: P Q,
all: x:A. B[x],
eclass: EClass(A[eo; e]),
bind-class: X >x> Y[x],
defined-class: defined-class(prg),
bind-comb-program: bind-comb-program(B;PX;PY),
spreadn: spread3,
ifthenelse: if b then t else f fi ,
dataflow-set-class: dataflow-set-class(x.P[x]),
fpf-cap: f(x)?z,
dataflow-history-val: dataflow-history-val(es;e;x.P[x]),
fpf-dom: x dom(f),
pi1: fst(t),
btrue: tt,
bfalse: ff,
eclass-program-type: eclass-program-type(prg),
prop: 
,
df-program-type: df-program-type(dfp),
null-df-program: null-df-program(B),
es-le-before: 
loc(e),
top: Top,
bind-dataflow-aux: bind-dataflow-aux(P;dfs;a.Q[a]),
pi2: snd(t),
subtype: S 
T,
suptype: suptype(S; T),
let: let,
so_apply: x[s],
bag: bag(T),
int_seg: {i..j
},
lelt: i j < k,
le: A B,
not: 
A,
false: False,
es-le: e loc e' ,
or: P 
Q,
guard: {T},
nat: 
,
map: map(f;as),
bag-combine: 
xbs.f[x],
bag-map: bag-map(f;bs),
ycomb: Y,
bag-union: bag-union(bbs),
concat: concat(ll),
reduce: reduce(f;k;as),
es-before: before(e),
assert: 
b,
compose: f o g,
last: last(L),
null: null(as),
length: ||as||,
bnot: 
b,
select: l[i],
le_int: i z j,
lt_int: i <z j,
eclass-program: eclass-program{i:l}(Info),
so_apply: x[s1;s2],
fpf: a:A fp-> B[a],
bool: 
,
unit: Unit,
sq_stable: SqStable(P),
uiff: uiff(P;Q),
sq_type: SQType(T),
it: 
,
bag-append: as + bs,
single-bag: {x},
empty-bag: {}
Lemmas :
bind-class_wf,
defined-class_wf,
eclass_wf,
squash_wf,
true_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc,
subtype_rel_self,
all_wf,
eclass-program-type_wf,
valueall-type_wf,
equal_wf,
eclass-program_wf,
deq-member_wf,
Id_wf,
id-deq_wf,
es-loc_wf,
bool_wf,
iff_transitivity,
assert_wf,
l_member_wf,
iff_weakening_uiff,
eqtt_to_assert,
assert-deq-member,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_iff,
bind-df-program-meaning,
dataflow-program_wf,
df-program-type_wf,
null-df-program_wf,
sq_stable__valueall-type,
es-le-before_wf2,
list-subtype-bag,
es-le_wf,
bag-combine_wf,
bag_wf,
eo-forward_wf,
member-eo-forward-E,
last_wf,
data-stream_wf,
map_wf,
es-info_wf,
es-le-before_wf,
df-program-meaning_wf,
dataflow_wf,
es-le-loc,
and_wf,
df-program-meaning_wf_null,
eo-forward-info,
iterate-bind-dataflow,
es-before_wf,
pi2_wf,
dataflow-ap_wf,
iterate-dataflow_wf,
eo-forward-E-subtype,
sq_stable_from_decidable,
decidable__es-le,
bag-map-append,
bag-map_wf,
bag-combine-append-left,
subtype_rel_dep_function,
int_seg_wf,
length_wf,
upto_wf,
lelt_wf,
length-map,
length_wf_nat,
nth_tl_wf,
firstn_wf,
select_wf,
non_neg_length,
map_length,
nat_wf,
less_than_wf,
es-before_wf3,
bag_qinc,
es-locl_wf,
subtype_rel_bag,
subtype_rel_sets,
es-le_weakening,
single-bag_wf,
bag-append_wf,
map-as-map-upto,
top_wf,
map-id,
decidable__es-locl,
bag-combine-map,
firstn_map,
le_wf,
firstn-before,
select-map,
nth_tl_map,
eo-forward-before,
member-es-before,
select_member,
filter_wf,
es-ble_wf,
nth_tl-es-before,
bag-combine-assoc,
uiff_transitivity,
es-first_wf,
subtype_base_sq,
bool_subtype_base,
btrue_wf,
eo-forward-first-trivial,
bag-map-map,
bag-append-empty,
map_append_sq,
last-data-stream,
append_wf,
null_wf3,
assert_of_null,
append_is_nil,
not_functionality_wrt_uiff,
last_append,
false_wf,
bind-dataflow_wf,
length_append,
firstn-append,
le_int_wf,
assert_of_le_int,
firstn_all,
lt_int_wf,
assert_functionality_wrt_uiff,
bnot_of_le_int,
assert_of_lt_int,
bfalse_wf,
es-le-before-not-null,
null-map,
null-data-stream,
dataflow_subtype,
pi1_wf_top,
eo-forward-loc,
subtype_rel-equal,
map-is-top-list,
member_wf,
empty-bag_wf,
data-stream-null-df-program,
last-map,
bag-combine-empty-left,
bag-combine-empty-right
\mforall{}[Info:Type]. \mforall{}[B:\{B:Type| valueall-type(B)\} ]. \mforall{}[P:eclass-program\{i:l\}(Info)].
\mforall{}[Q:x:eclass-program-type(P) {}\mrightarrow{} eclass-program\{i:l\}(Info)].
defined-class(bind-comb-program(B;P;Q)) = defined-class(P) >x> defined-class(Q x)
supposing \mforall{}x:eclass-program-type(P). (eclass-program-type(Q x) = B)
Date html generated:
2012_01_23-PM-12_36_11
Last ObjectModification:
2011_12_20-PM-12_22_27
Home
Index