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)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
and: P ∧ Q,
cand: A c∧ B,
top: Top,
all: ∀x:A. B[x],
concat-lifting-3: concat-lifting-3(f),
concat-lifting-loc-3: concat-lifting-loc-3(f),
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f)
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:
2016_05_17-AM-09_16_04
Last ObjectModification:
2015_12_29-PM-04_09_22
Theory : classrel!lemmas
Home
Index