---

run-lt-transitive-witness() ==
  a,b,c,%,%1.
   let n,%2 = %1 
   in let n1,%3 = % 
      in <n1 + n
         , letrec f(x)=n,%1,%2.
                        if x=0
                           then %2
                           else if x + n=0
                                   then 
                                   else let z1,%16 = %1 
                                        in <z1
                                           , let %17,%18 = %16 
                                             in <%17, f (x - 1) n %18 %2>
                                           > in
            f  
           n1 
           n 
           a 
           b 
           c 
           %3 
           %2
         >

---

Definitions occuring in Statement :  genrec: genrec,  it: ,  int_eq: if a=b  then c  else d,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions :  genrec: genrec,  lambda: x.A[x],  int_eq: if a=b  then c  else d,  add: n + m,  it: ,  spread: spread def,  pair: <a, b>,  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  run-lt-transitive-witness

---

run-lt-transitive-witness()  ==
    \mlambda{}a,b,c,\%,\%1.
      let  n,\%2  =  \%1 
      in  let  n1,\%3  =  \% 
            in  <n1  +  n
                  ,  letrec  f(x)=\mlambda{}n,\%1,\%2.
                                                if  x=0
                                                      then  \%2
                                                      else  if  x  +  n=0
                                                                      then  \mcdot{}
                                                                      else  let  z1,\%16  =  \%1 
                                                                                in  <z1,  let  \%17,\%18  =  \%16  in  <\%17,  f  (x  -  1)  n  \%18  \%2>>  in
                        f   
                      n1 
                      n 
                      a 
                      b 
                      c 
                      \%3 
                      \%2
                  >


Date html generated: 2011_08_17-PM-03_38_54
Last ObjectModification: 2010_12_22-AM-11_40_56

Home Index