Nuprl Lemma : nim_sum0_lemma
∀y:Top. (nim-sum(0;y) ~ y)
Proof
Definitions occuring in Statement :
nim-sum: nim-sum(x;y),
top: Top,
all: ∀x:A. B[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
nim-sum: nim-sum(x;y)
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
hypothesis,
introduction,
extract_by_obid,
sqequalRule
Latex:
\mforall{}y:Top. (nim-sum(0;y) \msim{} y)
Date html generated:
2018_05_21-PM-09_10_11
Last ObjectModification:
2018_05_19-PM-05_11_57
Theory : general
Home
Index