// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  LTL theorems
//
// **************************************************************************

module LTL(bool ?a,?b,?c,?d,?q) {
    nothing;
} satisfies {
// ---- implementing temporal operators by watchdogs ----------

  WatchWU : assert A (!q & G(X q <-> q | b)    -> ( [a WU b] <-> G(q|a|b)  ));
  WatchWB : assert A (!q & G(X q <-> q | a&!b) -> ( [a WB b] <-> G(q|!b)   ));
  WatchWW : assert A (!q & G(X q <-> q | b)    -> ( [a WW b] <-> G(q|a|!b) ));
  WatchSU : assert A (!q & G(X q <-> q | b)    -> ( [a SU b] <-> G(q|a|b)  & F b));
  WatchSB : assert A (!q & G(X q <-> q | a&!b) -> ( [a SB b] <-> G(q|!b)   & F a));
  WatchSW : assert A (!q & G(X q <-> q | b)    -> ( [a SW b] <-> G(q|a|!b) & F b));


// ---- recursion laws of temporal operators ------------------

  RecurG  : assert A ((G a) <-> a & X G a);
  RecurF  : assert A ((F a) <-> a | X F a);
  RecurSU : assert  A ([a SU b] <->  b | a & X[a SU b]);
  RecurWU : assert  A ([a WU b] <->  b | a & X[a WU b]);
  RecurSB : assert  A ([a SB b] <-> !b & (a | X[a SB b]));
  RecurWB : assert  A ([a WB b] <-> !b & (a | X[a WB b]));
  RecurSW : assert A ([a SW b] <->  b & a | !b & X[a SW b]);
  RecurWW : assert A ([a WW b] <->  b & a | !b & X[a WW b]);

  RecurPG  : assert A ((PG a) <-> a & PWX PG a);
  RecurPF  : assert A ((PF a) <-> a | PSX PF a);
  RecurPSU : assert A ([a PSU b] <->  b | a & PSX[a PSU b]);
  RecurPWU : assert A ([a PWU b] <->  b | a & PWX[a PWU b]);
  RecurPSB : assert A ([a PSB b] <-> !b & (a | PSX[a PSB b]));
  RecurPWB : assert A ([a PWB b] <-> !b & (a | PWX[a PWB b]));
  RecurPSW : assert A ([a PSW b] <->  b & a | !b & PSX[a PSW b]);
  RecurPWW : assert A ([a PWW b] <->  b & a | !b & PWX[a PWW b]);


// ---- negation normal form -----------------------

  NotG  : assert A (!G a <-> F !a);
  NotF  : assert A (!F a <-> G !a);
  NotX  : assert A (!X a <-> X !a);
  NotSU : assert A (![a SU b] <-> [(!a) WB b]);
  NotSB : assert A (![a SB b] <-> [(!a) WU b]);
  NotSW : assert A (![a SW b] <-> [(!a) WW b]);
  NotWU : assert A (![a WU b] <-> [(!a) SB b]);
  NotWB : assert A (![a WB b] <-> [(!a) SU b]);
  NotWW : assert A (![a WW b] <-> [(!a) SW b]);

  NotPG  : assert A (!PG a <-> PF !a);
  NotPF  : assert A (!PF a <-> PG !a);
  NotPSX : assert A (!PSX a <-> PWX !a);
  NotPSU : assert A (![a PSU b] <-> [(!a) PWB b]);
  NotPSB : assert A (![a PSB b] <-> [(!a) PWU b]);
  NotPSW : assert A (![a PSW b] <-> [(!a) PWW b]);
  NotPWX : assert A (!PWX a <-> PSX !a);
  NotPWU : assert A (![a PWU b] <-> [(!a) PSB b]);
  NotPWB : assert A (![a PWB b] <-> [(!a) PSU b]);
  NotPWW : assert A (![a PWW b] <-> [(!a) PSW b]);


// ---- CONJUNCTIVE_NORMAL_FORM -------------------- 

  Conj_X   : assert A G (X (a & b) <-> X a & X b);
  Conj_G   : assert A G (G (a & b) <-> G a & G b);
  Conj_WW  : assert A G ([(a & b) WW c] <-> [a WW c] & [b WW c]);
  Conj_SW  : assert A G ([(a & b) SW c] <-> [a SW c] & [b SW c]);
  Conj_WU  : assert A G ([(a & b) WU c] <-> [a WU c] & [b WU c]);
  Conj_SU  : assert A G ([(a & b) SU c] <-> [a SU c] & [b SU c]);
  Conj_WB  : assert A G ([c WB (a | b)] <-> [c WB a] & [c WB b]);
  Conj_SB  : assert A G ([c SB (a | b)] <-> [c SB a] & [c SB b]);
  Conj_PWX : assert A G (PWX (a & b) <-> PWX a & PWX b);
  Conj_PSX : assert A G (PSX (a & b) <-> PSX a & PSX b);
  Conj_PG  : assert A G (PG (a & b) <-> PG a & PG b);
  Conj_PWW : assert A G ([(a & b) PWW c] <-> [a PWW c] & [b PWW c]);
  Conj_PSW : assert A G ([(a & b) PSW c] <-> [a PSW c] & [b PSW c]);
  Conj_PWU : assert A G ([(a & b) PWU c] <-> [a PWU c] & [b PWU c]);
  Conj_PSU : assert A G ([(a & b) PSU c] <-> [a PSU c] & [b PSU c]);
  Conj_PWB : assert A G ([c PWB (a | b)] <-> [c PWB a] & [c PWB b]);
  Conj_PSB : assert A G ([c PSB (a | b)] <-> [c PSB a] & [c PSB b]);


// ---- DISJUNCTIVE_NORMAL_FORM --------------------------------

  Disj_X   : assert A G (X (a | b) <-> (X a | X b));
  Disj_F   : assert A G (F (a | b) <-> (F a | F b));
  Disj_WW  : assert A G ([(a | b) WW c] <-> ([a WW c] | [b WW c]));
  Disj_SW  : assert A G ([(a | b) SW c] <-> ([a SW c] | [b SW c]));
  Disj_WU  : assert  A G ([a WU (b | c)] <-> ([a WU b] | [a WU c]));
  Disj_SU  : assert A G ([a SU (b | c)] <-> ([a SU b] | [a SU c]));
  Disj_WB  : assert A G ([(a | b) WB c] <-> ([a WB c] | [b WB c]));
  Disj_SB  : assert A G ([(a | b) SB c] <-> ([a SB c] | [b SB c]));
  Disj_PWX : assert A G (PWX (a | b) <-> (PWX a | PWX b));
  Disj_PSX : assert A G (PSX (a | b) <-> (PSX a | PSX b));
  Disj_PF  : assert A G (PF (a | b) <-> (PF a | PF b));
  Disj_PWW : assert A G ([(a | b) PWW c] <-> ([a PWW c] | [b PWW c]));
  Disj_PSW : assert A G ([(a | b) PSW c] <-> ([a PSW c] | [b PSW c]));
  Disj_PWU : assert A G ([a PWU (b | c)] <-> ([a PWU b] | [a PWU c]));
  Disj_PSU : assert A G ([a PSU (b | c)] <-> ([a PSU b] | [a PSU c]));
  Disj_PWB : assert A G ([(a | b) PWB c] <-> ([a PWB c] | [b PWB c]));
  Disj_PSB : assert A G ([(a | b) PSB c] <-> ([a PSB c] | [b PSB c]));


// ---- SU and PSU are expressively complete ------------------

  G_as_SU  : assert A (G a <-> ![true SU (!a)]);
  F_as_SU  : assert A (F a <->  [true SU a]);
  SB_as_SU : assert A ([a SB b] <->  [(!b) SU (a&!b)]);
  SW_as_SU : assert A ([a SW b] <->  [(!b) SU (a&b)]);
  WU_as_SU : assert A ([a WU b] <-> ![(!b) SU (!a&!b)]);
  WB_as_SU : assert A ([a WB b] <-> ![(!a) SU b]);
  WW_as_SU : assert A ([a WW b] <-> ![(!a|!b) SU (!a&b)]);

  PG_as_PSU  : assert A (PG a <-> ![true PSU (!a)]);
  PF_as_PSU  : assert A (PF a <->  [true PSU a]);
  PSB_as_PSU : assert A ([a PSB b] <->  [(!b) PSU (a&!b)]);
  PSW_as_PSU : assert A ([a PSW b] <->  [(!b) PSU (a&b)]);
  PWU_as_PSU : assert A ([a PWU b] <-> ![(!b) PSU (!a&!b)]);
  PWB_as_PSU : assert A ([a PWB b] <-> ![(!a) PSU b]);
  PWW_as_PSU : assert A ([a PWW b] <-> ![(!a|!b) PSU (!a&b)]);


// ---- WU and PWU are expressively complete ------------------

  G_as_WU  : assert A (G a <->  [a WU false]);
  F_as_WU  : assert A (F a <-> ![(!a) WU false]);
  SU_as_WU : assert A ([a WU b] <-> ![(!b) SU (!a&!b)]);
  SB_as_WU : assert A ([a SB b] <-> ![(!a) WU b]);
  SW_as_WU : assert A ([a SW b] <-> ![(!a|!b) WU (!a&b)]);
  WB_as_WU : assert A ([a WB b] <->  [(!b) WU (a&!b)]);
  WW_as_WU : assert A ([a WW b] <->  [(!b) WU (a&b)]);

  PG_as_PWU  : assert A (PG a <->  [a PWU false]);
  PF_as_PWU  : assert A (PF a <-> ![(!a) PWU false]);
  PSU_as_PWU : assert A ([a PWU b] <-> ![(!b) PSU (!a&!b)]);
  PSB_as_PWU : assert A ([a PSB b] <-> ![(!a) PWU b]);
  PSW_as_PWU : assert A ([a PSW b] <-> ![(!a|!b) PWU (!a&b)]);
  PWB_as_PWU : assert A ([a PWB b] <->  [(!b) PWU (a&!b)]);
  PWW_as_PWU : assert A ([a PWW b] <->  [(!b) PWU (a&b)]);


// ---- SB and PSB are expressively complete ------------------

  G_as_SB  : assert A (G a <-> ![(!a) SB false]);
  F_as_SB  : assert A (F a <-> [a SB false]);
  SU_as_SB : assert A ([a SU b] <->  [b SB (!a & !b)]);
  SB_as_SB : assert A ([a WU b] <-> ![(!a) SB b]);
  SW_as_SB : assert A ([a SW b] <->  [b SB (!a & b)]);
  WB_as_SB : assert A ([a WW b] <-> ![b SB (a & b)]);
  WW_as_SB : assert A ([a WB b] <-> ![b SB (a & !b)]);

  PG_as_PSB  : assert A (PG a <-> ![(!a) PSB false]);
  PF_as_PSB  : assert A (PF a <-> [a PSB false]);
  PSU_as_PSB : assert A ([a PSU b] <->  [b PSB (!a & !b)]);
  PSB_as_PSB : assert A ([a PWU b] <-> ![(!a) PSB b]);
  PSW_as_PSB : assert A ([a PSW b] <->  [b PSB (!a & b)]);
  PWB_as_PSB : assert A ([a PWW b] <-> ![b PSB (a & b)]);
  PWW_as_PSB : assert A ([a PWB b] <-> ![b PSB (a & !b)]);


// ---- WB and PWB are expressively complete ------------------

  G_as_WB  : assert A (G a <->  [false WB (!a)]);
  F_as_WB  : assert A (F a <-> ![false WB a]);
  SU_as_WB : assert A ([a SU b] <-> ![(!a) WB b]);
  WU_as_WB : assert A ([a WU b] <->  [b WB (!a & !b)]);
  SW_as_WB : assert A ([a SW b] <-> ![b WB (a & b)]);
  SB_as_WB : assert A ([a SB b] <-> ![b WB (a & !b)]);
  WW_as_WB : assert A ([a WW b] <->  [(a & b) WB (!a & b)]);

  PG_as_PWB  : assert A (PG a <->  [false PWB (!a)]);
  PF_as_PWB  : assert A (PF a <-> ![false PWB a]);
  PSU_as_PWB : assert A ([a PSU b] <-> ![(!a) PWB b]);
  PWU_as_PWB : assert A ([a PWU b] <->  [b PWB (!a & !b)]);
  PSW_as_PWB : assert A ([a PSW b] <-> ![b PWB (a & b)]);
  PWW_as_PWB : assert A ([a PWW b] <->  [(a & b) PWB (!a & b)]);
  PSB_as_PWB : assert A ([a PSB b] <-> ![b PWB (a & !b)]);


// ---- SW and PSW are expressively complete ------------------

  G_as_SW  : assert A (G a <-> ![true SW (!a)]);
  F_as_SW  : assert A (F a <->  [true SW a]);
  SU_as_SW : assert A ([a SU b] <->  [b SW (a -> b)]);
  WU_as_SW : assert A ([a WU b] <-> ![(!b) SW (a -> b)]);
  WB_as_SW : assert A ([a WB b] <-> ![b SW (a | b)]);
  SB_as_SW : assert A ([a SB b] <->  [(!b) SW (a | b)]);
  WW_as_SW : assert A ([a WW b] <-> ![(!a) SW b]);

  PG_as_PSW  : assert A (PG a <-> ![true PSW (!a)]);
  PF_as_PSW  : assert A (PF a <->  [true PSW a]);
  PSU_as_PSW : assert A ([a PSU b] <->  [b PSW (a -> b)]);
  PWU_as_PSW : assert A ([a PWU b] <-> ![(!b) PSW (a -> b)]);
  PWW_as_PSW : assert A ([a PWW b] <-> ![(!a) PSW b]);
  PSB_as_PSW : assert A ([a PSB b] <->  [(!b) PSW (a | b)]);
  PWB_as_PSW : assert A ([a PWB b] <-> ![b PSW (a | b)]);


// ---- WW and PWW are expressively complete ------------------

  G_as_WW  : assert A (G a <->  [false WW (!a)]);
  F_as_WW  : assert A (F a <-> ![false WW a]);
  SU_as_WW : assert A ([a SU b] <-> ![(!b) WW (a -> b)]);
  WU_as_WW : assert A ([a WU b] <->  [  b  WW (a -> b)]);
  WB_as_WW : assert A ([a WB b] <->  [(!b) WW (a | b)]);
  SB_as_WW : assert A ([a SB b] <-> ![  b  WW (a | b)]);
  SW_as_WW : assert A ([a SW b] <-> ![(!a) WW b]);

  PG_as_PWW  : assert A (PG a <->  [false PWW (!a)]);
  PF_as_PWW  : assert A (PF a <-> ![false PWW a]);
  PSU_as_PWW : assert A ([a PSU b] <-> ![(!b) PWW (a -> b)]);
  PWU_as_PWW : assert A ([a PWU b] <->  [  b  PWW (a -> b)]);
  PSW_as_PWW : assert A ([a PSW b] <-> ![(!a) PWW b]);
  PSB_as_PWW : assert A ([a PSB b] <-> ![  b  PWW (a | b)]);
  PWB_as_PWW : assert A ([a PWB b] <->  [(!b) PWW (a | b)]);



// ------- adding redundancy ----------------------

  MoreEvent : assert A(
                       ([a WW b]  <-> [(a & b) WW b])   &
                       ([a WU b]  <-> [(a & !b) WU b])  &
                       ([a WB b]  <-> [(a & !b) WB b])  &
                       ([a SW b]  <-> [(a & b) SW b])   &
                       ([a SU b]  <-> [(a & !b) SU b])  &
                       ([a SB b]  <-> [(a & !b) SB b])  &
                       ([a PWW b] <-> [(a & b) PWW b])  &
                       ([a PWU b] <-> [(a & !b) PWU b]) &
                       ([a PWB b] <-> [(a & !b) PWB b]) &
                       ([a PSW b] <-> [(a & b) PSW b])  &
                       ([a PSU b] <-> [(a & !b) PSU b]) &
                       ([a PSB b] <-> [(a & !b) PSB b]) );


// ------- immediate presence of event that is awaited for ---------

  ImmediateEvent : assert A (b ->
               ([a WW b] <-> a) &
               ([a WU b] <-> true) &
               ([a WB b] <-> false) &
               ([b WB a] <-> !a) &
               ([a SW b] <-> a) &
               ([a SU b] <-> true) &
               ([a SB b] <-> false) &
               ([b SB a] <-> !a) &
               ([a PWW b] <-> a) &
               ([a PWU b] <-> true) &
               ([a PWB b] <-> false) &
               ([b PWB a] <-> !a) &
               ([a PSW b] <-> a) &
               ([a PSU b] <-> true) &
               ([a PSB b] <-> false) &
               ([b PSB a] <-> !a)
             );


// ---- INITIALISATION ---------------------- 

  Init_PWX : assert A(  PWX a);
  Init_PSX : assert A( !PSX a);
  Init_PG  : assert A( PG a <-> a);
  Init_PF  : assert A( PF a <-> a);
  Init_PSU : assert A( [a PSU b] <-> b);
  Init_PSW : assert A( [a PSW b] <-> a & b);
  Init_PSB : assert A( [a PSB b] <-> a & !b);
  Init_PWU : assert A( [a PWU b] <-> a | b);
  Init_PWW : assert A( [a PWW b] <-> a | !b);
  Init_PWB : assert A( [a PWB b] <-> !b);


// ---- FIXPOINTS -----------------------------------------------

  Fix_G   : assert A( G(q <-> a & X q) <-> G(q <-> G a) | G!q );
  Fix_F   : assert A( G(q <-> a | X q) <-> G(q <-> F a) | G q);
  Fix_U   : assert A( G(q <-> b | a & X q) <-> G(q <-> [a WU b]) | G(q <-> [a SU b]));
  Fix_W   : assert A( G(q <-> b & a | !b & X q) <-> G(q <-> [a WW b]) | G(q <-> [a SW b]));
  Fix_B   : assert A( G(q <-> !b & (a | X q))   <-> G(q <-> [a WB b]) | G(q <-> [a SB b]));
  Fix_PG  : assert A( G(q <-> a & PWX q) <-> G(q <-> PG a));
  Fix_PF  : assert A( G(q <-> a | PSX q) <-> G(q <-> PF a));
  Fix_PSU : assert A( G(q <-> b | a & PSX q) <-> G(q <-> [a PSU b]));
  Fix_PWU : assert A( G(q <-> b | a & PWX q) <-> G(q <-> [a PWU b]));
  Fix_PSB : assert A( G(q <-> !b & (a | PSX q)) <-> G(q <-> [a PSB b]));
  Fix_PWB : assert A( G(q <-> !b & (a | PWX q)) <-> G(q <-> [a PWB b]));
  Fix_PSW : assert A( G(q <-> a & b | !b & PSX q) <-> G(q <-> [a PSW b]));
  Fix_PWW : assert A( G(q <-> a & b | !b & PWX q) <-> G(q <-> [a PWW b]));


// ---- invariant reduction of weak temporal operators -----------

  Invariant_G  : assert A (q & G(q      -> a & X q) -> G a ); 
  Invariant_WU : assert A (q & G(q & !b -> a & X q) -> [a WU b] ); 
  Invariant_WB : assert A (q & G(q & !(a&!b) -> !b & X q) -> [a WB b] ); 
  Invariant_WW : assert A (q & G(q & !(a& b) -> !b & X q) -> [a WW b] ); 




// ---- Eliminating nestings of X with past temporal operators ---------

  Separate_X_Conj_PWX : assert A (X (a & PWX b) <-> (b & X a)) ;
  Separate_X_Conj_PSX : assert A (X (a & PSX b) <-> (b & X a)) ;
  Separate_X_Conj_PSU : assert A (X (a & [b PSU c]) <-> (X (a & c) |  [b PSU c] & X (a & b)));
  Separate_X_Conj_PWB : assert A (X (a & [b PWB c]) <-> (X (a & b & !c) | [b PWB c] & X (a & !c)));

  Separate_X_Disj_PWX : assert A (X (a | PWX b) <-> (b | X a));
  Separate_X_Disj_PSX : assert A (X (a | PSX b) <-> (b | X a));
  Separate_X_Disj_PSU : assert A (X (a | [b PSU c]) <-> (X (a |  c) | [b PSU c] & X b));
  Separate_X_Disj_PWB : assert A (X (a | [b PWB c]) <-> (X (a | !c) & ([b PWB c] | X (a | b))));



// ---- Eliminating nestings of SU with past temporal operators ---------

  Separate_SU_Conj_PWX : assert A ([a SU (b & PWX c)] <-> (b & PWX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSX : assert A ([a SU (b & PSX c)] <-> (b & PSX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSU : assert A ([a SU (b & [c PSU d])] <-> ([c PSU d] & [(a &  X c) SU b] | [a SU (d & [(a & X c) SU b])]));
  Separate_SU_Conj_PWB : assert A ([a SU (b & [c PWB d])] <-> ([c PWB d] & [(a & !X d) SU b] | [a SU (c & !d & [(a & !X d) SU b])]));

  Separate_SU_Conj_Left  : assert A ([(a & b) SU c] <-> ([a SU c] & [b SU c]));
  Separate_SU_Disj_Right : assert A ([a SU (b | c)] <-> ([a SU b] | [a SU c]));

  Separate_SU_Disj_PWX : assert A ([(a | PWX b) SU c] <-> (c | (a | PWX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSX : assert A ([(a | PSX b) SU c] <-> (c | (a | PSX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSU : assert A ([(a | [b PSU c]) SU d] 
                <-> ( ([b PSU c] | [(d | X c) WB (!a & !d)]) &
                      [(b | c | [(d | X c) WB (!a & !d) ]) SU d]));
  Separate_SU_Disj_PWB : assert A ([(a | [b PWB c]) SU d]
                <-> ( ([b PWB c] | [(d | X b) WB (!a & !d)]) &
                      [(!c | [(d | X b) WB (!a & !d)]) SU d]));



// ---- Eliminating nestings of WB with past temporal operators ---------

  Separate_WB_Disj_Left  : assert A ([(a | b) WB c] <-> ([a WB c] | [b WB c]));
  Separate_WB_Disj_Right : assert A ([a WB (b | c)] <-> ([a WB b] & [a WB c]));

  Separate_WB_Conj_Right_PWX : assert A ([a WB (b & PWX c)] <-> !(b & PWX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSX : assert A ([a WB (b & PSX c)] <-> !(b & PSX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSU : assert A ([a WB (b & [c PSU d])] 
                <-> ( [(!c) PWB d] | [(a | !X c) WB b]) &
                    [a WB (d & [(!a & X c) SU b])]);
  Separate_WB_Conj_Right_PWB : assert A ([a WB (b & [c PWB d])] 
                <-> ([(!c) PSU d] | [(a | X d) WB b]) &
                    [a WB (c & !d & [(!a & !X d) SU b])]);

  Separate_WB_Conj_Left_PWX : assert A ([(a & PWX b) WB c] <-> !c & a & PWX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSX : assert A ([(a & PSX b) WB c] <-> !c & a & PSX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSU : assert A ([(a & [b PSU c]) WB d]
                <-> [b PSU c] & [(!d & X b) SU (a & !d)] |
                    [(c & [(!d & X b) SU (a & !d)]) WB d]); 
  Separate_WB_Conj_Left_PWB : assert A ([(a & [b PWB c]) WB d]
                <-> [b PWB c] & [(!d & !X c) SU (a & !d)] |
                    [(b & !c &  [(!d & !X c) SU (a & !d)]) WB d]);


// ---- Eliminating nestings of PWX with future temporal operators ---------

  Separate_PWX_Conj_X  : assert A (PWX (a & X b) <-> ( (PWX false) | b & PWX a));
  Separate_PWX_Conj_SU : assert A (PWX (a & [b SU c]) <-> ( PWX (a & c) | [b SU c] & PWX (a & b)));
  Separate_PWX_Conj_WB : assert A (PWX (a & [b WB c]) <-> ( PWX (a & b & !c) | [b WB c] & PWX (a & !c) ));
  Separate_PWX_Disj_X  : assert A (PWX (a | X b) <-> (b | PWX a));
  Separate_PWX_Disj_SU : assert A (PWX (a | [b SU c]) <-> (PWX (a |  c) | [b SU c] & PWX b));
  Separate_PWX_Disj_WB : assert A (PWX (a | [b WB c]) <-> (PWX (a | !c) & ([b WB c] | PWX (a | b))));



// ---- Eliminating nestings of PSU with future temporal operators ---------

  Separate_PSU_Conj_X  : assert A ([a PSU (b & X c)] <-> (b & X c | [a PSU (a & c & PSX b)]));
  Separate_PSU_Conj_SU : assert A ([a PSU (b & [c SU d])] <-> 
                ([c SU d] & [(a & PWX c) PSU b] | 
                 [a PSU (d & [(a & PWX c) PSU b])]));
  Separate_PSU_Conj_WB : assert A ([a PSU (b & [c WB d])] <-> 
                ([c WB d] & [(a & !PWX d) PSU b] | 
                 [a PSU (c & !d & [(a & !PWX d) PSU b])]));

  Separate_PSU_Conj_Left  : assert A ([(a & b) PSU c] <-> ([a PSU c] & [b PSU c]));
  Separate_PSU_Disj_Right : assert A ([a PSU (b | c)] <-> ([a PSU b] | [a PSU c]));

  Separate_PSU_Disj_X  : assert A ([(a | X b) PSU c] <-> (c | (a | X b) & [(b | PWX a) PSU (PSX c)]));
  Separate_PSU_Disj_SU : assert A ([(a | [b SU c]) PSU d] 
                <-> ( ([b SU c] | [(d | PWX c) PWB (!a & !d)]) &
                      [(b | c | [(d | PWX c) PWB (!a & !d) ]) PSU d]));
  Separate_PSU_Disj_WB : assert A ([(a | [b PWB c]) PSU d] 
                <-> ( ([b PWB c] | [(d | PSX b) PWB (!a & !d)]) &
                      [(!c | [(d | PSX b) PWB (!a & !d)]) PSU d]));

}