diff --git a/client/src/LtlApp.js b/client/src/LtlApp.js
index 7b4a582fb0cab4a4751e9e045c5c0f2ea767c609..926029634bf41c8c10b942ce6a573a13e52e50b1 100644
--- a/client/src/LtlApp.js
+++ b/client/src/LtlApp.js
@@ -1005,6 +1005,8 @@ class LtlStudy extends React.Component {
             <Typography>
               This formula is <b>stutter-invariant</b> even if it might not look
               so syntactically.
+              {"stutter_invariant_eq" in res &&
+               (<><br/>Furthermore, it can be simplified to the following <i>syntactically sutter-invariant</i> formula:<br/><Ltl f={res["stutter_invariant_eq"]}/></>)}
             </Typography>
           )}
           {res["stutter_invariant"] === false && (
diff --git a/server/spotapi.py b/server/spotapi.py
index 0bae0b999f5cf1fcc34e789ae3c87a3a50575d55..8459ff7603ba4c92d2a95c39eb7285d89062509a 100755
--- a/server/spotapi.py
+++ b/server/spotapi.py
@@ -216,13 +216,19 @@ mp_class_to_english = {
 #
 # on success:
 # { mp_class: 'name',
-#   pathological: True,   (absent if not pathological)
+#   pathological: true,   (absent if not pathological)
 #   mp_hierarchy_svg: '<svg...'
 #   acc_word: 'word',     (an example of accepting word, or null)
 #   rej_word: 'word',     (an example of rejecting word, or null)
-#   stutter_invariant: False,   (or True, or 'no X')
+#   stutter_invariant: false,   (or true, or 'no X')
+#   stutter_invariant_eq: formula,  (* see below)
 #   safety_liveness: 'safety'  (or 'liveness', or 'both', or 'none')
 # }
+#
+# stutter_invariant_eq is only given if stutter_invariant=true (not 'no X'),
+# and simplifying the input ltlformula gives a syntactically stutter-invariant
+# formula.
+
 @app.route('/api/study/<path:ltlformula>')
 @cachecontrol()
 def study(ltlformula, method='GET'):
@@ -259,6 +265,11 @@ def study(ltlformula, method='GET'):
     ssi = f.is_syntactic_stutter_invariant()
 
     pos = spot.translate(f, 'med')
+
+    # f was simplified by translate.
+    if (ssi is False and f.is_syntactic_stutter_invariant()):
+        result['stutter_invariant_eq'] = str(f)
+
     neg = spot.translate(spot.formula_Not(f), 'med')
 
     if ssi: