diff --git a/doc/org/ltlmix.org b/doc/org/ltlmix.org
index d68cc937b..57371b18f 100644
--- a/doc/org/ltlmix.org
+++ b/doc/org/ltlmix.org
@@ -198,7 +198,7 @@ or	1
 Note that in the LTL case, =false= and =true= can be generated by
 default: when building leave, =alse= and =true= have the same
 probability to be selected as any input formula.
-example).  He
+
 
 * Randomizing atomic propositions with =-A= or =-P=
 
@@ -207,7 +207,7 @@ used in the input formulas.  This works as follows: if option =-A N=
 was given, every time an input formula φ is selected, its atomic
 propositions are replaced by atomic propositions randomly selected in
 a set of size $N$.  If φ uses $i$ atomic propositions and $i\ge N$,
-then those $i$ atomic proposition will be remapped to $i$ distinct
+then those $i$ atomic propositions will be remapped to $i$ distinct
 atomic propositions chosen randomly in that set.  If $i>N$, some of
 the new atomic propositions may replace several of the original atomic
 propositions.
@@ -231,7 +231,7 @@ These options solve two problems:
 
 
 Here is that same example with a single formula, =GFa=, whose atomic
-proposition will be randomly replaced by one of
+propositions will be randomly replaced by one of
 $\{p_0,p_1,p_2,p_3,p_4\}$.
 
 #+BEGIN_SRC sh :exports both
@@ -397,7 +397,7 @@ because we have to deal with two sets of atomic proposition: one set
 for input, and one set for output.
 
 [[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu et al. (IJCAI'17)]] generate their benchmark for LTL synthesis using
-a setup similar to the above, except that when atomic proposition are
+a setup similar to the above, except that when atomic propositions are
 randomized, we must make sure not to change their input or output
 nature.
 
@@ -435,7 +435,7 @@ When randomizing the atomic propositions in these formulas before
 combining them, we want to replace each input (resp. output)
 proposition by a random input (resp. output) proposition.  This is
 achieved by passing two numbers to =-A= or =-P=.  In the case of [[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu
-et al.]], they do not change the polarity of the proposition during
+et al.]], they do not change the polarity of the propositions during
 their generation, so we would use =-A= to mimic their setup.
 
 Here are 6 random conjunctions of the above four patterns, in which
@@ -489,6 +489,6 @@ chose from may help to get more realizable formulas.
 
 
 When the original LTL synthesis specification formulas have atomic
-proposition that do not start with =i= or =o=, options =--ins=,
-=--outs=, or =--part-file= can be used to specify the nature of the
+propositions that do not start with =i= or =o=, options =--ins=,
+=--outs=, or =--part-file= can be used to specify the nature of these
 atomic propositions.  These options work as [[file:ltlsynt.org::#input-options][=ltlsynt='s input options]].