simplechoice_stubborn.ppltl 1.53 KB
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 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
G ((n0 → X n1) ∧
  (n1 → X n1)) ∧
n0 ∧
¬ n1 ∧
G ¬ (n0 ∧
  n1) ∧
¬ R#t1_x#T_x#T ∧
¬ R#t1_x#T_s#T ∧
¬ R#t1_s#T_x#T ∧
¬ R#t1_s#T_s#T ∧
G (((n0 ∧
      X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨
          (O#t1_x#T ∧
            choice0_x#T_x#T))) ∧
      (X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨
          (O#t1_s#T ∧
            choice0_x#T_s#T))) ∧
      (X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨
          (O#t1_x#T ∧
            choice0_s#T_x#T))) ∧
      (X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨
          (O#t1_s#T ∧
            choice0_s#T_s#T))))) ∧
  ((n1 ∧
      X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧
      (X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧
      (X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧
      (X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧
¬ R#t2_x#T_x#T ∧
¬ R#t2_x#T_s#T ∧
¬ R#t2_s#T_x#T ∧
¬ R#t2_s#T_s#T ∧
G (((n0 ∧
      X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨
          (O#t2_x#T ∧
            choice0_x#T_x#T))) ∧
      (X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨
          (O#t2_s#T ∧
            choice0_x#T_s#T))) ∧
      (X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨
          (O#t2_x#T ∧
            choice0_s#T_x#T))) ∧
      (X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨
          (O#t2_s#T ∧
            choice0_s#T_s#T))))) ∧
  ((n1 ∧
      X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧
      (X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧
      (X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧
      (X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧
True ∧
F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)