simplechoice_stubborn.foltl 636 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
G ((n0() → X n1()) ∧
  (n1() → X n1())) ∧
n0() ∧
¬ n1() ∧
G ¬ (n0() ∧
  n1()) ∧
∀ x:T,s:T. ¬ R(t1)(x,s) ∧
G (((n0() ∧
      X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ (R(t1)(x,s) ∨
        (O(t1)(s) ∧
          choice0(x,s))))) ∧
  ((n1() ∧
      X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ R(t1)(x,s)))) ∧
∀ x:T,s:T. ¬ R(t2)(x,s) ∧
G (((n0() ∧
      X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ (R(t2)(x,s) ∨
        (O(t2)(s) ∧
          choice0(x,s))))) ∧
  ((n1() ∧
      X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ R(t2)(x,s)))) ∧
∃ x:T,s:T. (True ∧
  F ¬ (R(t1)(x,s) ↔ eq()))