Nuprl Definition : list-closed-test
list-closed-test(f;d;L) ==
isl(l-all-decider() L
(λx.(l-all-decider() (f x)
(λz.letrec list_ind(L)=eval v = L in
if v is a pair then let a,L = v
in case list_ind L
of inl(%2) =>
if d z a
then inl <0, Ax, Ax>
else inl let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
fi
| inr(%2) =>
if d z a then inl <0, Ax, Ax> else inr (λ%.Ax) fi
otherwise if v = Ax then inr (λ%.Ax) otherwise fix((λx.x)) in
list_ind(L)))))
Definitions occuring in Statement :
l-all-decider: l-all-decider(),
genrec-ap: genrec-ap,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
isl: isl(x),
spreadn: spread3,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
add: n + m,
natural_number: $n,
axiom: Ax
Definitions occuring in definition :
lambda: λx.A[x],
fix: fix(F),
axiom: Ax,
inr: inr x ,
isaxiom: if z = Ax then a otherwise b,
pair: <a, b>,
natural_number: $n,
inl: inl x,
apply: f a,
ifthenelse: if b then t else f fi ,
add: n + m,
spreadn: spread3,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spread: spread def,
ispair: if z is a pair then a otherwise b,
callbyvalue: callbyvalue,
genrec-ap: genrec-ap,
l-all-decider: l-all-decider(),
isl: isl(x)
FDL editor aliases :
list-closed-test
Latex:
list-closed-test(f;d;L) ==
isl(l-all-decider() L
(\mlambda{}x.(l-all-decider() (f x)
(\mlambda{}z.letrec list$_{ind}$(L)=eval v = L in
if v is a pair then let a,L = v
in case list$_{ind}$ L
of inl(\%2) =>
if d z a
then inl ɘ, Ax, Ax>
else inl let i,\%4,\%5 = \%2 in
<i + 1, Ax, Ax>
fi
| inr(\%2) =>
if d z a
then inl ɘ, Ax, Ax>
else inr (\mlambda{}\%.Ax)
fi otherwise if v = Ax then inr (\mlambda{}\%.Ax)
otherwise fix((\mlambda{}x.x)) in
list$_{ind}$(L)))))
Date html generated:
2019_06_20-PM-01_51_33
Last ObjectModification:
2019_06_19-PM-04_33_58
Theory : list_1
Home
Index