Nuprl Lemma : unroll-pcorec-size
∀[a:Top]. (pcorec-size(lbl,p.a[lbl;p]) ~ λp,x. let lbl,z = x in 1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);a[lbl;p];z))
Proof
Definitions occuring in Statement :
pcorec-size: pcorec-size(lbl,p.a[lbl; p]),
add-sz: add-sz(sz;L;x),
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
lambda: λx.A[x],
spread: spread def,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
pcorec-size: pcorec-size(lbl,p.a[lbl; p])
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}[a:Top]
(pcorec-size(lbl,p.a[lbl;p]) \msim{} \mlambda{}p,x. let lbl,z = x
in 1 + add-sz(pcorec-size(lbl,p.a[lbl;p]);a[lbl;p];z))
Date html generated:
2019_06_20-PM-02_04_18
Last ObjectModification:
2019_02_22-PM-03_33_17
Theory : tuples
Home
Index