Nuprl Lemma : ws_nil_lemma
∀F:Top. (weighted-sum([];F) ~ 0)
Proof
Definitions occuring in Statement :
weighted-sum: weighted-sum(p;F),
nil: [],
top: Top,
all: ∀x:A. B[x],
natural_number: $n,
sqequal: s ~ t
Lemmas :
length_of_nil_lemma,
stuck-spread,
base_wf
\mforall{}F:Top. (weighted-sum([];F) \msim{} 0)
Date html generated:
2015_07_17-AM-07_58_10
Last ObjectModification:
2015_01_29-PM-06_40_06
Home
Index