\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{HWC002-0.ax} Definitions of AND, OR and NOT






$\mbox{and}(x,n_0) = n_0\qquad\mbox{cnf}(\mbox{and\_definition}_1,\mbox{axiom})$

$\mbox{and}(x,n_1) = x\qquad\mbox{cnf}(\mbox{and\_definition}_2,\mbox{axiom})$

$\mbox{or}(x,n_0) = x\qquad\mbox{cnf}(\mbox{or\_definition}_1,\mbox{axiom})$

$\mbox{or}(x,n_1) = n_1\qquad\mbox{cnf}(\mbox{or\_definition}_2,\mbox{axiom})$

$\mbox{not}(n_0) = n_1\qquad\mbox{cnf}(\mbox{not\_definition}_1,\mbox{axiom})$

$\mbox{not}(n_1) = n_0\qquad\mbox{cnf}(\mbox{not\_definition}_2,\mbox{axiom})$

\medskip\textbf{HWC001-0.ax} Definitions of AND, OR and NOT






$\mbox{and}(n_0,n_0) = n_0\qquad\mbox{cnf}(\mbox{and\_definition}_1,\mbox{axiom})$

$\mbox{and}(n_0,n_1) = n_0\qquad\mbox{cnf}(\mbox{and\_definition}_2,\mbox{axiom})$

$\mbox{and}(n_1,n_0) = n_0\qquad\mbox{cnf}(\mbox{and\_definition}_3,\mbox{axiom})$

$\mbox{and}(n_1,n_1) = n_1\qquad\mbox{cnf}(\mbox{and\_definition}_4,\mbox{axiom})$

$\mbox{or}(n_0,n_0) = n_0\qquad\mbox{cnf}(\mbox{or\_definition}_1,\mbox{axiom})$

$\mbox{or}(n_0,n_1) = n_1\qquad\mbox{cnf}(\mbox{or\_definition}_2,\mbox{axiom})$

$\mbox{or}(n_1,n_0) = n_1\qquad\mbox{cnf}(\mbox{or\_definition}_3,\mbox{axiom})$

$\mbox{or}(n_1,n_1) = n_1\qquad\mbox{cnf}(\mbox{or\_definition}_4,\mbox{axiom})$

$\mbox{not}(n_0) = n_1\qquad\mbox{cnf}(\mbox{not\_definition}_1,\mbox{axiom})$

$\mbox{not}(n_1) = n_0\qquad\mbox{cnf}(\mbox{not\_definition}_2,\mbox{axiom})$

\medskip\textbf{HWC001-1.p} Design an OR gate using NAND gates






$x\uparrow y = \mbox{not}(\mbox{and}(x,y))\qquad\mbox{cnf}(\mbox{nand\_definition},\mbox{axiom})$

$\mbox{and}(x,n_0) = n_0\qquad\mbox{cnf}(\mbox{and\_definition}_1,\mbox{axiom})$

$\mbox{and}(x,n_1) = x\qquad\mbox{cnf}(\mbox{and\_definition}_2,\mbox{axiom})$

$\mbox{not}(n_0) = n_1\qquad\mbox{cnf}(\mbox{not\_definition}_1,\mbox{axiom})$

$\mbox{not}(n_1) = n_0\qquad\mbox{cnf}(\mbox{not\_definition}_2,\mbox{axiom})$

