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