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

<a NAME="E1:45"/><span class="lab"><font color="Green" title="E62">A1</font></span>: 
 not <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K6" title="SCMFSA_2:func.6">:=</a> <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T6" title="SCMFSA7B:th.6">SCMFSA7B:6</a>, <a class="ref" href="scmfsa_2.html#T101" title="SCMFSA_2:th.101">SCMFSA_2:101</a></span>;<br/>
<a NAME="E2:45"/><span class="lab"><font color="Green" title="E63">A2</font></span>: 
 not  <a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>) <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T8" title="SCMFSA7B:th.8">SCMFSA7B:8</a>, <a class="ref" href="scmfsa_2.html#T101" title="SCMFSA_2:th.101">SCMFSA_2:101</a></span>;<br/>
<a NAME="E3:45"/><span class="lab"><font color="Green" title="E64">A3</font></span>: 
 not <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T14" title="SCMFSA7B:th.14">SCMFSA7B:14</a>, <a class="ref" href="scmfsa_2.html#T101" title="SCMFSA_2:th.101">SCMFSA_2:101</a></span>;<br/>
<a NAME="E4:45"/><span class="lab"><font color="Green" title="E65">A4</font></span>: 
 not <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T14" title="SCMFSA7B:th.14">SCMFSA7B:14</a>, <a class="ref" href="scmfsa_2.html#T101" title="SCMFSA_2:th.101">SCMFSA_2:101</a></span>;<br/>
