\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{HEN003-0.ax} Henkin model (equality) axioms






$\mbox{divide}(\mbox{divide}(x,y),x) = 0\qquad\mbox{cnf}(\mbox{quotient\_smaller\_than\_numerator},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(\mbox{divide}(x,z),\mbox{divide}(y,z)),\mbox{divide}(\mbox{divide}(x,y),z)) = 0\qquad\mbox{cnf}(\mbox{quotient\_property},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_is\_smallest},\mbox{axiom})$

$( \mbox{divide}(x,y) = 0\mbox{ and }\mbox{divide}(y,x) = 0 ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{divide\_and\_equal},\mbox{axiom})$

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{identity\_is\_largest},\mbox{axiom})$

\medskip\textbf{HEN002-0.ax} Henkin model axioms






$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{divide}(x,y) = 0\qquad\mbox{cnf}(\mbox{quotient\_less\_equal}_1,\mbox{axiom})$

$\mbox{divide}(x,y) = 0 \ \Rightarrow \ \mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{quotient\_less\_equal}_2,\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),x)\qquad\mbox{cnf}(\mbox{quotient\_smaller\_than\_numerator},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(\mbox{divide}(x,z),\mbox{divide}(y,z)),\mbox{divide}(\mbox{divide}(x,y),z))\qquad\mbox{cnf}(\mbox{quotient\_property},\mbox{axiom})$

$\mbox{less\_equal}(0,x)\qquad\mbox{cnf}(\mbox{zero\_is\_smallest},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,x) ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{less\_equal\_and\_equal},\mbox{axiom})$

$\mbox{less\_equal}(x,\mbox{identity})\qquad\mbox{cnf}(\mbox{identity\_is\_largest},\mbox{axiom})$

\medskip\textbf{HEN001-0.ax} Henkin model axioms






$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{quotient}(x,y,0)\qquad\mbox{cnf}(\mbox{quotient\_less\_equal},\mbox{axiom})$

$\mbox{quotient}(x,y,0) \ \Rightarrow \ \mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{less\_equal\_quotient},\mbox{axiom})$

$\mbox{quotient}(x,y,z) \ \Rightarrow \ \mbox{less\_equal}(z,x)\qquad\mbox{cnf}(\mbox{divisor\_existence},\mbox{axiom})$

$( \mbox{quotient}(x,y,v_1)\mbox{ and }\mbox{quotient}(y,z,v_2)\mbox{ and }\mbox{quotient}(x,z,v_3)\mbox{ and }\mbox{quotient}(v_3,v_2,v_4)\mbox{ and }\mbox{quotient}(v_1,z,v_5) ) \ \Rightarrow \ \mbox{less\_equal}(v_4,v_5)\qquad\mbox{cnf}(\mbox{quotient\_property},\mbox{axiom})$

$\mbox{less\_equal}(0,x)\qquad\mbox{cnf}(\mbox{zero\_is\_smallest},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,x) ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{less\_equal\_and\_equal},\mbox{axiom})$

$\mbox{less\_equal}(x,\mbox{identity})\qquad\mbox{cnf}(\mbox{identity\_is\_largest},\mbox{axiom})$

$\mbox{quotient}(x,y,\mbox{divide}(x,y))\qquad\mbox{cnf}(\mbox{closure},\mbox{axiom})$

$( \mbox{quotient}(x,y,z)\mbox{ and }\mbox{quotient}(x,y,w) ) \ \Rightarrow \ z = w\qquad\mbox{cnf}(\mbox{well\_defined},\mbox{axiom})$

