<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E8">Th10</font></span>: <a NAME="T10"><span class="comment"><font color="firebrick">:: SCMP_GCD:10</font></span><br/></a><div class="add">( <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> <a href="numbers.html#K5" title="NUMBERS:func.5">0</a> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <a href="scmp_gcd.html#K2" title="SCMP_GCD:func.2">GBP</a> <a href="scmpds_2.html#K5" title="SCMPDS_2:func.5">:=</a> <a href="numbers.html#K5" title="NUMBERS:func.5">0</a> &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 1 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a> <a href="scmpds_2.html#K5" title="SCMPDS_2:func.5">:=</a> 7 &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 2 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K6" title="SCMPDS_2:func.6">saveIC</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,<a href="scmpds_i.html#K15" title="SCMPDS_I:func.15">RetIC</a>) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 3 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K3" title="SCMPDS_2:func.3">goto</a> 2 &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 4 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="compos_1.html#K2" title="COMPOS_1:func.2">halt</a> <a href="scmpds_2.html#K1" title="SCMPDS_2:func.1">SCMPDS</a> &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 5 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,3) <a href="scmpds_2.html#K8" title="SCMPDS_2:func.8">&lt;=0_goto</a> 9 &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 6 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,6) <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">:=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,3) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 7 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K15" title="SCMPDS_2:func.15">Divide</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,2,<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,3) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 8 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,7) <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">:=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,3) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 9 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,<span class="p1">(<span class="default">4 <a href="nat_1.html#K1" title="NAT_1:func.1">+</a> <a href="scmpds_i.html#K14" title="SCMPDS_I:func.14">RetSP</a></span>)</span>) <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">:=</a> (<a href="scmp_gcd.html#K2" title="SCMP_GCD:func.2">GBP</a>,1) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 10 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K11" title="SCMPDS_2:func.11">AddTo</a> (<a href="scmp_gcd.html#K2" title="SCMP_GCD:func.2">GBP</a>,1,4) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 11 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K6" title="SCMPDS_2:func.6">saveIC</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,<a href="scmpds_i.html#K15" title="SCMPDS_I:func.15">RetIC</a>) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 12 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K3" title="SCMPDS_2:func.3">goto</a> <span class="p1">(<span class="default"><a href="xcmplx_0.html#K4" title="XCMPLX_0:func.4">-</a> 7</span>)</span> &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 13 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,2) <a href="scmpds_2.html#K16" title="SCMPDS_2:func.16">:=</a> (<a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a>,6) &amp; <a href="scmp_gcd.html#K4" title="SCMP_GCD:func.4">GCD-Algorithm</a> <a href="funct_1.html#K1" title="FUNCT_1:func.1">.</a> 14 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="scmpds_2.html#K4" title="SCMPDS_2:func.4">return</a> <a href="scmp_gcd.html#K3" title="SCMP_GCD:func.3">SBP</a> )</div></div>
