λδ digital library (LDDL)
Constant
Informal description: ""
λ[r:real].<{(λ[x:cut].{((x).pofrp).(r)}.is).(cut)}.amone>.λ[x:cut].λ[y:cut].λ[t:{((x).pofrp).(r)}.is].λ[u:{((y).pofrp).(r)}.is].{({(r).(real)}.refis).(u).(t).(y).(x).(r).(r)}.t22 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100