equal
deleted
inserted
replaced
1271 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*} |
1271 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*} |
1272 text{*\noindent We start to stepwise execute our new program in a calculation |
1272 text{*\noindent We start to stepwise execute our new program in a calculation |
1273 tree and check if every node implements that what we have wanted.*} |
1273 tree and check if every node implements that what we have wanted.*} |
1274 |
1274 |
1275 ML {* |
1275 ML {* |
1276 trace_rewrite := false; |
1276 trace_rewrite := false; (*true*) |
1277 trace_script := false; |
1277 trace_script := false; (*true*) |
1278 print_depth 9; |
1278 print_depth 9; |
1279 |
1279 |
1280 val fmz = |
1280 val fmz = |
1281 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", |
1281 ["filterExpression (X z = 3 / ((z::real) + 1/10 - 1/50*(1/z)))", |
1282 "stepResponse (x[n::real]::bool)"]; |
1282 "stepResponse (x[n::real]::bool)"]; |
1307 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1307 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1308 "Rewrite_Set norm_Rational"; |
1308 "Rewrite_Set norm_Rational"; |
1309 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; |
1309 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; |
1310 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1310 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1311 "SubProblem"; |
1311 "SubProblem"; |
|
1312 print_depth 3; |
1312 *} |
1313 *} |
1313 |
1314 |
1314 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had |
1315 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had |
1315 \ttfamily Empty\_Tac; \normalfont the search for the reason considered |
1316 \ttfamily Empty\_Tac; \normalfont the search for the reason considered |
1316 the following points:\begin{itemize} |
1317 the following points:\begin{itemize} |
1380 \item Was there an error message? NO -- ok |
1381 \item Was there an error message? NO -- ok |
1381 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\ |
1382 \item Has \ttfamily nxt = Add\_Find \normalfont been inserted in pt:\\ |
1382 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok |
1383 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok |
1383 \item What is the returned formula: |
1384 \item What is the returned formula: |
1384 \begin{verbatim} |
1385 \begin{verbatim} |
1385 print_depth 999; f; print_depth 999; |
1386 print_depth 999; f; print_depth 3; |
1386 { Find = [ Correct "solutions z_i"], |
1387 { Find = [ Correct "solutions z_i"], |
1387 With = [], |
1388 With = [], |
1388 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)", |
1389 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)", |
1389 Correct "solveFor z"], |
1390 Correct "solveFor z"], |
1390 Where = [...], |
1391 Where = [...], |