{ 
[A:Type]
f:a:A fp-> Top List. g:a:A fp-> Top. eq:EqDecider(A). x:A. R:Top.
((x 
fpf-domain(fpf-union-join(eq;R;f;g)))
(x fpf-domain(f)) 
(x fpf-domain(g))) }
{ Proof }
Definitions occuring in Statement :
fpf-union-join: fpf-union-join(eq;R;f;g),
fpf-domain: fpf-domain(f),
fpf: a:A fp-> B[a],
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
iff: P Q,
or: P Q,
list: type List,
universe: Type,
l_member: (x l),
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
fpf-domain: fpf-domain(f),
fpf-union-join: fpf-union-join(eq;R;f;g),
or: P Q,
pi1: fst(t),
fpf-dom: x dom(f),
member: t T,
so_lambda: 
x.t[x],
prop: 
,
and: P 
Q,
implies: P Q,
rev_implies: P Q,
fpf: a:A fp-> B[a],
so_apply: x[s],
decidable: Dec(P),
not: 
A,
uimplies: b supposing a,
false: False
Lemmas :
top_wf,
deq_wf,
fpf_wf,
l_member_wf,
append_wf,
filter_wf,
bnot_wf,
deq-member_wf,
assert_wf,
decidable__assert,
assert-deq-member,
not_functionality_wrt_iff,
not_wf,
iff_functionality_wrt_iff,
or_functionality_wrt_iff,
member_filter,
member_append,
and_functionality_wrt_iff,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot
\mforall{}[A:Type]
\mforall{}f:a:A fp-> Top List. \mforall{}g:a:A fp-> Top. \mforall{}eq:EqDecider(A). \mforall{}x:A. \mforall{}R:Top.
((x \mmember{} fpf-domain(fpf-union-join(eq;R;f;g))) \mLeftarrow{}{}\mRightarrow{} (x \mmember{} fpf-domain(f)) \mvee{} (x \mmember{} fpf-domain(g)))
Date html generated:
2011_08_10-AM-08_01_43
Last ObjectModification:
2011_06_18-AM-08_20_07
Home
Index