Question on Inductive Invariants (page 44)?

Working through the Inductive invariants for Euclid, I've encoded them as follows:

\* PC means `PartialCorrectness,' but it's a lot easier to write and read.

PC == (pc = "Done") => (x = y) /\ (x = GCD(M, N))

TypeOK == /\ x \in Nat \ {0}
          /\ y \in Nat \ {0}

Inv == /\ TypeOK
       /\ GCD(x, y) = GCD(M, N)
       /\ (pc = "Done") => (x = y)

InductiveInv == /\ Inv
                /\ (pc = "antanaresis") => (x /= y)

I1 == Init => Inv
I2 == Inv /\ Next => Inv'
I3 == Inv => PC

In the model checker, I can check them all except I2, which generates the following error (I labeled my while loop "loop"):

In evaluation, the identifier pc is either undefined or not an operator.
line 32, col 23 to line 32, col 24 of module ExtraSimpleEuclid
While working on the initial state:
/\ x = 30
/\ y = 18
/\ pc = "loop"

Which I interpreted as the checker trying to evaluate Inv /\ Next in when state Init is TRUE and getting undefined pc.

Fair enough, I modified I2 to be

I2 == ~Init /\ Inv /\ Next => Inv'

and I check in the model to ONLY verify the ivariant I2 (PC, Inv, InductiveInv, I1 and I3) are unchecked lest I get other more mysterious errors).

I get the error that "Invariant PC failed." But I didn't ask it to check PC? And if I uncheck I2 and check PC, it succeeds. I'm stumped, and I'd be grateful for advice.

My entire model is as follows:

------------------------- MODULE ExtraSimpleEuclid -------------------------

EXTENDS Integers, GCD

CONSTANTS M, N

ASSUME {M, N} \subseteq Nat \ {0} \* `subset' doesn't seem to work

(***************************************************************************
--fair algorithm Euclid
{ variables x = M, y = N;
    { loop: while (x /= y)
      \* The Greek word for the following process of repeated subtraction
      \* is `antanaresis.'
      { antanaresis: if (x < y) { y := y - x; }
                     else       { x := x - y; }
      }
} }
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES x, y, pc

vars == << x, y, pc >>

Init == (* Global variables *)
        /\ x = M
        /\ y = N
        /\ pc = "loop"

loop == /\ pc = "loop"
        /\ IF x /= y
              THEN /\ pc' = "antanaresis"
              ELSE /\ pc' = "Done"
        /\ UNCHANGED << x, y >>

antanaresis == /\ pc = "antanaresis"
               /\ IF x < y
                     THEN /\ y' = y - x
                          /\ x' = x
                     ELSE /\ x' = x - y
                          /\ y' = y
               /\ pc' = "loop"

Next == loop \/ antanaresis
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

\* PC means `PartialCorrectness,' but it's a lot easier to write and read.

PC == (pc = "Done") => (x = y) /\ (x = GCD(M, N))

TypeOK == /\ x \in Nat \ {0}
          /\ y \in Nat \ {0}

Inv == /\ TypeOK
       /\ GCD(x, y) = GCD(M, N)
       /\ (pc = "Done") => (x = y)

InductiveInv == /\ Inv
                /\ (pc = "antanaresis") => (x /= y)

I1 == Init => Inv
I2 == (~Init) /\ Inv /\ Next => Inv'
I3 == Inv => PC

=============================================================================