$$ Problem $2(40$ points$)$: Consider the set $AP$ of atomic propositions defined by

$1$ and consider a nonterminating sequential computer program $P$ that manipulates the variable $x.$

Formulate the following informally stated properties as linear time $($LT$)$ properties:

a$.$ false

b$.$ initially x is equal to zero

c$.$ initially $x$ differs from zero

d$.$ initially x is equal to zero, but at some point, x exceeds one

e$.$ x exceeds one only finitely many times

f$.$ x exceeds one infinitely often

g$.$ the value of $x$ alternates between zero and two

h$.$ true

Page $1$