diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index a767847eb..43c771c2a 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -14,8 +14,9 @@
     <script type="text/javascript" src="js/jquery.ba-bbq.min.js"></script>
     <script type="text/javascript">
     jQuery(document).ready(function(){
-        $.spotvars = { autoupdate: 0,
-                       scrolldown: 1 };
+        $.spotvars = { autoupdate: false,
+                       scrolldown: true,
+                       internalchange: false};
         $(".tabs").tabs();
 	$("#send").button();
 	$("#results").hide();
@@ -41,6 +42,17 @@
                              defaultPosition: "left",
                              content: "<b>Click<\/b> to fold/unfold."
                             });
+	$("#brcheckbox").change(function() {
+	    if (!$(this).is(':checked')) {
+              $("#lfcheckbox").removeAttr('checked');
+            }
+        })
+
+	$("#lfcheckbox").change(function() {
+	    if ($(this).is(':checked')) {
+              $("#brcheckbox").attr('checked', true);
+            }
+        })
 
 	function hideOrShowPanels(output, duration) {
 	    switch (output)
@@ -66,7 +78,7 @@
 	    var hashparam = jQuery.deparam.fragment();
 	    if (jQuery.isEmptyObject(hashparam))
 		return;
-	    if ($.spotvars.autoupdate == 0)
+	    if (!$.spotvars.internalchange)
 	      $("input,select", "#trform").each(function() {
 		var name = this.name;
 		var value = [];
@@ -96,7 +108,9 @@
 		    this.value=value.join(',');
 		}
 	      });
-            $.spotvars.autoupdate = 1;
+            $("#brcheckbox").change();
+            $.spotvars.autoupdate = true;
+            $.spotvars.internalchange = false;
 	    var o = $('input[name="o"]').val();
 	    hideOrShowPanels(o, duration);
 	    $("#output-tabs").tabs("select", "#tabs-o" + o);
@@ -144,6 +158,7 @@
             var str = $("#trform").serialize();
 	    // This will trigger updateResults.
             window.location.hash = "#" + str;
+            $.spotvars.internalchange = true;
 	    // updateResults();
         }
 
@@ -166,7 +181,7 @@
 			  fold($("#ltl-head"), function() {
 			    if ($.spotvars.scrolldown)
 			      $('html,body').animate({scrollTop: $("#results-head").offset().top}, 'slow');
-			    $.spotvars.scrolldown = 0;
+			    $.spotvars.scrolldown = false;
 			  });
 			  return true;
 		      });
@@ -183,7 +198,7 @@
         $('input[name="f"]').attr('spellcheck', false).focus()
 	    .keydown(function(e){
                 if (e.keyCode == 13) {
-                  $.spotvars.scrolldown = 1;
+                  $.spotvars.scrolldown = true;
 		  updateHash();
 		}
             });
@@ -349,8 +364,12 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	    <h3 class="ui-widget-header ui-corner-all head">Formula Simplifications<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
 	    <div>
 	      <label class="rtip" title="Apply simple, unconditional rewriting rules to simplify formula.  For instance <span class='formula'>F(a)|F(b)</span> is rewritten as <span class='formula'>F(a|b)</span>.">
-		<INPUT type="checkbox" name="r" value="br" checked>
+		<INPUT id="brcheckbox"  type="checkbox" name="r" value="br" checked>
 		basic rewritings
+	      </label>
+	      <label class="rtip" title="Enable basic rewriting rules that may produce bigger formulas.">
+		<INPUT id="lfcheckbox" type="checkbox" name="r" value="lf" checked>
+		allow larger formulas
 	      </label><br>
 	      <label class="rtip" title="Use rewriting rules based on implications between subformulas, when these implications can be proved syntactically.  For instance <span class='formula'>a U Fa</span> can be reduced to <span class='formula'>Fa</span> because the latter is obviously implied by <span class='formula'>a</span>.">
 	      <INPUT type="checkbox" name="r" value="si" checked>
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index e56c28457..7e5bd7cd9 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -8,6 +8,7 @@ Specifying the formula to work with
 Formula simplifications (pick many)
 
   r=br    enable Basic Reductions
+  r=lf    allow larger formulas
   r=si    enable Syntactic Implications
   r=eu    enable Eventuality and Universality
   r=lc    enable Language Containment
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 2c98dbb58..2fed10fcb 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -349,12 +349,15 @@ if not f:
     finish()
 
 # Formula simplifications
-simpopt = spot.ltl_simplifier_options(False, False, False, False, False)
+simpopt = spot.ltl_simplifier_options(False, False, False,
+                                      False, False, False, True)
 dored = False
 for r in form.getlist('r'):
     dored = True
     if r == 'br':
         simpopt.reduce_basics = True
+    elif r == 'lf':
+        simpopt.reduce_size_strictly = False
     elif r == 'si':
         simpopt.synt_impl = True
     elif r == 'eu':