λδ digital library (LDDL)
Constant
Informal description: ""
{λ[r:real].λ[s:real].λ[m:{(s).(r)}.moreis].λ[n:{((s).m0).(r)}.moreis]}.<{((s).abs).(r)}.moreis>.{(λ[t:{(s).((s).abs)}.is].{(m).({(t).(s).((s).abs).(real)}.symis).(r).((s).abs).(s)}.ismoreis2).(λ[t:{((s).m0).((s).abs)}.is].{(n).({(t).((s).m0).((s).abs).(real)}.symis).(r).((s).abs).((s).m0)}.ismoreis2).((s).t6).({((s).abs).(r)}.moreis).({(s).((s).abs)}.is).({((s).m0).((s).abs)}.is)}.orapp Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100