λδ digital library (LDDL)
Constant
Informal description: ""
{λ[sigma:Set]
.
λ[r:∀[x:sigma]
.
∀[y:sigma]
.
Prop]
.
λ[refr1:∀[x:sigma]
.
(x)
.
(x)
.
r]
.
λ[symr1:∀[x:sigma]
.
∀[y:sigma]
.
∀[t:(y)
.
(x)
.
r]
.
(x)
.
(y)
.
r]
.
λ[trr1:∀[x:sigma]
.
∀[y:sigma]
.
∀[z:sigma]
.
∀[t:(y)
.
(x)
.
r]
.
∀[u:(z)
.
(y)
.
r]
.
(z)
.
(x)
.
r]
.
λ[s:sigma]
.
λ[t:sigma]
.
λ[tsr:(t)
.
(s)
.
r]}
.
<{({(t)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
({(s)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
((sigma)
.
set
)}
.
is
>
.
{(λ[x:sigma]
.
λ[y:{({(t)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
(x)
.
(sigma)}
.
esti
]
.
{(y)
.
(x)
.
({(tsr)
.
(t)
.
(s)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
symr
)
.
(s)
.
(t)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
t1
)
.
(λ[x:sigma]
.
λ[y:{({(s)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
(x)
.
(sigma)}
.
esti
]
.
{(y)
.
(x)
.
(tsr)
.
(t)
.
(s)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
t1
)
.
({(t)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
({(s)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecelt
)
.
(sigma)}
.
isseti
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 21:59:53 +0100