Nuprl Lemma : term_size_var_lemma
∀v:Top. (term-size(varterm(v)) ~ 1)
Proof
Definitions occuring in Statement :
term-size: term-size(t),
varterm: varterm(v),
top: Top,
all: ∀x:A. B[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
term-size: term-size(t),
coterm-size: coterm-size(t),
varterm: varterm(v)
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
introduction,
extract_by_obid
Latex:
\mforall{}v:Top. (term-size(varterm(v)) \msim{} 1)
Date html generated:
2020_05_19-PM-09_53_47
Last ObjectModification:
2020_03_12-AM-10_53_25
Theory : terms
Home
Index