protocol: THEORY
BEGIN

  p, q, x, y, v, r, a: nat
  p0, q0, x0, y0, v0, r0, a0: nat

  S1: bool =
    p = 1 AND p0 = 2 AND v0 = x AND r0 = 1 AND
    q0 = q AND x0 = x AND y0 = y AND v0 = v AND a0 = a

  S2: bool =
    p = 2 AND p0 = 3 AND a = 1 AND r0 = 0 AND
    q0 = q AND x0 = x AND y0 = y AND v0 = v AND a0 = a

  S3: bool =
    p = 3 AND p0 = 1 AND a = 0 AND (x0 = 0 OR x0 = 1) AND
    q0 = q AND y0 = y AND v0 = v AND r0 = r AND a0 = a

  R1: bool =
    q = 1 AND q0 = 2 AND r = 1 AND y0 = v AND a0 = 1 AND
    p0 = p AND x0 = x AND v0 = v AND r0 = r

  R2: bool =
    q = 2 AND q0 = 1 AND r = 0 AND a0 = 0 AND
    p0 = p AND x0 = x AND y0 = y AND v0 = v AND r0 = r

  Init: bool =
    p = 1 AND q = 1 AND (x = 0 OR x = 1) AND
    v = 0 AND r = 0 AND a = 0

  Step: bool =
    S1 OR S2 OR S3 OR R1 OR R2

  Property: bool =
    q = 2 => y = x
    
  Invariant(p, q, x, y, v, r, a: nat): bool =
    (p = 1 OR p = 2 OR p = 3) AND
    (q = 1 OR q = 2) AND
    (x = 0 OR x = 1) AND
    (v = 0 OR v = 1) AND
    (r = 0 OR r = 1) AND
    (a = 0 OR a = 1) AND
    (p = 1 => q = 1 AND r = 0 AND a = 0) AND
    (p = 2 => r = 1) AND
    (p = 3 => r = 0) AND
    (q = 1 => a = 0) AND
    (q = 2 => (p = 2 OR p = 3) AND a = 1 AND y = x) AND
    (r = 1 => p = 2 AND v = x)

  VC0: THEOREM
    Invariant(p, q, x, y, v, r, a) => Property

  VC1: THEOREM
    Init => Invariant(p, q, x, y, v, r, a)

  VC2: THEOREM
    Step AND Invariant(p, q, x, y, v, r, a) => 
      Invariant(p0, q0, x0, y0, v0, r0, a0)

END protocol