Warning: this is an htmlized version! The original is across this link, and the conversion rules are here.
```-- Why is the pentagon DAG a non-distributive lattice?
-- Eduard Ochs, 2011mar08
-- (find-books "__alg/__alg.el" "gratzer")
-- (find-gratzerpage (+ 31 109) "II. Distributive Lattices")
-- (find-LATEX "2011ebl-abs.tex" "FHAs")

--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
--]]

Elts = split "T L+ R L- bt"
And = {}
Or = {}
feed = function (Op, P, results)
Op[P] = {}
for i,Q in ipairs(Elts) do
Op[P][Q] = split(results)[i]
end
end

-- (fooi "aa" "T " "bb" "L+" "cc" "R " "dd" "L-" "ee" "bt")
--   T
-- L+
--     R
-- L-
--   bt

--          * |  T  L+ R  L- bt
----+-----------------
feed(And, "T" , "T  L+ R  L- bt")
feed(And, "L+", "L+ L+ bt L- bt")
feed(And, "R" , "R  bt R  bt bt")
feed(And, "L-", "L- L- bt L- bt")
feed(And, "bt", "bt bt bt bt bt")

--         v |  T  L+ R  L- bt
----+-----------------
feed(Or, "T" , "T  T  T  T  T ")
feed(Or, "L+", "T  L+ T  L+ L+")
feed(Or, "R" , "T  T  R  T  R ")
feed(Or, "L-", "T  L+ T  L- L-")
feed(Or, "bt", "T  L+ R  L- bt")

PP(And)
PP(Or)

testcomm = function (op)
local Op = _G[op]
for _,P in ipairs(Elts) do
for _,Q in ipairs(Elts) do
if Op[P][Q] ~= Op[Q][P] then print("not comm", op, P, Q) end
end
end
end
testassoc = function (op)
local Op = _G[op]
for _,P in ipairs(Elts) do
for _,Q in ipairs(Elts) do
for _,R in ipairs(Elts) do
if Op[Op[P][Q]][R] ~= Op[P][Op[Q][R]] then
print("not assoc", op, P, Q, R)
end
end
end
end
end
testdistr = function (times, plus)
local Times, Plus = _G[times], _G[plus]
local pl = function (P, Q) return P.." "..plus.." "..Q end
local ti = function (P, Q) return P.." "..times.." "..Q end
local ppl = function (P, Q) return "("..pl(P, Q)..")" end
local pti = function (P, Q) return "("..ti(P, Q)..")" end
for _,P in ipairs(Elts) do
for _,Q in ipairs(Elts) do
for _,R in ipairs(Elts) do
if Times[Plus[P][Q]][R] ~= Plus[Times[P][R]][Times[Q][R]] then
-- print("not distr", times, plus, P, Q, R)
print(ti(ppl(P, Q), R).." ~= "..pl(pti(P, R), pti(Q, R)))
end
end
end
end
end

testcomm("And")
testcomm("Or")
testassoc("And")
testassoc("Or")
testdistr("And", "Or")
testdistr("Or", "And")

--[[

T         (R v L-) & L+  ==  (R & L+) v (L- & L+)
L+   \	       \----/             \----/     \-----/
|     R        T                  B           L-
L-   /	      \-----------/       \----------------/
B	              L+                  L-
\------------------------------------/
0

(R & L+) v L-  ==  (R v L-) & (L+ v L-)
\----/             \----/     \-----/
B                  T          L+
\-----------/      \------------------/
L-                  L+
\-------------------------------------/
0

.
.   .
.   .   .
.   v   .   .
.   P   Q   R   .
.   .   &   .
.   &   .
.   .
.               (P&Q)vR<->(P&R)v(Q&R)

--]]

--[[
%*
% (eedn4a-bounded)
% (find-sh0 "cd ~/LATEX/ && dvips  -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-sh0 "cd ~/LATEX/ && dvired -D 600 -P pk -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

\$L^+ = §∧L^+ = (R∨L^-)∧L^+ \neq (R∧L^+)∨(L^-∧L^+) = ®∨L^- = L^-\$

%:*&*\land *
%:*v*\lor *

This proof presents no problems:
%:
%:  ------  ------
%:  P&Q|-P  P|-PvQ
%:  -------------   --------  ------  ------
%:     P&Q|-PvQ     Q&R|-PvQ  P&R|-R  Q&R|-R
%:     ---------------------  --------------
%:      (P&R)v(Q&R)|-PvQ      (P&R)v(Q&R)|-R
%:      ------------------------------------
%:            (P&R)v(Q&R)|-(PvQ)&R
%:
%:            ^distr-ok
%:
\$\$\ded{distr-ok}\$\$

%:            P&((PvQ)&R)|-P  P&((PvQ)&R)|-R  Q&((PvQ)&R)|-Q  Q&((PvQ)&R)|-R
%:            ------------------------------  ------------------------------
%:                   P&((PvQ)&R)|-P&R            Q&((PvQ)&R)|-Q&R
%:                  -------------------         ------------------
%:                  P|-((PvQ)&R)->(P&R)         Q|-((PvQ)&R)->(Q&R)
%:                  -----------------------------------------------
%:  (PvQ)&R|-PvQ                  PvQ|-((PvQ)&R)->(P&R)
%:  =======================    ------------------------
%:  (PvQ)&R|-(PvQ)&((PvQ)&R)    (PvQ)&((PvQ)&R)|-P&RvQ&R
%:  -----------------------------------------------
%:            (PvQ)&R|-P&RvQ&R
%:
%:            ^distr-ok-hard
%:
\$\$\ded{distr-ok-hard}\$\$

This one, which seems to require `\$⊃\$', fails in some way:
%:
%:              (PvQ)&R       (PvQ)&R
%:              ------        -------
%:        [P]^1   R     [Q]^1   R
%:        ---------     ---------
%:              P&R       Q&R
%:            -------  -------
%:  (PvQ)&R   P&RvQ&R  P&RvQ&R
%:  -------   ---------------
%:    PvQ      P&RvQ&R
%:    ----------------1
%:          P&RvQ&R
%:
%:          ^distr-weird-1
%:
%:
%:  P,(PvQ)&R|-P  P,(PvQ)&R|-R  Q,(PvQ)&R|-Q  Q,(PvQ)&R|-R
%:  --------------------------  --------------------------
%:      P,(PvQ)&R|-P&R              Q,(PvQ)&R|-Q&R
%:    ==================          ==================
%:    P,(PvQ)&R|-P&RvQ&R          Q,(PvQ)&R|-P&RvQ&R
%:    ----------------------      ------------------
%:    P|-((PvQ)&R)⊃(P&RvQ&R)      Q|-((PvQ)&R)⊃(P&RvQ&R)
%:    --------------------------------------------------
%:             PvQ|-((PvQ)&R)⊃(P&RvQ&R)
%:            ==========================
%:            PvQ&R|-((PvQ)&R)⊃(P&RvQ&R)
%:
%:            ^distr-weird-2
%:
\$\$\ded{distr-weird-1}\$\$
\$\$\ded{distr-weird-2}\$\$

%*
--]]

-- Local Variables:
-- coding:  raw-text-unix
-- modes:   (fundamental-mode lua-mode latex-mode)
-- End:
```