\medskip\textbf{HEN010-6.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(z,y),\mbox{divide}(z,x))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),\mbox{divide}(y,z))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_property\_of\_inversion},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-5.p} Define X' as identity/X. Then X' = X'''






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

$( \mbox{divide}(x,y) = 0\mbox{ and }\mbox{divide}(y,z) = 0 ) \ \Rightarrow \ \mbox{divide}(x,z) = 0\qquad\mbox{cnf}(\mbox{transitivity\_of\_divide\_to\_zero},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(x,y),z) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(x,z),y) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{divide}(x,y) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(z,y),\mbox{divide}(z,x)) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-1.p} Define X' as identity/X. Then X' = X'''






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

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQ\_idQa},\mbox{idQ\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa}\ne \mbox{idQ\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_one\_inversion\_equals\_three},\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-7.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(z,y,w_1)\mbox{ and }\mbox{quotient}(z,x,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_zQyLEzQx},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(x,z,w_1)\mbox{ and }\mbox{quotient}(y,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_xQzLEyQz},\mbox{axiom})$

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQa},\mbox{idQ\_idQa},\mbox{idQa\_Q\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa}\ne \mbox{idQa\_Q\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_idQa\_equals\_idQa\_Q\_\_idQ\_idQa},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-6.p} X/zero = X






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0)\ne a\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-5.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$( \mbox{divide}(x,y) = 0\mbox{ and }\mbox{divide}(y,z) = 0 ) \ \Rightarrow \ \mbox{divide}(x,z) = 0\qquad\mbox{cnf}(\mbox{transitivity\_of\_divide\_to\_zero},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(x,y),z) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(x,z),y) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{divide}(x,y) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(x,z),\mbox{divide}(y,z)) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-3.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_property\_of\_inversion},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-2.p} The relation less\_equal is transitive






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$\mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{xLEy},\mbox{hypothesis})$

$\mbox{less\_equal}(y,z)\qquad\mbox{cnf}(\mbox{yLEz},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{prove\_transitivity\_of\_less\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-4.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(z,y),\mbox{divide}(z,x))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),\mbox{divide}(y,z))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_property\_of\_inversion},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-5.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{divide}(a,b) = 0\qquad\mbox{cnf}(\mbox{a\_divide\_b\_is\_zero},\mbox{hypothesis})$

$\mbox{divide}(\mbox{divide}(a,c),\mbox{divide}(b,c))\ne 0\qquad\mbox{cnf}(\mbox{prove\_property\_of\_divide}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-1.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQa},\mbox{idQ\_idQa},\mbox{idQa\_Q\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa}\ne \mbox{idQa\_Q\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_idQa\_equals\_idQa\_Q\_\_idQ\_idQa},\mbox{negated\_conjecture})$

