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: 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