If it is clear how the later calculation should look like

 All evaluation in the prototyp's Lucas-Interpreter is done by term rewriting on

 %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation'

 Isabelle's terms, see \S\ref{math} below; in this section some of respective

 %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den

 preparations are described. In order to work reliably with term rewriting, the

 %WN3 Anfang von \sect.3

 respective rule-sets must be confluent and terminating~\cite{nipk:rew-all-that},

 %WN3 

 then they are called (canonical) simplifiers. These properties do not go without

 %WN3 Im Folgenden sind einige Ungenauigkeiten:

 saying, their establishment is a difficult task for the programmer; this task is

  and when

 not yet supported in the prototype.\par

 which mathematic rule 

 %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe

 % If it is clear how the later calculation should look like

 %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten

 % %WN3 ... Allgem.<-->Konkret ist gut: aber hier ist 'calculation'

 %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich;

 % %WN3 zu weit weg: der Satz geh"ort bestenfalls gleich an den

 %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen,

 % %WN3 Anfang von \sect.3

 %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen;

 % %WN3 

 %WN3 das gilt insbesonders f"ur technische Begriffe wie oben

 % %WN3 Im Folgenden sind einige Ungenauigkeiten:

 should be applied, it can be started to find ways of

 %  and when

 simplifications. 

 % which mathematic rule 

 %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in

 % %WN3 rewrite-rule oder theorem ! Ein Paper enth"alt viele Begriffe

 %WN3 das Programm auf S.12 gewinnen.

 % %WN3 und man versucht, die Anzahl so gering wie m"oglich zu halten

 This includes in e.g. the simplification of reational 

 % %WN3 und die verbleibenden so pr"azise zu definieren wie m"oglich;

 expressions or also rewrites of an expession.

 % %WN3 das Vermeiden von Wiederholungen muss mit anderen Mitteln erfolgen,

 \par

 % %WN3 als dieselbe Sache mit verschiedenen Namen zu benennen;

 %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12

 % %WN3 das gilt insbesonders f"ur technische Begriffe wie oben

 %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist.

 % should be applied, it can be started to find ways of

 %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren

 % simplifications. 

 %WN3 braucht, als es wert ist ...

 % %WN3 ... zu allgemein. Das Folgende w"urde durch einen Verweis in

 Obligate is the use of the function \texttt{drop\_questionmarks} 

 % %WN3 das Programm auf S.12 gewinnen.

 which excludes irrelevant symbols out of the expression. (Irrelevant symbols may 

 % This includes in e.g. the simplification of reational 

 be result out of the system during the calculation. The function has to be

 % expressions or also rewrites of an expession.

 applied for two reasons. First two make every placeholder in a expression 

 % \par

 useable as a constant and second to provide a better view at the frontend.) 

 % %WN3 das Folgende habe ich aus dem Beispielprogramm auf S.12

 \par

 % %WN3 gestrichen, weil es aus prinzipiellen Gr"unden unsch"on ist.

 %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten:

 % %WN3 Und es ist so kompliziert dass es mehr Platz zum Erkl"aren

 Most rewrites are represented through rulesets

 % %WN3 braucht, als es wert ist ...

 %WN3 ... das ist schlicht falsch:

 % Obligate is the use of the function \texttt{drop\_questionmarks} 

 %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition

 % which excludes irrelevant symbols out of the expression. (Irrelevant symbols may 

 %WN3 dieser W"orter).

 % be result out of the system during the calculation. The function has to be

  this

 % applied for two reasons. First two make every placeholder in a expression 

 rulesets tell the machine which terms have to be rewritten into which

 % useable as a constant and second to provide a better view at the frontend.) 

 representation. 

 % \par

 %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret:

 % %WN3 Da kommt eine ganze Reihe von Ungenauigkeiten:

 %WN3 so allgemein, wie es hier steht, ist es

 % Most rewrites are represented through rulesets

 %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert

 % %WN3 ... das ist schlicht falsch:

 %WN3   (a rule-set rewrites a certain term into another with certain properties)

 % %WN3 _alle_ rewrites werden durch rule-sets erzeugt (per definition

 %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich.

 % %WN3 dieser W"orter).

 %WN3 

 %  this

 %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel

 % rulesets tell the machine which terms have to be rewritten into which

 %WN3 unten verweisen,

 % representation. 

 %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom

 % %WN3 ... ist ein besonders "uberzeugendes Beispiel von Allgem.<-->Konkret:

 %WN3 Beispiel gefolgt wird.

 % %WN3 so allgemein, wie es hier steht, ist es

 In the upcoming programm a rewrite can be applied only in using

 % %WN3 # f"ur einen Fachmann klar und nicht ganz fachgem"ass formuliert

 such rulesets on existing terms.

 % %WN3   (a rule-set rewrites a certain term into another with certain properties)

 %WN3 Du willst wohl soetwas sagen wie ...

 % %WN3 # f"ur einen Nicht-Fachmann trotz allem unverst"andlich.

 %WN3 rewriting is the main concept to step-wise create and transform 

 % %WN3 

 %WN3 formulas in order to proceed towards a solution of a problem

 % %WN3 Wenn schon allgemeine S"atze, dann unmittelbar auf das Beispiel

 %WN3 ...?

 % %WN3 unten verweisen,

 \paragraph{The core} of our implemented problem is the Z-Transformation

 % %WN3 oder besser: den Satz dorthin schreiben, wo er unmittelbar vom

 %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die

 % %WN3 Beispiel gefolgt wird.

 %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ?

 % In the upcoming programm a rewrite can be applied only in using

 %WN3 

 % such rulesets on existing terms.

 %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder

 % %WN3 Du willst wohl soetwas sagen wie ...

 %WN3 vorne zur Einf"uhrung des Beispiels geh"ort,

 % %WN3 rewriting is the main concept to step-wise create and transform 

 %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16.

 % %WN3 formulas in order to proceed towards a solution of a problem

 (remember the description of the running example, introduced by

 % %WN3 ...?

 Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the

 % \paragraph{The core} of our implemented problem is the Z-Transformation

 transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in

 % %WN3 ^^^^^ ist nicht gut: was soll THE CORE vermitteln, wenn man die

 transformation tables).

 % %WN3 Seite "uberfliegt ? Dass hier das Zentrum Deiner Arbeit liegt ?

 \par

 % %WN3 

 %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen:

 % %WN3 Das Folgende ist eine allgemeine Design-"Uberlegung, die entweder

 %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen.

 % %WN3 vorne zur Einf"uhrung des Beispiels geh"ort,

 Rules, in {\sisac{}}'s programming language can be designed by the use of

 % %WN3 oder zur konkreten L"osung durch die Rechnung auf S.15/16.

 axiomatization. In this axiomatization we declare how a term has to look like

 % (remember the description of the running example, introduced by

 (left side) to be rewritten into another form (right side). Every line of this 

 % Fig.\ref{fig-interactive} on p.\pageref{fig-interactive}) due the fact that the

 axiomatizations starts with the name of the rule.

 % transformation itself would require higher math which isn't yet avaible in our system we decided to choose the way like it is applied in labratory and problem classes at our university - by applying transformation rules (collected in

 %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen

 % transformation tables).

 %\begin{example}

 % \par

 {\footnotesize

 % %WN3 Zum Folgenden: 'axiomatization' ist schon in 3.1. angesprochen:

   \label{eg:ruledef}

 % %WN3 entweder dort erg"anzen, wenn's wichtig ist, oder weglassen.

 %  \hfill\\

 % Rules, in {\sisac{}}'s programming language can be designed by the use of

   \begin{verbatim}

 % axiomatization. In this axiomatization we declare how a term has to look like

   axiomatization where

 % (left side) to be rewritten into another form (right side). Every line of this 

     rule1: ``1 = $\delta$[n]'' and

 % axiomatizations starts with the name of the rule.

     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and

     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''

 The prototype rewrites using theorems only. Axioms which are theorems as well 

 \end{verbatim}

 have been already shown in \S\ref{eg:neuper1} on p.\pageref{eg:neuper1} , we

 %\end{example}

 assemble them in a rule-set and apply them as follows:

 }

 % %WN3 Die folgenden Zeilen nehmen Platz weg: von hier auf S.6 verweisen

 Rules can be summarized in a ruleset (collection of rules) and afterwards tried to be applied to a given expression as puttet over in following code.

 % %\begin{example}

 % {\footnotesize

 %   \label{eg:ruledef}

 % %  \hfill\\

 %   \begin{verbatim}

 %   axiomatization where

 %     rule1: ``1 = $\delta$[n]'' and

 %     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and

 %     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''

 % \end{verbatim}

 % %\end{example}

 % }

 % Rules can be summarized in a ruleset (collection of rules) and afterwards tried % to be applied to a given expression as puttet over in following code.

   val inverse_Z = append_rls "inverse_Z" e_rls

 01  val inverse_Z = append_rls "inverse_Z" e_rls

     [ Thm ("rule1",num_str @{thm rule1}),

 02    [ Thm ("rule1",num_str @{thm rule1}),

       Thm ("rule2",num_str @{thm rule2}),

 03      Thm ("rule2",num_str @{thm rule2}),

       Thm ("rule3",num_str @{thm rule3})

 04      Thm ("rule3",num_str @{thm rule3})

     ];\end{verbatim}}

 05    ];\end{verbatim}}

   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}

 06  val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}}

 %WN3 

   val SOME (sample_term', asm) = 

 07  val SOME (sample_term', asm) = 

     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}

 08    rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}}

 The use of rulesets makes it much easier to develop our designated applications,

 but the programmer has to be careful and patient. When applying rulesets

 % The use of rulesets makes it much easier to develop our designated applications,

 two important issues have to be mentionend:

 % but the programmer has to be careful and patient. When applying rulesets

 \begin{enumerate}

 % two important issues have to be mentionend:

 \item How often the rules have to be applied? In case of

 % \begin{enumerate}

 transformations it is quite clear that we use them once but other fields

 % \item How often the rules have to be applied? In case of

 reuqire to apply rules until a special condition is reached (e.g.

 % transformations it is quite clear that we use them once but other fields

 a simplification is finished when there is nothing to be done left).

 % reuqire to apply rules until a special condition is reached (e.g.

 \item The order in which rules are applied often takes a big effect

 % a simplification is finished when there is nothing to be done left).

 and has to be evaluated for each purpose once again.

 % \item The order in which rules are applied often takes a big effect

 \end{enumerate}

 % and has to be evaluated for each purpose once again.

 In the special case of Signal Processing the rules defined in the

 % \end{enumerate}

 Example upwards have to be applied in a dedicated order to transform all 

 % In the special case of Signal Processing the rules defined in the

 constants first of all. After this first transformation step has been done it no 

 % Example upwards have to be applied in a dedicated order to transform all 

 mather which rule fit's next.

 % constants first of all. After this first transformation step has been done it no 

 % mather which rule fit's next.