Proof reading docs/papers/amend

docs/papers/amend.md

@@ -27,8 +27,8 @@ edge being *tainted* by the decision diagram's reduction rule [[ATVA
 v2.0
 ------------------------
 
-For *Nested Sweeping*, we need to mark an arc's *source* to be originating from
-the *outer sweep*. Yet, the *flag* was up to this point used to store the
+For *Nested Sweeping*, we need to *taint* an arc's *source* to be originating
+from the *outer sweep*. Yet, the *flag* was up to this point used to store the
 *out-index* of the source. Hence, for *internal nodes* we introduce the
 out-index (*p*) on the second least-significant bit - essentially adding a
 second (possibly non-Boolean) *flag*.
@@ -54,7 +54,7 @@ To get the maximum width safe from overflows back up to 6 TiB, we have removed
 the most significant *terminal bit flag*. Instead, now all pointers dedicate the
 ℓ most significant bits to its *level*. The largest level is dedicated to *null*
 and the second-largest to *terminals*. This decreases the number of BDD labels
-by 2 and also restricts *terminal* values to it into 64-ℓ-1-1 = 62-ℓ bits. Yet,
+by 2 and also restricts *terminal* values to fit into 64-ℓ-1-1 = 62-ℓ bits. Yet,
 this is fine for `bool`, `char`, `int`, and `float`.
 
 **Figure 10 (a):**