Nuprl Lemma : term_size_mkterm_lemma
∀bts,opr:Top. (term-size(mkterm(opr;bts)) ~ 1 + Σ(term-size(snd(bt)) | bt ∈ bts))
Proof
Definitions occuring in Statement :
term-size: term-size(t),
mkterm: mkterm(opr;bts),
lsum: Σ(f[x] | x ∈ L),
top: Top,
pi2: snd(t),
all: ∀x:A. B[x],
add: n + m,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
term-size: term-size(t),
mkterm: mkterm(opr;bts),
coterm-size: coterm-size(t),
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}bts,opr:Top. (term-size(mkterm(opr;bts)) \msim{} 1 + \mSigma{}(term-size(snd(bt)) | bt \mmember{} bts))
Date html generated:
2020_05_19-PM-09_53_48
Last ObjectModification:
2020_03_09-PM-04_08_21
Theory : terms
Home
Index