Nuprl Lemma : single-bag-not-null
∀T:Type. ∀x:T. (↑bag-null({x}) ~ False)
Proof
Definitions occuring in Statement :
assert: ↑b,
all: ∀x:A. B[x],
false: False,
universe: Type,
sqequal: s ~ t,
bag-null: bag-null(bs),
single-bag: {x}
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
single-bag: {x},
bag-size: #(bs),
top: Top,
eq_int: (i =z j),
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff
Latex:
\mforall{}T:Type. \mforall{}x:T. (\muparrow{}bag-null(\{x\}) \msim{} False)
Date html generated:
2016_05_17-AM-11_09_43
Last ObjectModification:
2015_12_29-PM-05_16_08
Theory : process-model
Home
Index