Nuprl Definition : pcw-path-rel
pcw-path-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g) ==
pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g)
∧ (∃n:ℕ. ((∀i:ℕn. (¬pcw-final-step(f i))) ∧ pcw-final-step(f n) ∧ (¬pcw-final-step(g n))))
Definitions occuring in Statement :
pcw-consistent-paths: pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g),
pcw-final-step: pcw-final-step(s),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in 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),
exists: ∃x:A. B[x],
nat: ℕ,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
and: P ∧ Q,
not: ¬A,
pcw-final-step: pcw-final-step(s),
apply: f a
FDL editor aliases :
pcw-path-rel
Latex:
pcw-path-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g) ==
pcw-consistent-paths(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];f;g)
\mwedge{} (\mexists{}n:\mBbbN{}. ((\mforall{}i:\mBbbN{}n. (\mneg{}pcw-final-step(f i))) \mwedge{} pcw-final-step(f n) \mwedge{} (\mneg{}pcw-final-step(g n))))
Date html generated:
2016_05_14-AM-06_12_50
Last ObjectModification:
2015_09_22-PM-05_47_05
Theory : co-recursion
Home
Index