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

<b>let </b><font color="Maroon">c1</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">x1</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">x2</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">x3</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">x4</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">y1</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">y2</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">y3</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">y4</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">c2</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">c3</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">c4</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">c5</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">n1</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">n2</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">n3</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">n4</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">n</font> be    <a href="hidden.html#M1">set</a> , <font color="Maroon">c5b</font> be    <a href="hidden.html#M1">set</a> ;<br/>

<b>assume </b><b>that </b><br/><a NAME="E1:37"/><i><font color="Green">E71</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x1</font>,<font color="Maroon">y1</font>,<font color="Maroon">c1</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c2</font> )
 <b>and </b><br/><a NAME="E2:37"/><i><font color="Green">E72</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x2</font>,<font color="Maroon">y2</font>,<font color="Maroon">c2</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c3</font> )
 <b>and </b><br/><a NAME="E3:37"/><i><font color="Green">E73</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x3</font>,<font color="Maroon">y3</font>,<font color="Maroon">c3</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c4</font> )
 <b>and </b><br/><a NAME="E4:37"/><i><font color="Green">E74</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x4</font>,<font color="Maroon">y4</font>,<font color="Maroon">c4</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5</font> )
 <b>and </b><br/><a NAME="E5:37"/><i><font color="Green">E75</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n1</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">x1</font>,<font color="Maroon">y1</font> )
 <b>and </b><br/><a NAME="E6:37"/><i><font color="Green">E76</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n2</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">x2</font>,<font color="Maroon">y2</font> )
 <b>and </b><br/><a NAME="E7:37"/><i><font color="Green">E77</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">x3</font>,<font color="Maroon">y3</font> )
 <b>and </b><br/><a NAME="E8:37"/><i><font color="Green">E78</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">x4</font>,<font color="Maroon">y4</font> )
 <b>and </b><br/><a NAME="E9:37"/><i><font color="Green">E79</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K18" target="_self">AND5</a> <font color="Maroon">c1</font>,<font color="Maroon">n1</font>,<font color="Maroon">n2</font>,<font color="Maroon">n3</font>,<font color="Maroon">n4</font> )
 <b>and </b><br/><a NAME="E10:37"/><i><font color="Green">E80</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5b</font> implies  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">c5</font>,<font color="Maroon">n</font> )
 <b>and </b><br/><a NAME="E11:37"/><i><font color="Green">E81</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">c5</font>,<font color="Maroon">n</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5b</font> )
 ;<br/>

<b>thus </b><a NAME="E12:37"/>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5</font> implies  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5b</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D31" target="_self">Def31</a>, , </i>;<br/>

<b>assume </b><a NAME="E13:37"/>
 <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5b</font>
 ;<br/>

<a NAME="E14:37"/><b>then </b>
 <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K3" target="_self">OR2</a> <font color="Maroon">c5</font>,<font color="Maroon">n</font>
 
<b>by </b><i><a class="ref" href="gate_1.html#D30" target="_self">Def30</a></i>;<br/>
<a NAME="E15:37"/><b>then </b><i><font color="Green">E82</font></i>: 
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5</font> or  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n</font> )
 
<b>by </b><i/>;<br/>
<div><a class="txt" onclick="hs2(this)" href="javascript:()" title="37_1"><b>now </b></a><div class="add"><b>assume </b><a NAME="E1:37_1"/>
 <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n</font>
 ;<br/><a NAME="E2:37_1"/><b>then </b>
 <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K18" target="_self">AND5</a> <font color="Maroon">c1</font>,<font color="Maroon">n1</font>,<font color="Maroon">n2</font>,<font color="Maroon">n3</font>,<font color="Maroon">n4</font>
 <b>by </b><i><a class="ref" href="gate_1.html#D29" target="_self">Def29</a></i>;<br/><a NAME="E3:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c1</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n1</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D7" target="_self">Def7</a></i>;<br/><a NAME="E4:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c1</font> &amp; (  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">x1</font> or  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">y1</font> ) &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D25" target="_self">Def25</a>, </i>;<br/><a NAME="E5:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x1</font>,<font color="Maroon">y1</font>,<font color="Maroon">c1</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i>, </i>;<br/><a NAME="E6:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D21" target="_self">Def21</a></i>;<br/><a NAME="E7:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c2</font> &amp; (  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">x2</font> or  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">y2</font> ) &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D26" target="_self">Def26</a>, </i>;<br/><a NAME="E8:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x2</font>,<font color="Maroon">y2</font>,<font color="Maroon">c2</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i>, </i>;<br/><a NAME="E9:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D22" target="_self">Def22</a></i>;<br/><a NAME="E10:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c3</font> &amp; (  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">x3</font> or  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">y3</font> ) &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D27" target="_self">Def27</a>, </i>;<br/><a NAME="E11:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x3</font>,<font color="Maroon">y3</font>,<font color="Maroon">c3</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i>, </i>;<br/><a NAME="E12:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c4</font> &amp;  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">n4</font> )
 <b>by </b><i><a class="ref" href="gate_1.html#D23" target="_self">Def23</a></i>;<br/><a NAME="E13:37_1"/><b>then </b>
(  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c4</font> &amp; (  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">x4</font> or  <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">y4</font> ) )
 <b>by </b><i><a class="ref" href="gate_1.html#D28" target="_self">Def28</a>, </i>;<br/><b>hence </b><a NAME="E14:37_1"/>
 <a href="gate_1.html#NR1" target="_self">$</a>  <a href="gate_1.html#K11" target="_self">MAJ3</a> <font color="Maroon">x4</font>,<font color="Maroon">y4</font>,<font color="Maroon">c4</font>
 <b>by </b><i>, </i>;<br/></div><b>end;</b></div>
<b>hence </b><a NAME="E17:37"/>
 <a href="gate_1.html#NR1" target="_self">$</a> <font color="Maroon">c5</font>
 <b>by </b><i><a class="ref" href="gate_1.html#D24" target="_self">Def24</a>, <a class="ref" href="gate_1.html#D32" target="_self">Def32</a></i>;<br/>


</div>
