λδ digital library (LDDL)
Constant
Informal description: ""
{λ[a1:cut].λ[a2:cut].λ[b1:cut].λ[b2:cut]}.<{({({(b1).(a2)}.pl).({(b2).(a1)}.pl)}.df).({({(b2).(b1)}.df).({(a2).(a1)}.df)}.md)}.eq>.{({(b1).(b2).(a2).(a1)}.pdeq12a).({({(b2).(b1)}.m0deqa).({(a2).(a1)}.df).({(b1).(b2)}.df).(({(b2).(b1)}.df).m0d)}.eqpd2).({({(b1).(a2)}.pl).({(b2).(a1)}.pl)}.df).({({(b1).(b2)}.df).({(a2).(a1)}.df)}.pd).({({(b2).(b1)}.df).({(a2).(a1)}.df)}.md)}.treq Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100