What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?

Revising for an exam and I'm trying to get to grips with operational semantics. Here's the exam question that prompted me posting this:

Exam Question:

We add to the language $\mathsf{SIMP}$ two new commands, with abstract syntax defined by the grammar rule:

$$C ::= \mathsf{assert}\ B\ \mathsf{before}\ C \mid \mathsf{abort}$$

The small step semantics of $\mathsf{SIMP}$ is extended with the following rules:

$$\frac{\langle B, s \rangle \to \!\, \langle B', s' \rangle}{\langle \mathsf{assert}\ B\ \mathsf{before}\ C, s \rangle \to \!\, \langle \mathsf{assert}\ B'\ \mathsf{before}\ C, s' \rangle}$$

$$\frac{}{\langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ C, s\rangle \to \!\, \langle C, s \rangle}$$

$$\frac{}{\langle \mathsf{assert}\ \mathsf{False}\ \mathsf{before}\ C, s\rangle \to \!\, \langle \mathsf{abort}, s \rangle}$$

The configuration $\langle \mathsf{abort}, s \rangle$ is stuck (no transitions are available from this configuration). Explain with your own words the behaviour of the new commands.

Given $\mathsf{SIMP}$ Language:

$$
\begin{align*}
C &::= \mathsf{skip} \mid l\ \mathsf{:=}\ E \mid C;\, C \mid \mathsf{if}\ B\ \mathsf{then}\ C\ \mathsf{else}\ C \mid \mathsf{while}\ B\ \mathsf{do}\ C \\
E &::= \mathsf{!}l \mid n \mid E\ op\ E \\
op &::= \mathsf{+} \mid \mathsf{-} \mid \mathsf{*} \mid \mathsf{/} \\
B &::= \mathsf{True} \mid \mathsf{False} \mid E\ bop\ E \mid \neg B \mid B \wedge B \\
bop &::= \mathsf{>} \mid \mathsf{<} \mid \mathsf{=} \\
\end{align*}
$$

My Question:

Firstly let me get my understanding of the question out of the way: We're adding a new command $(C)$ to the list of commands we have defined in our $\mathsf{SIMP}$ language. $C$ asserts $B$ before $C$ or aborts the program/process running. Using small step semantics the question has shown us each step of the process as it runs. Here's my issue:

Assuming my knowledge is correct, every rule written below the line holds if what is written above it holds. If this is the case, w

It seems you have some doubts about the first added evaluation rule
$$
\frac
{\langle B, s \rangle \to \!\, \langle B', s' \rangle}
{\langle \mathsf{assert}\ B\ \mathsf{before}\ C, s \rangle \to \!\, \langle \mathsf{assert}\ B'\ \mathsf{before}\ C, s' \rangle}
$$

It might be redundant, but I ought to point out it's one rule: the top part is called a premise of the rule, the bottom part is called a conclusion.

We call rules of this type rules of congruence (and the next two are computation rules). One needs rules of congruence to reduce subparts of a bigger expression or command, i.e. reduce something in its context. Usually, one applies rules of congruence until one can use a computation rule to dispose of some parts of the context. Here, the premise serves you as a means of reducing a Boolean expression $B$ to its value $(\mathsf{True}$ or $\mathsf{False})$.

Let me illustrate this by example: if you have a command $\mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}$, and an initial state $s$, then you reduce it to $\mathsf{skip}$ (without changing $s$) using the second added rule:
$$
\langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle \to \!\, \langle \mathsf{skip}, s \rangle
$$

But what should we do if the command we've got is $\mathsf{assert}\ \mathsf{True \wedge \mathsf{True}}\ \mathsf{before}\ \mathsf{skip}$? There is no computation rules for this, i.e. rules that are able to get rid of the $\mathsf{assert}$... part. Here comes the congruence rule: first you reduce $\mathsf{True \wedge \mathsf{True}}$ to $\mathsf{True}$, using some evaluation rule defined for Booleans (not shown here) -- that's why you need the premise ${\langle B, s \rangle \to \!\, \langle B', s' \rangle}$ -- then you use the 2nd added rule to finish off your computation:

$$
\langle \mathsf{assert}\ \mathsf{True} \wedge \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle
\to
\langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle
\to
\!\, \langle \mathsf{skip}, s \rangle
$$

StackExchange Computer Science Q#57681, answer score: 2