% (find-LATEX "2022agda-logic-1.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2022agda-logic-1.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2022agda-logic-1.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2022agda-logic-1.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2022agda-logic-1.pdf"))
% (defun e () (interactive) (find-LATEX "2022agda-logic-1.tex"))
% (defun u () (interactive) (find-latex-upload-links "2022agda-logic-1"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022agda-logic-1.pdf"))
%          (code-eec-LATEX "2022agda-logic-1")
% (find-pdf-page   "~/LATEX/2022agda-logic-1.pdf")
% (find-sh0 "cp -v  ~/LATEX/2022agda-logic-1.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2022agda-logic-1.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2022agda-logic-1.pdf
%               file:///tmp/2022agda-logic-1.pdf
%           file:///tmp/pen/2022agda-logic-1.pdf
% http://angg.twu.net/LATEX/2022agda-logic-1.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2022agda-logic-1")

% «.co»			(to "co")
% «.simple»		(to "simple")
% «.distributivity1»	(to "distributivity1")

\documentclass[oneside,10pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
%\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
% (find-es "tex" "geometry")
\usepackage[%a5paper,
            paperheight=18.5cm, paperwidth=15cm,
            bottom=1cm, includefoot,
            left=1cm, right=1cm]{geometry}
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% «co»  (to ".co")
% (find-LATEX "2019emacsconf.tex" "co")
\def\cocolor{}
\def\cocolor{\color{DarkGreen!80!black}}
\def\co#1{{%
  \cocolor%
  \def\%{\char37}%
  \def\\{\char92}%
  \def\^{\char94}%
  \def\~{\char126}%
  \tt#1%
  }}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\pco#1{\par\co{#1}}


% «simple»  (to ".simple")
% (al1p 1 "simple")
% (al1a   "simple")

\co{simple1} and 

\co{simple2}:

\msk

%:
%:        P∧Q
%:        ---
%:  P∧Q    Q    Q→R  
%:  ---    --------
%:   P        R
%:   ----------
%:     P∧R
%:
%:     ^simple-1
%:
\pu
$$\cded{simple-1}
  \quad
  \begin{array}[c]{rcl}
      \angg{P} &:=& π \angg{P∧Q} \\
      \angg{Q} &:=& π' \angg{P∧Q} \\
      \angg{R} &:=& \angg{Q→R} \angg{Q} \\
    \angg{P∧R} &:=& (\angg{P},\angg{R}) \\
  \end{array}
$$

%:
%:           [P∧Q]^1
%:           -------
%:  [P∧Q]^1     Q     Q→R  
%:  -------     ---------
%:     P            R
%:     --------------
%:          P∧R
%:        -------1
%:        P∧Q→P∧R
%:
%:        ^simple-2
%:
\pu
$$\cded{simple-2}
  \quad
  \begin{array}[c]{rcl}
      \angg{P} &:=& π \angg{P∧Q} \\
      \angg{Q} &:=& π' \angg{P∧Q} \\
      \angg{R} &:=& \angg{Q→R} \angg{Q} \\
    \angg{P∧R} &:=& (\angg{P},\angg{R}) \\
    \angg{P∧Q→P∧R} &:=& λ\angg{P∧Q}.\angg{P∧R} \\
  \end{array}
$$


\newpage

% «distributivity1»  (to ".distributivity1")
% (al1p 2 "distributivity1")
% (al1a   "distributivity1")
% (disp 1 "simple")
% (disa   "simple")
% (find-angg "AGDA/Logic1.agda" "distrib-1")

% This proof presents no problems:
%
% (It uses ``ND with a single hypothesis'')

\co{distributivity1}:

%:
%:  
%:             [P∧R]^1           [Q∧R]^1
%:             -------           -------
%:                P     [P∧R]^1     Q       [Q∧R]^1
%:               ---    -------    ----     ----
%:               P∨Q       R       P∨Q       R
%:               -----------       -----------
%:  (P∧R)∨(Q∧R)    (P∨Q)∧R           (P∨Q)∧R
%:  ----------------------------------------
%:            (P∨Q)∧R
%:  
%:            ^distr-ok-dn
%:  
%:             [P∧R]^1  [Q∧R]^1       
%:             -------  -------       
%:                P        Q                 [P∧R]^1  [Q∧R]^1        
%:               ---      ----               -------  -------                 
%:  (P∧R)∨(Q∧R)  P∨Q      P∨Q    (P∧R)∨(Q∧R)     R       R
%:  --------------------------   -------------------------
%:            (P∨Q)                         R
%:            -------------------------------
%:                     (P∨Q)∧R
%:  
%:                     ^distr-ok-dn2
%:
%:  
\pu
$$\ded{distr-ok-dn}$$

\newpage


$$\ded{distr-ok-dn2}$$



This one, which seems to require `$→$', fails in some way:
%:  
%:              (P∨Q)∧R       (P∨Q)∧R
%:              ------        -------
%:        [P]^1   R     [Q]^1   R
%:        ---------     ---------
%:              P∧R           Q∧R
%:            ------------   -----------
%:  (P∨Q)∧R   (P∧R)∨(Q∧R)  (P∧R)∨(Q∧R)
%:  -------   --------------------------
%:    P∨Q      (P∧R)∨(Q∧R)
%:    ----------------1
%:          (P∧R)∨(Q∧R)
%:  
%:          ^distr-weird-1
%:  
$$\pu
  \ded{distr-weird-1}
$$





\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2022agda-logic-1 veryclean
make -f 2019.mk STEM=2022agda-logic-1 pdf

% Local Variables:
% coding: utf-8-unix
% ee-tla: "al1"
% End: