Skip to main content

Browse the archive

https://github.com/coq-ext-lib/coq-ext-lib
05 April 2024, 22:27:30 UTC
Raw File
Tip revision: 4e16cb58bb743938ce27de4155ca97a43796db45 authored by Yishuai Li on 17 January 2024, 23:01:51 UTC
Update templates
Tip revision: 4e16cb5
ExtLib.Data.Set.TwoThreeTrees.html 
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="resources/config.js"></script>
<script type="text/javascript" src="resources/coqdocjs.js"></script>
</head>

<body onload="document.getElementById('content').focus()">
  <div id="header">
    <span class="left">
      <span class="modulename"> <script> document.write(document.title) </script> </span>
    </span>

    <span class="button" id="toggle-proofs"></span>

    <span class="right">
      <a href="../">Project Page</a>
      <a href="./indexpage.html"> Index </a>
      <a href="./toc.html"> Table of Contents </a>
    </span>
</div>
    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
    <div id="main">
<h1 class="libtitle">ExtLib.Data.Set.TwoThreeTrees</h1>

<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Structures.Monads.html#"><span class="id" title="library">ExtLib.Structures.Monads</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Data.Monads.OptionMonad.html#"><span class="id" title="library">ExtLib.Data.Monads.OptionMonad</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Programming.Extras.html#"><span class="id" title="library">ExtLib.Programming.Extras</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">FunNotation</span>.<br/>

<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Maximal</span> <span class="id" title="keyword">Implicit</span> <span class="id" title="var">Insertion</span>.<br/>

