λδ digital library (LDDL)
Constant
Informal description: ""
λ[x:complex].<(((x).mod2).neg).not>.{(λ[t:{(0c).(x)}.nis].{({(t).(x)}.lemma4).((x).mod2)}.pnotn).(λ[t:{(0c).(x)}.is].{({(t).(x)}.lemma3).((x).mod2)}.0notn).((((x).mod2).neg).not).({(0c).(x)}.is)}.th1 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100