Nuprl Definition : pcw-pp

PartialPath ==
  {nss:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]))|
   let n,ss = nss
   in ∀i:ℕn - 1. StepRel(ss i;ss (i + 1))}

Definitions occuring in Statement : pcw-steprel: StepRel(s1;s2), pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]), int_seg: {i..j^-}, nat: ℕ, all: ∀x:A. B[x], set: {x:A| B[x]} , apply: f a, function: x:A ⟶ B[x], spread: spread def, product: x:A × B[x], subtract: n - m, add: n + m, natural_number: $n
Definitions occuring in definition : set: {x:A| B[x]} , product: x:A × B[x], nat: ℕ, function: x:A ⟶ B[x], pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]), spread: spread def, all: ∀x:A. B[x], int_seg: {i..j^-}, subtract: n - m, pcw-steprel: StepRel(s1;s2), apply: f a, add: n + m, natural_number: $n
FDL editor aliases : pcw-pp

Latex:
PartialPath == \{nss:n:\mBbbN{} \mtimes{} (\mBbbN{}n {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]))| let n,ss = nss in \mforall{}i:\mBbbN{}n - 1. StepRel(ss i;ss (i + 1))\} Date html generated: 2016_05_14-AM-06_12_54 Last ObjectModification: 2015_09_22-PM-05_47_06 Theory : co-recursion Home Index