\medskip\textbf{HEN003-4.p} X/X = zero






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_x\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-3.p} Define X' as identity/X. Then X' = X'''






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

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{part\_of\_theorem},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},a) = b\qquad\mbox{cnf}(\mbox{id\_divide\_a\_is\_b},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},b) = c\qquad\mbox{cnf}(\mbox{id\_divide\_b\_is\_c},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},c) = d\qquad\mbox{cnf}(\mbox{id\_divide\_c\_is\_d},\mbox{hypothesis})$

$b\ne d\qquad\mbox{cnf}(\mbox{prove\_b\_equals\_d},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-3.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,c),\mbox{divide}(b,c))\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_c\_LE\_b\_divide\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN002-5.p} zero/X = zero






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

$\mbox{divide}(0,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_zero\_divide\_anything\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-1.p} X/zero = X






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

$\neg\,\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{prove\_x\_divde\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-3.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{less\_equal}(\mbox{divide}(a,b),d)\qquad\mbox{cnf}(\mbox{a\_divide\_b\_LE\_d},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,d),b)\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_d\_LE\_b},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-1.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{aLEb},\mbox{hypothesis})$

$\mbox{quotient}(a,c,\mbox{aQc})\qquad\mbox{cnf}(\mbox{aQc},\mbox{hypothesis})$

$\mbox{quotient}(b,c,\mbox{bQc})\qquad\mbox{cnf}(\mbox{bQc},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{aQc},\mbox{bQc})\qquad\mbox{cnf}(\mbox{prove\_aQcLEbQc},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-4.p} Define X' as identity/X. Then X' = X'''






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(z,y),\mbox{divide}(z,x))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),\mbox{divide}(y,z))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-6.p} Define X' as identity/X. Then X' = X'''






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),\mbox{divide}(y,z))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},a)\ne \mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{part\_of\_theorem},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},a) = b\qquad\mbox{cnf}(\mbox{id\_divide\_a\_is\_b},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},b) = c\qquad\mbox{cnf}(\mbox{id\_divide\_b\_is\_c},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},c) = d\qquad\mbox{cnf}(\mbox{id\_divide\_c\_is\_d},\mbox{hypothesis})$

$b\ne d\qquad\mbox{cnf}(\mbox{prove\_b\_equals\_d},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-4.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(z,y),\mbox{divide}(z,x))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,c),\mbox{divide}(b,c))\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_c\_LE\_b\_divide\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN007-6.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{xLEy},\mbox{hypothesis})$

$\mbox{quotient}(z,y,\mbox{zQy})\qquad\mbox{cnf}(\mbox{zQy},\mbox{hypothesis})$

$\mbox{quotient}(z,x,\mbox{zQx})\qquad\mbox{cnf}(\mbox{zQx},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{zQy},\mbox{zQx})\qquad\mbox{cnf}(\mbox{prove\_zQyLEzQx},\mbox{negated\_conjecture})$

\medskip\textbf{HEN002-1.p} zero/X = zero






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

$\neg\,\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{prove\_zero\_divide\_anything\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN011-3.p} This operation is commutative

Define \& on the set of Z', where Z' = identity/Z,
 by X' \& Y'=X'/(identity/Y'). The operation is commutative.




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

$\mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},b)))\ne \mbox{divide}(\mbox{divide}(\mbox{identity},b),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{part\_of\_theorem},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},a) = c\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},b) = d\qquad\mbox{cnf}(\mbox{identity\_divide\_b},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},c) = e\qquad\mbox{cnf}(\mbox{identity\_divide\_c},\mbox{hypothesis})$

$\mbox{divide}(\mbox{identity},d) = g\qquad\mbox{cnf}(\mbox{identity\_divide\_d},\mbox{hypothesis})$

$\mbox{divide}(c,g)\ne \mbox{divide}(d,e)\qquad\mbox{cnf}(\mbox{prove\_commutativity},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-6.p} The relation less\_equal is transitive






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\mbox{less\_equal}(b,c)\qquad\mbox{cnf}(\mbox{b\_LE\_c},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(a,c)\qquad\mbox{cnf}(\mbox{prove\_a\_LE\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-4.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(a,b),d)\qquad\mbox{cnf}(\mbox{a\_divide\_b\_LE\_d},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,d),b)\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_d\_LE\_b},\mbox{negated\_conjecture})$

\medskip\textbf{HEN003-1.p} X/X = zero






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

$\neg\,\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_x\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN001-3.p} X/identity = zero






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

$\mbox{divide}(a,\mbox{identity})\ne 0\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_id\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-4.p} The relation less\_equal is transitive






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,0) = x\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\mbox{less\_equal}(b,c)\qquad\mbox{cnf}(\mbox{b\_LE\_c},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(a,c)\qquad\mbox{cnf}(\mbox{prove\_a\_LE\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-3.p} The relation less\_equal is transitive






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

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\mbox{less\_equal}(b,c)\qquad\mbox{cnf}(\mbox{b\_LE\_c},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(a,c)\qquad\mbox{cnf}(\mbox{prove\_a\_LE\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN012-1.p} X $\leq$ X






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

$\neg\,\mbox{less\_equal}(x,x)\qquad\mbox{cnf}(\mbox{prove\_X\_less\_than\_or\_equal\_to\_X},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-1.p} The relation less\_equal is transitive






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

$\mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{xLEy},\mbox{hypothesis})$

$\mbox{less\_equal}(y,z)\qquad\mbox{cnf}(\mbox{yLEz},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{prove\_transitivity\_of\_less\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{HEN011-2.p} This operation is commutative

Define \& on the set of Z', where Z' = identity/Z,
 by X' \& Y' = X'/(identity/Y'). The operation is commutative.




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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(z,y,w_1)\mbox{ and }\mbox{quotient}(z,x,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_zQyLEzQx},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(x,z,w_1)\mbox{ and }\mbox{quotient}(y,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_xQzLEyQz},\mbox{axiom})$

$( \mbox{quotient}(\mbox{identity},x,y_1)\mbox{ and }\mbox{quotient}(\mbox{identity},y_1,y_2)\mbox{ and }\mbox{quotient}(\mbox{identity},y_2,y_3) ) \ \Rightarrow \ y_1 = y_3\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$( \mbox{quotient}(\mbox{identity},x,y_1)\mbox{ and }\mbox{quotient}(\mbox{identity},y_1,y_2)\mbox{ and }\mbox{quotient}(y_1,y_2,y_3) ) \ \Rightarrow \ y_1 = y_3\qquad\mbox{cnf}(\mbox{inversion\_lemma},\mbox{axiom})$

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},b,\mbox{idQb})\qquad\mbox{cnf}(\mbox{identity\_divide\_b},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQb},\mbox{idQ\_idQb})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQb},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQa},\mbox{idQ\_idQb},\mbox{idQa\_Q\_\_idQ\_idQb})\qquad\mbox{cnf}(\mbox{idQa\_divide\_idQ\_idQb},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQb},\mbox{idQ\_idQa},\mbox{idQb\_Q\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{idQb\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa\_Q\_\_idQ\_idQb}\ne \mbox{idQb\_Q\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_idQa\_Q\_\_idQ\_idQb\_equals\_idQb\_Q\_\_idQ\_idQa},\mbox{negated\_conjecture})$

\medskip\textbf{HEN007-1.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$\mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{xLEy},\mbox{hypothesis})$

$\mbox{quotient}(z,y,\mbox{zQy})\qquad\mbox{cnf}(\mbox{zQy},\mbox{hypothesis})$

$\mbox{quotient}(z,x,\mbox{zQx})\qquad\mbox{cnf}(\mbox{zQx},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{zQy},\mbox{zQx})\qquad\mbox{cnf}(\mbox{prove\_zQyLEzQx},\mbox{negated\_conjecture})$

\medskip\textbf{HEN002-2.p} zero/X = zero






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\neg\,\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{prove\_zero\_divide\_anything\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN007-4.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(c,b),\mbox{divide}(c,a))\qquad\mbox{cnf}(\mbox{prove\_c\_divide\_b\_LE\_c\_divide\_a},\mbox{negated\_conjecture})$

\medskip\textbf{HEN010-2.p} Define X' as identity/X. Then X' = X'/(identity/X')






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(z,y,w_1)\mbox{ and }\mbox{quotient}(z,x,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_zQyLEzQx},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(x,z,w_1)\mbox{ and }\mbox{quotient}(y,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_xQzLEyQz},\mbox{axiom})$

$( \mbox{quotient}(\mbox{identity},x,y_1)\mbox{ and }\mbox{quotient}(\mbox{identity},y_1,y_2)\mbox{ and }\mbox{quotient}(\mbox{identity},y_2,y_3) ) \ \Rightarrow \ y_1 = y_3\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQa},\mbox{idQ\_idQa},\mbox{idQa\_Q\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa}\ne \mbox{idQa\_Q\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_idQa\_equals\_idQa\_Q\_\_idQ\_idQa},\mbox{negated\_conjecture})$

\medskip\textbf{HEN013-2.p} Henkin model axioms






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

\medskip\textbf{HEN007-5.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$( \mbox{divide}(x,y) = 0\mbox{ and }\mbox{divide}(y,z) = 0 ) \ \Rightarrow \ \mbox{divide}(x,z) = 0\qquad\mbox{cnf}(\mbox{transitivity\_of\_divide\_to\_zero},\mbox{axiom})$

$\mbox{divide}(a,b) = 0\qquad\mbox{cnf}(\mbox{a\_divide\_b\_is\_zero},\mbox{hypothesis})$

$\mbox{divide}(\mbox{divide}(c,b),\mbox{divide}(c,a))\ne 0\qquad\mbox{cnf}(\mbox{prove\_property\_of\_divide}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HEN001-1.p} X/identity = zero






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

$\neg\,\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{prove\_everything\_divide\_identity\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-2.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{quotient}(x,y,\mbox{xQy})\qquad\mbox{cnf}(\mbox{xQy},\mbox{hypothesis})$

$\mbox{less\_equal}(\mbox{xQy},z)\qquad\mbox{cnf}(\mbox{xQyLEz},\mbox{hypothesis})$

$\mbox{quotient}(x,z,\mbox{xQz})\qquad\mbox{cnf}(\mbox{xQz},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{xQz},y)\qquad\mbox{cnf}(\mbox{prove\_xQzLEy},\mbox{negated\_conjecture})$

\medskip\textbf{HEN013-1.p} Henkin model axioms






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

\medskip\textbf{HEN002-3.p} zero/X = zero






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

$\mbox{divide}(0,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_zero\_over\_a\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-2.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(z,y,w_1)\mbox{ and }\mbox{quotient}(z,x,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_zQyLEzQx},\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{aLEb},\mbox{hypothesis})$

$\mbox{quotient}(a,c,\mbox{aQc})\qquad\mbox{cnf}(\mbox{aQc},\mbox{hypothesis})$

$\mbox{quotient}(b,c,\mbox{bQc})\qquad\mbox{cnf}(\mbox{bQc},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{aQc},\mbox{bQc})\qquad\mbox{cnf}(\mbox{prove\_aQcLEbQc},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-5.p} X/zero = X






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

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0)\ne a\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN011-1.p} This operation is commutative

Define \& on the set of Z', where Z' = identity/Z,
 by X' \& Y' = X'/(identity/Y'). The operation is commutative.




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

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},b,\mbox{idQb})\qquad\mbox{cnf}(\mbox{identity\_divide\_b},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQb},\mbox{idQ\_idQb})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQb},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQa},\mbox{idQ\_idQb},\mbox{idQa\_Q\_\_idQ\_idQb})\qquad\mbox{cnf}(\mbox{idQa\_divide\_idQ\_idQb},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{idQb},\mbox{idQ\_idQa},\mbox{idQb\_Q\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{idQb\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa\_Q\_\_idQ\_idQb}\ne \mbox{idQb\_Q\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_idQa\_Q\_\_idQ\_idQb\_equals\_idQb\_Q\_\_idQ\_idQa},\mbox{negated\_conjecture})$

\medskip\textbf{HEN003-5.p} X/X = zero






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

$\mbox{divide}(a,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_x\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN001-5.p} X/identity = zero






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

$\mbox{divide}(a,\mbox{identity})\ne 0\qquad\mbox{cnf}(\mbox{prove\_everything\_divide\_id\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN002-4.p} zero/X = zero






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_zero\_over\_a\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-5.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{divide}(x,0) = x\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(a,b),d) = 0\qquad\mbox{cnf}(\mbox{a\_divide\_b\_divide\_d\_is\_zero},\mbox{hypothesis})$

$\mbox{divide}(\mbox{divide}(a,d),b)\ne 0\qquad\mbox{cnf}(\mbox{prove\_property\_of\_divide}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-6.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(a,b),d)\qquad\mbox{cnf}(\mbox{a\_divide\_b\_LE\_d},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,d),b)\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_d\_LE\_b},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-3.p} X/zero = X






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

$\mbox{divide}(a,0)\ne a\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN011-4.p} This operation is commutative

Define \& on the set of Z', where Z' = identity/Z,
 by X' \& Y' = X'/(identity/Y'). The operation is commutative.




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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0) = a\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$\mbox{less\_equal}(\mbox{divide}(x,y),z) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),y)\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(z,y),\mbox{divide}(z,x))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{less\_equal}(x,y) \ \Rightarrow \ \mbox{less\_equal}(\mbox{divide}(x,z),\mbox{divide}(y,z))\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(\mbox{identity},x),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{property\_of\_inversion},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},b)))\ne \mbox{divide}(\mbox{divide}(\mbox{identity},b),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HEN009-2.p} Define X' as identity/X. Then X' = X'''






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(z,y,w_1)\mbox{ and }\mbox{quotient}(z,x,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_zQyLEzQx},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{quotient}(x,z,w_1)\mbox{ and }\mbox{quotient}(y,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_1,w_2)\qquad\mbox{cnf}(\mbox{xLEy\_implies\_xQzLEyQz},\mbox{axiom})$

