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