Proof Linear: Model of Computer

• State of computer given by contents of memory
• All memory, input and output registers but exclude PC
• N memory bits $\Rightarrow 2^{N}$ states
• Execution $\equiv$ state $\rightarrow$ next state
• In general state $\neq$ next state but allow state = next state
• Computer designed so all states accessible
• Symmetric instruction set, state $\rightleftharpoons$ next state