Nuprl Definition : DCC-order-type

DCC-order-type() ==
  λf,%. let x,x,y = f 0 in 
       y 
       (λn.(primrec(n;λx.x;λm,H,x. (H let x1,x1,v3 = f (m + 1) in let x1,x1,v5 = f m in let x1,v2 = % m in x1 x)) 
            let A,<,v3 = f (n + 1) in 
            let A1,<1,v5 = f n in 
            let f@0,f@0,v1 = % n in 
            f@0)) 
       (λi.if (i + 1) < (1)
              then Ax
              else (letrec f@0(n)=λa1,a2,%13. if (n) < (1)
                                                 then %13
                                                 else (f@0 (n - 1) 
                                                       let A,<,v3 = f ((n - 1) + 1) in 
                                                       let A1,<1,v5 = f (n - 1) in 
                                                       let A,v2 = % (n - 1) 
                                                       in A a1 
                                                       let A,<,v3 = f ((n - 1) + 1) in 
                                                       let A1,<1,v5 = f (n - 1) in 
                                                       let A,v2 = % (n - 1) 
                                                       in A a2 
                                                       let A,<,v3 = f ((n - 1) + 1) in 
                                                       let A1,<1,v5 = f (n - 1) in 
                                                       let f@0,b1,%22,%23 = % (n - 1) 
                                                       in %22 a1 a2 %13  ) in
                     f@0(i) 
                    let A,<,v3 = f (i + 1) in 
                    let A1,<1,v5 = f i in 
                    let A1,v4 = % i 
                    in A1 let A1,<1,v4 = f ((i + 1) + 1) in let f@0,f@0,v1 = % (i + 1) in f@0 
                    let A,<,v3 = f (i + 1) in 
                    let A1,<1,v5 = f i in 
                    let f@0,f@0,v1 = % i in 
                    f@0 
                    let x,<,y1 = f (i + 1) in 
                    let A1,<1,v5 = f i in 
                    let x1,x1,%11,%12 = % i 
                    in %12 let A,<1,v3 = f ((i + 1) + 1) in let f@0,f@0,v1 = % (i + 1) in f@0  ))


Definitions occuring in Statement :  genrec-ap: genrec-ap,  primrec: primrec(n;b;c),  spreadn: spread4,  spreadn: spread3,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  subtract: n - m,  add: n + m,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  spreadn: spread3,  apply: f a,  natural_number: $n,  subtract: n - m,  spreadn: spread4,  add: n + m,  spread: spread def,  less: if (a) < (b)  then c  else d,  lambda: λx.A[x],  genrec-ap: genrec-ap,  axiom: Ax,  primrec: primrec(n;b;c)
FDL editor aliases :  DCC-order-type
Latex:
DCC-order-type()  ==
    \mlambda{}f,\%.  let  x,x,y  =  f  0  in 
              y 
              (\mlambda{}n.(primrec(n;\mlambda{}x.x;\mlambda{}m,H,x.  (H 
                                                                        let  x1,x1,v3  =  f  (m  +  1)  in 
                                                                        let  x1,x1,v5  =  f  m  in 
                                                                        let  x1,v2  =  \%  m 
                                                                        in  x1  x)) 
                        let  A,<,v3  =  f  (n  +  1)  in 
                        let  A1,ə,v5  =  f  n  in 
                        let  f@0,f@0,v1  =  \%  n  in 
                        f@0)) 
              (\mlambda{}i.if  (i  +  1)  <  (1)
                            then  Ax
                            else  (letrec  f@0(n)=\mlambda{}a1,a2,\%13.  if  (n)  <  (1)
                                                                                                  then  \%13
                                                                                                  else  (f@0  (n  -  1) 
                                                                                                              let  A,<,v3  =  f  ((n  -  1)  +  1)  in 
                                                                                                              let  A1,ə,v5  =  f  (n  -  1)  in 
                                                                                                              let  A,v2  =  \%  (n  -  1) 
                                                                                                              in  A  a1 
                                                                                                              let  A,<,v3  =  f  ((n  -  1)  +  1)  in 
                                                                                                              let  A1,ə,v5  =  f  (n  -  1)  in 
                                                                                                              let  A,v2  =  \%  (n  -  1) 
                                                                                                              in  A  a2 
                                                                                                              let  A,<,v3  =  f  ((n  -  1)  +  1)  in 
                                                                                                              let  A1,ə,v5  =  f  (n  -  1)  in 
                                                                                                              let  f@0,b1,\%22,\%23  =  \%  (n  -  1) 
                                                                                                              in  \%22  a1  a2  \%13    )  in
                                          f@0(i) 
                                        let  A,<,v3  =  f  (i  +  1)  in 
                                        let  A1,ə,v5  =  f  i  in 
                                        let  A1,v4  =  \%  i 
                                        in  A1  let  A1,ə,v4  =  f  ((i  +  1)  +  1)  in  let  f@0,f@0,v1  =  \%  (i  +  1)  in  f@0 
                                        let  A,<,v3  =  f  (i  +  1)  in 
                                        let  A1,ə,v5  =  f  i  in 
                                        let  f@0,f@0,v1  =  \%  i  in 
                                        f@0 
                                        let  x,<,y1  =  f  (i  +  1)  in 
                                        let  A1,ə,v5  =  f  i  in 
                                        let  x1,x1,\%11,\%12  =  \%  i 
                                        in  \%12  let  A,ə,v3  =  f  ((i  +  1)  +  1)  in  let  f@0,f@0,v1  =  \%  (i  +  1)  in  f@0    ))


Date html generated: 2018_05_21-PM-07_14_20
Last ObjectModification: 2018_01_11-PM-00_30_17

Theory : general


Home Index