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