Nuprl Lemma : weighted-sum-nil
∀[F:Top]. (weighted-sum([];F) ~ 0)
Proof
Definitions occuring in Statement :
weighted-sum: weighted-sum(p;F),
nil: [],
uall: ∀[x:A]. B[x],
top: Top,
natural_number: $n,
sqequal: s ~ t
Lemmas :
ws_nil_lemma,
top_wf
\mforall{}[F:Top]. (weighted-sum([];F) \msim{} 0)
Date html generated:
2015_07_17-AM-07_58_13
Last ObjectModification:
2015_01_27-AM-11_23_59
Home
Index