Nuprl Definition : pcorec-size
pcorec-size(lbl,p.a[lbl; p]) == fix((λsz,p,x. let lbl,z = x in 1 + add-sz(sz;a[lbl; p];z)))
Definitions occuring in Statement :
add-sz: add-sz(sz;L;x),
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
add: n + m,
natural_number: $n,
add-sz: add-sz(sz;L;x)
Latex:
pcorec-size(lbl,p.a[lbl; p]) == fix((\mlambda{}sz,p,x. let lbl,z = x in 1 + add-sz(sz;a[lbl; p];z)))
Date html generated:
2019_06_20-PM-02_04_15
Last ObjectModification:
2019_02_22-PM-03_31_37
Theory : tuples
Home
Index