λδ digital library (LDDL)
Constant
Informal description: ""
{λ[p:cut].λ[q:cut].λ[r:cut].λ[s:cut]}.<{({({(s).(q)}.pl).({(r).(p)}.pl)}.pl).({({(s).(r)}.pl).({(q).(p)}.pl)}.pl)}.is>.{({({(s).(q)}.pl).(r).(p)}.asspl2).({({(s).(r).(q)}.3pl12).(p).({({(s).(q)}.pl).(r)}.pl).({({(s).(r)}.pl).(q)}.pl)}.ispl2).({({(s).(r)}.pl).(q).(p)}.asspl1).({({(s).(q)}.pl).({(r).(p)}.pl)}.pl).({({({(s).(q)}.pl).(r)}.pl).(p)}.pl).({({({(s).(r)}.pl).(q)}.pl).(p)}.pl).({({(s).(r)}.pl).({(q).(p)}.pl)}.pl).(cut)}.tr3is Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100