HTab-1.7.2: rc/sab_loop_diamond.frm

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

theory

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

 [][][sb][][][] false;
 [][][][][]<> true;
}