<kat>
<lib><id>L10</id><condeqn>~B;C;b;c;d = ~B;b;c;d;D</condeqn><task></task><proof><LAMBDAS><id>B</id><id>b</id><id>c</id><id>F</id><id>d</id><id>D</id><id>E</id><id>C</id><SUBST><focus>0 0 3</focus><eqn>~B;C;b;c;d = ~B;b;c;d;D</eqn><dir>L</dir><APPLYF><CONST>S7</CONST><fsub><cterm>& phi & x//t & </cterm><term>~B;C</term></fsub><fsub><cterm>x := t</cterm><term>b</term></fsub><fsub><cterm>x := t</cterm><term>b</term></fsub><fsub><cterm>phi</cterm><term>~B;E</term></fsub></APPLYF><SUBST><focus>0 1 3</focus><eqn>b;~B;E;c;d = ~B;b;c;d;D</eqn><dir>L</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>& phi & A[x]//s & </cterm><term>E</term></fsub><fsub><cterm>A[x] := s</cterm><term>c</term></fsub><fsub><cterm>A[x] := s</cterm><term>c</term></fsub><fsub><cterm>phi</cterm><term>F</term></fsub></APPLYF><SUBST><focus>0 1 2</focus><eqn>b;~B;c;F;d = ~B;b;c;d;D</eqn><dir>L</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>& phi & A[x]//s & </cterm><term>~B</term></fsub><fsub><cterm>A[x] := s</cterm><term>c</term></fsub><fsub><cterm>A[x] := s</cterm><term>c</term></fsub><fsub><cterm>phi</cterm><term>~B</term></fsub></APPLYF><SUBST><focus>0 3 3</focus><eqn>b;~B;c;~B;F;d = ~B;b;c;d;D</eqn><dir>L</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>& phi & A[x]//s & </cterm><term>F</term></fsub><fsub><cterm>A[x] := s</cterm><term>d</term></fsub><fsub><cterm>A[x] := s</cterm><term>d</term></fsub><fsub><cterm>phi</cterm><term>D</term></fsub></APPLYF><SUBST><focus>0 1 3</focus><eqn>b;~B;c;~B;d;D = ~B;b;c;d;D</eqn><dir>R</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>A[x] := s</cterm><term>c</term></fsub><fsub><cterm>phi</cterm><term>~B</term></fsub><fsub><cterm>& phi & A[x]//s & </cterm><term>~B</term></fsub><fsub><cterm>A[x] := s</cterm><term>c</term></fsub></APPLYF><SUBST><focus>0 0 3</focus><eqn>b;~B;~B;c;d;D = ~B;b;c;d;D</eqn><dir>R</dir><APPLYF><CONST>S7</CONST><fsub><cterm>x := t</cterm><term>b</term></fsub><fsub><cterm>phi</cterm><term>~B;~B</term></fsub><fsub><cterm>& phi & x//t & </cterm><term>~B;~B</term></fsub><fsub><cterm>x := t</cterm><term>b</term></fsub></APPLYF><SUBST><focus>0 0 2</focus><eqn>~B;~B;b;c;d;D = ~B;b;c;d;D</eqn><dir>L</dir><APPLYS><CONST>idemp.</CONST><sub><id>B</id><term>~B</term></sub></APPLYS><APPLYS><CONST>ref=</CONST><sub><id>x</id><term>~B;b;c;d;D</term></sub></APPLYS></SUBST></SUBST></SUBST></SUBST></SUBST></SUBST></SUBST></LAMBDAS></proof><table><bterms><bterm><slang>$F(t,A[i]) = 1</slang><term>F</term></bterm><bterm><slang>$F(t,A[j]) = 1</slang><term>E</term></bterm><bterm><slang>$F(A[j],A[i]) = 1</slang><term>D</term></bterm><bterm><slang>$F(A[i],A[j]) = 1</slang><term>C</term></bterm><bterm><slang>$i = j</slang><term>B</term></bterm></bterms><cterms><cterm><slang>A[j] := t</slang><term>d</term></cterm><cterm><slang>A[i] := A[j]</slang><term>c</term></cterm><cterm><slang>t := A[i]</slang><term>b</term></cterm></cterms></table></lib>
</kat>
