provable by propositional logic
always
|- always
|- always always always
always always
|- always ( and ) (always )
and (always )
|- (eventually always ) and (eventually always )
eventually always ( and )
and (c in S)
( ( or exists d in S: (c
d) and ))
((exists c in S:
) )
a well-founded partial order on set S