Nuprl Lemma : concat-lifting-loc-2-strict
∀[f:Top]. ∀[b:bag(Top)]. ∀[i:Top]. ((f@Loc i {} b ~ {}) ∧ (f@Loc i b {} ~ {}))
Proof
Definitions occuring in Statement :
concat-lifting-loc-2: f@Loc,
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,
concat-lifting-2: f@,
concat-lifting-loc-2: f@Loc,
concat-lifting2-loc: concat-lifting2-loc(f;abag;bbag;loc),
concat-lifting2: concat-lifting2(f;abag;bbag),
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f)
Latex:
\mforall{}[f:Top]. \mforall{}[b:bag(Top)]. \mforall{}[i:Top]. ((f@Loc i \{\} b \msim{} \{\}) \mwedge{} (f@Loc i b \{\} \msim{} \{\}))
Date html generated:
2016_05_17-AM-09_15_58
Last ObjectModification:
2015_12_29-PM-04_09_11
Theory : classrel!lemmas
Home
Index