<a NAME="E5:45"/><span class="lab"><font color="Green" title="E66">A5</font></span>: 
 not (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T15" title="SCMFSA7B:th.15">SCMFSA7B:15</a></span>;<br/>
<a NAME="E6:45"/><span class="lab"><font color="Green" title="E67">A6</font></span>: 
 not (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa7b.html#R3" title="SCMFSA7B:pred.3">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa7b.html#T15" title="SCMFSA7B:th.15">SCMFSA7B:15</a></span>;<br/>
<a NAME="E7:45"/><span class="lab"><font color="Green" title="E68">A7</font></span>: 
 not  <a href="compos_1.html#K6" title="COMPOS_1:func.6">Stop</a> <a href="scmfsa_2.html#K1" title="SCMFSA_2:func.1">SCM+FSA</a> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="ref" href="scmfsa8c.html#T56" title="SCMFSA8C:th.56">SCMFSA8C:56</a></span>;<br/>
<a NAME="E8:45"/>
 not <span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p3">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p2">(<span class="default">(<span class="p3">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p1">(<span class="default">(<span class="p2">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="#E4:45"><span class="lab"><font color="Green" title="E65">A4</font></span></a>, <a class="txt" href="#E5:45"><span class="lab"><font color="Green" title="E66">A5</font></span></a>, <a class="txt" href="#E6:45"><span class="lab"><font color="Green" title="E67">A6</font></span></a>, <a class="ref" href="scmfsa8c.html#T54" title="SCMFSA8C:th.54">SCMFSA8C:54</a>, <a class="ref" href="scmfsa8c.html#T55" title="SCMFSA8C:th.55">SCMFSA8C:55</a></span>;<br/>
<a NAME="E9:45"/><span class="kw">then </span><span class="lab"><font color="Green" title="E69">A8</font></span>: 
 not  <a href="scmfsa8b.html#K2" title="SCMFSA8B:func.2">if&gt;0</a> (<span class="p1">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p2">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p4">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p3">(<span class="default">(<span class="p4">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p2">(<span class="default">(<span class="p3">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span></span>)</span>,<span class="p1">(<span class="default"><a href="compos_1.html#K6" title="COMPOS_1:func.6">Stop</a> <a href="scmfsa_2.html#K1" title="SCMFSA_2:func.1">SCM+FSA</a></span>)</span>) <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="#E7:45"><span class="lab"><font color="Green" title="E68">A7</font></span></a>, <a class="ref" href="scmfsa8c.html#T88" title="SCMFSA8C:th.88">SCMFSA8C:88</a></span>;<br/>
<a NAME="E10:45"/>
 not <span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K6" title="SCMFSA_2:func.6">:=</a> <span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p2">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p1">(<span class="default"><span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p2">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="#E1:45"><span class="lab"><font color="Green" title="E62">A1</font></span></a>, <a class="txt" href="#E2:45"><span class="lab"><font color="Green" title="E63">A2</font></span></a>, <a class="txt" href="#E3:45"><span class="lab"><font color="Green" title="E64">A3</font></span></a>, <a class="ref" href="scmfsa8c.html#T54" title="SCMFSA8C:th.54">SCMFSA8C:54</a>, <a class="ref" href="scmfsa8c.html#T55" title="SCMFSA8C:th.55">SCMFSA8C:55</a></span>;<br/>
<a NAME="E11:45"/><span class="kw">then </span>
 not <span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K6" title="SCMFSA_2:func.6">:=</a> <span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p3">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p2">(<span class="default"><span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p3">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p1">(<span class="default"><span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p2">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="scmbsort.html#E46"><span class="lab"><font color="Green" title="E45">Lm13</font></span></a>, <a class="ref" href="scmfsa7b.html#T14" title="SCMFSA7B:th.14">SCMFSA7B:14</a>, <a class="ref" href="scmfsa8c.html#T54" title="SCMFSA8C:th.54">SCMFSA8C:54</a></span>;<br/>
<a NAME="E12:45"/><span class="kw">then </span>
 not <span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K6" title="SCMFSA_2:func.6">:=</a> <span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p4">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p4">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p2">(<span class="default"><span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p3">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p1">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 
<span class="kw">by</span> <span class="lab"><a class="txt" href="scmbsort.html#E46"><span class="lab"><font color="Green" title="E45">Lm13</font></span></a>, <a class="ref" href="scmfsa7b.html#T8" title="SCMFSA7B:th.8">SCMFSA7B:8</a>, <a class="ref" href="scmfsa8c.html#T54" title="SCMFSA8C:th.54">SCMFSA8C:54</a></span>;<br/>
<span class="kw">hence </span><a NAME="E13:45"/>
 not <span class="p1">(<span class="default"><span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><span class="p0">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K6" title="SCMFSA_2:func.6">:=</a> <span class="p0">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p5">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p0">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p0">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p5">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p3">(<span class="default"><span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p4">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p2">(<span class="default"><a href="scmfsa_2.html#K8" title="SCMFSA_2:func.8">SubFrom</a> (<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p3">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p4">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span></span>)</span> <a href="scmfsa6a.html#K4" title="SCMFSA6A:func.4">';'</a> <span class="p1">(<span class="default"><a href="scmfsa8b.html#K2" title="SCMFSA8B:func.2">if&gt;0</a> (<span class="p2">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p3">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>,<span class="p2">(<span class="default"><span class="p3">(<span class="default"><span class="p4">(<span class="default"><span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span> <a href="scmfsa_2.html#K14" title="SCMFSA_2:func.14">:=</a> (<span class="p5">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>)</span>)</span> <a href="scmfsa6a.html#K7" title="SCMFSA6A:func.7">';'</a> <span class="p4">(<span class="default">(<span class="p5">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">2 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p5">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p0">(<span class="default">5 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span></span>)</span> <a href="scmfsa6a.html#K6" title="SCMFSA6A:func.6">';'</a> <span class="p3">(<span class="default">(<span class="p4">(<span class="default"><a href="scmfsa_2.html#K5" title="SCMFSA_2:func.5">fsloc</a> <a href="numbers.html#K6" title="NUMBERS:func.6">0</a></span>)</span>,<span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">3 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span>) <a href="scmfsa_2.html#K15" title="SCMFSA_2:func.15">:=</a> <span class="p4">(<span class="default"><a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p5">(<span class="default">4 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span></span>)</span></span>)</span></span>)</span>,<span class="p2">(<span class="default"><a href="compos_1.html#K6" title="COMPOS_1:func.6">Stop</a> <a href="scmfsa_2.html#K1" title="SCMFSA_2:func.1">SCM+FSA</a></span>)</span>)</span>)</span> <a href="scmfsa7b.html#R4" title="SCMFSA7B:pred.4">destroys</a>  <a href="scmfsa_2.html#K4" title="SCMFSA_2:func.4">intloc</a> <span class="p1">(<span class="default">1 <a href="nat_1.html#K2" title="NAT_1:func.2">+</a> 1</span>)</span>
 <span class="kw">by</span> <span class="lab"><a class="txt" href="#E9:45"><span class="lab"><font color="Green" title="E69">A8</font></span></a>, <a class="ref" href="scmfsa8c.html#T52" title="SCMFSA8C:th.52">SCMFSA8C:52</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>