$( \mbox{output}(x_1,x_2,x_3,x_4)\mbox{ and }\mbox{output}(y_1,y_2,y_3,y_4) ) \ \Rightarrow \ \mbox{output}(x_1\uparrow y_1,x_2\uparrow y_2,x_3\uparrow y_3,x_4\uparrow y_4)\qquad\mbox{cnf}(\mbox{nand\_table\_definition},\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_0,n_1,n_1)\qquad\mbox{cnf}(\mbox{input}_1,\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_1,n_0,n_1)\qquad\mbox{cnf}(\mbox{input}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{output}(n_0,n_1,n_1,n_1)\qquad\mbox{cnf}(\mbox{prove\_cannot\_make\_or},\mbox{negated\_conjecture})$

\medskip\textbf{HWC004-1.p} Definitions of AND, OR and NOT






$\mbox{include}(\mbox{'Axioms/HWC001-0.ax'})$

\medskip\textbf{HWC004-2.p} Definitions of AND, OR and NOT






$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

\medskip\textbf{HWC003-2.p} Invert 3 inputs with 2 not gates






$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

$\mbox{add\_inverter}(\mbox{list}(x,y),z) = \mbox{list}(x,\mbox{add\_inverter}(y,z))\qquad\mbox{cnf}(\mbox{add\_inverter\_definition}_1,\mbox{axiom})$

$\mbox{add\_inverter}(x,y) = \mbox{list}(y,x)\qquad\mbox{cnf}(\mbox{add\_inverter\_definition}_2,\mbox{axiom})$

$\mbox{make\_reverse\_list}(\mbox{list}(\mbox{inverter\_table}(x_{000},x_{001},x_{010},x_{011},x_{100},x_{101},x_{110},x_{111}),v)) = \mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r00m},x_{000},x_{001}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r01m},x_{010},x_{011}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r10m},x_{100},x_{101}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r11m},x_{110},x_{111}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r0m}_0,x_{000},x_{010}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r0m}_1,x_{001},x_{011}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r1m}_0,x_{100},x_{110}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r1m}_1,x_{101},x_{111}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{00},x_{000},x_{100}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{01},x_{001},x_{101}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{10},x_{010},x_{110}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{11},x_{011},x_{111}),\mbox{make\_reverse\_list}(v)))))))))))))\qquad\mbox{cnf}(\mbox{make\_reverse\_list\_definition}_1,\mbox{axiom})$

$\mbox{make\_reverse\_list}(v) = \mbox{end}\qquad\mbox{cnf}(\mbox{make\_reverse\_list\_definition}_2,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},n_1,n_0) = \mbox{xname}\qquad\mbox{cnf}(\mbox{possible\_reversion}_1,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},n_0,n_1) = \mbox{not\_reversion}\qquad\mbox{cnf}(\mbox{possible\_reversion}_2,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},x,x) = \mbox{not\_reversion}\qquad\mbox{cnf}(\mbox{possible\_reversion}_3,\mbox{axiom})$

$\mbox{list\_reversion}(\mbox{not\_reversion},x) = x\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_1,\mbox{axiom})$

$\mbox{list\_reversion}(x,\mbox{list\_reversion}(y,z)) = \mbox{list\_reversion}(y,\mbox{list\_reversion}(x,z))\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_2,\mbox{axiom})$

$\mbox{list\_reversion}(x,\mbox{list\_reversion}(x,y)) = \mbox{list\_reversion}(x,y)\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_3,\mbox{axiom})$

$( \mbox{basic\_output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\mbox{ and }\mbox{basic\_output}(y_1,y_2,y_3,y_4,y_5,y_6,y_7,y_8,v) ) \ \Rightarrow \ \mbox{basic\_output}(\mbox{and}(x_1,y_1),\mbox{and}(x_2,y_2),\mbox{and}(x_3,y_3),\mbox{and}(x_4,y_4),\mbox{and}(x_5,y_5),\mbox{and}(x_6,y_6),\mbox{and}(x_7,y_7),\mbox{and}(x_8,y_8),v)\qquad\mbox{cnf}(\mbox{and\_output\_definition},\mbox{axiom})$

$( \mbox{basic\_output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\mbox{ and }\mbox{output}(y_1,y_2,y_3,y_4,y_5,y_6,y_7,y_8,v) ) \ \Rightarrow \ \mbox{output}(\mbox{or}(x_1,y_1),\mbox{or}(x_2,y_2),\mbox{or}(x_3,y_3),\mbox{or}(x_4,y_4),\mbox{or}(x_5,y_5),\mbox{or}(x_6,y_6),\mbox{or}(x_7,y_7),\mbox{or}(x_8,y_8),v)\qquad\mbox{cnf}(\mbox{or\_output\_definition},\mbox{axiom})$

$\mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v) \ \Rightarrow \ \mbox{test}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8),\mbox{add\_inverter}(v,\mbox{inverter\_table}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8))),\mbox{make\_reverse\_list}(\mbox{list}(\mbox{inverter\_table}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8)),v)))\qquad\mbox{cnf}(\mbox{inverter\_test},\mbox{axiom})$

