What is this operator in "The Temporal Logic of Programs" Pnueli 1977? In The Temporal Logic of Programs there is an operator first appearing on page 3 (48) under "Partial Correctness" that looks like an elongated super set symbol. What is it?
It's implication as indicated in en.wikipedia.org/wiki/List_of_mathematical_symbols