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

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r2082 r2084  
    309309program size. Here, we only need {\tt out\_of\_program\_none},
    310310{\tt sigma\_compact} and the fact that $\sigma(0) = 0$.
     311
     312Termination 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
     315property holds, or every iteration up to $2n$ is different. In the latter case,
     316since the only changes between the iterations can be from shorter jumps to
     317longer jumps, in iteration $2n$ every jump must be long. In this case,
     318iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
Note: See TracChangeset for help on using the changeset viewer.