<kat>
<lib><id>L0</id><condeqn>~A;a;b;c;d = ~A;e;f;g;d</condeqn><task>T110</task><proof><LAMBDAS><id>A</id><id>f</id><id>j</id><id>k</id><id>g</id><id>a</id><id>e</id><id>d</id><id>b</id><id>c</id><SUBST><focus>1 4 1</focus><eqn>~A;a;b;c;d = ~A;e;f;g;d</eqn><dir>R</dir><APPLYF><CONST>S3</CONST><fsub><cterm>x := & t & x//s & </cterm><term>d</term></fsub><fsub><cterm>x := s</cterm><term>a</term></fsub><fsub><cterm>x := t</cterm><term>d</term></fsub></APPLYF><SUBST><focus>1 0 2</focus><eqn>~A;a;b;c;d = ~A;e;f;g;a;d</eqn><dir>L</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>& phi & A[x]//s & </cterm><term>~A</term></fsub><fsub><cterm>A[x] := s</cterm><term>e</term></fsub><fsub><cterm>A[x] := s</cterm><term>e</term></fsub><fsub><cterm>phi</cterm><term>~A</term></fsub></APPLYF><SUBST><focus>1 2 2</focus><eqn>~A;a;b;c;d = ~A;e;~A;f;g;a;d</eqn><dir>L</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>& phi & A[x]//s & </cterm><term>~A</term></fsub><fsub><cterm>A[x] := s</cterm><term>f</term></fsub><fsub><cterm>A[x] := s</cterm><term>f</term></fsub><fsub><cterm>phi</cterm><term>~A</term></fsub></APPLYF><SUBST><focus>1 4 3</focus><eqn>~A;a;b;c;d = ~A;e;~A;f;~A;g;a;d</eqn><dir>L</dir><APPLYF><CONST>Arr6</CONST><fsub><cterm>A[x] := s</cterm><term>g</term></fsub><fsub><cterm>y := t</cterm><term>a</term></fsub><fsub><cterm>y := & t & A[x]//s & </cterm><term>j</term></fsub><fsub><cterm>A[x] := s</cterm><term>g</term></fsub></APPLYF><SUBST><focus>1 5 2</focus><eqn>~A;a;b;c;d = ~A;e;~A;f;~A;j;g;d</eqn><dir>R</dir><APPLYF><CONST>Arr7</CONST><fsub><cterm>x := s</cterm><term>j</term></fsub><fsub><cterm>A[& y & x//s & ] := & t & x//s & </cterm><term>g</term></fsub><fsub><cterm>x := s</cterm><term>j</term></fsub><fsub><cterm>A[y] := t</cterm><term>k</term></fsub></APPLYF><SUBST><focus>1 2 3</focus><eqn>~A;a;b;c;d = ~A;e;~A;f;~A;j;k;d</eqn><dir>R</dir><APPLYF><CONST>Arr4</CONST><fsub><cterm>A[x] := s</cterm><term>f</term></fsub><fsub><cterm>phi</cterm><term>~A</term></fsub><fsub><cterm>& phi & A[x]//s & </cterm><term>~A</term></fsub><fsub><cterm>A[x] := s</cterm><term>f</term></fsub></APPLYF><TASK><id>T110</id><condeqn>~A;a;b;c;d = ~A;e;~A;~A;f;j;k;d</condeqn><focus>1 3 3</focus></TASK></SUBST></SUBST></SUBST></SUBST></SUBST></SUBST></LAMBDAS></proof><table><bterms><bterm><slang>$i = j</slang><term>A</term></bterm></bterms><cterms><cterm><slang>A[i] := t</slang><term>k</term></cterm><cterm><slang>t := (A[i] - A[j])</slang><term>j</term></cterm><cterm><slang>A[i] := (A[i] - t)</slang><term>i</term></cterm><cterm><slang>t := A[j]</slang><term>h</term></cterm><cterm><slang>A[i] := (A[i] - A[j])</slang><term>g</term></cterm><cterm><slang>A[j] := (A[i] - A[j])</slang><term>f</term></cterm><cterm><slang>A[i] := (A[i] + A[j])</slang><term>e</term></cterm><cterm><slang>t := 0</slang><term>d</term></cterm><cterm><slang>A[j] := t</slang><term>c</term></cterm><cterm><slang>A[i] := A[j]</slang><term>b</term></cterm><cterm><slang>t := A[i]</slang><term>a</term></cterm></cterms></table></lib>
</kat>
