Nuprl Lemma : fun_exp_add_sq_again
∀[n,m:ℕ]. ∀[f,i:Top]. (f^n + m i ~ f^n (f^m i))
Proof
Definitions occuring in Statement :
fun_exp: f^n,
nat: ℕ,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
add: n + m,
sqequal: s ~ t
Lemmas referenced :
fun_exp_add_sq
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}[n,m:\mBbbN{}]. \mforall{}[f,i:Top]. (f\^{}n + m i \msim{} f\^{}n (f\^{}m i))
Date html generated:
2016_05_15-PM-03_54_21
Last ObjectModification:
2015_12_27-PM-01_24_20
Theory : general
Home
Index