$\mbox{quotient}(\mbox{identity},a,\mbox{idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_a},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQa},\mbox{idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQa},\mbox{hypothesis})$

$\mbox{quotient}(\mbox{identity},\mbox{idQ\_idQa},\mbox{idQ\_\_idQ\_idQa})\qquad\mbox{cnf}(\mbox{identity\_divide\_idQ\_idQa},\mbox{hypothesis})$

$\mbox{idQa}\ne \mbox{idQ\_\_idQ\_idQa}\qquad\mbox{cnf}(\mbox{prove\_one\_inversion\_equals\_three},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-4.p} X/zero = X






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(a,0)\ne a\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN013-3.p} Henkin model (equality) axioms






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

\medskip\textbf{HEN006-1.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{quotient}(x,y,\mbox{xQy})\qquad\mbox{cnf}(\mbox{xQy},\mbox{hypothesis})$

$\mbox{less\_equal}(\mbox{xQy},z)\qquad\mbox{cnf}(\mbox{xQyLEz},\mbox{hypothesis})$

$\mbox{quotient}(x,z,\mbox{xQz})\qquad\mbox{cnf}(\mbox{xQz},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{xQz},y)\qquad\mbox{cnf}(\mbox{prove\_xQzLEy},\mbox{negated\_conjecture})$

\medskip\textbf{HEN003-2.p} X/X = zero






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\neg\,\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_x\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN003-3.p} X/X = zero






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

