Problem 9.13

Define the Pulverizer state machine to have:

states ::= N^6

start state ::= (a,b,0,1,1,0) where a ≥ b>0

transitions ::=

(x,y,s,t,u,v) → (y, rem(x,y), u— sq,v-tq,s,t)

where q = qent(x,y) and y > 0).

(a) Show that all of the following properties are preserved invariants for the Pulverizer machine:

ged(x,y) = ged(a,b),

sa+tb = y, and

ua + vb = x

(b) Conclude that the Pulverizer machine is partially correct.

(c) Explain why the machine terminates after at most the same number of transitions as the

Euclidean algorithm.