HTab-1.7.2: rc/sab_loop.frm

signature {
propositions { a, b }
nominals { }
relations { sb }
}

theory

{
 <>(a & !b & <><>a);
 <>(b & !a & <><>b);
 [sb](a --> [][]!a);
 [sb](b --> [][]!b);
}