Nuprl Definition : pcw-consistent-paths

pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g) ==
∀n:ℕ. ((¬pcw-final-step(f n)) ⇒ ((f n) = (g n) ∈ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b])))

Definitions occuring in Statement : pcw-final-step: pcw-final-step(s), pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]), nat: ℕ, all: ∀x:A. B[x], not: ¬A, implies: P ⇒ Q, apply: f a, equal: s = t ∈ T
Definitions occuring in definition : all: ∀x:A. B[x], nat: ℕ, implies: P ⇒ Q, not: ¬A, pcw-final-step: pcw-final-step(s), equal: s = t ∈ T, pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]), apply: f a
FDL editor aliases : pcw-consistent-paths

Latex:
pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g) == \mforall{}n:\mBbbN{}. ((\mneg{}pcw-final-step(f n)) {}\mRightarrow{} ((f n) = (g n))) Date html generated: 2016_05_14-AM-06_12_47 Last ObjectModification: 2015_09_22-PM-05_47_04 Theory : co-recursion Home Index