Nuprl Definition : pcw-pp-barred
A partial path ⌜<n, ss>⌝ is barred if it is non-empty and the last step
has "decision" d = inr ⋅ .
This means that the path does not continue with a decision d = inl b
that picks a member of the domain of ⌜snd(w)⌝.⋅
Barred(pp) == let n,ss = pp in 0 < n ∧ let p,w,d = ss (n - 1) in ↑isr(d)
Definitions occuring in Statement :
assert: ↑b,
isr: isr(x),
less_than: a < b,
spreadn: spread3,
and: P ∧ Q,
apply: f a,
spread: spread def,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
spread: spread def,
and: P ∧ Q,
less_than: a < b,
spreadn: spread3,
apply: f a,
subtract: n - m,
natural_number: $n,
assert: ↑b,
isr: isr(x)
FDL editor aliases :
pcw-pp-barred
Latex:
Barred(pp) == let n,ss = pp in 0 < n \mwedge{} let p,w,d = ss (n - 1) in \muparrow{}isr(d)
Date html generated:
2016_07_08-PM-04_47_44
Last ObjectModification:
2015_09_22-PM-05_47_09
Theory : co-recursion
Home
Index