HTab-1.7.2: rc/gsab_infinite.frm

signature {
propositions { s }
nominals { }
relations { sb, gsb }
}

theory

{
  s;
  []!s;
  <> true;
  [](  <>s &   <gsb>!<>s );
  []<>!s;
  [][]( !s --> ( <>s  & <gsb>!<>s) );
  [gsb]( (<>(<>s  & <>(!s & !<>s)) )  -->  <>!<>s);
  [gsb][]( (!<>s)   -->  []<>s );
  [gsb](!<>( (!<>s) & <><>( !s & (<>s) & <>!<>s)));
  [gsb][gsb]( (<>((!<>s) & <><>(!s & !<>s))) --> <>(!<>s & <>!<>s));
}