{ 
[A:Type]
eq:EqDecider(A)
[B:A 
Type]
f,g:a:A fp-> B[a] List. R:
a:A. (B[a] List B[a] 
). a:A.
x:B[a]
((x 
fpf-union-join(eq;R;f;g)(a))
(((
a dom(f)) 
(x f(a))) 
((a dom(g)) (x g(a)))))
supposing a dom(fpf-union-join(eq;R;f;g)) }
{ Proof }
Definitions occuring in Statement :
fpf-union-join: fpf-union-join(eq;R;f;g),
fpf-ap: f(x),
fpf-dom: x dom(f),
fpf: a:A fp-> B[a],
assert: b,
bool: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
isect: x:A. B[x],
function: x:A B[x],
list: type List,
universe: Type,
l_member: (x l),
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
so_apply: x[s],
uimplies: b supposing a,
implies: P Q,
member: t T,
so_lambda: 
x.t[x],
assert: b,
or: P Q,
and: P Q,
fpf-union: fpf-union(f;g;eq;R;x),
top: Top,
ifthenelse: if b then t else f fi ,
band: p 
q,
fpf-cap: f(x)?z,
btrue: tt,
prop: 
,
bfalse: ff,
true: True,
cand: A c B,
guard: {T},
iff: P 
Q,
rev_implies: P Q,
bool: ,
unit: Unit,
false: False,
it: 
Lemmas :
assert_witness,
fpf-dom_wf,
fpf-union-join_wf,
fpf-trivial-subtype-top,
fpf_wf,
top_wf,
l_member_wf,
fpf-ap_wf,
assert_wf,
bool_wf,
deq_wf,
fpf-union-join-ap,
iff_weakening_uiff,
eqtt_to_assert,
append_wf,
filter_wf,
not_wf,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
false_wf,
nil_member,
member_append,
or_functionality_wrt_iff,
member_filter,
true_wf
\mforall{}[A:Type]
\mforall{}eq:EqDecider(A)
\mforall{}[B:A {}\mrightarrow{} Type]
\mforall{}f,g:a:A fp-> B[a] List. \mforall{}R:\mcap{}a:A. (B[a] List {}\mrightarrow{} B[a] {}\mrightarrow{} \mBbbB{}). \mforall{}a:A.
\mforall{}x:B[a]
((x \mmember{} fpf-union-join(eq;R;f;g)(a))
{}\mRightarrow{} (((\muparrow{}a \mmember{} dom(f)) \mwedge{} (x \mmember{} f(a))) \mvee{} ((\muparrow{}a \mmember{} dom(g)) \mwedge{} (x \mmember{} g(a)))))
supposing \muparrow{}a \mmember{} dom(fpf-union-join(eq;R;f;g))
Date html generated:
2011_08_10-AM-08_01_51
Last ObjectModification:
2011_06_18-AM-08_20_12
Home
Index