<kat>
<lib><id>sup0R</id><condeqn>x + y = 0 -> y = 0</condeqn><task></task><proof><LAMBDAS><id>y</id><id>x</id><LAMBDAP><id>P9</id><APPLYP><APPLYS><CONST>@=</CONST><sub><id>x</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x + y</term></sub><sub><id>x</id><term>y</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYS><CONST>supR</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>0</term></sub></APPLYS><VAR>P9</VAR></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>sup0L</id><condeqn>x + y = 0 -> x = 0</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P8</id><APPLYP><APPLYS><CONST>@=</CONST><sub><id>x</id><term>x</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x + y</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYS><CONST>supL</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>0</term></sub></APPLYS><VAR>P8</VAR></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>sup0</id><condeqn>x = 0 -> y = 0 -> x + y = 0</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P10</id><id>P11</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + 0</term></sub><sub><id>x</id><term>x + y</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><VAR>P11</VAR></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0 + 0</term></sub><sub><id>x</id><term>x + 0</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><VAR>P10</VAR></APPLYP><APPLYS><CONST>id+R</CONST><sub><id>x</id><term>0</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>@=</id><condeqn>x @ 0 -> x = 0</condeqn><task></task><proof><LAMBDAS><id>x</id><LAMBDAP><id>P12</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + 0</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x + 0</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><APPLYS><CONST>id+R</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>0</term></sub></APPLYS><VAR>P12</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>pC1</id><condeqn>p = p;C -> p;~C = 0</condeqn><task></task><proof><LAMBDAS><id>p</id><id>C</id><LAMBDAP><id>P3</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;C;~C</term></sub><sub><id>x</id><term>p;~C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>p;C</term></sub><sub><id>z</id><term>~C</term></sub></APPLYS><VAR>P3</VAR></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;0</term></sub><sub><id>x</id><term>p;C;~C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>C;~C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYS><CONST>compl.</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP><APPLYS><CONST>annihR</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>pC2</id><condeqn>p;~C = 0 -> p = p;C</condeqn><task></task><proof><LAMBDAS><id>p</id><id>C</id><LAMBDAP><id>P4</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;(C + ~C)</term></sub><sub><id>x</id><term>p</term></sub><sub><id>z</id><term>p;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>p;(C + ~C)</term></sub><sub><id>y</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;1</term></sub><sub><id>x</id><term>p;(C + ~C)</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>C + ~C</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYS><CONST>compl+</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;C + p;~C</term></sub><sub><id>x</id><term>p;(C + ~C)</term></sub><sub><id>z</id><term>p;C</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>C</term></sub><sub><id>z</id><term>~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;C + 0</term></sub><sub><id>x</id><term>p;C + p;~C</term></sub><sub><id>z</id><term>p;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>p;C</term></sub><sub><id>y</id><term>p;~C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><VAR>P4</VAR></APPLYP><APPLYS><CONST>id+R</CONST><sub><id>x</id><term>p;C</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>pC3</id><condeqn>p = p;~C -> p;C = 0</condeqn><task></task><proof><LAMBDAS><id>p</id><id>C</id><LAMBDAP><id>P6</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;~~C</term></sub><sub><id>x</id><term>p;C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>C</term></sub><sub><id>z</id><term>~~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>~~C</term></sub><sub><id>y</id><term>C</term></sub></APPLYS><APPLYS><CONST>~~</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>pC1</CONST><sub><id>C</id><term>~C</term></sub><sub><id>p</id><term>p</term></sub></APPLYS><VAR>P6</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>pC4</id><condeqn>p;C = 0 -> p = p;~C</condeqn><task></task><proof><LAMBDAS><id>p</id><id>C</id><LAMBDAP><id>P7</id><APPLYP><APPLYS><CONST>pC2</CONST><sub><id>C</id><term>~C</term></sub><sub><id>p</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;C</term></sub><sub><id>x</id><term>p;~~C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>~~C</term></sub><sub><id>z</id><term>C</term></sub></APPLYS><APPLYS><CONST>~~</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP><VAR>P7</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>Bp3</id><condeqn>p = ~B;p -> B;p = 0</condeqn><task></task><proof><LAMBDAS><id>B</id><id>p</id><LAMBDAP><id>P1</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;~B;p</term></sub><sub><id>x</id><term>B;p</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>p</term></sub><sub><id>z</id><term>~B;p</term></sub></APPLYS><VAR>P1</VAR></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0;p</term></sub><sub><id>x</id><term>B;~B;p</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>B;~B</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYS><CONST>compl.</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP><APPLYS><CONST>annihL</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>Bp4</id><condeqn>B;p = 0 -> p = ~B;p</condeqn><task></task><proof><LAMBDAS><id>p</id><id>B</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>(B + ~B);p</term></sub><sub><id>x</id><term>p</term></sub><sub><id>z</id><term>~B;p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>1;p</term></sub><sub><id>x</id><term>p</term></sub><sub><id>z</id><term>(B + ~B);p</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>1;p</term></sub><sub><id>y</id><term>p</term></sub></APPLYS><APPLYS><CONST>id.L</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>B + ~B</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>B + ~B</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>compl+</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;p + ~B;p</term></sub><sub><id>x</id><term>(B + ~B);p</term></sub><sub><id>z</id><term>~B;p</term></sub></APPLYS><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>~B</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0 + ~B;p</term></sub><sub><id>x</id><term>B;p + ~B;p</term></sub><sub><id>z</id><term>~B;p</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>B;p</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>~B;p</term></sub></APPLYS><VAR>P0</VAR></APPLYP><APPLYS><CONST>id+L</CONST><sub><id>x</id><term>~B;p</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>Bp1</id><condeqn>p = B;p -> ~B;p = 0</condeqn><task></task><proof><LAMBDAS><id>B</id><id>p</id><LAMBDAP><id>P3</id><APPLYP><APPLYS><CONST>Bp3</CONST><sub><id>B</id><term>~B</term></sub><sub><id>p</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;p</term></sub><sub><id>x</id><term>p</term></sub><sub><id>z</id><term>~~B;p</term></sub></APPLYS><VAR>P3</VAR><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>~~B</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>~~B</term></sub><sub><id>y</id><term>B</term></sub></APPLYS><APPLYS><CONST>~~</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>Bp2</id><condeqn>~B;p = 0 -> p = B;p</condeqn><task></task><proof><LAMBDAS><id>p</id><id>B</id><LAMBDAP><id>P2</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~~B;p</term></sub><sub><id>x</id><term>p</term></sub><sub><id>z</id><term>B;p</term></sub></APPLYS><APPLYP><APPLYS><CONST>Bp4</CONST><sub><id>B</id><term>~B</term></sub><sub><id>p</id><term>p</term></sub></APPLYS><VAR>P2</VAR></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>~~B</term></sub><sub><id>y</id><term>B</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYS><CONST>~~</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>assg</id><condeqn>B;p = p;C -> ~B;p = p;~C</condeqn><task></task><proof><LAMBDAS><id>B</id><id>p</id><id>C</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~B;p;~C</term></sub><sub><id>x</id><term>~B;p</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~B;p;(C + ~C)</term></sub><sub><id>x</id><term>~B;p</term></sub><sub><id>z</id><term>~B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~B;p;1</term></sub><sub><id>x</id><term>~B;p</term></sub><sub><id>z</id><term>~B;p;(C + ~C)</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>~B;p;1</term></sub><sub><id>y</id><term>~B;p</term></sub></APPLYS><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>~B;p</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>~B;p</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>C + ~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>C + ~C</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>compl+</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~B;p;C + ~B;p;~C</term></sub><sub><id>x</id><term>~B;p;(C + ~C)</term></sub><sub><id>z</id><term>~B;p;~C</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>~B;p</term></sub><sub><id>y</id><term>C</term></sub><sub><id>z</id><term>~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0 + ~B;p;~C</term></sub><sub><id>x</id><term>~B;p;C + ~B;p;~C</term></sub><sub><id>z</id><term>~B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>~B;p;C</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>~B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>~B;B;p</term></sub><sub><id>x</id><term>~B;p;C</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>~B</term></sub><sub><id>y</id><term>p;C</term></sub><sub><id>z</id><term>B;p</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>B;p</term></sub><sub><id>y</id><term>p;C</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0;p</term></sub><sub><id>x</id><term>~B;B;p</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>~B;B</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>p</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;~B</term></sub><sub><id>x</id><term>~B;B</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYS><CONST>commut.</CONST><sub><id>B</id><term>~B</term></sub><sub><id>C</id><term>B</term></sub></APPLYS><APPLYS><CONST>compl.</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP></APPLYP><APPLYS><CONST>annihL</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYS><CONST>id+L</CONST><sub><id>x</id><term>~B;p;~C</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;p;~C + ~B;p;~C</term></sub><sub><id>x</id><term>~B;p;~C</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>0 + ~B;p;~C</term></sub><sub><id>x</id><term>~B;p;~C</term></sub><sub><id>z</id><term>B;p;~C + ~B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>0 + ~B;p;~C</term></sub><sub><id>y</id><term>~B;p;~C</term></sub></APPLYS><APPLYS><CONST>id+L</CONST><sub><id>x</id><term>~B;p;~C</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>0</term></sub><sub><id>y</id><term>B;p;~C</term></sub><sub><id>z</id><term>~B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;C;~C</term></sub><sub><id>x</id><term>0</term></sub><sub><id>z</id><term>B;p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>p;0</term></sub><sub><id>x</id><term>0</term></sub><sub><id>z</id><term>p;C;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>p;0</term></sub><sub><id>y</id><term>0</term></sub></APPLYS><APPLYS><CONST>annihR</CONST><sub><id>x</id><term>p</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>p</term></sub><sub><id>y</id><term>0</term></sub><sub><id>z</id><term>C;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>C;~C</term></sub><sub><id>y</id><term>0</term></sub></APPLYS><APPLYS><CONST>compl.</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>p;C</term></sub><sub><id>y</id><term>B;p</term></sub><sub><id>z</id><term>~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>B;p</term></sub><sub><id>y</id><term>p;C</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>(B + ~B);p;~C</term></sub><sub><id>x</id><term>B;p;~C + ~B;p;~C</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>(B + ~B);p;~C</term></sub><sub><id>y</id><term>B;p;~C + ~B;p;~C</term></sub></APPLYS><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>~B</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>1;p;~C</term></sub><sub><id>x</id><term>(B + ~B);p;~C</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>B + ~B</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>p;~C</term></sub></APPLYS><APPLYS><CONST>compl+</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP><APPLYS><CONST>id.L</CONST><sub><id>x</id><term>p;~C</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>cond</id><condeqn>C;B;p;~D = 0 -> C;~B;q;~D = 0 -> C;(B;p + ~B;q);~D = 0</condeqn><task></task><proof><LAMBDAS><id>C</id><id>B</id><id>p</id><id>q</id><id>D</id><LAMBDAP><id>P0</id><id>P1</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>C;B;p;~D + C;~B;q;~D</term></sub><sub><id>x</id><term>C;(B;p + ~B;q);~D</term></sub><sub><id>z</id><term>0</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>(C;B;p + C;~B;q);~D</term></sub><sub><id>x</id><term>C;(B;p + ~B;q);~D</term></sub><sub><id>z</id><term>C;B;p;~D + C;~B;q;~D</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>C;(B;p + ~B;q)</term></sub><sub><id>y</id><term>C;B;p + C;~B;q</term></sub><sub><id>z</id><term>~D</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>B;p</term></sub><sub><id>z</id><term>~B;q</term></sub></APPLYS></APPLYP><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>C;B;p</term></sub><sub><id>y</id><term>C;~B;q</term></sub><sub><id>z</id><term>~D</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>sup0</CONST><sub><id>x</id><term>C;B;p;~D</term></sub><sub><id>y</id><term>C;~B;q;~D</term></sub></APPLYS><VAR>P0</VAR><VAR>P1</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>comp</id><condeqn>C;p = C;p;D -> D;q = D;q;E -> C;p;q = C;p;q;E</condeqn><task></task><proof><LAMBDAS><id>C</id><id>p</id><id>q</id><id>E</id><id>D</id><LAMBDAP><id>P2</id><id>P3</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>C;p;D;q</term></sub><sub><id>x</id><term>C;p;q</term></sub><sub><id>z</id><term>C;p;q;E</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>C;p</term></sub><sub><id>y</id><term>C;p;D</term></sub><sub><id>z</id><term>q</term></sub></APPLYS><VAR>P2</VAR></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>C;p;D;q;E</term></sub><sub><id>x</id><term>C;p;D;q</term></sub><sub><id>z</id><term>C;p;q;E</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>C;p</term></sub><sub><id>y</id><term>D;q</term></sub><sub><id>z</id><term>D;q;E</term></sub></APPLYS><VAR>P3</VAR></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>C;p;D</term></sub><sub><id>y</id><term>C;p</term></sub><sub><id>z</id><term>q;E</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>C;p</term></sub><sub><id>y</id><term>C;p;D</term></sub></APPLYS><VAR>P2</VAR></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>while'</id><condeqn>C;q = C;q;C -> C;q* = C;q*;C</condeqn><task></task><proof><LAMBDAS><id>C</id><id>q</id><LAMBDAP><id>P2</id><APPLYP><APPLYS><CONST>antisym</CONST><sub><id>x</id><term>C;q*</term></sub><sub><id>y</id><term>C;q*;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>*L</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>q</term></sub><sub><id>z</id><term>C;q*;C</term></sub></APPLYS><SUBST><focus>0 0 2 2</focus><eqn>C;q*;C;q + C @ C;q*;C</eqn><dir>L</dir><VAR>P2</VAR><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>C;q*;q;C + C</term></sub><sub><id>x</id><term>C;q*;C;q;C + C</term></sub><sub><id>z</id><term>C;q*;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono+R</CONST><sub><id>x</id><term>C;q*;C;q;C</term></sub><sub><id>y</id><term>C;q*;q;C</term></sub><sub><id>z</id><term>C</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>C;q*;C</term></sub><sub><id>y</id><term>C;q*</term></sub><sub><id>z</id><term>q;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.L</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>q*;C</term></sub><sub><id>z</id><term>q*</term></sub></APPLYS><SUBST><focus>1 1</focus><eqn>q*;C @ q*</eqn><dir>R</dir><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>q*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.L</CONST><sub><id>x</id><term>q*</term></sub><sub><id>y</id><term>C</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>@1</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP></SUBST></APPLYP></APPLYP></APPLYP><SUBST><focus>0 1 1</focus><eqn>C;q*;q;C + C @ C;q*;C</eqn><dir>R</dir><APPLYS><CONST>idemp.</CONST><sub><id>B</id><term>C</term></sub></APPLYS><SUBST><focus>0 1 0 1</focus><eqn>C;q*;q;C + C;C @ C;q*;C</eqn><dir>R</dir><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>C</term></sub></APPLYS><SUBST><focus>0 1</focus><eqn>C;q*;q;C + C;1;C @ C;q*;C</eqn><dir>R</dir><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>q*;q;C</term></sub><sub><id>z</id><term>1;C</term></sub></APPLYS><SUBST><focus>0 1 1</focus><eqn>C;(q*;q;C + 1;C) @ C;q*;C</eqn><dir>R</dir><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>q*;q</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>C</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>C;(q*;q + 1)</term></sub><sub><id>y</id><term>C;q*</term></sub><sub><id>z</id><term>C</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.L</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>q*;q + 1</term></sub><sub><id>z</id><term>q*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>q*;q + 1</term></sub><sub><id>y</id><term>q*</term></sub></APPLYS><SUBST><focus>0 1</focus><eqn>q*;q + 1 = q*</eqn><dir>L</dir><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>q*;q</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>unwindR</CONST><sub><id>x</id><term>q</term></sub></APPLYS></SUBST></APPLYP></APPLYP></APPLYP></SUBST></SUBST></SUBST></SUBST></APPLYP></SUBST></APPLYP><SUBST><focus>1 1</focus><eqn>C;q*;C @ C;q*</eqn><dir>R</dir><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>C;q*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.L</CONST><sub><id>x</id><term>C;q*</term></sub><sub><id>y</id><term>C</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>C</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>@1</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP></SUBST></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>while</id><condeqn>B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B</condeqn><task></task><proof><LAMBDAS><id>C</id><id>B</id><id>p</id><LAMBDAP><id>P0</id><SUBST><focus>1 2 2</focus><eqn>C;(B;p)*;~B = C;(B;p)*;~B;C;~B</eqn><dir>L</dir><APPLYS><CONST>commut.</CONST><sub><id>B</id><term>~B</term></sub><sub><id>C</id><term>C</term></sub></APPLYS><SUBST><focus>1 3 2</focus><eqn>C;(B;p)*;~B = C;(B;p)*;C;~B;~B</eqn><dir>L</dir><APPLYS><CONST>idemp.</CONST><sub><id>B</id><term>~B</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>C;(B;p)*</term></sub><sub><id>y</id><term>C;(B;p)*;C</term></sub><sub><id>z</id><term>~B</term></sub></APPLYS><APPLYP><APPLYS><CONST>while'</CONST><sub><id>C</id><term>C</term></sub><sub><id>q</id><term>B;p</term></sub></APPLYS><SUBST><focus>0 0 2</focus><eqn>C;B;p = C;B;p;C</eqn><dir>L</dir><APPLYS><CONST>commut.</CONST><sub><id>B</id><term>C</term></sub><sub><id>C</id><term>B</term></sub></APPLYS><SUBST><focus>1 0 2</focus><eqn>B;C;p = C;B;p;C</eqn><dir>L</dir><APPLYS><CONST>commut.</CONST><sub><id>B</id><term>C</term></sub><sub><id>C</id><term>B</term></sub></APPLYS><VAR>P0</VAR></SUBST></SUBST></APPLYP></APPLYP></SUBST></SUBST></LAMBDAP></LAMBDAS></proof></lib>
</kat>
