Nuprl Definition : pcw-path-coPath

pcw-path-coPath(n;p) ==
  if (n =z 0)
  then ()
  else let param,w',d = p (n - 1) in 
       case d
        of inl(b) =>
        let pp = pcw-path-coPath(n - 1;p) in
            if (copath-length(pp) =z n - 1) then copath-extend(pp;b) else () fi 
        | inr(x) =>
        ()
  fi 


Definitions occuring in Statement :  copath-nil: (),  copath-length: copath-length(p),  copath-extend: copath-extend(q;t),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  let: let,  spreadn: spread3,  apply: f a,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  copath-nil: (),  copath-extend: copath-extend(q;t),  natural_number: $n,  subtract: n - m,  copath-length: copath-length(p),  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  let: let,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  spreadn: spread3
FDL editor aliases :  pcw-path-coPath
Latex:
pcw-path-coPath(n;p)  ==
    if  (n  =\msubz{}  0)
    then  ()
    else  let  param,w',d  =  p  (n  -  1)  in 
              case  d
                of  inl(b)  =>
                let  pp  =  pcw-path-coPath(n  -  1;p)  in
                        if  (copath-length(pp)  =\msubz{}  n  -  1)  then  copath-extend(pp;b)  else  ()  fi 
                |  inr(x)  =>
                ()
    fi 


Date html generated: 2018_07_25-PM-01_41_33
Last ObjectModification: 2018_07_23-AM-10_08_13

Theory : co-recursion


Home Index