<kat>
<lib><id>app*L</id><condeqn>y @ z -> y @ x*;z</condeqn><task></task><proof><LAMBDAS><id>y</id><id>x</id><id>z</id><LAMBDAP><id>P2</id><SUBST><focus>1 0 1</focus><eqn>y @ x*;z</eqn><dir>R</dir><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>x</term></sub></APPLYS><SUBST><focus>1 1</focus><eqn>y @ (1 + x;x*);z</eqn><dir>L</dir><APPLYS><CONST>distrR</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>x;x*</term></sub><sub><id>z</id><term>z</term></sub></APPLYS><SUBST><focus>1 0 1</focus><eqn>y @ 1;z + x;x*;z</eqn><dir>L</dir><APPLYS><CONST>id.L</CONST><sub><id>x</id><term>z</term></sub></APPLYS><APPLYP><APPLYS><CONST>monosupL</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub><sub><id>z</id><term>x;x*;z</term></sub></APPLYS><VAR>P2</VAR></APPLYP></SUBST></SUBST></SUBST></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>app*R</id><condeqn>x @ y -> x @ y;z*</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P7</id><SUBST><focus>1 1 1</focus><eqn>x @ y;z*</eqn><dir>R</dir><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>z</term></sub></APPLYS><SUBST><focus>1 1</focus><eqn>x @ y;(1 + z;z*)</eqn><dir>L</dir><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>z;z*</term></sub></APPLYS><SUBST><focus>1 0 1</focus><eqn>x @ y;1 + y;z;z*</eqn><dir>L</dir><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>y</term></sub></APPLYS><APPLYP><APPLYS><CONST>monosupL</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>y;z;z*</term></sub></APPLYS><VAR>P7</VAR></APPLYP></SUBST></SUBST></SUBST></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>x*x*</id><condeqn>x*;x* @ x*</condeqn><task></task><proof><LAMBDAS><id>x</id><APPLYP><APPLYS><CONST>*R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sup</CONST><sub><id>x</id><term>x;x*</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>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><APPLYS><CONST>ref@</CONST><sub><id>x</id><term>x*</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAS></proof></lib>
<lib><id>xx*</id><condeqn>x @ x*</condeqn><task></task><proof><LAMBDAS><id>x</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1 + x;x*</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>monosupR</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>x;x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x;(1 + x;x*)</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>x;x*</term></sub></APPLYS><SUBST><focus>1 1</focus><eqn>x @ x;(1 + x;x*)</eqn><dir>L</dir><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>x;x*</term></sub></APPLYS><SUBST><focus>1 0 1</focus><eqn>x @ x;1 + x;x;x*</eqn><dir>L</dir><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>x</term></sub></APPLYS><APPLYS><CONST>supL</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x;x;x*</term></sub></APPLYS></SUBST></SUBST><SUBST><focus>0 1 1</focus><eqn>x;(1 + x;x*) @ x;x*</eqn><dir>L</dir><APPLYS><CONST>unwindL</CONST><sub><id>x</id><term>x</term></sub></APPLYS><APPLYS><CONST>ref@</CONST><sub><id>x</id><term>x;x*</term></sub></APPLYS></SUBST></APPLYP></APPLYP><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></LAMBDAS></proof></lib>
<lib><id>**</id><condeqn>x** @ x*</condeqn><task></task><proof><LAMBDAS><id>x</id><APPLYP><APPLYS><CONST>*1R</CONST><sub><id>x</id><term>x*</term></sub><sub><id>y</id><term>x*</term></sub></APPLYS><APPLYP><APPLYS><CONST>sup</CONST><sub><id>x</id><term>x*;x*</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>x*</term></sub></APPLYS><APPLYS><CONST>x*x*</CONST><sub><id>x</id><term>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></LAMBDAS></proof></lib>
<lib><id>1x*</id><condeqn>1 @ x*</condeqn><task></task><proof><LAMBDAS><id>x</id><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></LAMBDAS></proof></lib>
<lib><id>@*</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>P5</id><id>P6</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x*;z*</term></sub><sub><id>x</id><term>x;y</term></sub><sub><id>z</id><term>z*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.LR</CONST><sub><id>w</id><term>z*</term></sub><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>x*</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><APPLYS><CONST>xx*</CONST><sub><id>x</id><term>x</term></sub></APPLYS><VAR>P6</VAR></APPLYP><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>z*;z*</term></sub><sub><id>x</id><term>x*;z*</term></sub><sub><id>z</id><term>z*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.LR</CONST><sub><id>w</id><term>z*</term></sub><sub><id>x</id><term>x*</term></sub><sub><id>y</id><term>z*</term></sub><sub><id>z</id><term>z*</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>z**</term></sub><sub><id>x</id><term>x*</term></sub><sub><id>z</id><term>z*</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono*</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z*</term></sub></APPLYS><VAR>P5</VAR></APPLYP><APPLYS><CONST>**</CONST><sub><id>x</id><term>z</term></sub></APPLYS></APPLYP><APPLYS><CONST>ref@</CONST><sub><id>x</id><term>z*</term></sub></APPLYS></APPLYP><APPLYS><CONST>x*x*</CONST><sub><id>x</id><term>z</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>*1L</id><condeqn>y;x + 1 @ y -> x* @ y</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><LAMBDAP><id>P1</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>1;x*</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>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>*L</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>x</term></sub><sub><id>z</id><term>y</term></sub></APPLYS><VAR>P1</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>*1R</id><condeqn>x;y + 1 @ 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><VAR>P0</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
</kat>