$\mbox{divide}(a,a)\ne 0\qquad\mbox{cnf}(\mbox{prove\_x\_divide\_x\_is\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN008-6.p} X $\leq$ Y =$>$ X/Z $\leq$ Y/Z






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

$\mbox{divide}(x,\mbox{identity}) = 0\qquad\mbox{cnf}(\mbox{everything\_divide\_id\_is\_zero},\mbox{axiom})$

$\mbox{divide}(0,x) = 0\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(a,c),\mbox{divide}(b,c))\qquad\mbox{cnf}(\mbox{prove\_a\_divide\_c\_LE\_b\_divide\_c},\mbox{negated\_conjecture})$

\medskip\textbf{HEN007-2.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$( \mbox{less\_equal}(x,y)\mbox{ and }\mbox{less\_equal}(y,z) ) \ \Rightarrow \ \mbox{less\_equal}(x,z)\qquad\mbox{cnf}(\mbox{transitivity\_of\_less\_equal},\mbox{axiom})$

$( \mbox{quotient}(x,y,w_1)\mbox{ and }\mbox{less\_equal}(w_1,z)\mbox{ and }\mbox{quotient}(x,z,w_2) ) \ \Rightarrow \ \mbox{less\_equal}(w_2,y)\qquad\mbox{cnf}(\mbox{xQyLEz\_implies\_xQzLEy},\mbox{axiom})$

$\mbox{less\_equal}(x,y)\qquad\mbox{cnf}(\mbox{xLEy},\mbox{hypothesis})$

$\mbox{quotient}(z,y,\mbox{zQy})\qquad\mbox{cnf}(\mbox{zQy},\mbox{hypothesis})$

$\mbox{quotient}(z,x,\mbox{zQx})\qquad\mbox{cnf}(\mbox{zQx},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{zQy},\mbox{zQx})\qquad\mbox{cnf}(\mbox{prove\_zQyLEzQx},\mbox{negated\_conjecture})$

\medskip\textbf{HEN012-3.p} X $\leq$ X






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

$\neg\,\mbox{less\_equal}(a,a)\qquad\mbox{cnf}(\mbox{prove\_a\_LE\_a},\mbox{negated\_conjecture})$

\medskip\textbf{HEN011-5.p} This operation is commutative

Define \& on the set of Z', where Z' = identity/Z,
 by X' \& Y' = X'/(identity/Y'). The operation is commutative.




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

