spec LTL(bool a,b,c,d,q) {

// ---- implementing temporal operators by watchdogs ----------

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


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

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

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


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

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

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


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

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


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

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


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

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

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


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

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

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


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

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

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


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

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

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


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

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

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


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

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

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



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

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


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

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


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

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




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

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

  Separate_X_Disj_PWX : A (X (a | PWX b) <-> (b | X a));
  Separate_X_Disj_PSX : A (X (a | PSX b) <-> (b | X a));
  Separate_X_Disj_PSU : A (X (a | [b PSU c]) <-> (X (a |  c) | [b PSU c] & X b));
  Separate_X_Disj_PWB : 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 : A ([a SU (b & PWX c)] <-> (b & PWX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSX : A ([a SU (b & PSX c)] <-> (b & PSX c | [a SU (a & c & X b)]));
  Separate_SU_Conj_PSU : 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 : 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  : A ([(a & b) SU c] <-> ([a SU c] & [b SU c]));
  Separate_SU_Disj_Right : A ([a SU (b | c)] <-> ([a SU b] | [a SU c]));

  Separate_SU_Disj_PWX : A ([(a | PWX b) SU c] <-> (c | (a | PWX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSX : A ([(a | PSX b) SU c] <-> (c | (a | PSX b) & [(b | X a) SU (X c)]));
  Separate_SU_Disj_PSU : 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 : 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  : A ([(a | b) WB c] <-> ([a WB c] | [b WB c]));
  Separate_WB_Disj_Right : A ([a WB (b | c)] <-> ([a WB b] & [a WB c]));

  Separate_WB_Conj_Right_PWX : A ([a WB (b & PWX c)] <-> !(b & PWX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSX : A ([a WB (b & PSX c)] <-> !(b & PSX c) & (a | [(X a) WB (c & X b)]));
  Separate_WB_Conj_Right_PSU : 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 : 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 : A ([(a & PWX b) WB c] <-> !c & a & PWX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSX : A ([(a & PSX b) WB c] <-> !c & a & PSX b | !c & [(b & X a) WB (X c)]);
  Separate_WB_Conj_Left_PSU : 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 : 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  : A (PWX (a & X b) <-> ( (PWX false) | b & PWX a));
  Separate_PWX_Conj_SU : A (PWX (a & [b SU c]) <-> ( PWX (a & c) | [b SU c] & PWX (a & b)));
  Separate_PWX_Conj_WB : A (PWX (a & [b WB c]) <-> ( PWX (a & b & !c) | [b WB c] & PWX (a & !c) ));
  Separate_PWX_Disj_X  : A (PWX (a | X b) <-> (b | PWX a));
  Separate_PWX_Disj_SU : A (PWX (a | [b SU c]) <-> (PWX (a |  c) | [b SU c] & PWX b));
  Separate_PWX_Disj_WB : 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  : A ([a PSU (b & X c)] <-> (b & X c | [a PSU (a & c & PSX b)]));
  Separate_PSU_Conj_SU : 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 : 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  : A ([(a & b) PSU c] <-> ([a PSU c] & [b PSU c]));
  Separate_PSU_Disj_Right : A ([a PSU (b | c)] <-> ([a PSU b] | [a PSU c]));

  Separate_PSU_Disj_X  : A ([(a | X b) PSU c] <-> (c | (a | X b) & [(b | PWX a) PSU (PSX c)]));
  Separate_PSU_Disj_SU : 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 : 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]));

}