hylotab-1.2.0: examples/sat/form05.frm
begin
down x1 . [][] <->x1 ; { transitivity }
[] down x1 . <> true ; { irreflexivity }
<>true { initial successor }
end
begin
down x1 . [][] <->x1 ; { transitivity }
[] down x1 . <> true ; { irreflexivity }
<>true { initial successor }
end