{ 
[dd1,dd2:DeclSet]. (es-decl-set-join(dd1;dd2) 
DeclSet) }
{ Proof }
Definitions occuring in Statement :
es-decl-set-join: es-decl-set-join(dd1;dd2),
es-decl-set: DeclSet,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
es-decl-set: DeclSet,
member: t T,
es-decl-set-join: es-decl-set-join(dd1;dd2),
spreadn: spread3,
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
implies: P 
Q,
btrue: tt,
prop: 
,
top: Top,
so_lambda: 
x.t[x],
bfalse: ff,
not: 
A,
iff: P 
Q,
and: P 
Q,
or: P 
Q,
false: False,
bool: 
,
unit: Unit,
so_apply: x[s],
uimplies: b supposing a,
it: 
Lemmas :
es-decl-set_wf,
member-remove-repeats,
Id_wf,
id-deq_wf,
append_wf,
member_append,
remove-repeats_wf,
deq-member_wf,
bool_wf,
iff_transitivity,
assert_wf,
l_member_wf,
iff_weakening_uiff,
eqtt_to_assert,
assert-deq-member,
null_wf3,
fpf-domain_wf,
Knd_wf,
hasloc_wf,
fpf-trivial-subtype-top,
fpf_wf,
top_wf,
subtype_rel_list,
uiff_transitivity,
assert_of_null,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
fpf-join_wf,
not_functionality_wrt_iff,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self
\mforall{}[dd1,dd2:DeclSet]. (es-decl-set-join(dd1;dd2) \mmember{} DeclSet)
Date html generated:
2011_08_16-AM-10_55_57
Last ObjectModification:
2011_06_18-AM-09_29_06
Home
Index