Christian Müller committed Oct 08, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 ``````Signature EmptyPredicates: msg(a, i, b), leader(a) AxiomPredicates: next(a, b), leq(a, b), btw(a, b, c) As: A(a) Bs: B(a,i,b) Constants: - Transition System msg(a,i,b) := (next(a,b) ∧ B(a,i,b)) loop { leader(b) := ∃a. msg(a, b, b) msg(a,i,b) := (A(a) ∧ next(a, b) ∧ ∃c. msg(c, i, a) ∧ leq(a, i)) } Invariant ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2), ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)), ∀n1,n2,n3. (n1 = n2 ∨ ¬msg(n3, n1, n1) ∨ ¬leq(n1, n2)), ∀n1,n2,n3,n4. (¬btw(n1,n2,n3) ∨ ¬msg(n4,n2,n1) ∨ ¬leq(n2,n3)) Axioms ∀x. leq(x,x), ∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)), ∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y), ∀x,y. (leq(x,y) ∨ leq(y,x)), ∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)), ∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)), ∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)), ∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)), ∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))``````