<?xml version="1.0"?>
<div class="add">

<span class="kw">set </span><font color="Maroon" title="c6">I</font> =  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a>;<br/>
<span class="kw">let </span><font color="Maroon" title="c7">W</font> be   <a href="compos_1.html#NM1" title="COMPOS_1:NM.1">Instruction</a> of <a href="scmpds_2.html#K1" title="SCMPDS_2:func.1">SCMPDS</a>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> ( <font color="Maroon" title="c7">W</font> is  <a href="extpro_1.html#V2" title="EXTPRO_1:attr.2">halting</a>  implies <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a> )</span><br/>

<span class="kw">assume </span><a NAME="E1:84"/><span class="lab"><font color="Green" title="E54">A1</font></span>: 
<font color="Maroon" title="c7">W</font> is  <a href="extpro_1.html#V2" title="EXTPRO_1:attr.2">halting</a> 
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span><br/>

<span class="kw">assume </span><a NAME="E2:84"/><span class="lab"><font color="Green" title="E55">A2</font></span>: 
 <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a> <a href="hidden.html#NR2" title="HIDDEN:NR.2">&lt;&gt;</a> <font color="Maroon" title="c7">W</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/>

<div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1"><span class="kw">per </span></a><a class="txt" onclick="hs(this)" href="javascript:()"><span class="kw">cases </span></a><span class="hide"><a NAME="E1:84_1"/>
(  ex <font color="Olive" title="b1">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <font color="Olive" title="b1">k1</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K5" title="SCMPDS_2:func.5">return</a> <font color="Olive" title="b1">a</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K7" title="SCMPDS_2:func.7">saveIC</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b1">a</font> <a href="scmpds_2.html#K6" title="SCMPDS_2:func.6">:=</a> <font color="Olive" title="b2">k1</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K11" title="SCMPDS_2:func.11">:=</a> <font color="Olive" title="b3">k2</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K8" title="SCMPDS_2:func.8">&lt;&gt;0_goto</a> <font color="Olive" title="b3">k2</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K9" title="SCMPDS_2:func.9">&lt;=0_goto</a> <font color="Olive" title="b3">k2</font> or  ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K10" title="SCMPDS_2:func.10">&gt;=0_goto</a> <font color="Olive" title="b3">k2</font> or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K12" title="SCMPDS_2:func.12">AddTo</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b4">k2</font>) or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K13" title="SCMPDS_2:func.13">AddTo</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>) or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K14" title="SCMPDS_2:func.14">SubFrom</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>) or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K15" title="SCMPDS_2:func.15">MultBy</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>) or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">Divide</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>) or  ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>) <a href="scmpds_2.html#K17" title="SCMPDS_2:func.17">:=</a> (<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>) )
 </span><span class="kw">by</span> <span class="lab"><a class="ref" href="scmpds_2.html#T79" target="_self" title="SCMPDS_2:th.79">Th91</a></span>;<br/><div class="add"><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_1"><span class="kw">suppose </span></a><a NAME="E1:84_1_1"/>
 ex <font color="Olive" title="b1">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">goto</a> <font color="Olive" title="b1">k1</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_1"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="txt" href="#E2:84"><span class="lab"><font color="Green" title="E55">A2</font></span></a>, <a class="ref" href="scmpds_2.html#T73" target="_self" title="SCMPDS_2:th.73">Th85</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_2"><span class="kw">suppose </span></a><a NAME="E1:84_1_2"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K5" title="SCMPDS_2:func.5">return</a> <font color="Olive" title="b1">a</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_2"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T77" target="_self" title="SCMPDS_2:th.77">Th89</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_3"><span class="kw">suppose </span></a><a NAME="E1:84_1_3"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K7" title="SCMPDS_2:func.7">saveIC</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_3"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T78" target="_self" title="SCMPDS_2:th.78">Th90</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_4"><span class="kw">suppose </span></a><a NAME="E1:84_1_4"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <font color="Olive" title="b1">a</font> <a href="scmpds_2.html#K6" title="SCMPDS_2:func.6">:=</a> <font color="Olive" title="b2">k1</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_4"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T65" target="_self" title="SCMPDS_2:th.65">Th77</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_5"><span class="kw">suppose </span></a><a NAME="E1:84_1_5"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K11" title="SCMPDS_2:func.11">:=</a> <font color="Olive" title="b3">k2</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_5"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T66" target="_self" title="SCMPDS_2:th.66">Th78</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_6"><span class="kw">suppose </span></a><a NAME="E1:84_1_6"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K8" title="SCMPDS_2:func.8">&lt;&gt;0_goto</a> <font color="Olive" title="b3">k2</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_6"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T74" target="_self" title="SCMPDS_2:th.74">Th86</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_7"><span class="kw">suppose </span></a><a NAME="E1:84_1_7"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K9" title="SCMPDS_2:func.9">&lt;=0_goto</a> <font color="Olive" title="b3">k2</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_7"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T75" target="_self" title="SCMPDS_2:th.75">Th87</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_8"><span class="kw">suppose </span></a><a NAME="E1:84_1_8"/>
 ex <font color="Olive" title="b1">a</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b2">k1</font>, <font color="Olive" title="b3">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b2">k1</font>) <a href="scmpds_2.html#K10" title="SCMPDS_2:func.10">&gt;=0_goto</a> <font color="Olive" title="b3">k2</font>
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_8"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T76" target="_self" title="SCMPDS_2:th.76">Th88</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_9"><span class="kw">suppose </span></a><a NAME="E1:84_1_9"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K12" title="SCMPDS_2:func.12">AddTo</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_9"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T68" target="_self" title="SCMPDS_2:th.68">Th80</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_10"><span class="kw">suppose </span></a><a NAME="E1:84_1_10"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K13" title="SCMPDS_2:func.13">AddTo</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_10"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T69" target="_self" title="SCMPDS_2:th.69">Th81</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_11"><span class="kw">suppose </span></a><a NAME="E1:84_1_11"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K14" title="SCMPDS_2:func.14">SubFrom</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_11"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T70" target="_self" title="SCMPDS_2:th.70">Th82</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_12"><span class="kw">suppose </span></a><a NAME="E1:84_1_12"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K15" title="SCMPDS_2:func.15">MultBy</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_12"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T71" target="_self" title="SCMPDS_2:th.71">Th83</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_13"><span class="kw">suppose </span></a><a NAME="E1:84_1_13"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">Divide</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>,<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_13"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T72" target="_self" title="SCMPDS_2:th.72">Th84</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div><div><a class="txt" onclick="hsNdiv(this)" href="javascript:()" title="84_1_14"><span class="kw">suppose </span></a><a NAME="E1:84_1_14"/>
 ex <font color="Olive" title="b1">a</font>, <font color="Olive" title="b2">b</font> being    <a href="scmpds_2.html#M1" title="SCMPDS_2:mode.1">Int_position</a>  ex <font color="Olive" title="b3">k1</font>, <font color="Olive" title="b4">k2</font> being   <a href="int_1.html#NM1" title="INT_1:NM.1">Integer</a> st <font color="Maroon" title="c7">W</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<font color="Olive" title="b1">a</font>,<font color="Olive" title="b3">k1</font>) <a href="scmpds_2.html#K17" title="SCMPDS_2:func.17">:=</a> (<font color="Olive" title="b2">b</font>,<font color="Olive" title="b4">k2</font>)
 ; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> contradiction</span><br/><div class="add"><span class="kw">hence </span><a NAME="E2:84_1_14"/>
contradiction
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:84"><span class="lab"><font color="Green" title="E54">A1</font></span></a>, <a class="ref" href="scmpds_2.html#T67" target="_self" title="SCMPDS_2:th.67">Th79</a></span>; <a class="txt" onclick="hs(this)" href="javascript:()"><span class="comment"><font color="firebrick">::  thesis: </font></span></a><span class="hide"> verum</span><br/></div><span class="kw">end;</span></div></div><span class="kw">end;</span></div>

</div>
