Changeset 2084 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 15, 2012, 1:17:15 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2082 r2084 309 309 program size. Here, we only need {\tt out\_of\_program\_none}, 310 310 {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. 311 312 Termination can now be proven through the fact that there is a $k \leq 2n$, with 313 $n$ the length of the program, such that iteration $k$ is equal to iteration 314 $k+1$. There are two possibilities: either there is a $k < 2n$ such that this 315 property holds, or every iteration up to $2n$ is different. In the latter case, 316 since the only changes between the iterations can be from shorter jumps to 317 longer jumps, in iteration $2n$ every jump must be long. In this case, 318 iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
Note: See TracChangeset
for help on using the changeset viewer.