<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">MonadNotation</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">MonadPlusNotation</span>.<br/>
<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">monad_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="tree"><span class="id" title="section">tree</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Variable</span> <a name="tree.E"><span class="id" title="variable">E</span></a>:<span class="id" title="keyword">Type</span>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Variable</span> <a name="tree.comp"><span class="id" title="variable">comp</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#comparison"><span class="id" title="inductive">comparison</span></a>.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;a&nbsp;two-three&nbsp;tree&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Inductive</span> <a name="tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Null_t&nbsp;=&nbsp;_&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="Null_t"><span class="id" title="constructor">Null_t</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;Two_t&nbsp;X&nbsp;a&nbsp;Y&nbsp;=&nbsp;&nbsp;/&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;Invariant:&nbsp;x&nbsp;in&nbsp;X&nbsp;=&gt;&nbsp;x&nbsp;&lt;&nbsp;a;&nbsp;y&nbsp;in&nbsp;Y&nbsp;=&gt;&nbsp;y&nbsp;&gt;&nbsp;a<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="Two_t"><span class="id" title="constructor">Two_t</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><span class="inlinecode"><span class="id" title="var">b</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;Three_t&nbsp;X&nbsp;a&nbsp;Y&nbsp;b&nbsp;Z&nbsp;=&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y&nbsp;&nbsp;&nbsp;Z<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;Invariant:&nbsp;x&nbsp;in&nbsp;X&nbsp;=&gt;&nbsp;x&nbsp;&lt;&nbsp;a;&nbsp;y&nbsp;in&nbsp;Y&nbsp;=&gt;&nbsp;a&nbsp;&lt;&nbsp;y&nbsp;&lt;&nbsp;b;&nbsp;z&nbsp;in&nbsp;Z&nbsp;=&gt;&nbsp;z&nbsp;&gt;&nbsp;b<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="Three_t"><span class="id" title="constructor">Three_t</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a><br/>
&nbsp;&nbsp;.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="height_t"><span class="id" title="definition">height_t</span></a> (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">_</span> <span class="id" title="var">tr</span> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Peano.html#max"><span class="id" title="abbreviation">max</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#height_t"><span class="id" title="definition">height_t</span></a> <span class="id" title="var">tl</span>) (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#height_t"><span class="id" title="definition">height_t</span></a> <span class="id" title="var">tr</span>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">_</span> <span class="id" title="var">tm</span> <span class="id" title="var">_</span> <span class="id" title="var">tr</span> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Peano.html#max"><span class="id" title="abbreviation">max</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Peano.html#max"><span class="id" title="abbreviation">max</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#height_t"><span class="id" title="definition">height_t</span></a> <span class="id" title="var">tl</span>) (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#height_t"><span class="id" title="definition">height_t</span></a> <span class="id" title="var">tm</span>)) (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#height_t"><span class="id" title="definition">height_t</span></a> <span class="id" title="var">tr</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;a&nbsp;context&nbsp;of&nbsp;a&nbsp;two-three&nbsp;tree.&nbsp;this&nbsp;is&nbsp;the&nbsp;type&nbsp;of&nbsp;taking&nbsp;a&nbsp;tree&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;replacing&nbsp;a&nbsp;sub-tree&nbsp;with&nbsp;a&nbsp;hole.<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Inductive</span> <a name="context"><span class="id" title="inductive">context</span></a> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Top_c&nbsp;=&nbsp;_&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="Top_c"><span class="id" title="constructor">Top_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;TwoLeftHole_c&nbsp;a&nbsp;Y&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;?&nbsp;&nbsp;&nbsp;Y<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;TwoRightHole_c&nbsp;X&nbsp;a&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;?<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;ThreeLeftHole&nbsp;a&nbsp;Y&nbsp;b&nbsp;Z&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><span class="inlinecode"><span class="id" title="var">b</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;?&nbsp;&nbsp;&nbsp;Y&nbsp;&nbsp;&nbsp;Z<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;ThreeMiddleHole&nbsp;X&nbsp;a&nbsp;b&nbsp;Z&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><span class="inlinecode"><span class="id" title="var">b</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;?&nbsp;&nbsp;&nbsp;Z<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;ThreeRightHole_c&nbsp;X&nbsp;a&nbsp;Y&nbsp;b&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><span class="inlinecode"><span class="id" title="var">b</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y&nbsp;&nbsp;&nbsp;?<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><br/>
&nbsp;&nbsp;.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;zip&nbsp;takes&nbsp;a&nbsp;context&nbsp;(which&nbsp;can&nbsp;be&nbsp;thought&nbsp;of&nbsp;as&nbsp;a&nbsp;tree&nbsp;with&nbsp;a&nbsp;hole),&nbsp;and&nbsp;a<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;subtree,&nbsp;and&nbsp;fills&nbsp;the&nbsp;hole&nbsp;with&nbsp;the&nbsp;subtree<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="zip"><span class="id" title="definition">zip</span></a> (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) (<span class="id" title="var">c</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">c'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">c'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="fuse"><span class="id" title="definition">fuse</span></a> (<span class="id" title="var">c1</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) (<span class="id" title="var">c2</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c1"><span class="id" title="variable">c1</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> <span class="id" title="var">c1'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> <span class="id" title="var">c1'</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">c1'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> <span class="id" title="var">c1'</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c1'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> <span class="id" title="var">c1'</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c1'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> <span class="id" title="var">c1'</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> <span class="id" title="var">c1'</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">em</span> <span class="id" title="var">er</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> <span class="id" title="var">c1'</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c2"><span class="id" title="variable">c2</span></a>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Inductive</span> <a name="location"><span class="id" title="inductive">location</span></a> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;TwoHole_l&nbsp;X&nbsp;Y&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode">?</span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="TwoHole_l"><span class="id" title="constructor">TwoHole_l</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#location"><span class="id" title="inductive">location</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;TwoHole_l&nbsp;X&nbsp;Y&nbsp;b&nbsp;Z&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode">?</span><span class="inlinecode"><span class="id" title="var">b</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y&nbsp;&nbsp;&nbsp;Z<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="ThreeLeftHole_l"><span class="id" title="constructor">ThreeLeftHole_l</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#location"><span class="id" title="inductive">location</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;TwoHole_l&nbsp;X&nbsp;a&nbsp;Y&nbsp;Z&nbsp;C&nbsp;=&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span><span class="inlinecode">?</span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;X&nbsp;&nbsp;&nbsp;Y&nbsp;&nbsp;&nbsp;Z<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a name="ThreeRightHole_l"><span class="id" title="constructor">ThreeRightHole_l</span></a> : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#location"><span class="id" title="inductive">location</span></a><br/>
&nbsp;&nbsp;.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="fillLocation"><span class="id" title="definition">fillLocation</span></a> (<span class="id" title="var">e</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a>) (<span class="id" title="var">l</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#location"><span class="id" title="inductive">location</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#l"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoHole_l"><span class="id" title="constructor">TwoHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tr</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_l"><span class="id" title="constructor">ThreeLeftHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tm</span> <span class="id" title="var">vr</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tm</span> <span class="id" title="var">vr</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_l"><span class="id" title="constructor">ThreeRightHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tr</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="locate"><span class="id" title="definition">locate</span></a> (<span class="id" title="var">e</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a>) (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) (<span class="id" title="var">c</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#location"><span class="id" title="inductive">location</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.comp"><span class="id" title="variable">comp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">em</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">em</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoHole_l"><span class="id" title="constructor">TwoHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.comp"><span class="id" title="variable">comp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">el</span>, <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.comp"><span class="id" title="variable">comp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">er</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a>, <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a>, <span class="id" title="var">_</span> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_l"><span class="id" title="constructor">ThreeLeftHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tm</span> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">er</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_l"><span class="id" title="constructor">ThreeRightHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="locateGreatest"><span class="id" title="definition">locateGreatest</span></a> (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) (<span class="id" title="var">c</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">)</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> =&gt; <a class="idref" href="ExtLib.Structures.Monad.html#liftM"><span class="id" title="definition">liftM</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#sum_tot"><span class="id" title="definition">sum_tot</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locateGreatest"><span class="id" title="definition">locateGreatest</span></a> <span class="id" title="var">tr</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Structures.MonadPlus.html#1ccf5cb3409233ebd0446c3b758b1c65"><span class="id" title="notation">&lt;+&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Structures.Monad.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">em</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> =&gt; <a class="idref" href="ExtLib.Structures.Monad.html#liftM"><span class="id" title="definition">liftM</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#sum_tot"><span class="id" title="definition">sum_tot</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locateGreatest"><span class="id" title="definition">locateGreatest</span></a> <span class="id" title="var">tr</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Structures.MonadPlus.html#1ccf5cb3409233ebd0446c3b758b1c65"><span class="id" title="notation">&lt;+&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Structures.Monad.html#ret"><span class="id" title="method">ret</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">er</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="single"><span class="id" title="definition">single</span></a> <span class="id" title="var">e</span> := <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a>.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;if&nbsp;insertion&nbsp;results&nbsp;in&nbsp;a&nbsp;subtree&nbsp;which&nbsp;is&nbsp;too&nbsp;tall,&nbsp;propegate&nbsp;it&nbsp;up&nbsp;into<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;its&nbsp;context.<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="insertUp"><span class="id" title="definition">insertUp</span></a> (<span class="id" title="var">tet</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">*</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) (<span class="id" title="var">c</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">tl</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">em</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">tr</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> := <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tet"><span class="id" title="variable">tet</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;_<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><span class="inlinecode"><span class="id" title="var">em'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;//&nbsp;\\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span><span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;\\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a>  <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span> ) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;\\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;tm&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;//&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;tr&nbsp;tm&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr'</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#insertUp"><span class="id" title="definition">insertUp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;\\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;tl&nbsp;tr&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr'</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#insertUp"><span class="id" title="definition">insertUp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el</span> <span class="id" title="var">tl</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">em</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tr</span> <span class="id" title="var">er</span> <span class="id" title="var">tr'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;\\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;tm&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;//&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;tm&nbsp;tl&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#insertUp"><span class="id" title="definition">insertUp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">er</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">em</span> <span class="id" title="var">tr</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;insert&nbsp;an&nbsp;element&nbsp;into&nbsp;the&nbsp;two-three&nbsp;tree&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="insert"><span class="id" title="definition">insert</span></a> (<span class="id" title="var">e</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a>) (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">c</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#insertUp"><span class="id" title="definition">insertUp</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">l</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fillLocation"><span class="id" title="definition">fillLocation</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">l</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;if&nbsp;remove&nbsp;results&nbsp;in&nbsp;a&nbsp;tree&nbsp;which&nbsp;is&nbsp;too&nbsp;short,&nbsp;propegate&nbsp;the&nbsp;gap&nbsp;into&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;context&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <a name="removeUp"><span class="id" title="definition">removeUp</span></a> (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) (<span class="id" title="var">c</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#context"><span class="id" title="inductive">context</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;_<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;||<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;e&nbsp;&nbsp;=&gt;&nbsp;&nbsp;e<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;//&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;t&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tm'&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;tl'&nbsp;tm'&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tl'</span>) <span class="id" title="var">el'</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;||<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><span class="inlinecode"><span class="id" title="var">em'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;//&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">em</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">em</span> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;&nbsp;tm'&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;tm'&nbsp;tr'&nbsp;&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">em</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span>) <span class="id" title="var">er'</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tr'</span> <span class="id" title="var">em</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;||<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em</span></span>&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span><span class="inlinecode"><span class="id" title="var">em</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tr'&nbsp;&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">em</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span> <span class="id" title="var">em</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;t&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span>&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tm'&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;tl'&nbsp;tm'&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">el'</span> <span class="id" title="var">tl'</span>) <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;//&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">el</span> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er'</span></span><span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;||&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span>&nbsp;&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tm'&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tm'&nbsp;&nbsp;tr'&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span>) <span class="id" title="var">er'</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tr'</span> <span class="id" title="var">el</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">el'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;||&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tm'&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tm'&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">er</span> <span class="id" title="var">tl'</span>) <span class="id" title="var">el'</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;||&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span><span class="inlinecode"><span class="id" title="var">el</span></span>&nbsp;&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl'&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">el</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span> <span class="id" title="var">el</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>) <span class="id" title="var">er</span> <span class="id" title="var">tr</span>) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;||&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><span class="inlinecode"><span class="id" title="var">em'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tr'<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">er</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="var">er</span> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;tl&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span><span class="inlinecode"><span class="id" title="var">er'</span></span>&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el'</span></span>&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tm'&nbsp;&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;tm'&nbsp;tr'&nbsp;&nbsp;&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span> <span class="id" title="var">er'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">el'</span> <span class="id" title="var">tm'</span>) <span class="id" title="var">er'</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tr'</span> <span class="id" title="var">er</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;c'<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><span class="inlinecode"><span class="id" title="var">er</span></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">el</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span>&nbsp;&nbsp;t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">em'</span></span><span class="inlinecode"><span class="id" title="var">er</span></span><br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;\&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/&nbsp;&nbsp;&nbsp;|&nbsp;&nbsp;&nbsp;\<br/>
&nbsp;&nbsp;&nbsp;*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;&nbsp;&nbsp;tr'&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tl'&nbsp;&nbsp;tr&nbsp;&nbsp;&nbsp;t<br/>
&nbsp;&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span>) <span class="id" title="var">er</span> <span class="id" title="var">c'</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Two_t"><span class="id" title="constructor">Two_t</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Three_t"><span class="id" title="constructor">Three_t</span></a> <span class="id" title="var">tl'</span> <span class="id" title="var">em'</span> <span class="id" title="var">tr'</span> <span class="id" title="var">er</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a>)) <span class="id" title="var">c'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="comment">(*&nbsp;not&nbsp;wf&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoRightHole_c"><span class="id" title="constructor">TwoRightHole_c</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="comment">(*&nbsp;not&nbsp;wf&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="comment">(*&nbsp;not&nbsp;wf&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="comment">(*&nbsp;not&nbsp;wf&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_c"><span class="id" title="constructor">ThreeRightHole_c</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="comment">(*&nbsp;not&nbsp;wf&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="remove"><span class="id" title="definition">remove</span></a> (<span class="id" title="var">e</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree.E"><span class="id" title="variable">E</span></a>) (<span class="id" title="var">t</span>:<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a>) : <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="inductive">tree</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locate"><span class="id" title="definition">locate</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;element&nbsp;doesn't&nbsp;exist&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#t"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;element&nbsp;found&nbsp;at&nbsp;location&nbsp;<span class="inlinecode"><span class="id" title="var">loc</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">loc</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">loc</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;element&nbsp;found&nbsp;at&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoHole_l"><span class="id" title="constructor">TwoHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">mkContext</span> <span class="id" title="var">g</span> <span class="id" title="var">c'</span> := <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#TwoLeftHole_c"><span class="id" title="constructor">TwoLeftHole_c</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#g"><span class="id" title="variable">g</span></a> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c'"><span class="id" title="variable">c'</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locateGreatest"><span class="id" title="definition">locateGreatest</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;no&nbsp;children:&nbsp;turn&nbsp;into&nbsp;a&nbsp;hole&nbsp;and&nbsp;propagate&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;two-node:&nbsp;replace&nbsp;it&nbsp;with&nbsp;a&nbsp;hole&nbsp;and&nbsp;propagate&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;three-node:&nbsp;turn&nbsp;it&nbsp;into&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#single"><span class="id" title="definition">single</span></a> <span class="id" title="var">el</span>) <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;element&nbsp;found&nbsp;on&nbsp;left&nbsp;side&nbsp;of&nbsp;three-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_l"><span class="id" title="constructor">ThreeLeftHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">mkContext</span> <span class="id" title="var">g</span> <span class="id" title="var">c'</span> := <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeLeftHole_c"><span class="id" title="constructor">ThreeLeftHole_c</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#g"><span class="id" title="variable">g</span></a> <span class="id" title="var">tm</span> <span class="id" title="var">er</span> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c'"><span class="id" title="variable">c'</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locateGreatest"><span class="id" title="definition">locateGreatest</span></a> <span class="id" title="var">tl</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;no&nbsp;children:&nbsp;turn&nbsp;into&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#single"><span class="id" title="definition">single</span></a> <span class="id" title="var">er</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;two-node:&nbsp;replace&nbsp;it&nbsp;with&nbsp;a&nbsp;hole&nbsp;and&nbsp;propagate&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;three-node:&nbsp;turn&nbsp;it&nbsp;into&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#single"><span class="id" title="definition">single</span></a> <span class="id" title="var">el</span>) <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;element&nbsp;found&nbsp;on&nbsp;right&nbsp;side&nbsp;of&nbsp;three-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeRightHole_l"><span class="id" title="constructor">ThreeRightHole_l</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <span class="id" title="var">tm</span> <span class="id" title="var">tr</span> <span class="id" title="var">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">mkContext</span> <span class="id" title="var">g</span> <span class="id" title="var">c'</span> := <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#ThreeMiddleHole_c"><span class="id" title="constructor">ThreeMiddleHole_c</span></a> <span class="id" title="var">tl</span> <span class="id" title="var">el</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#g"><span class="id" title="variable">g</span></a> <span class="id" title="var">tr</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#c'"><span class="id" title="variable">c'</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#locateGreatest"><span class="id" title="definition">locateGreatest</span></a> <span class="id" title="var">tm</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Top_c"><span class="id" title="constructor">Top_c</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;no&nbsp;children:&nbsp;turn&nbsp;into&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#single"><span class="id" title="definition">single</span></a> <span class="id" title="var">el</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;two-node:&nbsp;replace&nbsp;it&nbsp;with&nbsp;a&nbsp;hole&nbsp;and&nbsp;propagate&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#removeUp"><span class="id" title="definition">removeUp</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;greatest&nbsp;leaf&nbsp;is&nbsp;a&nbsp;three-node:&nbsp;turn&nbsp;it&nbsp;into&nbsp;a&nbsp;two-node&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">el</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">c'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a> =&gt; <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#zip"><span class="id" title="definition">zip</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#single"><span class="id" title="definition">single</span></a> <span class="id" title="var">el</span>) <a class="idref" href="ExtLib.Programming.Extras.html#2980cfb53961d5189e0a1f3e473d6bf0"><span class="id" title="notation">$</span></a> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#fuse"><span class="id" title="definition">fuse</span></a> (<a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#mkContext"><span class="id" title="variable">mkContext</span></a> <span class="id" title="var">g</span> <span class="id" title="var">c'</span>) <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#tree"><span class="id" title="section">tree</span></a>.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="ExtLib.Data.Set.TwoThreeTrees.html#Null_t"><span class="id" title="constructor">Null_t</span></a> {<span class="id" title="var">E</span>}.<br/>

