λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:nat].λ[y:nat]}.<{(({(y).(x)}.pl).suc).({(y).((x).suc)}.pl)}.is>.{(y).((x).t29).(λ[z:nat].((z).(x).plus).suc).(((x).suc).plus).(nat).(nat)}.fise Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100