λδ digital library (LDDL)
Constant
Informal description: ""
{λ[p:∀[x:
nat
]
.
Prop]
.
λ[n:
nat
]
.
λ[m:
nat
]
.
λ[mn:{(n)
.
(p)}
.
min
]
.
λ[mm:{(m)
.
(p)}
.
min
]}
.
<{(m)
.
(n)}
.
is
>
.
{({({(mm)
.
(mn)
.
(m)
.
(n)
.
(p)}
.
t45
)
.
(m)
.
(n)}
.
satz10d
)
.
({({(mm)
.
(mn)
.
(m)
.
(n)
.
(p)}
.
t46
)
.
(n)
.
(m)}
.
satz14
)
.
({(m)
.
(n)}
.
is
)
.
({(m)
.
(n)}
.
more
)}
.
ore2
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 23:00:45 +0100