$\mbox{basic\_output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v) \ \Rightarrow \ \mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\qquad\mbox{cnf}(\mbox{basic\_output\_definition},\mbox{axiom})$

$\mbox{test}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v,\mbox{xrevlist}) \ \Rightarrow \ \mbox{basic\_output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\qquad\mbox{cnf}(\mbox{create\_test},\mbox{axiom})$

$\mbox{output}(n_0,n_0,n_0,n_0,n_1,n_1,n_1,n_1,x)\qquad\mbox{cnf}(\mbox{input}_1,\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_0,n_1,n_1,n_0,n_0,n_1,n_1,x)\qquad\mbox{cnf}(\mbox{input}_2,\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_1,n_0,n_1,n_0,n_1,n_0,n_1,x)\qquad\mbox{cnf}(\mbox{input}_3,\mbox{negated\_conjecture})$

$( \mbox{output}(n_1,n_1,n_1,n_1,n_0,n_0,n_0,n_0,v)\mbox{ and }\mbox{output}(n_1,n_1,n_0,n_0,n_1,n_1,n_0,n_0,v) ) \ \Rightarrow \ \neg\,\mbox{output}(n_1,n_0,n_1,n_0,n_1,n_0,n_1,n_0,v)\qquad\mbox{cnf}(\mbox{prove\_cannot\_construct\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HWC003-1.p} Invert 3 inputs with 2 not gates






$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

$\mbox{add\_inverter}(\mbox{list}(x,y),z) = \mbox{list}(x,\mbox{add\_inverter}(y,z))\qquad\mbox{cnf}(\mbox{add\_inverter\_definition}_1,\mbox{axiom})$

$\mbox{add\_inverter}(x,y) = \mbox{list}(y,x)\qquad\mbox{cnf}(\mbox{add\_inverter\_definition}_2,\mbox{axiom})$

$\mbox{make\_reverse\_list}(\mbox{list}(\mbox{inverter\_table}(x_{000},x_{001},x_{010},x_{011},x_{100},x_{101},x_{110},x_{111}),v)) = \mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r00m},x_{000},x_{001}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r01m},x_{010},x_{011}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r10m},x_{100},x_{101}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r11m},x_{110},x_{111}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r0m}_0,x_{000},x_{010}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r0m}_1,x_{001},x_{011}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r1m}_0,x_{100},x_{110}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{r1m}_1,x_{101},x_{111}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{00},x_{000},x_{100}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{01},x_{001},x_{101}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{10},x_{010},x_{110}),\mbox{list\_reversion}(\mbox{possible\_reversion}(\mbox{rm}_{11},x_{011},x_{111}),\mbox{make\_reverse\_list}(v)))))))))))))\qquad\mbox{cnf}(\mbox{make\_reverse\_list\_definition}_1,\mbox{axiom})$

$\mbox{make\_reverse\_list}(v) = \mbox{end}\qquad\mbox{cnf}(\mbox{make\_reverse\_list\_definition}_2,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},n_1,n_0) = \mbox{xname}\qquad\mbox{cnf}(\mbox{possible\_reversion}_1,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},n_0,n_1) = \mbox{not\_reversion}\qquad\mbox{cnf}(\mbox{possible\_reversion}_2,\mbox{axiom})$

