-- 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")
-- (find-angg "LATEX/2017distributivity.tex")

--[[
* (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")

--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "distributivity.lua"

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: