State-OK (s ) -> Int (s , n) = Map (Int (Map (s ), k)).A A A C AFigure 1 illustrates this theorem. The theorem says that given an initial legal abstract state s as defined byA-1Abstract-State-OK, and time n, there exists a time k such that Map of the concrete interpreter result is identicalto the final state reached by the abstract interpreter. The theorem form is slightly more complex when aninterpreter which requires an oracle argument is under consideration. We refer back to...