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