λδ digital library (LDDL)
Constant
Informal description: ""
λ[x:nat].<((x).pdofnt).natd>.{(λ[t:((x).pdofnt).posd].{(t).(x)}.t32).((x).t28).(∀[t:((x).pdofnt).posd].({(t).((x).pdofnt)}.rpofpd).natrp).(((x).pdofnt).posd)}.andi Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100