Nuprl Definition : test-mutual-corec-size

test-mutual-corec-size(i;x) ==
  fix((λf,i,x. if (i =z 0)
              then case x of inl(_) => 0 | inr(p) => let a,L = p in 1 + (f 0 a) + Σ(f 1 L[i] | i < ||L||)
              else case x of inl(_) => 0 | inr(p) => let a,L = p in 1 + (f 1 a) + Σ(f 0 L[i] | i < ||L||)
              fi )) 
  i 
  x


Definitions occuring in Statement :  sum: Σ(f[x] | x < k),  select: L[n],  length: ||as||,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  add: n + m,  sum: Σ(f[x] | x < k),  length: ||as||,  apply: f a,  natural_number: $n,  select: L[n]
FDL editor aliases :  test-mutual-corec-size
Latex:
test-mutual-corec-size(i;x)  ==
    fix((\mlambda{}f,i,x.  if  (i  =\msubz{}  0)
                            then  case  x
                                        of  inl($_{}$)  =>
                                        0
                                        |  inr(p)  =>
                                        let  a,L  =  p 
                                        in  1  +  (f  0  a)  +  \mSigma{}(f  1  L[i]  |  i  <  ||L||)
                            else  case  x
                                        of  inl($_{}$)  =>
                                        0
                                        |  inr(p)  =>
                                        let  a,L  =  p 
                                        in  1  +  (f  1  a)  +  \mSigma{}(f  0  L[i]  |  i  <  ||L||)
                            fi  )) 
    i 
    x


Date html generated: 2018_05_21-PM-00_31_49
Last ObjectModification: 2017_10_18-PM-05_12_53

Theory : int_2


Home Index