<kat>
<lib><id>id+L</id><condeqn>0 + x = x</condeqn><task></task><proof><LAMBDAS><id>x</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + 0</term></sub><sub><id>x</id><term>0 + x</term></sub><sub><id>z</id><term>x</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>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></LAMBDAS></proof></lib>
<lib><id>cong+L</id><condeqn>y = z -> x + y = x + z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P1</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>y + x</term></sub><sub><id>x</id><term>x + y</term></sub><sub><id>z</id><term>x + z</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>z + x</term></sub><sub><id>x</id><term>y + x</term></sub><sub><id>z</id><term>x + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub><sub><id>z</id><term>x</term></sub></APPLYS><VAR>P1</VAR></APPLYP><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>z</term></sub><sub><id>y</id><term>x</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>ref@</id><condeqn>x @ x</condeqn><task></task><proof><LAMBDAS><id>x</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP></LAMBDAS></proof></lib>
<lib><id>antisym</id><condeqn>x @ y -> y @ x -> x = y</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P0</id><id>P1</id><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>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>y + x</term></sub><sub><id>x</id><term>x + y</term></sub><sub><id>z</id><term>x</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><VAR>P1</VAR></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>trans@</id><condeqn>x @ y -> y @ z -> x @ z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>z</id><id>y</id><LAMBDAP><id>P2</id><id>P3</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + y + z</term></sub><sub><id>x</id><term>x + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>y + z</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P3</VAR></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>y + z</term></sub><sub><id>x</id><term>x + y + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><VAR>P2</VAR></APPLYP></APPLYP><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P3</VAR></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>supL</id><condeqn>x @ x + y</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x + y</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + x</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAS></proof></lib>
<lib><id>supR</id><condeqn>y @ x + y</condeqn><task></task><proof><LAMBDAS><id>y</id><id>x</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>x + y</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + y + y</term></sub><sub><id>x</id><term>y + x + y</term></sub><sub><id>z</id><term>x + y</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>y + x</term></sub><sub><id>y</id><term>x + y</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>x</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y + y</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>y</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></LAMBDAS></proof></lib>
<lib><id>sup</id><condeqn>x @ z -> y @ z -> x + y @ z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P0</id><id>P1</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>y + z</term></sub><sub><id>x</id><term>x + y + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + z + y</term></sub><sub><id>x</id><term>x + y + z</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y + z</term></sub><sub><id>z</id><term>z + y</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>z + y</term></sub><sub><id>x</id><term>x + z + y</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + z</term></sub><sub><id>y</id><term>z</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>z</term></sub><sub><id>y</id><term>y</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P1</VAR></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>=@</id><condeqn>x = y -> x @ y</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + x</term></sub><sub><id>x</id><term>x + y</term></sub><sub><id>z</id><term>y</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>x</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x</term></sub><sub><id>x</id><term>x + x</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>x</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono+L</id><condeqn>y @ z -> x + y @ x + z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>x + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + x + y + z</term></sub><sub><id>x</id><term>x + y + x + z</term></sub><sub><id>z</id><term>x + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y + x + z</term></sub><sub><id>z</id><term>x + y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>y + x</term></sub><sub><id>y</id><term>x + y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>x</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + y + z</term></sub><sub><id>x</id><term>x + x + y + z</term></sub><sub><id>z</id><term>x + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + x</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono+R</id><condeqn>x @ y -> x + z @ y + z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>z</id><id>y</id><LAMBDAP><id>P2</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x + z</term></sub><sub><id>y</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + y + z + z</term></sub><sub><id>x</id><term>x + z + y + z</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + z + y</term></sub><sub><id>y</id><term>x + y + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z + y</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>z</term></sub><sub><id>y</id><term>y</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + y + z</term></sub><sub><id>x</id><term>x + y + z + z</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>z + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYS><CONST>idemp+</CONST><sub><id>x</id><term>z</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><VAR>P2</VAR></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono.L</id><condeqn>y @ z -> x;y @ x;z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P1</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x;y</term></sub><sub><id>y</id><term>x;z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x;(y + z)</term></sub><sub><id>x</id><term>x;y + x;z</term></sub><sub><id>z</id><term>x;z</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x;(y + z)</term></sub><sub><id>y</id><term>x;y + x;z</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y + z</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS><VAR>P1</VAR></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono.R</id><condeqn>x @ y -> x;z @ y;z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>z</id><id>y</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>@intro</CONST><sub><id>x</id><term>x;z</term></sub><sub><id>y</id><term>y;z</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>(x + y);z</term></sub><sub><id>x</id><term>x;z + y;z</term></sub><sub><id>z</id><term>y;z</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>(x + y);z</term></sub><sub><id>y</id><term>x;z + y;z</term></sub></APPLYS><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>@elim</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono*</id><condeqn>x @ y -> x* @ y*</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x*;1</term></sub><sub><id>x</id><term>x*</term></sub><sub><id>z</id><term>y*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>x*</term></sub><sub><id>y</id><term>x*;1</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x*;1</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><APPLYP><APPLYS><CONST>*R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>y*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + y;y*</term></sub><sub><id>x</id><term>x;y* + 1</term></sub><sub><id>z</id><term>y*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>y;y* + 1</term></sub><sub><id>x</id><term>x;y* + 1</term></sub><sub><id>z</id><term>1 + y;y*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono+R</CONST><sub><id>x</id><term>x;y*</term></sub><sub><id>y</id><term>y;y*</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>y*</term></sub></APPLYS><VAR>P0</VAR></APPLYP></APPLYP><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>y;y* + 1</term></sub><sub><id>y</id><term>1 + y;y*</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>y;y*</term></sub><sub><id>y</id><term>1</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>1 + y;y*</term></sub><sub><id>y</id><term>y*</term></sub></APPLYS><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>y</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>slide</id><condeqn>x;(y;x)* = (x;y)*;x</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><APPLYP><APPLYS><CONST>antisym</CONST><sub><id>x</id><term>x;(y;x)*</term></sub><sub><id>y</id><term>(x;y)*;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>*L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y;x</term></sub><sub><id>z</id><term>(x;y)*;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>(x;y)*;x;y;x + x</term></sub><sub><id>y</id><term>(x;y)*;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>(x;y)*;x;y;x + 1;x</term></sub><sub><id>x</id><term>(x;y)*;x;y;x + x</term></sub><sub><id>z</id><term>(x;y)*;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+L</CONST><sub><id>x</id><term>(x;y)*;x;y;x</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>1;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>1;x</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><APPLYS><CONST>id.L</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>((x;y)*;x;y + 1);x</term></sub><sub><id>x</id><term>(x;y)*;x;y;x + 1;x</term></sub><sub><id>z</id><term>(x;y)*;x</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>((x;y)*;x;y + 1);x</term></sub><sub><id>y</id><term>(x;y)*;x;y;x + 1;x</term></sub></APPLYS><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>(x;y)*;x;y</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>x</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.R</CONST><sub><id>x</id><term>(x;y)*;x;y + 1</term></sub><sub><id>y</id><term>(x;y)*</term></sub><sub><id>z</id><term>x</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>1 + (x;y)*;x;y</term></sub><sub><id>x</id><term>(x;y)*;x;y + 1</term></sub><sub><id>z</id><term>(x;y)*</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>(x;y)*;x;y</term></sub><sub><id>y</id><term>1</term></sub></APPLYS><APPLYS><CONST>unwindR</CONST><sub><id>x</id><term>x;y</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>*R</CONST><sub><id>x</id><term>x;y</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>x;(y;x)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>x;y;x;(y;x)* + x</term></sub><sub><id>y</id><term>x;(y;x)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x + x;y;x;(y;x)*</term></sub><sub><id>x</id><term>x;y;x;(y;x)* + x</term></sub><sub><id>z</id><term>x;(y;x)*</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>x;y;x;(y;x)*</term></sub><sub><id>y</id><term>x</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x;1 + x;y;x;(y;x)*</term></sub><sub><id>x</id><term>x + x;y;x;(y;x)*</term></sub><sub><id>z</id><term>x;(y;x)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x;1</term></sub><sub><id>z</id><term>x;y;x;(y;x)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x;1</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><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>x;(1 + y;x;(y;x)*)</term></sub><sub><id>x</id><term>x;1 + x;y;x;(y;x)*</term></sub><sub><id>z</id><term>x;(y;x)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>x;(1 + y;x;(y;x)*)</term></sub><sub><id>y</id><term>x;1 + x;y;x;(y;x)*</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>y;x;(y;x)*</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>1 + y;x;(y;x)*</term></sub><sub><id>z</id><term>(y;x)*</term></sub></APPLYS><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>y;x</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAS></proof></lib>
<lib><id>denest</id><condeqn>x*;(y;x*)* = (x + y)*</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><APPLYP><APPLYS><CONST>antisym</CONST><sub><id>x</id><term>x*;(y;x*)*</term></sub><sub><id>y</id><term>(x + y)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>*L</CONST><sub><id>x</id><term>x*</term></sub><sub><id>y</id><term>y;x*</term></sub><sub><id>z</id><term>(x + y)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sup</CONST><sub><id>x</id><term>(x + y)*;y;x*</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>(x + y)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>*L</CONST><sub><id>x</id><term>(x + y)*;y</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>(x + y)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>(x + y)*;(x + y)</term></sub><sub><id>x</id><term>(x + y)*;x + (x + y)*;y</term></sub><sub><id>z</id><term>(x + y)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>(x + y)*;x + (x + y)*;y</term></sub><sub><id>y</id><term>(x + y)*;(x + y)</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>(x + y)*;(x + y)</term></sub><sub><id>y</id><term>(x + y)*;x + (x + y)*;y</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>(x + y)*</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>y</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + (x + y)*;(x + y)</term></sub><sub><id>x</id><term>(x + y)*;(x + y)</term></sub><sub><id>z</id><term>(x + y)*</term></sub></APPLYS><APPLYS><CONST>supR</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>(x + y)*;(x + y)</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>1 + (x + y)*;(x + y)</term></sub><sub><id>y</id><term>(x + y)*</term></sub></APPLYS><APPLYS><CONST>unwindR</CONST><sub><id>x</id><term>x + y</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>mono*</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x + y</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></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>(x + y)*;1</term></sub><sub><id>x</id><term>(x + y)*</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>(x + y)*</term></sub><sub><id>y</id><term>(x + y)*;1</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>(x + y)*;1</term></sub><sub><id>y</id><term>(x + y)*</term></sub></APPLYS><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>(x + y)*</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>*R</CONST><sub><id>x</id><term>x + y</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x;x*;(y;x*)* + y;x*;(y;x*)* + 1</term></sub><sub><id>x</id><term>(x + y);x*;(y;x*)* + 1</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>(x + y);x*;(y;x*)* + 1</term></sub><sub><id>y</id><term>x;x*;(y;x*)* + y;x*;(y;x*)* + 1</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>(x + y);x*;(y;x*)*</term></sub><sub><id>y</id><term>x;x*;(y;x*)* + y;x*;(y;x*)*</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>sup</CONST><sub><id>x</id><term>x;x*;(y;x*)*</term></sub><sub><id>y</id><term>y;x*;(y;x*)* + 1</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>x;x*</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + x;x*</term></sub><sub><id>x</id><term>x;x*</term></sub><sub><id>z</id><term>x*</term></sub></APPLYS><APPLYS><CONST>supR</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>x;x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>1 + x;x*</term></sub><sub><id>y</id><term>x*</term></sub></APPLYS><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + y;x*;(y;x*)*</term></sub><sub><id>x</id><term>y;x*;(y;x*)* + 1</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>y;x*;(y;x*)* + 1</term></sub><sub><id>y</id><term>1 + y;x*;(y;x*)*</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>y;x*;(y;x*)*</term></sub><sub><id>y</id><term>1</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>(y;x*)*</term></sub><sub><id>x</id><term>1 + y;x*;(y;x*)*</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>1 + y;x*;(y;x*)*</term></sub><sub><id>y</id><term>(y;x*)*</term></sub></APPLYS><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>y;x*</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1;(y;x*)*</term></sub><sub><id>x</id><term>(y;x*)*</term></sub><sub><id>z</id><term>x*;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>(y;x*)*</term></sub><sub><id>y</id><term>1;(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>1;(y;x*)*</term></sub><sub><id>y</id><term>(y;x*)*</term></sub></APPLYS><APPLYS><CONST>id.L</CONST><sub><id>x</id><term>(y;x*)*</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>(y;x*)*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + x;x*</term></sub><sub><id>x</id><term>1</term></sub><sub><id>z</id><term>x*</term></sub></APPLYS><APPLYS><CONST>supL</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>x;x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>=@</CONST><sub><id>x</id><term>1 + x;x*</term></sub><sub><id>y</id><term>x*</term></sub></APPLYS><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>x</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></APPLYP></LAMBDAS></proof></lib>
</kat>
