λδ digital library (LDDL)
Constant
Informal description: ""
{λ[r:real].λ[s:real].λ[n:((r).neg).not].λ[o:((s).neg).not].λ[i:{(s).(r)}.is]}.<{({(o).(s)}.sqrt).({(n).(r)}.sqrt)}.is>.{({(i).({(n).(r)}.thsqrt1b).(s).(r).({({(n).(r)}.sqrt).({(n).(r)}.sqrt)}.ts).(real)}.tris).({(n).(r)}.thsqrt1a).({(n).(r)}.sqrt).(o).(s)}.thsqrt2 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100