λδ digital library (LDDL)
Constant
Informal description: ""
{λ[t:real].λ[n:((t).neg).not].λ[c0:dif].λ[cit:{((t).class).(c0)}.inn].λ[a0:dif].λ[a:{({(c0).({(a0).(a0)}.td)}.eq).(((a0).negd).not)}.and]}.<(λ[u:real].{({(t).({(u).(u)}.ts)}.is).(((u).neg).not)}.and).some>.{({(a).(a0).(cit).(c0).(n).(t)}.t9).({(a).(a0).(cit).(c0).(n).(t)}.ar).(λ[u:real].{({(t).({(u).(u)}.ts)}.is).(((u).neg).not)}.and).(real)}.somei Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100