Nuprl Lemma : concat-lifting-loc-3-strict
∀[f,i:Top]. ∀[b,b':bag(Top)].
((concat-lifting-loc-3(f) i {} b b' ~ {})
∧ (concat-lifting-loc-3(f) i b {} b' ~ {})
∧ (concat-lifting-loc-3(f) i b b' {} ~ {}))
Proof
Definitions occuring in Statement :
concat-lifting-loc-3: concat-lifting-loc-3(f),
uall: ∀[x:A]. B[x],
top: Top,
and: P ∧ Q,
apply: f a,
sqequal: s ~ t,
empty-bag: {},
bag: bag(T)
Lemmas :
concat-lifting-3-strict,
bag_wf,
top_wf
Latex:
\mforall{}[f,i:Top]. \mforall{}[b,b':bag(Top)].
((concat-lifting-loc-3(f) i \{\} b b' \msim{} \{\})
\mwedge{} (concat-lifting-loc-3(f) i b \{\} b' \msim{} \{\})
\mwedge{} (concat-lifting-loc-3(f) i b b' \{\} \msim{} \{\}))
Date html generated:
2015_07_22-PM-00_08_17
Last ObjectModification:
2015_01_28-AM-11_42_08
Home
Index