\documentclass{article}
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{conjecture}{Conjecture}
\newcommand\unicdcdgdad{\not=}
\newcommand\unicdcdcdbg{\cup}
\newcommand\unicdcdbdgd{\setminus}
\newcommand\unicdcdcdjd{\cap}
\newcommand\unicdcdadad{\forall}
\newcommand\unicdbdjdcd{\Rightarrow}
\newcommand\unicdcdadjd{\notin}
\newcommand\unicdbdjded{\Leftrightarrow}
\newcommand\unicdcdcdid{\lor}
\newcommand\unicdcdcdhd{\land}
\newcommand\uniddcgcg{\lambda}
\newcommand\unicdcdaddd{\exists}
\newcommand\unicdcdidid{\not\subseteq}
\newcommand\preoh[1]{\lnot #1}
\newcommand\mname[1]{{\mathsf{#1}}}
\begin{document}
\title{t4\_gate\_4 (TMPFkLek6biowpqRTSS7kaTt7xz6D496hN6)}
\maketitle
Let $ v1\_xboole\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k4\_gate\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ k2\_gate\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((\preoh v1\_xboole\_0~X0){\unicdcdcdhd}(\preoh v1\_xboole\_0~X1)){\unicdbdjdcd}\\
(v1\_xboole\_0~(k4\_gate\_1~X0~X1))\end{array}
\label{hyp:ggdgjdpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((v1\_xboole\_0~X0){\unicdcdcdhd}(v1\_xboole\_0~X1)){\unicdbdjdcd}(\\
v1\_xboole\_0~(k4\_gate\_1~X0~X1))\end{array}
\label{hyp:ggdgidpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((v1\_xboole\_0~X0){\unicdcdcdhd}(\preoh v1\_xboole\_0~X1)){\unicdbdjdcd}\\
(\preoh v1\_xboole\_0~(k4\_gate\_1~X0~X1))\end{array}
\label{hyp:ggdghdpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  (v1\_xboole\_0~X0){\unicdbdjdcd}(v1\_xboole\_0~(k2\_gate\_1~\\
X0~X1))\end{array}
\label{hyp:ggdgedpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  ((\preoh v1\_xboole\_0~X0){\unicdcdcdhd}(\preoh v1\_xboole\_0~X1)){\unicdbdjdcd}\\
(\preoh v1\_xboole\_0~(k2\_gate\_1~X0~X1))\end{array}
\label{hyp:ggdgddpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{\unicdcdadad} X1 .  {{{{k4\_gate\_1}~{X0}}~{X1}}={{{k4\_gate\_1}~{X1}}~{X0}}}}}\label{hyp:dgpgngngfhehbgehjgghjgehjhpflgedpfhgbgehfgpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{\unicdcdadad} X1 .  {{{{k2\_gate\_1}~{X0}}~{X1}}={{{k2\_gate\_1}~{X1}}~{X0}}}}}\label{hyp:dgpgngngfhehbgehjgghjgehjhpflgcdpfhgbgehfgpfbd}
\end{equation}
\begin{theorem}\label{thm:ehedpfhgbgehfgpfed}
$$\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  {\unicdcdadad} X2 .  {\unicdcdadad} X3 .  {\unicdcdadad} X4 .  {\unicdcdadad} X5 .  \\
{\unicdcdadad} X6 .  {\unicdcdadad} X7 .  {\unicdcdadad} X8 .  {\unicdcdadad} X9 .  {\unicdcdadad} X10 .  {\unicdcdadad} X11 .  \\
{\unicdcdadad} X12 .  {\unicdcdadad} X13 .  {\unicdcdadad} X14 .  {\unicdcdadad} X15 .  {\unicdcdadad} X16 .  \\
{\unicdcdadad} X17 .  {\unicdcdadad} X18 .  {\unicdcdadad} X19 .  {\unicdcdadad} X20 .  {\unicdcdadad} X21 .  \\
{\unicdcdadad} X22 .  {\unicdcdadad} X23 .  {\unicdcdadad} X24 .  {\unicdcdadad} X25 .  {\unicdcdadad} X26 .  \\
{\unicdcdadad} X27 .  {\unicdcdadad} X28 .  {\unicdcdadad} X29 .  {\unicdcdadad} X30 .  {\unicdcdadad} X31 .  \\
{\unicdcdadad} X32 .  {\unicdcdadad} X33 .  {\unicdcdadad} X34 .  {\unicdcdadad} X35 .  {\unicdcdadad} X36 .  \\
{\unicdcdadad} X37 .  {\unicdcdadad} X38 .  {\unicdcdadad} X39 .  {\unicdcdadad} X40 .  {\unicdcdadad} X41 .  \\
{\unicdcdadad} X42 .  {\unicdcdadad} X43 .  {\unicdcdadad} X44 .  {\unicdcdadad} X45 .  {\unicdcdadad} X46 .  \\
{\unicdcdadad} X47 .  {\unicdcdadad} X48 .  {\unicdcdadad} X49 .  {\unicdcdadad} X50 .  (v1\_xboole\_0~\\
X49){\unicdbdjdcd}((v1\_xboole\_0~X0){\unicdcdcdid}(((\preoh v1\_xboole\_0~X33){\unicdcdcdhd}(v1\_xboole\_0~(\\
k4\_gate\_1~X50~X32))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X50~X32)){\unicdcdcdhd}(v1\_xboole\_0~\\
X33)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X34){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X17~(k2\_gate\_1~\\
X1~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X17~(k2\_gate\_1~X1~X33))){\unicdcdcdhd}\\
(v1\_xboole\_0~X34)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X35){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~\\
X18~(k2\_gate\_1~X2~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X18~(k2\_gate\_1~\\
X2~X33))){\unicdcdcdhd}(v1\_xboole\_0~X35)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X36){\unicdcdcdhd}(v1\_xboole\_0~\\
(k4\_gate\_1~X19~(k2\_gate\_1~X3~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~\\
X19~(k2\_gate\_1~X3~X33))){\unicdcdcdhd}(v1\_xboole\_0~X36)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X37){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X20~(k2\_gate\_1~X4~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X20~(k2\_gate\_1~X4~X33))){\unicdcdcdhd}(v1\_xboole\_0~X37)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X38){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X21~(k2\_gate\_1~X5~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X21~(k2\_gate\_1~X5~X33))){\unicdcdcdhd}(v1\_xboole\_0~X38)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X39){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X22~(k2\_gate\_1~X6~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X22~(k2\_gate\_1~X6~X33))){\unicdcdcdhd}(v1\_xboole\_0~X39)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X40){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X23~(k2\_gate\_1~X7~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X23~(k2\_gate\_1~X7~X33))){\unicdcdcdhd}(v1\_xboole\_0~X40)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X41){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X24~(k2\_gate\_1~X8~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X24~(k2\_gate\_1~X8~X33))){\unicdcdcdhd}(v1\_xboole\_0~X41)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X42){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X25~(k2\_gate\_1~X9~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
(k4\_gate\_1~X25~(k2\_gate\_1~X9~X33))){\unicdcdcdhd}(v1\_xboole\_0~X42)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X43){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X26~(k2\_gate\_1~X10~X33)))){\unicdcdcdid}(((\preoh \\
v1\_xboole\_0~(k4\_gate\_1~X26~(k2\_gate\_1~X10~X33))){\unicdcdcdhd}(v1\_xboole\_0~\\
X43)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X44){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X27~(k2\_gate\_1~\\
X11~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X27~(k2\_gate\_1~X11~X33))){\unicdcdcdhd}\\
(v1\_xboole\_0~X44)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X45){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~\\
X28~(k2\_gate\_1~X12~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X28~(k2\_gate\_1~\\
X12~X33))){\unicdcdcdhd}(v1\_xboole\_0~X45)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X46){\unicdcdcdhd}(v1\_xboole\_0~\\
(k4\_gate\_1~X29~(k2\_gate\_1~X13~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~\\
X29~(k2\_gate\_1~X13~X33))){\unicdcdcdhd}(v1\_xboole\_0~X46)){\unicdcdcdid}(((\preoh v1\_xboole\_0~\\
X47){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X30~(k2\_gate\_1~X14~X33)))){\unicdcdcdid}(((\preoh \\
v1\_xboole\_0~(k4\_gate\_1~X30~(k2\_gate\_1~X14~X33))){\unicdcdcdhd}(v1\_xboole\_0~\\
X47)){\unicdcdcdid}(((\preoh v1\_xboole\_0~X48){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~X31~(k2\_gate\_1~\\
X15~X33)))){\unicdcdcdid}(((\preoh v1\_xboole\_0~(k4\_gate\_1~X31~(k2\_gate\_1~X15~X33))){\unicdcdcdhd}\\
(v1\_xboole\_0~X48)){\unicdcdcdid}((\preoh (\preoh v1\_xboole\_0~X48){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~\\
(k4\_gate\_1~X31~(k2\_gate\_1~X15~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X15~\\
X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X31~(k2\_gate\_1~\\
X15~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X15~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X48)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X47){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X30~\\
(k2\_gate\_1~X14~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X14~X50))))){\unicdcdcdhd}((\\
\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X30~(k2\_gate\_1~X14~X32))~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X14~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X47)){\unicdcdcdhd}((\preoh \\
(\preoh v1\_xboole\_0~X46){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X29~(k2\_gate\_1~\\
X13~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X13~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k4\_gate\_1~(k4\_gate\_1~X29~(k2\_gate\_1~X13~X32))~(k4\_gate\_1~X49~(\\
k2\_gate\_1~X13~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X46)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X45){\unicdcdcdhd}\\
(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X28~(k2\_gate\_1~X12~X32))~(k4\_gate\_1~\\
X49~(k2\_gate\_1~X12~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~\\
X28~(k2\_gate\_1~X12~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X12~X50)))){\unicdcdcdhd}\\
(v1\_xboole\_0~X45)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X44){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~\\
(k4\_gate\_1~X27~(k2\_gate\_1~X11~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X11~\\
X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X27~(k2\_gate\_1~\\
X11~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X11~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X44)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X43){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X26~\\
(k2\_gate\_1~X10~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X10~X50))))){\unicdcdcdhd}((\\
\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X26~(k2\_gate\_1~X10~X32))~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X10~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X43)){\unicdcdcdhd}((\preoh \\
(\preoh v1\_xboole\_0~X42){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X25~(k2\_gate\_1~\\
X9~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X9~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
(k4\_gate\_1~(k4\_gate\_1~X25~(k2\_gate\_1~X9~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~\\
X9~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X42)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X41){\unicdcdcdhd}(v1\_xboole\_0~\\
(k4\_gate\_1~(k4\_gate\_1~X24~(k2\_gate\_1~X8~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~\\
X8~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X24~(k2\_gate\_1~\\
X8~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X8~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X41)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X40){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X23~\\
(k2\_gate\_1~X7~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X7~X50))))){\unicdcdcdhd}((\preoh (\\
\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X23~(k2\_gate\_1~X7~X32))~(k4\_gate\_1~\\
X49~(k2\_gate\_1~X7~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X40)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X39){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X22~(k2\_gate\_1~X6~X32))~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X6~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~\\
(k4\_gate\_1~X22~(k2\_gate\_1~X6~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X6~\\
X50)))){\unicdcdcdhd}(v1\_xboole\_0~X39)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X38){\unicdcdcdhd}(v1\_xboole\_0~\\
(k4\_gate\_1~(k4\_gate\_1~X21~(k2\_gate\_1~X5~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~\\
X5~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X21~(k2\_gate\_1~\\
X5~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X5~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X38)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X37){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X20~\\
(k2\_gate\_1~X4~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X4~X50))))){\unicdcdcdhd}((\preoh (\\
\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X20~(k2\_gate\_1~X4~X32))~(k4\_gate\_1~\\
X49~(k2\_gate\_1~X4~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X37)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X36){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X19~(k2\_gate\_1~X3~X32))~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X3~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~\\
(k4\_gate\_1~X19~(k2\_gate\_1~X3~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X3~\\
X50)))){\unicdcdcdhd}(v1\_xboole\_0~X36)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~X35){\unicdcdcdhd}(v1\_xboole\_0~\\
(k4\_gate\_1~(k4\_gate\_1~X18~(k2\_gate\_1~X2~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~\\
X2~X50))))){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X18~(k2\_gate\_1~\\
X2~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X2~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X35)){\unicdcdcdhd}\\
((\preoh (\preoh v1\_xboole\_0~X34){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X17~\\
(k2\_gate\_1~X1~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X1~X50))))){\unicdcdcdhd}((\preoh (\\
\preoh v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X17~(k2\_gate\_1~X1~X32))~(k4\_gate\_1~\\
X49~(k2\_gate\_1~X1~X50)))){\unicdcdcdhd}(v1\_xboole\_0~X34)){\unicdcdcdhd}((\preoh (\preoh v1\_xboole\_0~\\
X33){\unicdcdcdhd}(v1\_xboole\_0~(k4\_gate\_1~(k4\_gate\_1~X49~(k2\_gate\_1~X0~X32))~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X0~X50))))){\unicdcdcdhd}(\preoh (\preoh v1\_xboole\_0~(k4\_gate\_1~\\
(k4\_gate\_1~X49~(k2\_gate\_1~X0~X32))~(k4\_gate\_1~X49~(k2\_gate\_1~X0~\\
X50)))){\unicdcdcdhd}(v1\_xboole\_0~X33))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
