leaderelection_inductive_withB_stubborn.strategies 188 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3
Strategies:
  strategy for B(a1,b1,i1): ∀ n2:T. ((b1 = n2) ∨ ¬ leq(b1,n2) ∨ ¬ next(a1,b1) ∨ ¬ (b1 = i1)) ∧ ∀ n3:T. (¬ btw(b1,i1,n3) ∨ ¬ leq(i1,n3) ∨ ¬ next(a1,b1))