% This file: (find-LATEX "2019J-ops-midway.tex")
%       See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-midway.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-midway.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-midway.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-midway"))
% (find-pdf-page   "~/LATEX/2019J-ops-midway.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-midway.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-midway.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019J-ops-midway.pdf
%               file:///tmp/2019J-ops-midway.pdf
%           file:///tmp/pen/2019J-ops-midway.pdf
% http://angg.twu.net/LATEX/2019J-ops-midway.pdf
% (find-LATEX "2019.mk")

% «.cuts-stopping-midway»		(to "cuts-stopping-midway")
% «.no-Y-cuts-no-L-cuts»		(to "no-Y-cuts-no-L-cuts")

\directlua{tf_push("2019J-ops-midway.tex")}



%   ____      _             _                    _             
%  / ___|   _| |_ ___   ___| |_ ___  _ __  _ __ (_)_ __   __ _ 
% | |  | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
%  \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
%                                   |_|   |_|            |___/ 
%
% «cuts-stopping-midway»  (to ".cuts-stopping-midway")
% (jonp 11 "cuts-stopping-midway")
% (jom     "cuts-stopping-midway")
% (p2lp 3 "cuts-stopping-midway")
% (p2l    "cuts-stopping-midway")
\section{Cuts stopping midway}
\label{cuts-stopping-midway}

Look at the figure below, that shows a partition of a ZHA $A=[00,66]$
into five regions, each region being an interval; this partition does
not come from a slashing, as it has cuts that stop midway. Define an
operation `$·^*$' on $A$, that works by taking each truth-value $P$ in
it to the top element of its region; for example, $30^*=61$.
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234567654321")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
  \foo
$$
%
It is easy to see that `$·^*$' obeys $\J1$ and $\J2$; however, it does
{\sl not} obey $\J3$ --- we will prove that in
sec.\ref{no-Y-cuts-no-L-cuts}. As we will see, {\sl the partitions of
a ZHA into intervals that obey $\J1$, $\J2$, $\J3$ ae exactly the
slashings;} or, in other words, {\sl every J-operator comes from a
slashing}.



%  _   _        __   __             _       
% | \ | | ___   \ \ / /   ___ _   _| |_ ___ 
% |  \| |/ _ \   \ V /   / __| | | | __/ __|
% | |\  | (_) |   | |   | (__| |_| | |_\__ \
% |_| \_|\___/    |_|    \___|\__,_|\__|___/
%                                           
% «no-Y-cuts-no-L-cuts» (to ".no-Y-cuts-no-L-cuts")
% (jonp 11 "no-Y-cuts-no-L-cuts")
% (jom     "no-Y-cuts-no-L-cuts")
% (p2lp 4 "no-Y-cuts-no-L-cuts")
% (p2l    "no-Y-cuts-no-L-cuts")
\subsection{The are no Y-cuts and no $\lambda$-cuts}
\label  {no-Y-cuts-no-L-cuts}
% Good (ph2p 12 "no-Y-cuts-no-L-cuts")

We want to see that if a partition of a ZHA $H$ into intervals has
``Y-cuts'' or ``$λ$-cuts'', like these parts of the last diagram in
sec.\ref{cuts-stopping-midway},
%
%R local Y, La =
%R 2/  22  \, 2/  25  \
%R  |21  12|   |24  15|
%R  \  11  /   \  14  /
%R 
%R Y :tozmp({def="Ycut", scale="10pt"}):addcells():addcuts("00w-01n 10e-10n"):output()
%R La:tozmp({def="Lcut", scale="10pt"}):addcells():addcuts("00w-00n 00e-10n"):output()
$$\pu
  \begin{array}{rcl}
  \Ycut &\Leftarrow& \text{this is a Y-cut}  \\\\
  \Lcut &\Leftarrow& \text{this is a $λ$-cut}\\
  \end{array}
$$
%
then the operation $J$ that takes each element to the top of its
equivalence class cannot obey $\J1$, $\J2$ and $\J3$ at the same time.
We will prove that by deriving rules that say that if $11 \eqJ 12$
then $21 \eqJ 22$, and that if $15 \eqJ 25$ then $14 \eqJ 24$;
actually, our rules will say that if $11^* = 12^*$ then $(11∨21)^* =
(12∨21)^*$, and that if $15^*=25^*$ then $(15∧24)^*=(25∧24)^*$. The
rules are:

% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%
%:                                     Q¹=R¹
%:                                  ---------
%:                                  P∨Q¹=P∨R¹
%:                               ---------------
%:      Q¹=R¹                    (P∨Q¹)¹=(P∨R¹)¹
%:  ---------------\NoYcuts  :=  ===============\ostarcube
%:  (P∨Q)¹=(P∨R)¹                 (P∨Q)¹=(P∨R)¹           
%:
%:  ^NoYcuts1-                     ^NoYcuts2-
%:
%:                                     P¹=Q¹
%:                                  ---------
%:                                  P∨R¹=Q∨R¹
%:                               ---------------
%:      P¹=Q¹                    (P∨R¹)¹=(Q∨R¹)¹
%:  ---------------\NoYcuts  :=  ================\oor_6=\oor_4
%:  (P∨R)¹=(Q∨R)¹               (P∨R)¹=(Q∨R)¹
%:
%:  ^NoYcuts1                      ^NoYcuts2
%:
%:
%:                                  Q¹=R¹
%:                               ----------
%:      Q¹=R¹                    P¹∧Q¹=P¹∧R¹
%:  ---------------\NoLcuts  :=  ------------\J3
%:  (P∧Q)¹=(P∧R)¹                (P∧Q)¹=(P∧R)¹
%:
%:  ^NoLcuts1-                    ^NoLcuts2-
%:
%:                                  P¹=Q¹
%:                               ----------
%:      P¹=Q¹                    P¹∧R¹=Q¹∧R¹
%:  ---------------\NoLcuts  :=  ------------\J3
%:  (P∧R)¹=(Q∧R)¹                (P∧R)¹=(Q∧R)¹
%:
%:  ^NoLcuts1                     ^NoLcuts2
%:
$$\pu
  \begin{array}{rcl}
  \ded{NoYcuts1} &:=& \ded{NoYcuts2} \\ \\
  \ded{NoLcuts1} &:=& \ded{NoLcuts2} \\ \\
  \end{array}
$$

The expansion of double bar labeled `$\oor_6=\oor_4$' in the top
derivation uses twice the derived rule $\oor_6=\oor_4$, that is easy
to prove using the cubes of sec.\ref{cubes}.



\directlua{tf_pop()}


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