leaderelection_inductive_withB2_stubborn.strategies 147 Bytes
Newer Older
1 2 3
Strategies:
  strategy for B(a1,b1): ∀ n2:T. ((a1 = n2) ∨ ¬ leq(a1,n2) ∨ ¬ (a1 = b1)) ∧ ∀ n3:T. (¬ btw(b1,a1,n3) ∨ ¬ leq(a1,n3))