Nuprl Definition : bfs-equiv
bfs-equiv(K;S;fs1;fs2) == least-equiv(basic-formal-sum(K;S);λas,bs. bfs-reduce(K;S;as;bs)) fs1 fs2
Definitions occuring in Statement :
bfs-reduce: bfs-reduce(K;S;as;bs),
basic-formal-sum: basic-formal-sum(K;S),
least-equiv: least-equiv(A;R),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
apply: f a,
least-equiv: least-equiv(A;R),
basic-formal-sum: basic-formal-sum(K;S),
lambda: λx.A[x],
bfs-reduce: bfs-reduce(K;S;as;bs)
FDL editor aliases :
bfs-equiv
Latex:
bfs-equiv(K;S;fs1;fs2) == least-equiv(basic-formal-sum(K;S);\mlambda{}as,bs. bfs-reduce(K;S;as;bs)) fs1 fs2
Date html generated:
2018_05_22-PM-09_45_00
Last ObjectModification:
2018_01_08-PM-03_31_24
Theory : linear!algebra
Home
Index