Changeset 2084 for src/ASM/CPP2012-policy/proof.tex

Ignore:
Timestamp:
Jun 15, 2012, 1:17:15 AM (7 years ago)
Message:
• changed bibliography style
• added CerCo? thanks
• some words of conclusion
File:
1 edited

Legend:

Unmodified
 r2082 program size. Here, we only need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. Termination can now be proven through the fact that there is a $k \leq 2n$, with $n$ the length of the program, such that iteration $k$ is equal to iteration $k+1$. There are two possibilities: either there is a $k < 2n$ such that this property holds, or every iteration up to $2n$ is different. In the latter case, since the only changes between the iterations can be from shorter jumps to longer jumps, in iteration $2n$ every jump must be long. In this case, iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.