{ 
[A:Type]
eq:EqDecider(A)
[P:x:A 
Type 
]
f,g:x:A fp-> Type.
(y
dom(f). w=f(y) 
P[y;w]
ydom(g). w=g(y) P[y;w]
ydom(f 
g). w=f g(y) P[y;w]) }
{ Proof }
Definitions occuring in Statement :
fpf-all: xdom(f). v=f(x) P[x; v],
fpf-join: f g,
fpf: a:A fp-> B[a],
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type,
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
prop: ,
implies: P Q,
fpf-all: xdom(f). v=f(x) P[x; v],
so_apply: x[s1;s2],
member: t T,
top: Top,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
so_apply: x[s],
iff: P 
Q,
and: P 
Q,
bool: 
,
unit: Unit,
or: P 
Q,
not: 
A,
false: False,
it: 
,
guard: {T}
Lemmas :
assert_witness,
fpf-dom_wf,
fpf-join_wf,
top_wf,
fpf-trivial-subtype-top,
fpf-join-dom2,
fpf-join-ap-sq,
assert_wf,
fpf-all_wf,
fpf_wf,
deq_wf,
bool_wf,
not_wf,
bnot_wf,
iff_weakening_uiff,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot
\mforall{}[A:Type]
\mforall{}eq:EqDecider(A)
\mforall{}[P:x:A {}\mrightarrow{} Type {}\mrightarrow{} \mBbbP{}]
\mforall{}f,g:x:A fp-> Type.
(\mforall{}y\mmember{}dom(f). w=f(y) {}\mRightarrow{} P[y;w]
{}\mRightarrow{} \mforall{}y\mmember{}dom(g). w=g(y) {}\mRightarrow{} P[y;w]
{}\mRightarrow{} \mforall{}y\mmember{}dom(f \moplus{} g). w=f \moplus{} g(y) {}\mRightarrow{} P[y;w])
Date html generated:
2011_08_10-AM-08_07_37
Last ObjectModification:
2011_06_18-AM-08_25_25
Home
Index