newcontext "protocol"; p: NAT; q: NAT; x: NAT; y: NAT; v: NAT; r: NAT; a: NAT; p0: NAT; q0: NAT; x0: NAT; y0: NAT; v0: NAT; r0: NAT; a0: NAT; S1: BOOLEAN = 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: BOOLEAN = 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: BOOLEAN = 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: BOOLEAN = 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: BOOLEAN = 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: BOOLEAN = p = 1 AND q = 1 AND (x = 0 OR x = 1) AND v = 0 AND r = 0 AND a = 0; Step: BOOLEAN = S1 OR S2 OR S3 OR R1 OR R2; Property: BOOLEAN = q = 2 => y = x; Invariant: (NAT, NAT, NAT, NAT, NAT, NAT, NAT)->BOOLEAN = LAMBDA(p, q, x, y, v, r, a: NAT): (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: FORMULA Invariant(p, q, x, y, v, r, a) => Property; VC1: FORMULA Init => Invariant(p, q, x, y, v, r, a); VC2: FORMULA Step AND Invariant(p, q, x, y, v, r, a) => Invariant(p0, q0, x0, y0, v0, r0, a0);