<kat>
<lib><id>cong~</id><condeqn>B = C -> ~B = ~C</condeqn><task></task><proof><AXIOM>cong~</AXIOM></proof></lib>
<lib><id>mono~</id><condeqn>B @ C -> ~C @ ~B</condeqn><task></task><proof><AXIOM>mono~</AXIOM></proof></lib>
<lib><id>commut.</id><condeqn>B;C = C;B</condeqn><task></task><proof><AXIOM>commut.</AXIOM></proof></lib>
<lib><id>idemp.</id><condeqn>B;B = B</condeqn><task></task><proof><AXIOM>idemp.</AXIOM></proof></lib>
<lib><id>~~</id><condeqn>~~B = B</condeqn><task></task><proof><AXIOM>~~</AXIOM></proof></lib>
<lib><id>deMorgan+</id><condeqn>~(B + C) = ~B;~C</condeqn><task></task><proof><AXIOM>deMorgan+</AXIOM></proof></lib>
<lib><id>deMorgan.</id><condeqn>~(B;C) = ~B + ~C</condeqn><task></task><proof><AXIOM>deMorgan.</AXIOM></proof></lib>
<lib><id>~0</id><condeqn>~0 = 1</condeqn><task></task><proof><AXIOM>~0</AXIOM></proof></lib>
<lib><id>~1</id><condeqn>~1 = 0</condeqn><task></task><proof><AXIOM>~1</AXIOM></proof></lib>
<lib><id>compl+</id><condeqn>B + ~B = 1</condeqn><task></task><proof><AXIOM>compl+</AXIOM></proof></lib>
<lib><id>compl.</id><condeqn>B;~B = 0</condeqn><task></task><proof><AXIOM>compl.</AXIOM></proof></lib>
<lib><id>@1</id><condeqn>B + 1 = 1</condeqn><task></task><proof><AXIOM>@1</AXIOM></proof></lib>
<lib><id>distr.L</id><condeqn>B + C;D = (B + C);(B + D)</condeqn><task></task><proof><AXIOM>distr.L</AXIOM></proof></lib>
<lib><id>distr.R</id><condeqn>B;C + D = (B + D);(C + D)</condeqn><task></task><proof><AXIOM>distr.R</AXIOM></proof></lib>
<lib><id>abs+</id><condeqn>B + B;C = B</condeqn><task></task><proof><LAMBDAS><id>B</id><id>C</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;1 + B;C</term></sub><sub><id>x</id><term>B + B;C</term></sub><sub><id>z</id><term>B</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>B;1</term></sub><sub><id>z</id><term>B;C</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>B;1</term></sub><sub><id>y</id><term>B</term></sub></APPLYS><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>B</term></sub></APPLYS></APPLYP></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;(1 + C)</term></sub><sub><id>x</id><term>B;1 + B;C</term></sub><sub><id>z</id><term>B</term></sub></APPLYS><APPLYP><APPLYS><CONST>sym</CONST><sub><id>x</id><term>B;(1 + C)</term></sub><sub><id>y</id><term>B;1 + B;C</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>1</term></sub><sub><id>z</id><term>C</term></sub></APPLYS></APPLYP><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;1</term></sub><sub><id>x</id><term>B;(1 + C)</term></sub><sub><id>z</id><term>B</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong.L</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>1 + C</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>C + 1</term></sub><sub><id>x</id><term>1 + C</term></sub><sub><id>z</id><term>1</term></sub></APPLYS><APPLYS><CONST>commut+</CONST><sub><id>x</id><term>1</term></sub><sub><id>y</id><term>C</term></sub></APPLYS><APPLYS><CONST>@1</CONST><sub><id>B</id><term>C</term></sub></APPLYS></APPLYP></APPLYP><APPLYS><CONST>id.R</CONST><sub><id>x</id><term>B</term></sub></APPLYS></APPLYP></APPLYP></APPLYP></LAMBDAS></proof></lib>
<lib><id>abs.</id><condeqn>B;(B + C) = B</condeqn><task></task><proof><LAMBDAS><id>B</id><id>C</id><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B;B + B;C</term></sub><sub><id>x</id><term>B;(B + C)</term></sub><sub><id>z</id><term>B</term></sub></APPLYS><APPLYS><CONST>distrL</CONST><sub><id>x</id><term>B</term></sub><sub><id>y</id><term>B</term></sub><sub><id>z</id><term>C</term></sub></APPLYS><APPLYP><APPLYS><CONST>trans=</CONST><sub><id>y</id><term>B + B;C</term></sub><sub><id>x</id><term>B;B + B;C</term></sub><sub><id>z</id><term>B</term></sub></APPLYS><APPLYP><APPLYS><CONST>cong+R</CONST><sub><id>x</id><term>B;B</term></sub><sub><id>y</id><term>B</term></sub><sub><id>z</id><term>B;C</term></sub></APPLYS><APPLYS><CONST>idemp.</CONST><sub><id>B</id><term>B</term></sub></APPLYS></APPLYP><APPLYS><CONST>abs+</CONST><sub><id>B</id><term>B</term></sub><sub><id>C</id><term>C</term></sub></APPLYS></APPLYP></APPLYP></LAMBDAS></proof></lib>
</kat>
