%%
%% This is file `boolalg.sty',
%% Copyright (C) 2026 Param Srivastava
%%
%% This work may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3c
%% of this license or (at your option) any later version.
%% The latest version of this license is in
%%   https://www.latex-project.org/lppl.txt
%% and version 1.3c or later is part of all distributions of LaTeX
%% version 2008 or later.
%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{boolalg}[2026/10/22 v1.0.0 Boolean logic truth tables, simplifier, and prover]

\ifdefined\pdfstrcmp\else
  \RequirePackage{pdftexcmds}
  \let\pdfstrcmp\pdf@strcmp
\fi

%% ================================================================
%% Boolean Logic Macros - Usage Guide
%% ================================================================
%%
%% COMMANDS
%%   \btable{<expr>}          Truth table (aliases: \btruth, \truthtable, \btruthtable, \booltruthtable)
%%   \btable*{<expr>}         Truth table with simplified answer
%%   \bsimplify{<expr>}       Step-by-step simplification (alias: \boolsimplify)
%%   \bsimplify*{<expr>}      Final simplified answer only
%%   \bprove{<lhs> = <rhs>}   Step-by-step proof or counterexample (alias: \boolprove)
%% INPUT SYNTAX (highest to lowest priority)
%%   Variables : Single letters A-Z, a-z
%%   Constants : 0, 1
%%   Grouping  : ( ... )
%%   1. NOT    : not, \not, \lnot, \neg, ', !, ~
%%   2. AND    : AB, *, ., &, and, \and, \land, \wedge, \cdot
%%      NAND   : nand, \nand, \uparrow, \barwedge
%%   3. OR     : +, |, or, \or, \lor, \vee
%%      NOR    : nor, \nor, \downarrow
%%   4. XOR    : ^, xor, \xor, \oplus, \veebar
%%      XNOR   : xnor, \xnor, \odot, \equiv, \leftrightarrow, \iff
%%
%%   Examples: AB means A AND B; A' and !A both mean NOT A.
%%   Note: Put a space after word operators, e.g. "not A".
%%
%% EXAMPLES
%%   \btable*{A'B + AB'}
%%   \bsimplify{(A + B)(A + B')}
%%   \bprove{A \oplus B = (A + B)(AB)'}
%%   \bprove{A + B = AB}                  % Prints counterexample: A=0, B=1
%%
%% SETTINGS (override with \def)
%%   \def\boolfname{f}            % Name of the output column (use \empty to hide)
%%   \def\booltablemaxvars{5}     % Skip truth tables with more than 5 variables
%%   \def\bool<op>sym{<symbol>}   % Customise operator symbols (e.g. \def\boolandsym{\land})
%% ================================================================
%% ---------------------------------------------------------------- configuration options
\def\boolandsym{\land}
\def\boolorsym{\lor}
\def\boolnotsym{\lnot}
\def\boolxorsym{\oplus}
\def\boolxnorsym{\odot}
\def\boolnandsym{\uparrow}
\def\boolnorsym{\downarrow}
\def\boolfname{f}
\def\booltablemaxvars{5}
%% ================================================================
%% Boolean Logic Prover, Simplifier & Truth Table Generator
%% ================================================================
\newcount\bl@cnt \newcount\bl@idx \newcount\bl@ca \newcount\bl@cb
\newif\ifbl@post \newif\ifbl@err \newif\ifbl@trace \newif\ifbl@showtab \newif\ifbl@star
\newbox\bl@tbox\newwrite\bl@tracefile
\def\bl@stop{\bl@stop}\def\bl@nil{\bl@nil}\def\bl@stopall{\bl@stopall}\def\bl@SP{\bl@SP}
\def\bl@ret{}\def\bl@law{}\def\bl@flag{0}\def\bl@key{}\def\bl@done{0}\def\bl@errmsg{}
%% ---------------------------------------------------------------- helpers
\def\bl@return{%
  \edef\bl@tmp{\endgroup
    \def\noexpand\bl@ret{\unexpanded\expandafter{\bl@ret}}%
    \def\noexpand\bl@law{\unexpanded\expandafter{\bl@law}}%
    \def\noexpand\bl@flag{\bl@flag}%
    \def\noexpand\bl@key{\unexpanded\expandafter{\bl@key}}}%
  \bl@tmp}
\def\bl@init{\def\bl@done{0}\let\bl@ret\@empty}
\def\bl@args#1#2#3{\edef\bl@tmp{\def\noexpand\bl@op{#1}\def\noexpand\bl@p{#2}\def\noexpand\bl@q{#3}}\bl@tmp}
\def\bl@seterr#1{\ifbl@err\else\global\bl@errtrue\xdef\bl@errmsg{#1}\fi}
\long\def\bl@emit#1{\g@addto@macro\bl@out{#1}}
\long\def\bl@for#1#2#3#4{\edef#1{\the\numexpr#2\relax}\bl@for@#1{#3}{#4}}
\long\def\bl@for@#1#2#3{\ifnum#1>\numexpr#2\relax\expandafter\@gobble\else\expandafter\@firstofone\fi
  {#3\edef#1{\the\numexpr#1+1\relax}\bl@for@#1{#2}{#3}}}
\long\def\bl@forb#1#2#3#4{\edef#1{\the\numexpr#2\relax}\bl@forb@#1{#3}{#4}}
\long\def\bl@forb@#1#2#3{\ifnum\ifnum#1>\numexpr#2\relax1\else\bl@done\fi=\@ne
  \expandafter\@gobble\else\expandafter\@firstofone\fi
  {#3\edef#1{\the\numexpr#1+1\relax}\bl@forb@#1{#2}{#3}}}
%% arrays: \bl@@{name}{i}, \bl@@{name}{n}
\def\bl@@#1#2{\csname bl@#1@#2\endcsname}
\def\bl@arrinit#1{\expandafter\def\csname bl@#1@n\endcsname{0}}
\def\bl@push#1#2{\edef\bl@tmp{\noexpand\bl@push@{#1}{\the\numexpr\bl@@{#1}{n}+1\relax}{#2}}\bl@tmp}
\def\bl@push@#1#2#3{\expandafter\def\csname bl@#1@n\endcsname{#2}\expandafter\def\csname bl@#1@#2\endcsname{#3}}
\def\bl@gpush#1#2{\edef\bl@tmp{\noexpand\bl@gpush@{#1}{\the\numexpr\bl@@{#1}{n}+1\relax}{#2}}\bl@tmp}
\def\bl@gpush@#1#2#3{\expandafter\gdef\csname bl@#1@n\endcsname{#2}\expandafter\gdef\csname bl@#1@#2\endcsname{#3}}
\def\bl@arr#1#2{\bl@cnt\z@\bl@arr@{#2}#1\bl@stop\expandafter\edef\csname bl@#2@n\endcsname{\the\bl@cnt}}
\def\bl@arr@#1#2{\ifx\bl@stop#2\expandafter\@gobble\else\expandafter\@firstofone\fi
  {\advance\bl@cnt\@ne\expandafter\def\csname bl@#1@\the\bl@cnt\endcsname{#2}\bl@arr@{#1}}}
\def\bl@inarr#1#2{\edef\bl@tmpe{#1}\def\bl@flag{0}%
  \bl@for\bl@ik{1}{\bl@@{#2}{n}}{\ifnum\pdfstrcmp{\bl@tmpe}{\bl@@{#2}{\bl@ik}}=0 \def\bl@flag{1}\fi}}
\def\bl@subset#1#2{\def\bl@sflag{1}%
  \bl@for\bl@si{1}{\bl@@{#1}{n}}{\bl@inarr{\bl@@{#1}{\bl@si}}{#2}\ifnum\bl@flag=0 \def\bl@sflag{0}\fi}%
  \let\bl@flag\bl@sflag}
\def\bl@foldarr#1#2#3{\let\bl@fold\@empty
  \bl@for\bl@fi{1}{\bl@@{#2}{n}}{\ifnum\bl@fi=#3 \else
    \ifx\bl@fold\@empty\edef\bl@fold{\bl@@{#2}{\bl@fi}}\else\edef\bl@fold{#1{\bl@fold}{\bl@@{#2}{\bl@fi}}}\fi\fi}}
\def\bl@sortarr#1#2{\bl@for\bl@so{2}{\bl@@{#1}{n}}{\edef\bl@sj{\bl@so}\bl@sort@{#1}{#2}}}
\def\bl@sort@#1#2{\let\bl@next\relax
  \ifnum\bl@sj>\@ne
    \ifnum\pdfstrcmp{#2{\bl@@{#1}{\the\numexpr\bl@sj-1\relax}}}{#2{\bl@@{#1}{\bl@sj}}}>\z@
      \expandafter\let\expandafter\bl@tmpa\csname bl@#1@\bl@sj\endcsname
      \expandafter\let\csname bl@#1@\bl@sj\expandafter\endcsname\csname bl@#1@\the\numexpr\bl@sj-1\relax\endcsname
      \expandafter\let\csname bl@#1@\the\numexpr\bl@sj-1\relax\endcsname\bl@tmpa
      \edef\bl@sj{\the\numexpr\bl@sj-1\relax}\def\bl@next{\bl@sort@{#1}{#2}}%
    \fi
  \fi\bl@next}
\def\bl@joinarr#1#2{\edef\bl@jn{\bl@@{#1}{1}}%
  \bl@for\bl@ji{2}{\bl@@{#1}{n}}{\edef\bl@jn{\bl@jn#2\bl@@{#1}{\bl@ji}}}}
%% ---------------------------------------------------------------- nodes
%% Node tags:
%%   v = variable, k = constant (0/1), n = NOT
%%   a = AND, o = OR, x = XOR, b = XNOR, d = NAND, r = NOR
\def\bl@T#1#2#3{#1}\def\bl@A#1#2#3{#2}\def\bl@B#1#2#3{#3}
\def\bl@dual#1{\if a#1o\else a\fi}
\def\bl@opch#1{\if a#1\string&\else\if o#1|\else\if x#1\string^\else\if b#1=\else\if d#1\string~\string&\else\string~|\fi\fi\fi\fi\fi}
\def\bl@ifao#1{\expandafter\bl@ifao@\romannumeral-`0#1}
\def\bl@ifao@#1#2#3{\ifnum0\if a#11\fi\if o#11\fi=\@ne\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi}
\def\bl@ifbin#1{\expandafter\bl@ifbin@\romannumeral-`0#1}
\def\bl@ifbin@#1#2#3{\ifnum0\if a#11\fi\if o#11\fi\if x#11\fi\if b#11\fi\if d#11\fi\if r#11\fi=\@ne\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi}
\def\bl@ifnegof#1#2{\edef\bl@tmp{\noexpand\bl@negtest{#1}{#2}}\bl@tmp}
\def\bl@negtest#1#2{\ifnum\numexpr\bl@neg@#1\@nil{#2}+\bl@neg@#2\@nil{#1}\relax>\z@
  \expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi}
