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)
Lemmas :
concat-lifting-2-strict,
top_wf,
bag_wf
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:
2015_07_22-PM-00_08_15
Last ObjectModification:
2015_01_28-AM-11_41_48
Home
Index