λδ digital library (LDDL)
Constant
Informal description: ""
{λ[p:cut].λ[q:cut].λ[r:cut].λ[s:cut]}.<{({({(q).(r)}.pl).({(s).(p)}.pl)}.pl).({({(s).(r)}.pl).({(q).(p)}.pl)}.pl)}.is>.{({({(q).(r)}.pl).(s).(p)}.asspl2).({({(s).(r).(q)}.3pl13).(p).({({(q).(r)}.pl).(s)}.pl).({({(s).(r)}.pl).(q)}.pl)}.ispl2).({({(s).(r)}.pl).(q).(p)}.asspl1).({({(q).(r)}.pl).({(s).(p)}.pl)}.pl).({({({(q).(r)}.pl).(s)}.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