{ 
[f:Top]. [b:bag(Top)].
b':bag(Top)
((concat-lifting-3(f) {} b b' ~ {})
(concat-lifting-3(f) b {} b' ~ {})
(concat-lifting-3(f) b b' {} ~ {})) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-3: concat-lifting-3(f),
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
and: P Q,
apply: f a,
sqequal: s ~ t,
empty-bag: {},
bag: bag(T)
Lemmas :
true_wf,
null_wf,
ifthenelse_wf,
bag-subtype-list,
subtype_rel_wf,
permutation_wf,
null_wf3,
lifting-gen-strict,
nat_wf,
member_wf,
select_wf,
empty-bag_wf,
top_wf,
bag_wf,
int_seg_wf,
assert_wf,
false_wf,
le_wf,
not_wf
\mforall{}[f:Top]. \mforall{}[b:bag(Top)].
\mforall{}b':bag(Top)
((concat-lifting-3(f) \{\} b b' \msim{} \{\})
\mwedge{} (concat-lifting-3(f) b \{\} b' \msim{} \{\})
\mwedge{} (concat-lifting-3(f) b b' \{\} \msim{} \{\}))
Date html generated:
2011_08_17-PM-06_11_42
Last ObjectModification:
2011_06_28-PM-03_48_26
Home
Index