$\mbox{possible\_reversion}(\mbox{xname},x,x) = \mbox{not\_reversion}\qquad\mbox{cnf}(\mbox{possible\_reversion}_3,\mbox{axiom})$

$\mbox{list\_reversion}(\mbox{not\_reversion},x) = x\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_1,\mbox{axiom})$

$\mbox{list\_reversion}(x,\mbox{list\_reversion}(y,z)) = \mbox{list\_reversion}(y,\mbox{list\_reversion}(x,z))\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_2,\mbox{axiom})$

$\mbox{list\_reversion}(x,\mbox{list\_reversion}(x,y)) = \mbox{list\_reversion}(x,y)\qquad\mbox{cnf}(\mbox{list\_reversion\_definition}_3,\mbox{axiom})$

$( \mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\mbox{ and }\mbox{output}(y_1,y_2,y_3,y_4,y_5,y_6,y_7,y_8,v) ) \ \Rightarrow \ \mbox{output}(\mbox{and}(x_1,y_1),\mbox{and}(x_2,y_2),\mbox{and}(x_3,y_3),\mbox{and}(x_4,y_4),\mbox{and}(x_5,y_5),\mbox{and}(x_6,y_6),\mbox{and}(x_7,y_7),\mbox{and}(x_8,y_8),v)\qquad\mbox{cnf}(\mbox{and\_output\_definition},\mbox{axiom})$

$( \mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\mbox{ and }\mbox{output}(y_1,y_2,y_3,y_4,y_5,y_6,y_7,y_8,v) ) \ \Rightarrow \ \mbox{output}(\mbox{or}(x_1,y_1),\mbox{or}(x_2,y_2),\mbox{or}(x_3,y_3),\mbox{or}(x_4,y_4),\mbox{or}(x_5,y_5),\mbox{or}(x_6,y_6),\mbox{or}(x_7,y_7),\mbox{or}(x_8,y_8),v)\qquad\mbox{cnf}(\mbox{or\_output\_definition},\mbox{axiom})$

$\mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v) \ \Rightarrow \ \mbox{test}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8),\mbox{add\_inverter}(v,\mbox{inverter\_table}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8))),\mbox{make\_reverse\_list}(\mbox{list}(\mbox{inverter\_table}(\mbox{not}(x_1),\mbox{not}(x_2),\mbox{not}(x_3),\mbox{not}(x_4),\mbox{not}(x_5),\mbox{not}(x_6),\mbox{not}(x_7),\mbox{not}(x_8)),v)))\qquad\mbox{cnf}(\mbox{inverter\_test},\mbox{axiom})$

$\mbox{test}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v,\mbox{xrevlist}) \ \Rightarrow \ \mbox{output}(x_1,x_2,x_3,x_4,x_5,x_6,x_7,x_8,v)\qquad\mbox{cnf}(\mbox{create\_test},\mbox{axiom})$

$\mbox{output}(n_0,n_0,n_0,n_0,n_1,n_1,n_1,n_1,x)\qquad\mbox{cnf}(\mbox{input}_1,\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_0,n_1,n_1,n_0,n_0,n_1,n_1,x)\qquad\mbox{cnf}(\mbox{input}_2,\mbox{negated\_conjecture})$

$\mbox{output}(n_0,n_1,n_0,n_1,n_0,n_1,n_0,n_1,x)\qquad\mbox{cnf}(\mbox{input}_3,\mbox{negated\_conjecture})$

$( \mbox{output}(n_1,n_1,n_1,n_1,n_0,n_0,n_0,n_0,v)\mbox{ and }\mbox{output}(n_1,n_1,n_0,n_0,n_1,n_1,n_0,n_0,v) ) \ \Rightarrow \ \neg\,\mbox{output}(n_1,n_0,n_1,n_0,n_1,n_0,n_1,n_0,v)\qquad\mbox{cnf}(\mbox{prove\_cannot\_construct\_this},\mbox{negated\_conjecture})$

\medskip
\end{document}