<br/>
<span class="comment">(*<br/>
Section&nbsp;treeWfP.<br/>
&nbsp;&nbsp;Context&nbsp;{E:Type}&nbsp;{TO:TotalOrder&nbsp;E}&nbsp;{TOP:TotalOrderP&nbsp;E}.<br/>
&nbsp;&nbsp;Context&nbsp;{EP:EquivP&nbsp;E}&nbsp;{POEP:PreOrderEquivP&nbsp;_&nbsp;EP}.<br/>
<br/>
&nbsp;&nbsp;Inductive&nbsp;tree_wf&nbsp;:&nbsp;tree&nbsp;E&nbsp;-&gt;&nbsp;nat&nbsp;-&gt;&nbsp;EtndTopBot&nbsp;E&nbsp;-&gt;&nbsp;EtndTopBot&nbsp;E&nbsp;-&gt;&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;|&nbsp;NullTreeWf&nbsp;:&nbsp;forall&nbsp;eLL&nbsp;eRR,&nbsp;tree_wf&nbsp;Null_t&nbsp;O&nbsp;eLL&nbsp;eRR<br/>
&nbsp;&nbsp;|&nbsp;TwoTreeWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;em&nbsp;tr&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;eLL&nbsp;&lt;&lt;&nbsp;IncEtndTopBot&nbsp;em<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;IncEtndTopBot&nbsp;em&nbsp;&lt;&lt;&nbsp;eRR<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;tl&nbsp;h&nbsp;eLL&nbsp;(IncEtndTopBot&nbsp;em)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;tr&nbsp;h&nbsp;(IncEtndTopBot&nbsp;em)&nbsp;eRR<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)&nbsp;(S&nbsp;h)&nbsp;eLL&nbsp;eRR<br/>
&nbsp;&nbsp;|&nbsp;ThreeTreWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr&nbsp;eLL&nbsp;eRR&nbsp;h,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;eLL&nbsp;&lt;&lt;&nbsp;IncEtndTopBot&nbsp;el<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;el&nbsp;&lt;&lt;&nbsp;er<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;IncEtndTopBot&nbsp;er&nbsp;&lt;&lt;&nbsp;eRR<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;tl&nbsp;h&nbsp;eLL&nbsp;(IncEtndTopBot&nbsp;el)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;tm&nbsp;h&nbsp;(IncEtndTopBot&nbsp;el)&nbsp;(IncEtndTopBot&nbsp;er)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;tr&nbsp;h&nbsp;(IncEtndTopBot&nbsp;er)&nbsp;eRR<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;(Three_t&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr)&nbsp;(S&nbsp;h)&nbsp;eLL&nbsp;eRR<br/>
&nbsp;&nbsp;.<br/>
<br/>
&nbsp;&nbsp;Inductive&nbsp;tree_in&nbsp;:&nbsp;E&nbsp;-&gt;&nbsp;tree&nbsp;E&nbsp;-&gt;&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;|&nbsp;TwoTreeIn&nbsp;:&nbsp;forall&nbsp;e&nbsp;tl&nbsp;em&nbsp;tr,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;e&nbsp;~=&nbsp;em<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;tree_in&nbsp;e&nbsp;tl<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;tree_in&nbsp;e&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_in&nbsp;e&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)<br/>
&nbsp;&nbsp;|&nbsp;ThreeTreeIn&nbsp;:&nbsp;forall&nbsp;e&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;e&nbsp;~=&nbsp;el<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;e&nbsp;~=&nbsp;er<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;tree_in&nbsp;e&nbsp;tl<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;tree_in&nbsp;e&nbsp;tm<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\/&nbsp;tree_in&nbsp;e&nbsp;tr<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_in&nbsp;e&nbsp;(Three_t&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr)<br/>
&nbsp;&nbsp;.<br/>
<br/>
&nbsp;&nbsp;<span class="comment">(*<br/>
&nbsp;&nbsp;Lemma&nbsp;swapTwoWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;em&nbsp;tr&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;em',<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tree_wf&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)&nbsp;h&nbsp;eLL&nbsp;eRR<br/>
&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;em&nbsp;~=&nbsp;em'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;-&gt;&nbsp;tree_wf&nbsp;(Two_t&nbsp;tl&nbsp;em'&nbsp;tr)&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros&nbsp;;&nbsp;induction&nbsp;h.<br/>
&nbsp;&nbsp;inversion&nbsp;H.<br/>
&nbsp;&nbsp;inversion&nbsp;H&nbsp;;&nbsp;subst&nbsp;;&nbsp;clear&nbsp;H.&nbsp;constructor.&nbsp;repeat&nbsp;(ohsnap&nbsp;;&nbsp;girlforeal).<br/>
&nbsp;&nbsp;unfold&nbsp;ltP&nbsp;in&nbsp;H5.&nbsp;destruct&nbsp;eLL&nbsp;;&nbsp;repeat&nbsp;(ohsnap&nbsp;;&nbsp;girlforeal).<br/>
&nbsp;&nbsp;...<br/>
&nbsp;&nbsp;*)</span><br/>
<br/>
End&nbsp;treeWfP.<br/>
<br/>
<br/>
<span class="comment">(*<br/>
&nbsp;&nbsp;Definition&nbsp;context_wf&nbsp;(c:context)&nbsp;(sth:nat)&nbsp;(sel:E+bool)&nbsp;(ser:E+bool)&nbsp;(th:nat)&nbsp;(eLL:E+bool)&nbsp;(eRR:E+bool)&nbsp;:&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;forall&nbsp;t:tree,&nbsp;tree_wf&nbsp;t&nbsp;sth&nbsp;sel&nbsp;ser&nbsp;-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;t&nbsp;c)&nbsp;th&nbsp;eLL&nbsp;eRR.<br/>
<br/>
&nbsp;&nbsp;Lemma&nbsp;twoLeftHoleZipWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;em&nbsp;tr&nbsp;c&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;tree_wf&nbsp;(zip&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)&nbsp;c)&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;tl&nbsp;(TwoLeftHole_c&nbsp;em&nbsp;tr&nbsp;c))&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;induction&nbsp;tl&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;twoLeftHoleZipWf&nbsp;:&nbsp;twoThreeDb.<br/>
&nbsp;&nbsp;Lemma&nbsp;twoRightHoleZipWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;em&nbsp;tr&nbsp;c&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;tree_wf&nbsp;(zip&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)&nbsp;c)&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;tr&nbsp;(TwoRightHole_c&nbsp;tl&nbsp;em&nbsp;c))&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;induction&nbsp;tl&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;twoRightHoleZipWf&nbsp;:&nbsp;twoThreeDb.<br/>
&nbsp;&nbsp;Lemma&nbsp;threeLeftHoleZipWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr&nbsp;c&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;tree_wf&nbsp;(zip&nbsp;(Three_t&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr)&nbsp;c)&nbsp;h&nbsp;eLL&nbsp;eRR-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;tl&nbsp;(ThreeLeftHole_c&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr&nbsp;c))&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;induction&nbsp;tl&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;threeLeftHoleZipWf&nbsp;:&nbsp;twoThreeDb.<br/>
&nbsp;&nbsp;Lemma&nbsp;threeMiddleHoleZipWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr&nbsp;c&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;tree_wf&nbsp;(zip&nbsp;(Three_t&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr)&nbsp;c)&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;tm&nbsp;(ThreeMiddleHole_c&nbsp;tl&nbsp;el&nbsp;er&nbsp;tr&nbsp;c))&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;induction&nbsp;tl&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;threeMiddleHoleZipWf&nbsp;:&nbsp;twoThreeDb.<br/>
&nbsp;&nbsp;Lemma&nbsp;threeRightHoleZipWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr&nbsp;c&nbsp;h&nbsp;eLL&nbsp;eRR,<br/>
&nbsp;&nbsp;tree_wf&nbsp;(zip&nbsp;(Three_t&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;tr)&nbsp;c)&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;-&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;tr&nbsp;(ThreeRightHole_c&nbsp;tl&nbsp;el&nbsp;tm&nbsp;er&nbsp;c))&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;induction&nbsp;tl&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;threeRightHoleZipWf&nbsp;:&nbsp;twoThreeDb.<br/>
<br/>
&nbsp;&nbsp;Definition&nbsp;location_wf&nbsp;(l:location)&nbsp;h&nbsp;eLL&nbsp;eRR&nbsp;:&nbsp;Prop&nbsp;:=&nbsp;forall&nbsp;e:E,&nbsp;tree_wf&nbsp;(fillLocation&nbsp;e&nbsp;l)&nbsp;h&nbsp;eLL&nbsp;eRR.<br/>
<br/>
&nbsp;&nbsp;Lemma&nbsp;zipLocationWf&nbsp;:&nbsp;forall&nbsp;tl&nbsp;em&nbsp;tr&nbsp;c,&nbsp;tree_wf&nbsp;(zip&nbsp;(Two_t&nbsp;tl&nbsp;em&nbsp;tr)&nbsp;c)&nbsp;-&gt;&nbsp;location_wf&nbsp;(TwoHole_l&nbsp;tl&nbsp;tr&nbsp;c).<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;unfold&nbsp;location_wf.&nbsp;intros.&nbsp;simpl.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;em.&nbsp;auto.&nbsp;Qed.&nbsp;Hint&nbsp;Immediate&nbsp;zipLocationWf&nbsp;:&nbsp;twoThreeDb.<br/>
<br/>
&nbsp;&nbsp;Lemma&nbsp;locate_wf&nbsp;:&nbsp;forall&nbsp;e&nbsp;t&nbsp;c,&nbsp;tree_wf&nbsp;(zip&nbsp;t&nbsp;c)&nbsp;-&gt;&nbsp;match&nbsp;locate&nbsp;e&nbsp;t&nbsp;c&nbsp;with&nbsp;inl&nbsp;c&nbsp;=&gt;&nbsp;tree_wf&nbsp;(zip&nbsp;Null_t&nbsp;c)&nbsp;|&nbsp;inr&nbsp;(_,l)&nbsp;=&gt;&nbsp;location_wf&nbsp;l&nbsp;end.<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.&nbsp;gd&nbsp;c.&nbsp;gd&nbsp;e.<br/>
&nbsp;&nbsp;induction&nbsp;t&nbsp;;&nbsp;intros&nbsp;;&nbsp;simpl&nbsp;;&nbsp;auto.&nbsp;destruct&nbsp;(compareo&nbsp;e0&nbsp;e).<br/>
&nbsp;&nbsp;pose&nbsp;(twoLeftHoleZipWf&nbsp;_&nbsp;_&nbsp;_&nbsp;_&nbsp;H).&nbsp;specialize&nbsp;(IHt1&nbsp;e0&nbsp;_&nbsp;t).&nbsp;apply&nbsp;IHt1.<br/>
&nbsp;&nbsp;eauto&nbsp;with&nbsp;twoThreeDb.<br/>
&nbsp;&nbsp;pose&nbsp;(twoRightHoleZipWf&nbsp;_&nbsp;_&nbsp;_&nbsp;_&nbsp;H).&nbsp;specialize&nbsp;(IHt2&nbsp;e0&nbsp;_&nbsp;t).&nbsp;apply&nbsp;IHt2.<br/>
<br/>
&nbsp;&nbsp;Lemma&nbsp;single_wf&nbsp;:&nbsp;forall&nbsp;e,&nbsp;tree_wf&nbsp;(single&nbsp;e).&nbsp;Proof.&nbsp;intros.&nbsp;simpl.&nbsp;auto.&nbsp;Qed.<br/>
<br/>
&nbsp;&nbsp;Definition&nbsp;insert_wf&nbsp;:&nbsp;forall&nbsp;e&nbsp;t,&nbsp;tree_wf&nbsp;t&nbsp;-&gt;&nbsp;tree_wf&nbsp;(insert&nbsp;e&nbsp;t).<br/>
&nbsp;&nbsp;Proof.&nbsp;intros.<br/>
&nbsp;&nbsp;destruct&nbsp;t.&nbsp;simpl.&nbsp;auto.<br/>
&nbsp;&nbsp;unfold&nbsp;insert.&nbsp;simpl.<br/>
&nbsp;&nbsp;destruct&nbsp;(compareo&nbsp;e&nbsp;e0).<br/>
&nbsp;&nbsp;unfold&nbsp;insert.<br/>
&nbsp;&nbsp;destruct&nbsp;(locate&nbsp;e&nbsp;t&nbsp;Top_c).&nbsp;simpl.<br/>
&nbsp;&nbsp;*)</span><br/>
<br/>
&nbsp;&nbsp;*)</span><br/>
</div>
</div>
<div id="footer">
  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>

</html>
back to top