λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:complex].λ[y:complex].λ[n:({((y).mod).((x).mod)}.ts).neg]}.<con>.{(λ[t:{(((y).mod).pos).(((x).mod).neg)}.and].({(t).(((y).mod).pos).(((x).mod).neg)}.ande1).(x).satz264c).(λ[t:{(((y).mod).neg).(((x).mod).pos)}.and].({(t).(((y).mod).neg).(((x).mod).pos)}.ande2).(y).satz264c).({(n).((y).mod).((x).mod)}.satz196h).(con).({(((y).mod).pos).(((x).mod).neg)}.and).({(((y).mod).neg).(((x).mod).pos)}.and)}.orapp Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100