Nuprl Definition : vdf-eq
vdf-eq(A;f;L) == dep-all(||L||;i.let a,b,c = L[i] in a = (f firstn(i;L) b) ∈ A)
Definitions occuring in Statement :
dep-all: dep-all(n;i.P[i]),
firstn: firstn(n;as),
select: L[n],
length: ||as||,
spreadn: spread3,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
dep-all: dep-all(n;i.P[i]),
length: ||as||,
spreadn: spread3,
select: L[n],
equal: s = t ∈ T,
apply: f a,
firstn: firstn(n;as)
FDL editor aliases :
vdf-eq
Latex:
vdf-eq(A;f;L) == dep-all(||L||;i.let a,b,c = L[i] in a = (f firstn(i;L) b))
Date html generated:
2020_05_19-PM-09_39_56
Last ObjectModification:
2020_03_04-PM-09_14_08
Theory : co-recursion-2
Home
Index