HTab-1.7.2: rc/gsab_confluence.frm

signature {
propositions { a, b, c }
nominals { }
relations { gsb }
}

theory

{
 <>(a & !b &  <><>a );
 <>(b & !a &  <><>b );
 [][](c & []!c);
 <gsb>[][][] false;
}