equal
deleted
inserted
replaced
94 "ack2 0 (Suc m) = ack2 (Suc 0) m" | |
94 "ack2 0 (Suc m) = ack2 (Suc 0) m" | |
95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m" |
95 "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m" |
96 |
96 |
97 text{* The order of arguments has no influence on whether |
97 text{* The order of arguments has no influence on whether |
98 \isacommand{fun} can prove termination of a function. For more details |
98 \isacommand{fun} can prove termination of a function. For more details |
99 see elsewhere~\cite{bulwahnKN07}. |
99 see elsewhere~@{cite bulwahnKN07}. |
100 |
100 |
101 \subsection{Simplification} |
101 \subsection{Simplification} |
102 \label{sec:fun-simplification} |
102 \label{sec:fun-simplification} |
103 |
103 |
104 Upon a successful termination proof, the recursion equations become |
104 Upon a successful termination proof, the recursion equations become |