λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x0:
rat
]
.
λ[y0:
rat
]
.
λ[x1:
frac
]
.
λ[y1:
frac
]
.
λ[x1ix0:{((x0)
.
class
)
.
(x1)}
.
inf
]
.
λ[y1iy0:{((y0)
.
class
)
.
(y1)}
.
inf
]
.
λ[l:{(y0)
.
(x0)}
.
less
]}
.
<{(y1)
.
(x1)}
.
lessf
>
.
{(y1iy0)
.
(x1ix0)
.
(y1)
.
(x1)
.
(l)
.
(y0)
.
(x0)}
.
also19
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 22:56:16 +0100