Nuprl Definition : stream-lex
stream-lex(T;R) == ∨lex.λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) lex 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,
implies: P ⇒ Q,
and: P ∧ Q,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
bigrel: ∨R.F[R],
lambda: λx.A[x],
and: P ∧ Q,
implies: P ⇒ Q,
equal: s = t ∈ T,
s-hd: s-hd(s),
infix_ap: x f y,
s-tl: s-tl(s)
FDL editor aliases :
stream-lex
Latex:
stream-lex(T;R) ==
\mvee{}lex.\mlambda{}s1,s2. ((s-hd(s1) R s-hd(s2)) \mwedge{} ((s-hd(s1) = s-hd(s2)) {}\mRightarrow{} (s-tl(s1) lex s-tl(s2))))
Date html generated:
2016_05_14-AM-06_23_55
Last ObjectModification:
2015_09_22-PM-05_48_05
Theory : co-recursion
Home
Index