Chapter 3 - Short tree strategy mice

Summary

The main purpose of this chapter is to isolate the definition of short tree strategy mice. The main problem with defining this concept is the fact that it is possible that maximal iteration trees (which should not have branches indexed in the strategy predicate) may core down to short iteration trees (which must have branches indexed in the strategy predicate), thus causing indexing issues. To resolve this issue we will design an authentication procedure which will carefully choose iteration trees and index their branches. Thus, if some iteration tree doesn’t have a branch indexed in the strategy predicate then it is because the authentication procedure hasn’t yet found an authenticated branch, and therefore, such iteration trees cannot core down to an iteration tree whose branch is authenticated.