$\mbox{divide}(x,x) = 0\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{divide}(x,0) = x\qquad\mbox{cnf}(\mbox{x\_divide\_zero\_is\_x},\mbox{axiom})$

$( \mbox{divide}(x,y) = 0\mbox{ and }\mbox{divide}(y,z) = 0 ) \ \Rightarrow \ \mbox{divide}(x,z) = 0\qquad\mbox{cnf}(\mbox{transitivity\_of\_divide\_to\_zero},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(x,y),z) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(x,z),y) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_1,\mbox{axiom})$

$\mbox{divide}(x,y) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(z,y),\mbox{divide}(z,x)) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_2,\mbox{axiom})$

$\mbox{divide}(x,y) = 0 \ \Rightarrow \ \mbox{divide}(\mbox{divide}(x,z),\mbox{divide}(y,z)) = 0\qquad\mbox{cnf}(\mbox{property\_of\_divide}_3,\mbox{axiom})$

$\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{one\_inversion\_equals\_three},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(\mbox{identity},x),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},x))) = \mbox{divide}(\mbox{identity},x)\qquad\mbox{cnf}(\mbox{property\_of\_inversion},\mbox{axiom})$

$\mbox{divide}(\mbox{divide}(\mbox{identity},a),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},b)))\ne \mbox{divide}(\mbox{divide}(\mbox{identity},b),\mbox{divide}(\mbox{identity},\mbox{divide}(\mbox{identity},a)))\qquad\mbox{cnf}(\mbox{prove\_this},\mbox{negated\_conjecture})$

