Nuprl Definition : stream-pointwise
stream-pointwise(R) == ∨ptwse.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ (s-tl(s1) ptwse s-tl(s2)))
Definitions occuring in Statement :
s-tl: s-tl(s),
s-hd: s-hd(s),
bigrel: ∨R.F[R],
infix_ap: x f y,
and: P ∧ Q,
lambda: λx.A[x]
Definitions occuring in definition :
bigrel: ∨R.F[R],
lambda: λx.A[x],
and: P ∧ Q,
s-hd: s-hd(s),
infix_ap: x f y,
s-tl: s-tl(s)
FDL editor aliases :
stream-pointwise
Latex:
stream-pointwise(R) == \mvee{}ptwse.\mlambda{}s1,s2. ((s-hd(s1) R s-hd(s2)) \mwedge{} (s-tl(s1) ptwse s-tl(s2)))
Date html generated:
2016_05_14-AM-06_24_27
Last ObjectModification:
2015_09_22-PM-05_48_07
Theory : co-recursion
Home
Index