Nuprl Lemma : ws_single_lemma
∀F,p:Top. (weighted-sum([p];F) ~ 0 + ((F 0) * p))
Proof
Definitions occuring in Statement :
weighted-sum: weighted-sum(p;F),
cons: [a / b],
nil: [],
top: Top,
all: ∀x:A. B[x],
apply: f a,
natural_number: $n,
sqequal: s ~ t,
qmul: r * s,
qadd: r + s
Lemmas :
top_wf,
length_of_cons_lemma,
length_of_nil_lemma
\mforall{}F,p:Top. (weighted-sum([p];F) \msim{} 0 + ((F 0) * p))
Date html generated:
2015_07_17-AM-07_58_12
Last ObjectModification:
2015_01_27-AM-11_24_02
Home
Index