\medskip\textbf{HEN004-2.p} X/zero = X






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\neg\,\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{prove\_x\_divde\_zero\_is\_x},\mbox{negated\_conjecture})$

\medskip\textbf{HEN005-5.p} The relation less\_equal is transitive






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

$\mbox{divide}(a,b) = 0\qquad\mbox{cnf}(\mbox{a\_divide\_b\_is\_zero},\mbox{hypothesis})$

$\mbox{divide}(b,c) = 0\qquad\mbox{cnf}(\mbox{b\_divide\_c\_is\_zero},\mbox{hypothesis})$

$\mbox{divide}(a,c)\ne 0\qquad\mbox{cnf}(\mbox{prove\_transitivity\_of\_divide\_to\_zero},\mbox{negated\_conjecture})$

\medskip\textbf{HEN006-7.p} X/Y $\leq$ Z =$>$ X/Z $\leq$ Y






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

$\mbox{quotient}(x,\mbox{identity},0)\qquad\mbox{cnf}(\mbox{everything\_divide\_identity\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(0,x,0)\qquad\mbox{cnf}(\mbox{zero\_divide\_anything\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,x,0)\qquad\mbox{cnf}(\mbox{x\_divide\_x\_is\_zero},\mbox{axiom})$

$\mbox{quotient}(x,0,x)\qquad\mbox{cnf}(\mbox{x\_divde\_zero\_is\_x},\mbox{axiom})$

$\mbox{quotient}(x,y,\mbox{xQy})\qquad\mbox{cnf}(\mbox{xQy},\mbox{hypothesis})$

$\mbox{less\_equal}(\mbox{xQy},z)\qquad\mbox{cnf}(\mbox{xQyLEz},\mbox{hypothesis})$

$\mbox{quotient}(x,z,\mbox{xQz})\qquad\mbox{cnf}(\mbox{xQz},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{xQz},y)\qquad\mbox{cnf}(\mbox{prove\_xQzLEy},\mbox{negated\_conjecture})$

\medskip\textbf{HEN007-3.p} X $\leq$ Y =$>$ Z/Y $\leq$ Z/X






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

$\mbox{less\_equal}(a,b)\qquad\mbox{cnf}(\mbox{a\_LE\_b},\mbox{hypothesis})$

$\neg\,\mbox{less\_equal}(\mbox{divide}(c,b),\mbox{divide}(c,a))\qquad\mbox{cnf}(\mbox{prove\_c\_divide\_b\_LE\_c\_divide\_a},\mbox{negated\_conjecture})$

\medskip
\end{document}