Help understand the notation
Answering your questions one by one:


The rules are part of an operational semantics, which defines how to evaluate expressions.
The notation with the horizontal line is an inference rule: if all the logical statements above the line are true, then you can conclude that the statement below the line is also true.
The arrow is a predicate that indicates that the left hand side can be evaluated (or reduced) to the right hand side.
The expressions separated by a comma form a tuple; for example, $A_p, cmd_1$ is a pair consisting of $A_p$ and $cmd_1$.
$\mathrm{dom}(f)$ returns the domain of the function $f$, that is, the set of values $x$ for which $f(x)$ is defined.


In these rules, $A_p$ is a state object: a function that maps variable names to values. (Think of it a bit like the heap on which you can allocate objects, and where the variable names are pointers.) The VAR rule performs variable lookup in that state:


If the statement above the line is true: $x \in \mathrm{dom}(A_p)$, that is, the function $A_p$ is defined for the argument $A_p(x)$,
Then the statement below the line is true: $A_p, x \Longrightarrow A_p(x)$, that is, the expression $x$ in the state $A_p$ can be evaluated to $A_p(x)$, which is just the value of the function $A_p$ when you pass in the variable name $x$ as argument.


Hope that helps. For more details, lecture notes on operational semantics (e.g. these from Cambridge) will further explain the notation.