Documentation: Fix typos.

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -766,7 +766,7 @@ What changed? Why?
 
 \subsubsection bitvector_subsubsection Using SAT to reason about data: Bit vectors
 
-So far, we have seen how to reason about simple propositional formulae. This
+So far, we have seen how to reason about simple propositional formulas. This
 seems to be quite far from our goal of reasoning about the behavior of programs.
 As a first step, let us see how we can lift SAT-based reasoning to reasoning about
 data such as machine integers.
@@ -811,7 +811,7 @@ Using the half-adder formulas, we can define the *full adder*, again given as
 two formulas, one for sum and the other for carry. We have
 FA_S(A,B,C_in) = HA(HA(A,B),C_in), giving the sum of A, B and C_in,
 and FA_C(A,B,C_in) = HA_C(A,B) or (C_in and HA_S(A,B)), which states
-whether the result is too big to fit into a bit. Not that the full adder
+whether the result is too big to fit into a bit. Note that the full adder
 has an additional input for carries; in the following step, we will use it
 to chain the full adders together to compute the actual sum.