Atomic Proposition	S0	S1	S2	S3..∞	+
A
B
Formula	S0	S1	S2	S3..∞
and(implies(not(next(not(A))), B), implies(B, not(next(not(A)))))					Remove

Syntax Cheatsheet

Concept	Description	Examples
Atomic propositions	Symbolic names (uppercase letters) that are either true or false in a state.	A B
Logical connectives	Operators from propositional logic.	not(A) and(A, B) or(A, B, C) implies(A, B)
Temporal operators	Operators that deal with time.	next(A) eventually(B) always(C) until(A, B)