<?xml version="1.0"?>
<div>:: <span class="kw">deftheorem </span>   defines <a href="bkmodel1.html#K1" title="BKMODEL1:func.1">Dir101</a> <a onclick="hs(this)" href="javascript:()">BKMODEL1:def 1 : <br/></a><span> <a href="bkmodel1.html#K1" title="BKMODEL1:func.1">Dir101</a>  <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="anproj_1.html#K2" title="ANPROJ_1:func.2">Dir</a> <span class="p1"><a href="euclid_5.html#K4" title="EUCLID_5:func.4">|[</a><span class="default">1,<a href="numbers.html#K5" title="NUMBERS:func.5">0</a>,1</span><a href="euclid_5.html#K4" title="EUCLID_5:func.4">]|</a></span>;<br/></span></div>
