λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:complex].λ[y:complex]}.<{(({((y).mod).((x).mod)}.mn).m0).(({(y).(x)}.mn).mod)}.moreis>.{({(x).(y)}.t4).({((x).mod).((y).mod)}.satz181a).({(({(y).(x)}.mn).satz272).({({(y).(x)}.satz219).({(x).(y)}.mn).(({(y).(x)}.mn).m0)}.ismod).((({(y).(x)}.mn).m0).mod).(({(y).(x)}.mn).mod).(({(x).(y)}.mn).mod).(real)}.tris1).(({((y).mod).((x).mod)}.mn).m0).({((x).mod).((y).mod)}.mn).(({(y).(x)}.mn).mod).(({(x).(y)}.mn).mod)}.ismoreis12 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100