λδ digital library (LDDL)
Constant
Informal description: ""
{λ[a1:cut].λ[a2:cut].λ[r:cut]}.<{({({(r).(a2)}.pl).({(r).(a1)}.pl)}.df).({(a2).(a1)}.df)}.eq>.{({({(a2).(r).(a1)}.asspl2).({({(r).(a2)}.compl).(a1).({(a2).(r)}.pl).({(r).(a2)}.pl)}.ispl2).({(a2).({(r).(a1)}.pl)}.pl).({({(a2).(r)}.pl).(a1)}.pl).({({(r).(a2)}.pl).(a1)}.pl).(cut)}.tris).({(r).(a2)}.pl).({(r).(a1)}.pl).(a2).(a1)}.eqi12 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100