\def\bl@neg@#1#2#3\@nil#4{\if n#1\ifnum\pdfstrcmp{#2}{#4}=0 1\else0\fi\else0\fi}
%% S(n): key
\def\bl@S#1{\expandafter\bl@S@\romannumeral-`0#1}
\def\bl@S@#1{\csname bl@S@#1\endcsname}
\def\bl@S@v#1#2{#1}\let\bl@S@k\bl@S@v
\def\bl@S@n#1#2{!\bl@S@#1}
\def\bl@S@a#1#2{(\bl@S@#1\string&\bl@S@#2)}
\def\bl@S@o#1#2{(\bl@S@#1|\bl@S@#2)}
\def\bl@S@x#1#2{(\bl@S@#1\string^\bl@S@#2)}
\def\bl@S@b#1#2{(\bl@S@#1=\bl@S@#2)}
\def\bl@S@d#1#2{(\bl@S@#1\string~\string&\bl@S@#2)}
\def\bl@S@r#1#2{(\bl@S@#1\string~|\bl@S@#2)}
%% ordering and shape
\def\bl@ok#1{\expandafter\bl@ok@\romannumeral-`0#1}
\def\bl@ok@#1{\csname bl@ok@#1\endcsname}
\def\bl@ok@v#1#2{#1}\let\bl@ok@k\bl@ok@v
\def\bl@ok@n#1#2{!\bl@ok@#1}
\def\bl@ok@a#1#2{(\bl@okc a#1\string&\bl@okc a#2)}
\def\bl@ok@o#1#2{(\bl@okc o#1|\bl@okc o#2)}
\def\bl@ok@x#1#2{(\bl@okc x#1\string^\bl@okc x#2)}
\def\bl@ok@b#1#2{(\bl@okc b#1=\bl@okc b#2)}
\def\bl@ok@d#1#2{(\bl@ok@#1\string~\string&\bl@ok@#2)}
\def\bl@ok@r#1#2{(\bl@ok@#1\string~|\bl@ok@#2)}
\def\bl@okc#1#2#3#4{\if#1#2\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi
  {\bl@okc#1#3\bl@opch#1\bl@okc#1#4}{\bl@ok@#2{#3}{#4}}}
\def\bl@sh#1{\expandafter\bl@sh@\romannumeral-`0#1}
\def\bl@sh@#1{\csname bl@sh@#1\endcsname}
\def\bl@sh@v#1#2{x}\let\bl@sh@k\bl@sh@v
\def\bl@sh@n#1#2{\bl@shn#1}
\def\bl@shn#1#2#3{\ifnum0\if v#11\fi\if k#11\fi=\@ne x\else!\bl@sh@#1{#2}{#3}\fi}
\def\bl@sh@a#1#2{(\bl@sh@#1\string&\bl@sh@#2)}
\def\bl@sh@o#1#2{(\bl@sh@#1|\bl@sh@#2)}
\def\bl@sh@x#1#2{(\bl@sh@#1\string^\bl@sh@#2)}
\def\bl@sh@b#1#2{(\bl@sh@#1=\bl@sh@#2)}
\def\bl@sh@d#1#2{(\bl@sh@#1\string~\string&\bl@sh@#2)}
\def\bl@sh@r#1#2{(\bl@sh@#1\string~|\bl@sh@#2)}
\def\bl@aclabel#1#2{%
  \ifnum\pdfstrcmp{\bl@ok{#1}}{\bl@ok{#2}}=0 \def\bl@law{Associativity}%
  \else\ifnum\pdfstrcmp{\bl@sh{#1}}{\bl@sh{#2}}=0 \def\bl@law{Commutativity}%
  \else\def\bl@law{Commutativity and associativity}\fi\fi}
%% flat(n, op) -> list {c1}{c2}...
\def\bl@flat#1#2{\expandafter\bl@fl@\expandafter#1\romannumeral-`0#2}
\def\bl@fl@#1#2#3#4{\if#1#2\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi
  {\bl@fl@#1#3\bl@fl@#1#4}{\unexpanded{{#2{#3}{#4}}}}}
\def\bl@flatarr#1#2#3{\edef\bl@tmp{\noexpand\bl@arr{\bl@flat{#2}{#3}}{#1}}\bl@tmp}
%% K(n): sorted key
\def\bl@K#1{\expandafter\bl@K@\romannumeral-`0#1}
\def\bl@K@#1{\csname bl@K@#1\endcsname}
\def\bl@K@v#1#2{\def\bl@key{#1}}\let\bl@K@k\bl@K@v
\def\bl@K@n#1#2{\bl@K@#1\edef\bl@key{!\bl@key}}
\def\bl@K@a#1#2{\bl@Kbin a{#1}{#2}}
\def\bl@K@o#1#2{\bl@Kbin o{#1}{#2}}
\def\bl@K@x#1#2{\bl@Kbin x{#1}{#2}}
\def\bl@K@b#1#2{\bl@Kbin b{#1}{#2}}
\def\bl@K@d#1#2{\bl@Kcomm d{#1}{#2}}
\def\bl@K@r#1#2{\bl@Kcomm r{#1}{#2}}
\def\bl@Kbin#1#2#3{\begingroup\bl@init
  \bl@flatarr{kc}{#1}{#1{#2}{#3}}%
  \bl@for\bl@i{1}{\bl@@{kc}{n}}{\bl@K{\bl@@{kc}{\bl@i}}\expandafter\let\csname bl@kk@\bl@i\endcsname\bl@key}%
  \expandafter\let\csname bl@kk@n\endcsname\bl@kc@n
  \bl@sortarr{kk}\@firstofone
  \bl@joinarr{kk}{\bl@opch#1}%
  \edef\bl@key{(\bl@jn)}%
  \bl@return}
\def\bl@Kcomm#1#2#3{\begingroup\bl@init
  \bl@K{#2}\let\bl@ka\bl@key
  \bl@K{#3}\let\bl@kb\bl@key
  \ifnum\pdfstrcmp{\bl@ka}{\bl@kb}>\z@
    \edef\bl@key{(\bl@kb\bl@opch#1\bl@ka)}%
  \else
    \edef\bl@key{(\bl@ka\bl@opch#1\bl@kb)}%
  \fi
  \bl@return}
%% rebuild tree
\def\bl@refill#1#2#3{\global\bl@idx\z@\def\bl@rfarr{#1}\edef\bl@rfop{#2}%
  \expandafter\bl@rf@\romannumeral-`0#3}
\def\bl@rf@#1#2#3{%
  \if\bl@rfop#1%
    \begingroup
      \bl@rf@#2\let\bl@rfl\bl@rf
      \bl@rf@#3%
      \edef\bl@rf{#1{\bl@rfl}{\bl@rf}}%
    \expandafter\endgroup\expandafter\def\expandafter\bl@rf\expandafter{\bl@rf}%
  \else
    \global\advance\bl@idx\@ne
    \edef\bl@rf{\bl@@\bl@rfarr{\the\bl@idx}}%
  \fi}
\def\bl@reform#1#2{\begingroup\bl@init
  \edef\bl@tmp{\def\noexpand\bl@p{#1}\def\noexpand\bl@tg{#2}}\bl@tmp
  \ifnum\pdfstrcmp{\bl@ok\bl@p}{\bl@ok\bl@tg}=0
    \let\bl@ret\bl@tg\def\bl@law{Associativity}%
  \else
    \edef\bl@ptag{\expandafter\bl@T\bl@p}%
    \bl@flatarr{rf}{\bl@ptag}{\bl@tg}%
    \bl@refill{rf}{\bl@ptag}{\bl@p}\let\bl@ret\bl@rf
    \def\bl@law{Commutativity}%
  \fi
  \bl@return}
%% ---------------------------------------------------------------- traversal
\def\bl@apply#1#2{\expandafter\bl@ap@\expandafter#1\romannumeral-`0#2}
\def\bl@ap@#1#2#3#4{\begingroup\let\bl@ret\@empty
  \ifbl@post\else#1{#2{#3}{#4}}\fi
  \ifx\bl@ret\@empty
    \if n#2\relax
      \bl@ap@#1#3%
      \ifx\bl@ret\@empty\else\edef\bl@ret{n{\bl@ret}{}}\fi
    \else\bl@ifbin@#2{}{}{%
      \bl@ap@#1#3%
      \ifx\bl@ret\@empty
        \bl@ap@#1#4%
        \ifx\bl@ret\@empty\else\edef\bl@ret{#2{#3}{\bl@ret}}\fi
      \else\edef\bl@ret{#2{\bl@ret}{#4}}\fi}{}%
    \fi
    \ifx\bl@ret\@empty\ifbl@post#1{#2{#3}{#4}}\fi\fi
  \fi
  \bl@return}
%% ---------------------------------------------------------------- rules
\def\bl@r@def#1{\expandafter\bl@r@def@\romannumeral-`0#1}
\def\bl@r@def@#1#2#3{\let\bl@ret\@empty
  \if d#1\edef\bl@ret{n{a{#2}{#3}}{}}\def\bl@law{Definition of NAND}\fi
  \if r#1\edef\bl@ret{n{o{#2}{#3}}{}}\def\bl@law{Definition of NOR}\fi
  \if x#1\edef\bl@ret{o{a{#2}{n{#3}{}}}{a{n{#2}{}}{#3}}}\def\bl@law{Definition of XOR}\fi
  \if b#1\edef\bl@ret{o{a{#2}{#3}}{a{n{#2}{}}{n{#3}{}}}}\def\bl@law{Definition of XNOR}\fi}
\def\bl@r@neg#1{\expandafter\bl@r@neg@\romannumeral-`0#1}
\def\bl@r@neg@#1#2#3{\let\bl@ret\@empty\if n#1\bl@r@negn#2\fi}
\def\bl@r@negn#1#2#3{%
  \if n#1\def\bl@ret{#2}\def\bl@law{Double negation}\fi
  \if k#1\edef\bl@ret{k{\the\numexpr1-#2\relax}{}}\def\bl@law{Complement}\fi}
\def\bl@iskv#1#2#3\@nil#4{\if k#1\ifnum#2=#4 1\else0\fi\else0\fi}
\def\bl@r@const#1{\expandafter\bl@r@const@\romannumeral-`0#1}
\def\bl@r@const@#1#2#3{\let\bl@ret\@empty
  \bl@ifao@#1{}{}{%
    \edef\bl@z{\if a#10\else1\fi}\edef\bl@u{\if a#11\else0\fi}%
    \ifnum\numexpr\bl@iskv#2\@nil\bl@z+\bl@iskv#3\@nil\bl@z\relax>\z@
      \edef\bl@ret{k{\bl@z}{}}\def\bl@law{Domination}%
    \else\ifnum\bl@iskv#2\@nil\bl@u=\@ne
      \def\bl@ret{#3}\def\bl@law{Identity}%
    \else\ifnum\bl@iskv#3\@nil\bl@u=\@ne
      \def\bl@ret{#2}\def\bl@law{Identity}%
    \fi\fi\fi}{}}
\def\bl@absorbs#1#2#3{\begingroup\bl@init\bl@args{#1}{#2}{#3}\def\bl@flag{0}%
  \edef\bl@d{\bl@dual\bl@op}%
  \if\bl@d\expandafter\bl@T\bl@q
    \bl@flatarr{iq}{\bl@d}{\bl@q}%
    \if\bl@d\expandafter\bl@T\bl@p
      \bl@flatarr{ip}{\bl@d}{\bl@p}%
      \ifnum\bl@@{ip}{n}<\bl@@{iq}{n}\relax\bl@subset{ip}{iq}\fi
    \else
      \bl@inarr\bl@p{iq}%
    \fi
  \fi
  \bl@return}
\def\bl@pr@simple#1#2#3{\begingroup\bl@init\bl@args{#1}{#2}{#3}%
  \ifnum\pdfstrcmp{\bl@p}{\bl@q}=0
    \let\bl@ret\bl@p\def\bl@law{Idempotence}%
  \else
    \bl@ifnegof\bl@p\bl@q{\edef\bl@ret{k{\if a\bl@op0\else1\fi}{}}\def\bl@law{Complement}}{}%
    \ifx\bl@ret\@empty
      \bl@absorbs\bl@op\bl@p\bl@q
      \ifnum\bl@flag=1 \let\bl@ret\bl@p\def\bl@law{Absorption}\fi
    \fi
    \ifx\bl@ret\@empty
      \bl@absorbs\bl@op\bl@q\bl@p
      \ifnum\bl@flag=1 \let\bl@ret\bl@q\def\bl@law{Absorption}\fi
    \fi
    \ifx\bl@ret\@empty
      \bl@K\bl@p\let\bl@kp\bl@key\bl@K\bl@q
      \ifnum\pdfstrcmp{\bl@kp}{\bl@key}=0
        \edef\bl@ret{\bl@op{\bl@p}{\bl@p}}\bl@aclabel\bl@q\bl@p
      \fi
    \fi
  \fi
  \bl@return}
\def\bl@pr@red#1#2#3{\begingroup\bl@init\bl@args{#1}{#2}{#3}%
  \edef\bl@d{\bl@dual\bl@op}%
  \bl@red@\bl@p\bl@q0%
  \ifx\bl@ret\@empty\bl@red@\bl@q\bl@p1\fi
  \bl@return}
\def\bl@red@#1#2#3{\let\bl@X#1\let\bl@Cm#2\def\bl@cmleft{#3}%
  \if\bl@d\expandafter\bl@T\bl@Cm
    \bl@flatarr{it}{\bl@d}{\bl@Cm}%
    \def\bl@ix{0}%
    \bl@for\bl@i{1}{\bl@@{it}{n}}{\ifnum\bl@ix=0 \bl@ifnegof{\bl@@{it}{\bl@i}}\bl@X{\edef\bl@ix{\bl@i}}{}\fi}%
    \ifnum\bl@ix>0
      \edef\bl@u{\expandafter\bl@A\bl@Cm}\edef\bl@v{\expandafter\bl@B\bl@Cm}%
      \def\bl@tmpf{0}%
      \bl@ifnegof\bl@u\bl@X{\def\bl@tmpf{1}}{}%
      \bl@ifnegof\bl@v\bl@X{\def\bl@tmpf{1}}{}%
      \ifnum\bl@tmpf=1
        \ifnum\bl@cmleft=1
          \edef\bl@ret{\bl@d{\bl@op{\bl@u}{\bl@X}}{\bl@op{\bl@v}{\bl@X}}}%
        \else
          \edef\bl@ret{\bl@d{\bl@op{\bl@X}{\bl@u}}{\bl@op{\bl@X}{\bl@v}}}%
        \fi
        \def\bl@law{Distributivity}%
      \else
        \bl@foldarr\bl@d{it}\bl@ix
        \edef\bl@nc{\bl@d{\bl@@{it}{\bl@ix}}{\bl@fold}}%
        \bl@reform\bl@Cm\bl@nc
        \ifnum\bl@cmleft=1 \edef\bl@ret{\bl@op{\bl@ret}{\bl@X}}\else\edef\bl@ret{\bl@op{\bl@X}{\bl@ret}}\fi
      \fi
    \fi
  \fi}
\def\bl@pr@adv#1#2#3{\bl@pr@red{#1}{#2}{#3}\ifx\bl@ret\@empty\bl@pr@fact{#1}{#2}{#3}\fi}
\def\bl@simp#1#2#3{\bl@pr@simple{#1}{#2}{#3}\ifx\bl@ret\@empty\bl@pr@adv{#1}{#2}{#3}\fi}
\def\bl@pr@fact#1#2#3{\begingroup\bl@init\bl@args{#1}{#2}{#3}%
  \edef\bl@d{\bl@dual\bl@op}%
  \ifnum0\if\bl@d\expandafter\bl@T\bl@p\if\bl@d\expandafter\bl@T\bl@q1\fi\fi=\@ne
    \bl@flatarr{ip}{\bl@d}{\bl@p}\bl@flatarr{iq}{\bl@d}{\bl@q}%
    \bl@arrinit{C}\bl@arrinit{Pr}\bl@arrinit{Qr}%
    \bl@for\bl@i{1}{\bl@@{ip}{n}}{\bl@inarr{\bl@@{ip}{\bl@i}}{iq}%
      \ifnum\bl@flag=1 \bl@push{C}{\bl@@{ip}{\bl@i}}\else\bl@push{Pr}{\bl@@{ip}{\bl@i}}\fi}%
    \bl@for\bl@i{1}{\bl@@{iq}{n}}{\bl@inarr{\bl@@{iq}{\bl@i}}{ip}%
      \ifnum\bl@flag=0 \bl@push{Qr}{\bl@@{iq}{\bl@i}}\fi}%
    \ifnum0\ifnum\bl@@{C}{n}=0 1\fi\ifnum\bl@@{Pr}{n}=0 1\fi\ifnum\bl@@{Qr}{n}=0 1\fi=0
      \bl@foldarr\bl@d{Pr}{0}\let\bl@Pn\bl@fold
      \bl@foldarr\bl@d{Qr}{0}\let\bl@Qn\bl@fold
      \bl@simp\bl@op\bl@Pn\bl@Qn
      \ifx\bl@ret\@empty\else
        \let\bl@ret\@empty
        \bl@sortarr{C}\bl@S
        \bl@foldarr\bl@d{C}{0}\let\bl@Cn\bl@fold
        \edef\bl@cp{\bl@d{\bl@Cn}{\bl@Pn}}\edef\bl@cq{\bl@d{\bl@Cn}{\bl@Qn}}%
        \ifnum\pdfstrcmp{\bl@p}{\bl@cp}=0
          \ifnum\pdfstrcmp{\bl@q}{\bl@cq}=0
            \edef\bl@ret{\bl@d{\bl@Cn}{\bl@op{\bl@Pn}{\bl@Qn}}}\def\bl@law{Distributivity}%
          \else
            \bl@reform\bl@q\bl@cq\edef\bl@ret{\bl@op{\bl@p}{\bl@ret}}%
          \fi
        \else
          \bl@reform\bl@p\bl@cp\edef\bl@ret{\bl@op{\bl@ret}{\bl@q}}%
        \fi
      \fi
    \fi
  \fi
  \bl@return}
\def\bl@nodefn#1#2{\expandafter\bl@nodefn@\expandafter#1\romannumeral-`0#2}
\def\bl@nodefn@#1#2#3#4{\let\bl@ret\@empty\bl@ifao@#2{}{}{#1#2{#3}{#4}}{}}
\def\bl@chainfn#1#2{\begingroup\bl@init\edef\bl@n{#2}%
  \bl@ifao\bl@n{%
    \edef\bl@op{\expandafter\bl@T\bl@n}%
    \bl@flatarr{it}{\bl@op}{\bl@n}%
    \ifnum\bl@@{it}{n}>2
      \bl@forb\bl@i{1}{\bl@@{it}{n}-1}{\bl@forb\bl@j{\bl@i+1}{\bl@@{it}{n}}{%
        #1\bl@op{\bl@@{it}{\bl@i}}{\bl@@{it}{\bl@j}}%
        \ifx\bl@ret\@empty\else\def\bl@done{1}\bl@chain@build\fi}}%
    \fi}{}%
  \bl@return}
\def\bl@chain@build{%
  \bl@arrinit{pm}\bl@push{pm}{\bl@@{it}{\bl@i}}\bl@push{pm}{\bl@@{it}{\bl@j}}%
  \bl@for\bl@k{1}{\bl@@{it}{n}}{\ifnum\bl@k=\bl@i\else\ifnum\bl@k=\bl@j\else\bl@push{pm}{\bl@@{it}{\bl@k}}\fi\fi}%
  \def\bl@tmpf{0}\ifnum\bl@i=1 \ifnum\bl@j=2 \def\bl@tmpf{1}\fi\fi
  \ifnum\bl@tmpf=1
    \bl@foldarr\bl@op{pm}{0}\let\bl@ret\bl@fold\def\bl@law{Associativity}%
  \else
    \bl@refill{pm}{\bl@op}{\bl@n}\let\bl@ret\bl@rf\def\bl@law{Commutativity}%
  \fi}
\def\bl@uadd#1{\bl@inarr{#1}{U}\ifnum\bl@flag=0 \bl@push{U}{#1}\fi}
\def\bl@eqset#1{\bl@arrinit{E}\def\bl@eflag{1}%
  \bl@for\bl@m{1}{\bl@@{#1}{n}}{\bl@inarr{\bl@@{#1}{\bl@m}}{U}%
    \ifnum\bl@flag=0 \def\bl@eflag{0}\else
      \bl@inarr{\bl@@{#1}{\bl@m}}{E}\ifnum\bl@flag=0 \bl@push{E}{\bl@@{#1}{\bl@m}}\fi\fi}%
  \ifnum\bl@@{E}{n}=\bl@@{U}{n}\relax\else\def\bl@eflag{0}\fi
  \let\bl@flag\bl@eflag}
\def\bl@r@cons#1{\begingroup\bl@init\edef\bl@n{#1}%
  \bl@ifao\bl@n{%
    \edef\bl@op{\expandafter\bl@T\bl@n}\edef\bl@d{\bl@dual\bl@op}%
    \bl@flatarr{it}{\bl@op}{\bl@n}%
    \ifnum\bl@@{it}{n}>2
      \bl@for\bl@i{1}{\bl@@{it}{n}}{\bl@flatarr{fl\bl@i}{\bl@d}{\bl@@{it}{\bl@i}}}%
      \bl@forb\bl@i{1}{\bl@@{it}{n}}{\bl@forb\bl@j{1}{\bl@@{it}{n}}{\ifnum\bl@i=\bl@j\else
        \bl@forb\bl@a{1}{\bl@@{fl\bl@i}{n}}{\bl@forb\bl@b{1}{\bl@@{fl\bl@j}{n}}{%
          \bl@ifnegof{\bl@@{fl\bl@i}{\bl@a}}{\bl@@{fl\bl@j}{\bl@b}}\bl@cons@try{}}}\fi}}%
    \fi}{}%
  \bl@return}
\def\bl@cons@try{%
  \bl@arrinit{U}%
  \bl@for\bl@k{1}{\bl@@{fl\bl@i}{n}}{\ifnum\bl@k=\bl@a\else\bl@uadd{\bl@@{fl\bl@i}{\bl@k}}\fi}%
  \bl@for\bl@k{1}{\bl@@{fl\bl@j}{n}}{\ifnum\bl@k=\bl@b\else\bl@uadd{\bl@@{fl\bl@j}{\bl@k}}\fi}%
  \ifnum\bl@@{U}{n}>0
    \bl@forb\bl@kk{1}{\bl@@{it}{n}}{\ifnum\bl@kk=\bl@i\else\ifnum\bl@kk=\bl@j\else
      \bl@eqset{fl\bl@kk}%
      \ifnum\bl@flag=1
        \bl@foldarr\bl@op{it}\bl@kk\let\bl@ret\bl@fold
        \def\bl@law{Consensus theorem}\def\bl@done{1}%
      \fi\fi\fi}%
  \fi}
\def\bl@r@dm#1{\expandafter\bl@r@dm@\romannumeral-`0#1}
\def\bl@r@dm@#1#2#3{\let\bl@ret\@empty\if n#1\bl@ifao@#2{\bl@dm@#2}{}\fi}
\def\bl@dm@#1#2#3{\edef\bl@ret{\bl@dual#1{n{#2}{}}{n{#3}{}}}\def\bl@law{De Morgan's law}}
\def\bl@r@dist#1{\expandafter\bl@r@dist@\romannumeral-`0#1}
\def\bl@r@dist@#1#2#3{\let\bl@ret\@empty
  \if a#1%
    \if o\bl@T#3%
      \edef\bl@ret{o{a{#2}{\bl@A#3}}{a{#2}{\bl@B#3}}}\def\bl@law{Distributivity}%
    \else\if o\bl@T#2%
      \edef\bl@ret{o{a{\bl@A#2}{#3}}{a{\bl@B#2}{#3}}}\def\bl@law{Distributivity}%
    \fi\fi
  \fi}
\def\bl@st@simple{\bl@nodefn\bl@pr@simple}
\def\bl@st@chsimple{\bl@chainfn\bl@pr@simple}
\def\bl@st@adv{\bl@nodefn\bl@pr@adv}
\def\bl@st@chadv{\bl@chainfn\bl@pr@adv}
%% ---------------------------------------------------------------- main
\def\bl@stage#1#2#3{\ifx\bl@ret\@empty\ifnum#3>\bl@dist\relax\else
  \ifnum#2=\@ne\bl@posttrue\else\bl@postfalse\fi
  \bl@apply#1\bl@cur\fi\fi}
\def\bl@run#1#2#3{\def\bl@rtag{#1}\def\bl@dist{#2}\edef\bl@cur{#3}%
  \bl@arrinit{st#1}\bl@arrinit{sl#1}%
  \expandafter\let\csname bl@st#1@0\endcsname\bl@cur
  \bl@run@}
\def\bl@run@{\let\bl@ret\@empty\let\bl@next\relax
  \bl@stage\bl@r@neg 10%
  \bl@stage\bl@r@const 10%
  \bl@stage\bl@st@simple 10%
  \bl@stage\bl@st@chsimple 00%
  \bl@stage\bl@r@def 10%
  \bl@stage\bl@r@dm 00%
  \bl@stage\bl@st@adv 10%
  \bl@stage\bl@st@chadv 00%
  \bl@stage\bl@r@cons 00%
  \bl@stage\bl@r@dist 01%
  \ifx\bl@ret\@empty\let\bl@final\bl@cur
  \else
    \bl@push{st\bl@rtag}{\bl@ret}\bl@push{sl\bl@rtag}{\bl@law}%
    \let\bl@cur\bl@ret
    \ifnum\bl@@{st\bl@rtag}{n}<400 \let\bl@next\bl@run@\else\bl@seterr{derivation too long}\fi
  \fi\bl@next}
\def\bl@lits#1{\the\numexpr0\expandafter\bl@lt@\romannumeral-`0#1\relax}
\def\bl@lt@#1{\csname bl@lt@#1\endcsname}
\def\bl@lt@v#1#2{+1}\let\bl@lt@k\bl@lt@v
\def\bl@lt@n#1#2{\bl@lt@#1}
\def\bl@lt@a#1#2{\bl@lt@#1\bl@lt@#2}\let\bl@lt@o\bl@lt@a
\let\bl@lt@x\bl@lt@a\let\bl@lt@b\bl@lt@a\let\bl@lt@d\bl@lt@a\let\bl@lt@r\bl@lt@a
%% ---------------------------------------------------------------- printing
\def\bl@tex#1{\expandafter\bl@tx@\romannumeral-`0#1}
\def\bl@tx@#1{\csname bl@tx@#1\endcsname}
\def\bl@tx@v#1#2{#1}\let\bl@tx@k\bl@tx@v
\def\bl@tx@n#1#2{\noexpand\boolnotsym\bl@side#1}
\def\bl@tx@a#1#2{\bl@side#1\noexpand\boolandsym\bl@side#2}
\def\bl@tx@o#1#2{\bl@side#1\noexpand\boolorsym\bl@side#2}
\def\bl@tx@x#1#2{\bl@side#1\noexpand\boolxorsym\bl@side#2}
\def\bl@tx@b#1#2{\bl@side#1\noexpand\boolxnorsym\bl@side#2}
\def\bl@tx@d#1#2{\bl@side#1\noexpand\boolnandsym\bl@side#2}
\def\bl@tx@r#1#2{\bl@side#1\noexpand\boolnorsym\bl@side#2}
\def\bl@side#1#2#3{\bl@ifbin@#1{}{}{(\bl@tx@#1{#2}{#3})}{\bl@tx@#1{#2}{#3}}}
%% minimal-bracket printing (truth-table headers)
\def\bl@htex#1{\expandafter\bl@hx@\romannumeral-`0#1}
\def\bl@hx@#1{\csname bl@hx@#1\endcsname}
\def\bl@hx@v#1#2{#1}\let\bl@hx@k\bl@hx@v
\def\bl@hx@n#1#2{\noexpand\boolnotsym\bl@hside n#1}
\def\bl@hx@a#1#2{\bl@hside a#1\noexpand\boolandsym\bl@hside a#2}
\def\bl@hx@o#1#2{\bl@hside o#1\noexpand\boolorsym\bl@hside o#2}
\def\bl@hx@x#1#2{\bl@hside x#1\noexpand\boolxorsym\bl@hside x#2}
\def\bl@hx@b#1#2{\bl@hside b#1\noexpand\boolxnorsym\bl@hside b#2}
\def\bl@hx@d#1#2{\bl@hside d#1\noexpand\boolnandsym\bl@hside d#2}
\def\bl@hx@r#1#2{\bl@hside r#1\noexpand\boolnorsym\bl@hside r#2}
\def\bl@hside#1#2#3#4{\bl@ifbin@#2{}{}{\ifcsname bl@has@#1#2\endcsname\bl@hx@#2{#3}{#4}\else(\bl@hx@#2{#3}{#4})\fi}{\bl@hx@#2{#3}{#4}}}
\@namedef{bl@has@aa}{}\@namedef{bl@has@oo}{}\@namedef{bl@has@xx}{}\@namedef{bl@has@bb}{}
%% ---------------------------------------------------------------- truth values
\def\bl@vars#1{\expandafter\bl@vr@\romannumeral-`0#1}
\def\bl@vr@#1{\csname bl@vr@#1\endcsname}
\def\bl@vr@v#1#2{\expandafter\def\csname bl@vf@#1\endcsname{}}
\def\bl@vr@k#1#2{}
\def\bl@vr@n#1#2{\bl@vr@#1}
\def\bl@vr@a#1#2{\bl@vr@#1\bl@vr@#2}\let\bl@vr@o\bl@vr@a
\let\bl@vr@x\bl@vr@a\let\bl@vr@b\bl@vr@a\let\bl@vr@d\bl@vr@a\let\bl@vr@r\bl@vr@a
\def\bl@sortvars{\bl@arrinit{vs}%
  \@tfor\bl@c:=ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz\do
    {\ifcsname bl@vf@\bl@c\endcsname\bl@push{vs}{\bl@c}\fi}%
  \bl@ca\@ne\bl@for\bl@vi{1}{\bl@@{vs}{n}}{\multiply\bl@ca\tw@}\edef\bl@pow{\the\bl@ca}}
\def\bl@assign#1{\bl@ca=#1\relax
  \bl@for\bl@vi{0}{\bl@@{vs}{n}-1}{%
    \edef\bl@vk{\the\numexpr\bl@@{vs}{n}-\bl@vi\relax}%
    \bl@cb\bl@ca\divide\bl@cb\tw@
    \expandafter\edef\csname bl@val@\bl@@{vs}{\bl@vk}\endcsname{\the\numexpr\bl@ca-2*\bl@cb\relax}%
    \bl@ca\bl@cb}}
\def\bl@eval#1{\expandafter\bl@ev@\romannumeral-`0#1}
\def\bl@ev@#1{\csname bl@ev@#1\endcsname}
\def\bl@ev@v#1#2{\csname bl@val@#1\endcsname}
\def\bl@ev@k#1#2{#1}
\def\bl@ev@n#1#2{\ifnum\bl@ev@#1=0 1\else0\fi}
\def\bl@ev@a#1#2{\ifnum\bl@ev@#1=0 0\else\bl@ev@#2\fi}
\def\bl@ev@o#1#2{\ifnum\bl@ev@#1=1 1\else\bl@ev@#2\fi}
\def\bl@ev@x#1#2{\ifnum\bl@ev@#1=0 \bl@ev@#2\else\ifnum\bl@ev@#2=0 1\else0\fi\fi}
\def\bl@ev@b#1#2{\ifnum\bl@ev@#1=0 \ifnum\bl@ev@#2=0 1\else0\fi\else\bl@ev@#2\fi}
\def\bl@ev@d#1#2{\ifnum\bl@ev@#1=0 1\else\ifnum\bl@ev@#2=0 1\else0\fi\fi}
\def\bl@ev@r#1#2{\ifnum\bl@ev@#1=1 0\else\ifnum\bl@ev@#2=1 0\else1\fi\fi}
%% ---------------------------------------------------------------- tokeniser
\def\bl@spsplit#1{\def\bl@pp{}\expandafter\bl@sps@#1 \bl@stopall}
\def\bl@sps@#1 #2\bl@stopall{\expandafter\def\expandafter\bl@pp\expandafter{\bl@pp#1}%
  \ifx\relax#2\relax\let\bl@next\relax\else
    \expandafter\def\expandafter\bl@pp\expandafter{\bl@pp\bl@SP}\def\bl@next{\bl@sps@#2\bl@stopall}\fi
  \bl@next}
\def\bl@tokenize#1{\gdef\bl@toks{}\bl@spsplit{#1}%
  \expandafter\bl@tz\bl@pp\bl@stop\bl@stop\bl@stop\bl@stop\bl@stop\bl@stop\bl@stopall}
\def\bl@addtok#1#2{\expandafter\gdef\expandafter\bl@toks\expandafter{\bl@toks{#1}{#2}}}
\def\bl@tz#1{%
  \ifx#1\bl@stop\let\bl@next\bl@tz@end
  \else\ifx#1\bl@SP\let\bl@next\bl@tz
  \else\def\bl@next{\bl@tz@char#1}\fi\fi
  \bl@next}
\def\bl@tz@end#1\bl@stopall{}
\def\bl@tzerr#1{\bl@seterr{#1}\bl@tz@end}
\def\bl@ifletter#1{\ifcat\relax\noexpand#1\expandafter\@secondoftwo\else
  \ifcsname bl@isL@#1\endcsname\expandafter\expandafter\expandafter\@firstoftwo
  \else\expandafter\expandafter\expandafter\@secondoftwo\fi\fi}
\def\bl@tz@char#1{%
  \ifcsname bl@ch@#1\endcsname\expandafter\let\expandafter\bl@next\csname bl@ch@#1\endcsname
  \else\ifcsname bl@isL@#1\endcsname
    \if n#1\def\bl@next{\bl@tz@n#1}%
    \else\if x#1\def\bl@next{\bl@tz@x#1}%
    \else\if a#1\def\bl@next{\bl@tz@a#1}%
    \else\if o#1\def\bl@next{\bl@tz@o#1}%
    \else\def\bl@next{\bl@addtok{v}{#1}\bl@tz}\fi\fi\fi\fi
  \else\def\bl@next{\bl@tzerr{unexpected character \bl@cleanch#1}}\fi\fi
  \bl@next}
\def\bl@tz@n#1#2#3#4#5{%
  \def\bl@next{\bl@addtok{v}{#1}\bl@tz#2#3#4#5}%
  \if o\noexpand#2\if t\noexpand#3\bl@ifletter#4{}{\def\bl@next{\bl@addtok{n}{}\bl@tz#4#5}}\fi\fi
  \if o\noexpand#2\if r\noexpand#3\bl@ifletter#4{}{\def\bl@next{\bl@addtok{r}{}\bl@tz#4#5}}\fi\fi
  \if a\noexpand#2\if n\noexpand#3\if d\noexpand#4\bl@ifletter#5{}{\def\bl@next{\bl@addtok{d}{}\bl@tz#5}}\fi\fi\fi
  \bl@next}
\def\bl@tz@x#1#2#3#4#5{%
  \def\bl@next{\bl@addtok{v}{#1}\bl@tz#2#3#4#5}%
  \if o\noexpand#2\if r\noexpand#3\bl@ifletter#4{}{\def\bl@next{\bl@addtok{x}{}\bl@tz#4#5}}\fi\fi
  \if n\noexpand#2\if o\noexpand#3\if r\noexpand#4\bl@ifletter#5{}{\def\bl@next{\bl@addtok{b}{}\bl@tz#5}}\fi\fi\fi
  \bl@next}
\def\bl@tz@a#1#2#3#4{%
  \def\bl@next{\bl@addtok{v}{#1}\bl@tz#2#3#4}%
  \if n\noexpand#2\if d\noexpand#3\bl@ifletter#4{}{\def\bl@next{\bl@addtok{a}{}\bl@tz#4}}\fi\fi
  \bl@next}
\def\bl@tz@o#1#2#3{%
  \def\bl@next{\bl@addtok{v}{#1}\bl@tz#2#3}%
  \if r\noexpand#2\bl@ifletter#3{}{\def\bl@next{\bl@addtok{o}{}\bl@tz#3}}\fi
  \bl@next}
\def\bl@tz@cmd#1{\bl@ifletter#1{\def\bl@word{#1}\bl@tz@word}%
  {\ifx\bl@stop#1\def\bl@next{\bl@tz\bl@stop}\else\let\bl@next\bl@tz\fi\bl@next}}
\def\bl@tz@word#1{\bl@ifletter#1{\edef\bl@word{\bl@word#1}\bl@tz@word}{\bl@tz@disp#1}}
\def\bl@tz@disp{\ifcsname bl@cw@\bl@word\endcsname
    \edef\bl@tmp{\noexpand\bl@addtok{\csname bl@cw@\bl@word\endcsname}{}}\bl@tmp\let\bl@next\bl@tz
  \else\def\bl@next{\bl@tzerr{unknown command ?\bl@word}}\fi\bl@next}
\def\bl@cleanch#1{\ifcsname bl@cc@#1\endcsname#1\else?\fi}
\def\bl@defch#1#2{\expandafter\def\csname bl@ch@#1\endcsname{#2}}
\bl@defch{+}{\bl@addtok{o}{}\bl@tz}
\bl@defch{|}{\bl@addtok{o}{}\bl@tz}
\bl@defch{*}{\bl@addtok{a}{}\bl@tz}
\bl@defch{.}{\bl@addtok{a}{}\bl@tz}
\bl@defch{&}{\bl@addtok{a}{}\bl@tz}
\bl@defch{!}{\bl@addtok{n}{}\bl@tz}
\expandafter\bl@defch\expandafter{\string~}{\bl@addtok{n}{}\bl@tz}
\expandafter\bl@defch\expandafter{\string^}{\bl@addtok{x}{}\bl@tz}
\bl@defch{'}{\bl@addtok{q}{}\bl@tz}
\bl@defch{(}{\bl@addtok{(}{}\bl@tz}
\bl@defch{)}{\bl@addtok{)}{}\bl@tz}
\bl@defch{0}{\bl@addtok{k}{0}\bl@tz}
\bl@defch{1}{\bl@addtok{k}{1}\bl@tz}
\expandafter\bl@defch\expandafter{\@backslashchar}{\bl@tz@cmd}
\@tfor\bl@c:=ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz\do
  {\expandafter\def\csname bl@isL@\bl@c\endcsname{}}
\@tfor\bl@c:=0123456789,:-.'()\do{\expandafter\def\csname bl@cc@\bl@c\endcsname{}}
\@namedef{bl@cw@lor}{o}\@namedef{bl@cw@vee}{o}\@namedef{bl@cw@or}{o}
\@namedef{bl@cw@land}{a}\@namedef{bl@cw@wedge}{a}\@namedef{bl@cw@and}{a}\@namedef{bl@cw@cdot}{a}
\@namedef{bl@cw@lnot}{n}\@namedef{bl@cw@neg}{n}\@namedef{bl@cw@not}{n}
\@namedef{bl@cw@xor}{x}\@namedef{bl@cw@oplus}{x}\@namedef{bl@cw@veebar}{x}
\@namedef{bl@cw@xnor}{b}\@namedef{bl@cw@odot}{b}\@namedef{bl@cw@equiv}{b}\@namedef{bl@cw@leftrightarrow}{b}\@namedef{bl@cw@iff}{b}
\@namedef{bl@cw@nand}{d}\@namedef{bl@cw@uparrow}{d}\@namedef{bl@cw@barwedge}{d}
\@namedef{bl@cw@nor}{r}\@namedef{bl@cw@downarrow}{r}
%% ---------------------------------------------------------------- parser
\def\bl@peek{\expandafter\bl@peek@\bl@toks\bl@stopall}
\def\bl@peek@#1#2#3\bl@stopall{\def\bl@pt{#1}\def\bl@pv{#2}}
\def\bl@pop{\expandafter\bl@pop@\bl@toks\bl@stopall}
\def\bl@pop@#1#2#3\bl@stopall{\gdef\bl@toks{#3}}
\@namedef{bl@sf@v}{}\@namedef{bl@sf@k}{}\@namedef{bl@sf@(}{}\@namedef{bl@sf@n}{}
\def\bl@pOr{\begingroup\bl@pDisj\let\bl@node\bl@ret\bl@pOr@\let\bl@ret\bl@node\bl@return}
\def\bl@pOr@{\bl@peek\let\bl@next\relax
  \ifbl@err\else
    \if x\bl@pt\bl@pop\def\bl@next{\bl@pDisj\edef\bl@node{x{\bl@node}{\bl@ret}}\bl@pOr@}%
    \else\if b\bl@pt\bl@pop\def\bl@next{\bl@pDisj\edef\bl@node{b{\bl@node}{\bl@ret}}\bl@pOr@}\fi\fi
  \fi\bl@next}
\def\bl@pDisj{\begingroup\bl@pAnd\let\bl@node\bl@ret\bl@pDisj@\let\bl@ret\bl@node\bl@return}
\def\bl@pDisj@{\bl@peek\let\bl@next\relax
  \ifbl@err\else
    \if o\bl@pt\bl@pop\def\bl@next{\bl@pAnd\edef\bl@node{o{\bl@node}{\bl@ret}}\bl@pDisj@}%
    \else\if r\bl@pt\bl@pop\def\bl@next{\bl@pAnd\edef\bl@node{r{\bl@node}{\bl@ret}}\bl@pDisj@}\fi\fi
  \fi\bl@next}
\def\bl@pAnd{\begingroup\bl@pFactor\let\bl@node\bl@ret\bl@pAnd@\let\bl@ret\bl@node\bl@return}
\def\bl@pAnd@{\bl@peek\let\bl@next\relax
  \ifbl@err\else
    \if a\bl@pt\bl@pop\def\bl@next{\bl@pFactor\edef\bl@node{a{\bl@node}{\bl@ret}}\bl@pAnd@}%
    \else\if d\bl@pt\bl@pop\def\bl@next{\bl@pFactor\edef\bl@node{d{\bl@node}{\bl@ret}}\bl@pAnd@}%
    \else\ifcsname bl@sf@\bl@pt\endcsname\def\bl@next{\bl@pFactor\edef\bl@node{a{\bl@node}{\bl@ret}}\bl@pAnd@}\fi\fi\fi
  \fi\bl@next}
\def\bl@pFactor{\begingroup\def\bl@ret{k{0}{}}\bl@peek
  \ifbl@err\let\bl@next\relax
  \else\if e\bl@pt\bl@seterr{unexpected end of expression}\let\bl@next\relax
  \else\if n\bl@pt\bl@pop\def\bl@next{\bl@pFactor\edef\bl@ret{n{\bl@ret}{}}}%
  \else\if v\bl@pt\edef\bl@ret{v{\bl@pv}{}}\bl@pop\let\bl@next\bl@pquotes
  \else\if k\bl@pt\edef\bl@ret{k{\bl@pv}{}}\bl@pop\let\bl@next\bl@pquotes
  \else\if (\bl@pt\bl@pop\def\bl@next{\bl@pOr\bl@pclose}%
  \else\bl@seterr{unexpected symbol}\let\bl@next\relax
  \fi\fi\fi\fi\fi\fi
  \bl@next\bl@return}
\def\bl@pclose{\let\bl@next\relax
  \ifbl@err\else\bl@peek\if )\bl@pt\bl@pop\let\bl@next\bl@pquotes\else\bl@seterr{missing )}\fi\fi\bl@next}
\def\bl@pquotes{\let\bl@next\relax
  \ifbl@err\else\bl@peek\if q\bl@pt\bl@pop\edef\bl@ret{n{\bl@ret}{}}\let\bl@next\bl@pquotes\fi\fi\bl@next}
\def\bl@parse#1{\bl@tokenize{#1}%
  \ifbl@err\else
    \bl@addtok{e}{}%
    \bl@pOr
    \ifbl@err\else\bl@peek\if e\bl@pt\else\bl@seterr{unexpected symbol (check the brackets)}\fi\fi
  \fi}
%% ---------------------------------------------------------------- output
\def\bl@reset{\global\bl@errfalse\gdef\bl@errmsg{}\def\bl@out{}\def\bl@done{0}%
  \let\bl@ret\@empty\def\bl@law{}\def\bl@flag{0}\def\bl@key{}}
\def\bl@emiterr#1{%
  \protected@edef\bl@tmp{\par\noindent\textbf{[#1: \bl@errmsg]}\par}%
  \expandafter\bl@emit\expandafter{\bl@tmp}}
\def\bl@flush{\ifbl@trace
    \immediate\write\bl@tracefile{\detokenize\expandafter{\bl@out}}\immediate\write\bl@tracefile{@@@}%
  \else\bl@out\fi}
\def\bl@printrows#1{%
  \protected@edef\bl@tmp{\noexpand\boolproofstart{\bl@tex{#1}}}%
  \expandafter\bl@emit\expandafter{\bl@tmp}%
  \bl@for\bl@i{1}{\bl@@{rw}{n}}{%
    \protected@edef\bl@tmp{\noexpand\boolrow{\bl@tex{\bl@@{rw}{\bl@i}}}{\bl@@{rl}{\bl@i}}}%
    \expandafter\bl@emit\expandafter{\bl@tmp}}%
  \bl@emit{\boolproofend}}
%% truth table builder
\def\bl@colsof#1{\begingroup\edef\bl@cn{#1}\expandafter\bl@colsof@\bl@cn\endgroup}
\def\bl@colsof@#1#2#3{%
  \if n#1\bl@colvisit{#2}\fi
  \if d#1\bl@colvisit{#2}\bl@colvisit{#3}\else
  \if r#1\bl@colvisit{#2}\bl@colvisit{#3}\else
  \bl@ifbin@#1{}{}{\bl@flatarr{cc}{#1}{#1{#2}{#3}}%
    \bl@for\bl@ci{1}{\bl@@{cc}{n}}{\bl@colvisit{\bl@@{cc}{\bl@ci}}}}{}\fi\fi}
\def\bl@colvisit#1{\edef\bl@cv{#1}\bl@colsof\bl@cv
  \ifnum\expandafter\bl@iscompound\bl@cv=\@ne
    \bl@inarr\bl@cv{cols}\ifnum\bl@flag=0 \bl@gpush{cols}\bl@cv\fi
  \fi}
\def\bl@iscompound#1#2#3{\if n#1\bl@ifbin@#2{1}{0}\else\bl@ifbin@#1{}{}{1}{0}\fi}
\def\bl@buildtable#1{%
  \edef\bl@ncol{\ifnum#1=\@ne\bl@@{cols}{n}\else0\fi}%
  \def\bl@tspec{r|}\def\bl@thdr{$m$}%
  \bl@for\bl@i{1}{\bl@@{vs}{n}}{\edef\bl@tspec{\bl@tspec c}%
    \edef\bl@thdr{\unexpanded\expandafter{\bl@thdr}&$\bl@@{vs}{\bl@i}$}}%
  \ifnum\bl@ncol>0 \edef\bl@tspec{\bl@tspec|}%
    \bl@for\bl@i{1}{\bl@ncol}{\edef\bl@tspec{\bl@tspec c}%
      \edef\bl@thdr{\unexpanded\expandafter{\bl@thdr}&$\bl@htex{\bl@@{cols}{\bl@i}}$}}\fi
  \edef\bl@tspec{\bl@tspec|c}%
  \edef\bl@thdr{\unexpanded\expandafter{\bl@thdr}&\noexpand\textbf{\noexpand\textit{\noexpand\boolfname}}}%
  \def\bl@tbody{}%
  \bl@for\bl@m{0}{\bl@pow-1}{\bl@assign\bl@m
    \edef\bl@row{\bl@m}%
    \bl@for\bl@i{1}{\bl@@{vs}{n}}{\edef\bl@row{\bl@row&\csname bl@val@\bl@@{vs}{\bl@i}\endcsname}}%
    \bl@for\bl@i{1}{\bl@ncol}{\edef\bl@row{\bl@row&\bl@eval{\bl@@{cols}{\bl@i}}}}%
    \edef\bl@row{\unexpanded\expandafter{\bl@row}&\ifnum\bl@eval\bl@Az=\@ne\noexpand\textbf{1}\else0\fi}%
    \edef\bl@tbody{\unexpanded\expandafter{\bl@tbody}\unexpanded\expandafter{\bl@row}\noexpand\\}}%
  \setbox\bl@tbox\hbox{\renewcommand\arraystretch{1.2}%
    \edef\bl@tmp{\noexpand\begin{tabular}{\bl@tspec}}\bl@tmp
    \bl@thdr\\\hline\bl@tbody\end{tabular}}}
\def\bl@truthtable{%
  \gdef\bl@cols@n{0}\bl@colsof\bl@Az
  \bl@buildtable\@ne
  \ifdim\wd\bl@tbox>\linewidth\ifnum\bl@@{cols}{n}>0 \bl@buildtable\z@\fi\fi
  \par\medskip\noindent\hbox to\linewidth{\hss\box\bl@tbox\hss}\par\medskip}
%% \booltruthtable
\newcommand*\booltruthtable{\@ifstar{\bl@startrue\bl@truthtable@}{\bl@starfalse\bl@truthtable@}}
\newcommand*\bl@truthtable@[1]{\par\begingroup\bl@reset
  \edef\bl@in{\detokenize{#1}}%
  \bl@parse\bl@in
  \ifbl@err\else
    \let\bl@Az\bl@ret
    \ifbl@star
      \bl@run{A}{0}{\bl@Az}\let\bl@Af\bl@final
      \ifbl@err\else\bl@run{B}{1}{\bl@Af}\let\bl@Bf\bl@final\fi
    \fi
  \fi
  \ifbl@err\bl@emiterr{booltruthtable}\else\bl@tab@out\fi
  \bl@flush\endgroup}
\def\bl@tab@out{%
  \bl@vars\bl@Az\bl@sortvars
  \protected@edef\bl@tmp{\par\medskip{\raggedright\sloppy\noindent\textbf{Truth table:}\enspace$%
    \ifx\boolfname\@empty\else\boolfname=\fi\bl@tex\bl@Az$\par}}%
  \expandafter\bl@emit\expandafter{\bl@tmp}%
  \ifnum\bl@@{vs}{n}>\booltablemaxvars\relax
    \protected@edef\bl@tmp{\par\smallskip\noindent\emph{(Truth table omitted: \bl@@{vs}{n} variables would need $2^{\bl@@{vs}{n}}=\bl@pow$ rows.)}\par\medskip}%
    \expandafter\bl@emit\expandafter{\bl@tmp}%
  \else
    \bl@emit{\bl@truthtable}%
  \fi
  \ifbl@star
    \ifnum\bl@@{stB}{n}>0 \ifnum\bl@lits\bl@Bf>\bl@lits\bl@Af\relax\else\let\bl@Af\bl@Bf\fi\fi
    \protected@edef\bl@tmp{{\raggedright\sloppy\noindent\textbf{Simplified:}\enspace$%
      \bl@tex\bl@Az=\bl@tex\bl@Af$\par}\medskip}%
    \expandafter\bl@emit\expandafter{\bl@tmp}%
  \fi}
%% \boolsimplify
\newcommand*\boolsimplify{\@ifstar{\bl@startrue\bl@simplify@}{\bl@starfalse\bl@simplify@}}
\newcommand*\bl@simplify@[1]{\par\begingroup\bl@reset
  \edef\bl@in{\detokenize{#1}}%
  \bl@parse\bl@in
  \ifbl@err\else
    \let\bl@Az\bl@ret
    \bl@run{A}{0}{\bl@Az}\let\bl@Af\bl@final
    \ifbl@err\else\bl@run{B}{1}{\bl@Af}\let\bl@Bf\bl@final\fi
  \fi
  \ifbl@err\bl@emiterr{boolsimplify}\else\bl@simp@out\fi
  \bl@flush\endgroup}
\def\bl@simp@out{%
  \bl@arrinit{rw}\bl@arrinit{rl}%
  \bl@for\bl@i{1}{\bl@@{stA}{n}}{\bl@push{rw}{\bl@@{stA}{\bl@i}}\bl@push{rl}{\bl@@{slA}{\bl@i}}}%
  \ifnum\bl@@{stB}{n}>0 \ifnum\bl@lits\bl@Bf>\bl@lits\bl@Af\relax\else
    \bl@for\bl@i{1}{\bl@@{stB}{n}}{\bl@push{rw}{\bl@@{stB}{\bl@i}}\bl@push{rl}{\bl@@{slB}{\bl@i}}}%
    \let\bl@Af\bl@Bf
  \fi\fi
  \protected@edef\bl@tmp{\par\medskip{\raggedright\sloppy\noindent\textbf{Simplify:}\enspace$%
    \bl@tex\bl@Az$\par}}%
  \expandafter\bl@emit\expandafter{\bl@tmp}%
  \ifnum\bl@@{rw}{n}=0
    \bl@emit{\smallskip\noindent This expression is already in its simplest form.\par\medskip}%
  \else
    \ifbl@star\smallskip\else\bl@printrows\bl@Az\fi
    \protected@edef\bl@tmp{{\raggedright\sloppy\noindent\textbf{Simplified:}\enspace$%
      \bl@tex\bl@Az=\bl@tex\bl@Af$\par}\medskip}%
    \expandafter\bl@emit\expandafter{\bl@tmp}%
  \fi}
%% \boolprove
\def\bl@splitq#1=#2\bl@nil\bl@stopall{\def\bl@lhs{#1}\def\bl@rhsraw{#2}}
\def\bl@stripeq#1=\bl@nil{\def\bl@rhs{#1}}
\newcommand*\boolprove[1]{\par\begingroup\bl@reset
  \edef\bl@in{\detokenize{#1}}%
  \expandafter\bl@splitq\bl@in=\bl@nil\bl@stopall
  \ifx\bl@rhsraw\@empty\bl@seterr{write the claim as A = B}\else
    \expandafter\bl@stripeq\bl@rhsraw\bl@nil
    \bl@parse\bl@lhs\let\bl@Az\bl@ret
    \ifbl@err\else\bl@parse\bl@rhs\let\bl@Bz\bl@ret\fi
    \ifbl@err\else\bl@run{A}{1}{\bl@Az}\let\bl@Af\bl@final\fi
    \ifbl@err\else\bl@run{B}{1}{\bl@Bz}\let\bl@Bf\bl@final\fi
    \ifbl@err\else\bl@prove@out\fi
  \fi
  \ifbl@err\bl@emiterr{boolprove}\fi
  \bl@flush\endgroup}
\def\bl@prove@out{%
  \bl@for\bl@j{0}{\bl@@{stB}{n}}{\bl@K{\bl@@{stB}{\bl@j}}\expandafter\let\csname bl@kB@\bl@j\endcsname\bl@key}%
  \def\bl@bi{-1}\def\bl@bj{-1}\def\bl@bc{-1}%
  \bl@for\bl@i{0}{\bl@@{stA}{n}}{\bl@K{\bl@@{stA}{\bl@i}}\let\bl@ka\bl@key
    \bl@for\bl@j{0}{\bl@@{stB}{n}}{%
      \ifnum\pdfstrcmp{\bl@ka}{\bl@@{kB}{\bl@j}}=0
        \edef\bl@c{\the\numexpr\bl@i+\bl@j
          +\ifnum\pdfstrcmp{\bl@@{stA}{\bl@i}}{\bl@@{stB}{\bl@j}}=0 0\else1\fi\relax}%
        \ifnum\ifnum\bl@bc<0 1\else\ifnum\bl@c<\bl@bc\space1\else0\fi\fi=\@ne
          \let\bl@bi\bl@i\let\bl@bj\bl@j\let\bl@bc\bl@c
        \fi
      \fi}}%
  \bl@arrinit{rw}\bl@arrinit{rl}\def\bl@neq{0}%
  \ifnum\bl@bc<0
    \bl@cex
    \ifnum\bl@neq=0
      \bl@for\bl@k{1}{\bl@@{stA}{n}}{\bl@push{rw}{\bl@@{stA}{\bl@k}}\bl@push{rl}{\bl@@{slA}{\bl@k}}}%
      \bl@push{rw}{\bl@Bf}\bl@push{rl}{Both sides have the same truth table}%
      \edef\bl@bj{\bl@@{stB}{n}}%
    \fi
  \else
    \bl@for\bl@k{1}{\bl@bi}{\bl@push{rw}{\bl@@{stA}{\bl@k}}\bl@push{rl}{\bl@@{slA}{\bl@k}}}%
    \ifnum\pdfstrcmp{\bl@@{stA}{\bl@bi}}{\bl@@{stB}{\bl@bj}}=0 \else
      \bl@aclabel{\bl@@{stA}{\bl@bi}}{\bl@@{stB}{\bl@bj}}%
      \bl@push{rw}{\bl@@{stB}{\bl@bj}}\bl@push{rl}{\bl@law}%
    \fi
  \fi
  \ifbl@err\else\ifnum\bl@neq=0
    \bl@for\bl@k{0}{\bl@bj-1}{%
      \edef\bl@kr{\the\numexpr\bl@bj-\bl@k\relax}%
      \edef\bl@prev{\bl@@{stB}{\the\numexpr\bl@kr-1\relax}}%
      \bl@push{rw}{\bl@prev}\bl@push{rl}{\bl@@{slB}{\bl@kr}}}%
    \ifnum\bl@@{rw}{n}=0 \bl@push{rw}{\bl@Bz}\bl@push{rl}{Identical}\fi
    \bl@printrows\bl@Az
  \fi\fi}
\def\bl@cex{%
  \bl@vars\bl@Az\bl@vars\bl@Bz\bl@sortvars
  \ifnum\bl@@{vs}{n}>14 \bl@seterr{too many variables}\else
    \bl@forb\bl@m{0}{\bl@pow-1}{%
      \bl@assign\bl@m
      \edef\bl@ea{\bl@eval\bl@Az}\edef\bl@eb{\bl@eval\bl@Bz}%
      \ifnum\bl@ea=\bl@eb\relax\else
        \def\bl@done{1}\def\bl@neq{1}\def\bl@cexs{}%
        \bl@for\bl@i{1}{\bl@@{vs}{n}}{\edef\bl@cexs{\bl@cexs\ifnum\bl@i>1 , \fi
          $\bl@@{vs}{\bl@i}{=}\csname bl@val@\bl@@{vs}{\bl@i}\endcsname$}}%
        \protected@edef\bl@tmp{\par\medskip\noindent\textbf{The two sides are not equal:} taking \bl@cexs\space the left side is $\bl@ea$ but the right side is $\bl@eb$.\par\medskip}%
        \expandafter\bl@emit\expandafter{\bl@tmp}%
      \fi}%
    \def\bl@done{0}%
  \fi}
%% ---------------------------------------------------------------- formatting
\newdimen\bpIndent \newdimen\bpAvail \newbox\bpEq \newbox\bpLaw \newif\ifbpFirst
\newcommand*\boolproofstart[1]{%
  \par\medskip\def\bpLHS{#1}%
  \setbox\bpEq\hbox{$\displaystyle#1$}\bpIndent=\wd\bpEq
  \ifdim\bpIndent>0.4\linewidth
    \noindent\parbox{\linewidth}{\raggedright\sloppy\noindent$\displaystyle#1$}\par\nointerlineskip\vskip 5pt \bpIndent=1.5em \bpFirstfalse
  \else\bpFirsttrue\fi}
\def\bplead{\ifbpFirst\hbox to\bpIndent{$\displaystyle\bpLHS$\hss}\else\hskip\bpIndent\fi}
\newcommand*\boolrow[2]{%
  \setbox\bpEq\hbox{$\displaystyle{}=#1$}\setbox\bpLaw\hbox{#2}%
  \bpAvail=\dimexpr\linewidth-\bpIndent\relax
  \ifdim\dimexpr\wd\bpEq+1.5em+\wd\bpLaw\relax<\bpAvail
    \hbox to\linewidth{\bplead\box\bpEq\hfil\box\bpLaw}%
  \else\ifdim\wd\bpEq<\bpAvail
    \hbox to\linewidth{\bplead\box\bpEq\hfil}\hbox to\linewidth{\hfil\box\bpLaw}%
  \else
    \hbox to\linewidth{\bplead\parbox[t]{\bpAvail}{\raggedright\sloppy\noindent$\displaystyle{}=#1$}\hfil}%
    \hbox to\linewidth{\hfil\box\bpLaw}%
  \fi\fi
  \bpFirstfalse\nointerlineskip\vskip 5pt }
\newcommand*\boolproofend{\par\medskip}
%% aliases
\providecommand*\truthtable{\booltruthtable}
\providecommand*\btruthtable{\booltruthtable}
\providecommand*\btruth{\booltruthtable}
\providecommand*\btable{\booltruthtable}
\providecommand*\bsimplify{\boolsimplify}
\providecommand*\bprove{\boolprove}

\endinput