{ 
[A:Type]
f,g:a:A fp-> Top. eq:EqDecider(A).
fpf-domain(f 
g) 
fpf-domain(f) @ fpf-domain(g) }
{ Proof }
Definitions occuring in Statement :
fpf-join: f g,
fpf-domain: fpf-domain(f),
fpf: a:A fp-> B[a],
append: as @ bs,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
universe: Type,
deq: EqDecider(T),
l_contains: A B
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
l_contains: A B,
l_all: (x
L.P[x]),
implies: P 
Q,
member: t T,
so_lambda: 
x.t[x],
prop: 
,
or: P 
Q,
rev_implies: P 
Q,
iff: P Q,
and: P 
Q,
so_apply: x[s],
guard: {T}
Lemmas :
deq_wf,
fpf_wf,
top_wf,
l_member_wf,
fpf-domain_wf,
fpf-join_wf,
append_wf,
implies_functionality_wrt_iff,
fpf-domain-join,
member_append
\mforall{}[A:Type]. \mforall{}f,g:a:A fp-> Top. \mforall{}eq:EqDecider(A). fpf-domain(f \moplus{} g) \msubseteq{} fpf-domain(f) @ fpf-domain(g)
Date html generated:
2011_08_10-AM-07_59_34
Last ObjectModification:
2011_06_18-AM-08_19_04
Home
Index