state reg_bound (any register during a computation of an IMP- program only has a number which is polynomially bounded by the input size and the number of steps taken), and maybe prove it as a "sanity check" (but you wont need it now)
prove size of result of PI is polynomially bounded
prove that PHI in SAS+ -> SAT is polynomially bounded
compose PI and PHI_all
prove that the composition going from IMP- to SAS+ is polynomially bounded
IMP-program only has a number which is polynomially bounded by the input size and the number of steps taken), and maybe prove it as a "sanity check" (but you wont need it now)PIandPHI_allIMP-toSAS+is polynomially boundedthis includes #9 and #10