Verification

Commands

Imandra has a number of powerful verification commands:

  • verify <func>: takes a function representing a goal and attempts to prove it. If the proof attempt fails, Imandra will try to synthesize a concrete counterexample illustrating the failure. Found counterexamples are installed by Imandra in the CX module.

  • instance <func>: takes a function representing a goal and attempts to synthesize an instance (i.e., a concrete value) that satisfies it. It is useful for answering the question "What is an example value that satisfies this particular property?". Found instances are installed by Imandra in the CX module.

  • theorem <name> <vars> = <body>: takes a name, variables and a function of the variables representing a goal to be proved. If Imandra proves the goal, the named theorem is installed and may be used in subsequent proofs. Theorems can be tagged with attributes instructing Imandra how the theorem should be (automatically) applied to prove other theorems in the future. Found counterexamples are installed by Imandra in the CX module.

  • lemma <name> <vars> = <body>: synonym of theorem, but idiomatically often used for "smaller" subsidiary results as one is working up to a larger theorem.

  • axiom <name> <vars> = <body>: declares an axiom, effectively the same as theorem but forcing Imandra to assume the truth of the conjecture, rather than verifying it. This is of course dangerous and should be used with extreme care.

Examples

In [1]:
verify (fun x -> x + 1 > x)
Out[1]:
- : int -> bool = <fun>
Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
rlimit count10
mk bool var5
num allocs1399881962
memory16.060000
max memory18.750000
Expand
  • start[0.019s] (:var_0: + 1) > :var_0:
  • simplify

    into
    true
    expansions
    []
    rewrite_steps
      forward_chaining
      • unsat

        (mp (asserted (not true)) (rewrite (= (not true) false)) false)
      In [2]:
      instance (fun x y -> x < 0 && x + y = 4)
      
      Out[2]:
      - : int -> Z.t -> bool = <fun>
      module CX : sig val x : Z.t val y : Z.t end
      
      Instance (after 0 steps, 0.022s):
       let x = (-1)
       let y = 5
      
      Instance
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.022s
      details
      Expand
      smt_stats
      num checks1
      eliminated vars1
      rlimit count120
      mk bool var7
      eliminated applications2
      num allocs1480122287
      final checks1
      memory16.280000
      max memory18.750000
      Expand
      • start[0.022s] :var_0: < 0 && :var_0: + :var_1: = 4
      • simplify

        into
        not (0 <= :var_0:) && :var_0: + :var_1: = 4
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let x = (-1) let y = 5 )
          In [3]:
          theorem succ_mono n m = succ n > succ m <==> n > m
          
          Out[3]:
          val succ_mono : int -> int -> bool = <fun>
          
          Proved
          proof
          ground_instances0
          definitions0
          inductions0
          search_time
          0.018s
          details
          Expand
          smt_stats
          rlimit count20
          mk bool var5
          num allocs1560905532
          memory16.630000
          max memory18.750000
          Expand
          • start[0.018s] (:var_0: + 1) > (:var_1: + 1) = :var_0: > :var_1:
          • simplify

            into
            true
            expansions
            []
            rewrite_steps
              forward_chaining
              • unsat

                (mp (asserted (not true)) (rewrite (= (not true) false)) false)
              In [4]:
              verify (fun n -> succ n <> 100)
              
              Out[4]:
              - : Z.t -> bool = <fun>
              module CX : sig val n : Z.t end
              
              Counterexample (after 0 steps, 0.020s):
               let n = 99
              
              Refuted
              proof attempt
              ground_instances0
              definitions0
              inductions0
              search_time
              0.020s
              details
              Expand
              smt_stats
              eliminated vars1
              rlimit count29
              mk bool var5
              num allocs1675071550
              memory16.460000
              max memory18.750000
              Expand
              • start[0.020s] not (:var_0: + 1 = 100)
              • simplify

                into
                not (:var_0: = 99)
                expansions
                []
                rewrite_steps
                  forward_chaining
                  • Sat (Some let n = 99 )

                  Attributes

                  Attributes can be used to give Imandra verification hints, and to instruct Imandra how it should use a proved theorem in subsequent verification efforts, via the installation of a theorem as a "rule".

                  Verification Hints

                  • [@@auto]: apply Imandra's "inductive waterfall" proof strategy, which combines simplification (including automatic subgoaling, conditional rewriting and forward-chaining using previously proved lemmas, decision procedures for datatypes and arithmetic, etc.), and may decide to do induction. This is the most common way to prove a theorem in Imandra.

                  • [@@induct <flag?>]: apply Imandra's "inductive waterfall" proof strategy, but control the top-level induction. The <flag?> can be one of:

                    • functional <func_name> - perform functional induction using an induction scheme derived from <func_name>
                    • structural <args?> - perform structural induction on the arguments <args?> if given, else on a heuristically chosen collection of variables. The types of the induction variables must be algebraic datatypes / variant types. An additive approach (linear in the total number of constructors) is taken for combining the schemes of individual variables into a composite induction scheme.
                    • structural_mult <args?> - like structural, except uses a "multiplicative" scheme, rather than an additive one
                    • structural_add <args?> - a synonym for structural
                  • [@@simp] or [@@simplify]: apply simplification to the goal before unrolling.

                  • [@@disable <f_1>,...,<f_k>]: If f_i is a rule, instructs Imandra to ignore f_i during the proof attempt. If f_i is a function, instructs Imandra to leave the function definition unexpanded during the proof attempt. This is especially useful in the presence of rewrite rules about non-recursive functions, as such rules will typically not apply unless the relevant non-recursive function is disabled. Imandra might choose to ignore this hint if ignoring it leads to immediate closure of the goal, or to the construction of a valid counterexample. Note that rules and functions can be globally disabled, using the #disable directive.

                  • [@@enable <f_1>,...,<f_k>]: The dual of @@disable. Note that rules and functions can be globally enabled, using the #enable directive.

                  • [@@apply <thm <arg_1> ... <arg_k>>]: instantiate thm with the given arguments and add its instantiation to the hypotheses of the goal. This is especially useful when thm is not naturally useable as a @@rewrite or @@forward-chaining rule, but is nevertheless needed (in an instantiated form) to prove a given theorem.

                  • [@@blast]: apply Imandra's blast procedure, which combines symbolic execution and SAT-based bit-blasting. This is useful for difficult combinatorial problems, and problems involving nontrivial (i.e., nonlinear) arithmetic over bounded discrete domains.

                  Rule Classes

                  Theorems may be installed as rules, which instructs Imandra to apply them in certain ways during subsequent proof attempts. The development of an appropriate collection of rules can be used to "teach" Imandra how to reason in a new domain.

                  Examples

                  In [5]:
                  verify (fun x y -> List.length (x@y) = List.length x + List.length y) [@@auto]
                  
                  Out[5]:
                  - : 'a list -> 'a list -> bool = <fun>
                  Goal:
                  
                  List.length (x @ y) = List.length x + List.length y.
                  
                  1 nontautological subgoal.
                  
                  Subgoal 1:
                  
                  |---------------------------------------------------------------------------
                   List.length (List.append x y) = List.length x + List.length y
                  
                  Verified up to bound 10 (after 0.025s).
                  
                  Must try induction.
                  
                  The recursive terms in the conjecture suggest 3 inductions.
                  Subsumption and merging reduces this to 2.
                  
                  Only 1 of those schemes are unflawed.
                  We shall induct according to a scheme derived from List.append.
                  
                  Induction scheme:
                  
                   (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x).
                  
                  2 nontautological subgoals.
                  
                  Subgoal 1.2:
                  
                   H0. x = []
                  |---------------------------------------------------------------------------
                   List.length (List.append x y) = List.length x + List.length y
                  
                  But simplification reduces this to true, using the definitions of List.append
                  and List.length.
                  
                  Subgoal 1.1:
                  
                   H0. not (x = [])
                   H1. List.length (List.append (List.tl x) y) =
                       List.length (List.tl x) + List.length y
                  |---------------------------------------------------------------------------
                   List.length (List.append x y) = List.length x + List.length y
                  
                  But simplification reduces this to true, using the definitions of List.append
                  and List.length.
                  
                  
                  Proved
                  proof
                  ground_instances0
                  definitions5
                  inductions1
                  search_time
                  0.086s
                  Expand
                  • start[0.086s, "Goal"]
                      List.length (List.append :var_0: :var_1:) =
                      List.length :var_0: + List.length :var_1:
                  • subproof

                    List.length (List.append x y) = List.length x + List.length y
                    • start[0.086s, "1"]
                        List.length (List.append x y) = List.length x + List.length y
                    • induction on (functional )
                      :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
                    • Split ((not (x = [])
                              || List.length (List.append x y) = List.length x + List.length y)
                             && (not
                                 (not (x = [])
                                  && List.length (List.append (List.tl x) y) =
                                     List.length (List.tl x) + List.length y)
                                 || List.length (List.append x y) = List.length x + List.length y)
                             :cases [not (x = [])
                                     || List.length (List.append x y) =
                                        List.length x + List.length y;
                                     (x = []
                                      || not
                                         (List.length (List.append (List.tl x) y) =
                                          List.length (List.tl x) + List.length y))
                                     || List.length (List.append x y) =
                                        List.length x + List.length y])
                      • subproof
                        (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y
                        • start[0.040s, "1.1"]
                            (x = []
                             || not
                                (List.length (List.append (List.tl x) y) =
                                 List.length (List.tl x) + List.length y))
                            || List.length (List.append x y) = List.length x + List.length y
                        • simplify
                          into
                          true
                          expansions
                          [List.length, List.length, List.append]
                          rewrite_steps
                            forward_chaining
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                            • List.len_nonnegative
                        • subproof
                          not (x = []) || List.length (List.append x y) = List.length x + List.length y
                          • start[0.040s, "1.2"]
                              not (x = [])
                              || List.length (List.append x y) = List.length x + List.length y
                          • simplify
                            into
                            true
                            expansions
                            [List.length, List.append]
                            rewrite_steps
                              forward_chaining
                              • List.len_nonnegative
                              • List.len_nonnegative
                              • List.len_nonnegative
                      In [6]:
                      verify (fun x -> x @ [] @ x = x @ x) [@@simp]
                      
                      Out[6]:
                      - : 'a list -> bool = <fun>
                      
                      Proved
                      proof
                      ground_instances0
                      definitions1
                      inductions0
                      search_time
                      0.037s
                      details
                      Expand
                      smt_stats
                      rlimit count357
                      mk bool var5
                      num allocs2212378121
                      memory23.640000
                      max memory23.940000
                      Expand
                      • start[0.037s]
                          List.append :var_0: (List.append [] :var_0:) = List.append :var_0: :var_0:
                      • simplify

                        into
                        true
                        expansions
                        List.append
                        rewrite_steps
                          forward_chaining
                          • unsat

                            (mp (asserted (not true)) (rewrite (= (not true) false)) false)
                          In [7]:
                          lemma len_append x y = List.length (x@y) = List.length x + List.length y [@@auto] [@@rw]
                          
                          Out[7]:
                          val len_append : 'a list -> 'a list -> bool = <fun>
                          Goal:
                          
                          List.length (x @ y) = List.length x + List.length y.
                          
                          1 nontautological subgoal.
                          
                          Subgoal 1:
                          
                          |---------------------------------------------------------------------------
                           List.length (List.append x y) = List.length x + List.length y
                          
                          Verified up to bound 10 (after 0.023s).
                          
                          Must try induction.
                          
                          The recursive terms in the conjecture suggest 3 inductions.
                          Subsumption and merging reduces this to 2.
                          
                          Only 1 of those schemes are unflawed.
                          We shall induct according to a scheme derived from List.append.
                          
                          Induction scheme:
                          
                           (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x).
                          
                          2 nontautological subgoals.
                          
                          Subgoal 1.2:
                          
                           H0. x = []
                          |---------------------------------------------------------------------------
                           List.length (List.append x y) = List.length x + List.length y
                          
                          But simplification reduces this to true, using the definitions of List.append
                          and List.length.
                          
                          Subgoal 1.1:
                          
                           H0. not (x = [])
                           H1. List.length (List.append (List.tl x) y) =
                               List.length (List.tl x) + List.length y
                          |---------------------------------------------------------------------------
                           List.length (List.append x y) = List.length x + List.length y
                          
                          But simplification reduces this to true, using the definitions of List.append
                          and List.length.
                          
                          
                          Proved
                          proof
                          ground_instances0
                          definitions5
                          inductions1
                          search_time
                          0.087s
                          Expand
                          • start[0.087s, "Goal"]
                              List.length (List.append :var_0: :var_1:) =
                              List.length :var_0: + List.length :var_1:
                          • subproof

                            List.length (List.append x y) = List.length x + List.length y
                            • start[0.087s, "1"]
                                List.length (List.append x y) = List.length x + List.length y
                            • induction on (functional )
                              :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
                            • Split ((not (x = [])
                                      || List.length (List.append x y) = List.length x + List.length y)
                                     && (not
                                         (not (x = [])
                                          && List.length (List.append (List.tl x) y) =
                                             List.length (List.tl x) + List.length y)
                                         || List.length (List.append x y) = List.length x + List.length y)
                                     :cases [not (x = [])
                                             || List.length (List.append x y) =
                                                List.length x + List.length y;
                                             (x = []
                                              || not
                                                 (List.length (List.append (List.tl x) y) =
                                                  List.length (List.tl x) + List.length y))
                                             || List.length (List.append x y) =
                                                List.length x + List.length y])
                              • subproof
                                (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y
                                • start[0.043s, "1.1"]
                                    (x = []
                                     || not
                                        (List.length (List.append (List.tl x) y) =
                                         List.length (List.tl x) + List.length y))
                                    || List.length (List.append x y) = List.length x + List.length y
                                • simplify
                                  into
                                  true
                                  expansions
                                  [List.length, List.length, List.append]
                                  rewrite_steps
                                    forward_chaining
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                    • List.len_nonnegative
                                • subproof
                                  not (x = []) || List.length (List.append x y) = List.length x + List.length y
                                  • start[0.043s, "1.2"]
                                      not (x = [])
                                      || List.length (List.append x y) = List.length x + List.length y
                                  • simplify
                                    into
                                    true
                                    expansions
                                    [List.length, List.append]
                                    rewrite_steps
                                      forward_chaining
                                      • List.len_nonnegative
                                      • List.len_nonnegative
                                      • List.len_nonnegative
                              In [8]:
                              theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]
                              
                              Out[8]:
                              val len_non_neg : 'a list -> bool = <fun>
                              
                              Proved
                              proof
                              ground_instances0
                              definitions0
                              inductions0
                              search_time
                              0.048s
                              details
                              Expand
                              smt_stats
                              rlimit count450
                              mk bool var5
                              num allocs2989594211
                              memory25.030000
                              max memory25.330000
                              Expand
                              • start[0.048s] List.length :var_0: >= 0
                              • simplify

                                into
                                true
                                expansions
                                []
                                rewrite_steps
                                  forward_chaining
                                  List.len_nonnegative
                                • unsat

                                  (mp (asserted (not true)) (rewrite (= (not true) false)) false)
                                In [9]:
                                lemma foo = (fun x -> x @ [] = x) [@@induct x] [@@disable List.append_to_nil]
                                
                                Out[9]:
                                val foo : 'a list -> bool = <fun>
                                Goal:
                                
                                x @ [] = x.
                                
                                1 nontautological subgoal.
                                
                                Subgoal 1:
                                
                                |---------------------------------------------------------------------------
                                 List.append x [] = x
                                
                                Verified up to bound 10 (after 0.024s).
                                
                                Must try induction.
                                
                                Induction scheme:
                                
                                 φ [] && (x <> [] && φ (List.tl x) ==> φ x).
                                
                                2 nontautological subgoals.
                                
                                Subgoal 1.2:
                                
                                |---------------------------------------------------------------------------
                                 List.append [] [] = []
                                
                                But simplification reduces this to true, using the definition of List.append.
                                
                                Subgoal 1.1:
                                
                                 H0. x <> []
                                 H1. List.append (List.tl x) [] = List.tl x
                                |---------------------------------------------------------------------------
                                 List.append x [] = x
                                
                                But simplification reduces this to true, using the definition of List.append.
                                
                                
                                Proved
                                proof
                                ground_instances0
                                definitions2
                                inductions1
                                search_time
                                0.043s
                                Expand
                                • start[0.043s, "Goal"] List.append :var_0: [] = :var_0:
                                • subproof

                                  List.append x [] = x
                                  • start[0.042s, "1"] List.append x [] = x
                                  • induction on (structural+ x)
                                    :scheme φ [] && (x <> [] && φ (List.tl x) ==> φ x)
                                  • Split (List.append [] [] = []
                                           && (not (x <> [] && List.append (List.tl x) [] = List.tl x)
                                               || List.append x [] = x)
                                           :cases [List.append [] [] = [];
                                                   (not (x <> []) || not (List.append (List.tl x) [] = List.tl x))
                                                   || List.append x [] = x])
                                    • subproof
                                      (not (x <> []) || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x
                                      • start[0.013s, "1.1"]
                                          (not (x <> []) || not (List.append (List.tl x) [] = List.tl x))
                                          || List.append x [] = x
                                      • simplify
                                        into
                                        true
                                        expansions
                                        List.append
                                        rewrite_steps
                                          forward_chaining
                                        • subproof
                                          List.append [] [] = []
                                          • start[0.013s, "1.2"] List.append [] [] = []
                                          • simplify
                                            into
                                            true
                                            expansions
                                            List.append
                                            rewrite_steps
                                              forward_chaining

                                        Verifying our Programs

                                        Now that we've learned the syntax of Imandra's verification statements, let's learn how we can use them to:

                                        • verify the absence of bugs,

                                        • generate counterexamples and test cases, and

                                        • prove program properties.

                                        Unrolling

                                        The first tool that Imandra makes available in our verification toolbox is recursive function unrolling, a form of bounded model checking backed by Satisfiability Modulo Theories (SMT) solving. This technique is completely automatic, and is in general not influenced by the presence of proved rules or enabled/disabled functions (except with used in conjunction with the [@@simp] attribute).

                                        Completeness

                                        For many classes of problems, unrolling is "complete" in various senses. For example, for goals involving only non-recursive functions, algebraic datatypes and linear arithmetic, unrolling will always be able to prove a true goal or refute a false goal in a finite amount of time and space. Moreover, for an even wider class of problems involving recursive functions, datatypes and arithmetic, unrolling is "complete for counterexamples." This means that if a counterexample to a goal exists, unrolling will in principle always be able to synthesize one. This relies on Imandra's "fair" strategy for incrementally expanding the "interpretation call-graph" of a goal.

                                        That said, part of the beauty of unrolling is that you don't need to understand it to apply it!

                                        Strategy

                                        In general, it's recommended to apply unrolling to a goal before you attempt other methods such as the inductive waterfall ([@@auto]). It's amazing how often seemingly true goals are false due to subtle edge cases, and the ability of unrolling to construct concrete counterexamples can be an invaluable filter on your conjectures.

                                        Examples

                                        To use unrolling, we simply use the verify or instance commands.

                                        Let's use unrolling to find an instance of two lists of integers, whose sum equals the length of the two lists concatenated. We shall constrain the total length of the two lists to be positive (for fun, at least 10), so we obtain something more interesting than the simple x=[],y=[] solution!

                                        In [10]:
                                        instance
                                          (fun x y -> List.length (x@y) > 10
                                            && List.fold_left (+) 0 (x@y) = List.length (x@y))
                                        
                                        Out[10]:
                                        - : Z.t list -> Z.t list -> bool = <fun>
                                        module CX : sig val x : Z.t list val y : Z.t list end
                                        
                                        Instance (after 31 steps, 0.081s):
                                         let x = [7854]
                                         let y = [38; (-8882); 8365; (-1); 0; 974; (-3099); 2455; (-3343); (-4350)]
                                        
                                        Instance
                                        proof attempt
                                        ground_instances31
                                        definitions0
                                        inductions0
                                        search_time
                                        0.081s
                                        details
                                        Expand
                                        smt_stats
                                        arith offset eqs19
                                        num checks63
                                        arith assert lower386
                                        arith pivots194
                                        rlimit count64559
                                        mk clause632
                                        datatype occurs check863
                                        mk bool var3458
                                        arith assert upper289
                                        datatype splits609
                                        decisions1399
                                        arith add rows1201
                                        arith bound prop8
                                        propagations1890
                                        interface eqs46
                                        conflicts121
                                        arith fixed eqs312
                                        datatype accessor ax529
                                        minimized lits2
                                        arith conflicts30
                                        arith assert diseq94
                                        datatype constructor ax617
                                        num allocs3301776798
                                        final checks162
                                        added eqs4824
                                        del clause544
                                        arith eq adapter338
                                        memory26.810000
                                        max memory27.640000
                                        Expand
                                        • start[0.081s]
                                            List.length (List.append :var_0: :var_1:) > 10
                                            && List.fold_left + 0 (List.append :var_0: :var_1:) =
                                               List.length (List.append :var_0: :var_1:)
                                        • simplify

                                          into
                                          not (List.length (List.append :var_0: :var_1:) <= 10)
                                          && List.fold_left + 0 (List.append :var_0: :var_1:) =
                                             List.length (List.append :var_0: :var_1:)
                                          expansions
                                          []
                                          rewrite_steps
                                            forward_chaining
                                            • unroll
                                              expr
                                              (|`List.fold_left +[0]`_2731| 0 (|List.append_2723| x_2715 y_2716))
                                              expansions
                                              • unroll
                                                expr
                                                (|List.append_2723| x_2715 y_2716)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|List.length_2728| (|List.append_2723| x_2715 y_2716))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|`List.fold_left +[0]`_2731|
                                                      (+ 0 (|get.::.0_2721| (|List.append_2723| x_2715 y_2716)))
                                                      (|get.:…
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (|List.append_2723| (|get.::.1_2722| x_2715) y_2716)
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (|List.length_2728| (|get.::.1_2722| (|List.append_2723| x_2715 y_2716)))
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (+ 0
                                                                        (|get.::.0_2721| (|List.append_2723| x_2715 y_2716))
                                                                        (|g…
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|List.length_2728|
                                                              (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723| x_2715 y_2716))))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                …
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (|List.append_2723| (|get.::.1_2722| (|get.::.1_2722| x_2715)) y_2716)
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                    …
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                      …
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                        …
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                          …
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|List.append_2723|
                                                                            (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715)))
                                                                            y_2716)
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                              …
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                …
                                                                              expansions
                                                                              • unroll
                                                                                expr
                                                                                (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                  …
                                                                                expansions
                                                                                • unroll
                                                                                  expr
                                                                                  (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                    …
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715))))))
                                                                                      (|List…
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                        …
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                          …
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                            …
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                              …
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715))))))
                                                                                                (|List…
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                                  …
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                                    …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                                      …
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (let ((a!1 (|get.::.0_2721| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                                        …
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| x_2715))))))
                                                                                                          (|List…
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (|get.::.1_2722| (|get.::.1_2722| (|get.::.1_2722| (|List.append_2723|
                                                                                                                            …
                                                                                                          expansions
                                                                                                          • Sat (Some let x = [7854] let y = [38; (-8882); 8365; (-1); 0; 974; (-3099); 2455; (-3343); (-4350)] )

                                                                                                          Imandra was able to find a solution instantly, and reflected it into our runtime in the CX module. Let's compute with it to better understand it:

                                                                                                          In [11]:
                                                                                                          List.length (CX.x@CX.y);;
                                                                                                          List.fold_left (+) 0 (CX.x@CX.y);;
                                                                                                          
                                                                                                          Out[11]:
                                                                                                          - : Z.t = 11
                                                                                                          - : Z.t = 11
                                                                                                          

                                                                                                          Unrolling limit

                                                                                                          Unrolling works by creating a symbolic call graph for the negation of the goal we've asked Imandra to verify (or dually the positive version of the goal in the case of instance), and by iteratively extending this graph with incremental interpretations of recursive functions, up to a given unrolling bound, checking at each step for satisfiability.

                                                                                                          If at any step of the unrolling process the negation of our original goal is satisfiable w.r.t. the interpreted approximations of the recursive functions, then Imandra has found a counterexample for our original goal, which has thus been refuted. In this case, Imandra will report Counterexample (after m steps) and install the found counterexample in the CX module.

                                                                                                          If, on the other hand, Imandra is able to prove that there is no counterexample in a manner that is independent of the bound on the approximations, then our original goal is indeed a theorem valid for all possible inputs, and Imandra will report Theorem Proved. This can always be done for a wide class of theorems on catamorphisms (e.g., List.fold_right), for example.

                                                                                                          Otherwise, if Imandra failed to find a counterexample or proof and stopped unrolling at the unrolling bound, we obtain a weaker result of the form Unknown (verified up to depth k), which effectively means: this may or may not be a theorem, but there are no counterexamples up to depth k. Such bounded results can nevertheless be very useful.

                                                                                                          The unrolling bound defaults to 100 and can be controlled using the #unroll <n> directive.

                                                                                                          Let's try to understand in practice how the unrolling bound plays into unrolling. Consider this simple function that recursively decreases an integer until it reaches 0, then returns 1:

                                                                                                          In [12]:
                                                                                                          let rec f x =
                                                                                                            if x <= 0 then
                                                                                                              1
                                                                                                            else
                                                                                                              f (x - 1)
                                                                                                          
                                                                                                          Out[12]:
                                                                                                          val f : int -> Z.t = <fun>
                                                                                                          
                                                                                                          termination proof

                                                                                                          Termination proof

                                                                                                          call `f (x - 1)` from `f x`
                                                                                                          originalf x
                                                                                                          subf (x - 1)
                                                                                                          original ordinalOrdinal.Int (if x >= 0 then x else 0)
                                                                                                          sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
                                                                                                          path[not (x <= 0)]
                                                                                                          proof
                                                                                                          detailed proof
                                                                                                          ground_instances1
                                                                                                          definitions0
                                                                                                          inductions0
                                                                                                          search_time
                                                                                                          0.012s
                                                                                                          details
                                                                                                          Expand
                                                                                                          smt_stats
                                                                                                          num checks3
                                                                                                          arith assert lower8
                                                                                                          arith pivots2
                                                                                                          rlimit count65586
                                                                                                          mk clause4
                                                                                                          datatype occurs check2
                                                                                                          mk bool var20
                                                                                                          arith assert upper3
                                                                                                          decisions2
                                                                                                          arith add rows3
                                                                                                          propagations2
                                                                                                          conflicts2
                                                                                                          arith fixed eqs2
                                                                                                          datatype accessor ax2
                                                                                                          arith conflicts1
                                                                                                          num allocs3364701230
                                                                                                          final checks1
                                                                                                          added eqs6
                                                                                                          del clause4
                                                                                                          arith eq adapter2
                                                                                                          memory29.770000
                                                                                                          max memory29.770000
                                                                                                          Expand
                                                                                                          • start[0.012s]
                                                                                                              not (x <= 0)
                                                                                                              && (if x >= 0 then x else 0) >= 0
                                                                                                                 && (if (x - 1) >= 0 then x - 1 else 0) >= 0
                                                                                                              ==> (x - 1) <= 0
                                                                                                                  || Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0) Ordinal.<<
                                                                                                                     Ordinal.Int (if x >= 0 then x else 0)
                                                                                                          • simplify
                                                                                                            into
                                                                                                            (not
                                                                                                             ((not (x <= 0) && (if x >= 0 then x else 0) >= 0)
                                                                                                              && (if x >= 1 then -1 + x else 0) >= 0)
                                                                                                             || x <= 1)
                                                                                                            || Ordinal.Int (if x >= 1 then -1 + x else 0) Ordinal.<<
                                                                                                               Ordinal.Int (if x >= 0 then x else 0)
                                                                                                            expansions
                                                                                                            []
                                                                                                            rewrite_steps
                                                                                                              forward_chaining
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (|Ordinal.<<_121| (|Ordinal.Int_112| (ite (>= x_2751 1) (+ (- 1) x_2751) 0))
                                                                                                                                  (|Ord…
                                                                                                                expansions
                                                                                                                • unsat
                                                                                                                  (let ((a!1 (not (= (ite (>= x_2751 0) x_2751 0) x_2751)))
                                                                                                                        (a!2 (>= (+ (ite (>= x_2751 0) x_275…

                                                                                                                Let's verify that for all x < 100, the function will return 1:

                                                                                                                In [13]:
                                                                                                                verify (fun x -> x < 100 ==> f x = 1)
                                                                                                                
                                                                                                                Out[13]:
                                                                                                                - : int -> bool = <fun>
                                                                                                                
                                                                                                                Proved
                                                                                                                proof
                                                                                                                ground_instances100
                                                                                                                definitions0
                                                                                                                inductions0
                                                                                                                search_time
                                                                                                                0.218s
                                                                                                                details
                                                                                                                Expand
                                                                                                                smt_stats
                                                                                                                num checks201
                                                                                                                arith assert lower99
                                                                                                                rlimit count59931
                                                                                                                mk clause300
                                                                                                                mk bool var504
                                                                                                                arith assert upper1
                                                                                                                propagations297
                                                                                                                conflicts101
                                                                                                                arith fixed eqs2
                                                                                                                num allocs3467926745
                                                                                                                final checks100
                                                                                                                added eqs300
                                                                                                                del clause297
                                                                                                                memory32.100000
                                                                                                                max memory32.100000
                                                                                                                Expand
                                                                                                                • start[0.218s] :var_0: < 100 ==> f :var_0: = 1
                                                                                                                • simplify

                                                                                                                  into
                                                                                                                  100 <= :var_0: || f :var_0: = 1
                                                                                                                  expansions
                                                                                                                  []
                                                                                                                  rewrite_steps
                                                                                                                    forward_chaining
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (f_2748 x_2761)
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (f_2748 (+ (- 1) x_2761))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (f_2748 (+ (- 1) (- 1) x_2761))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (f_2748 (+ (- 1) (- 1) (- 1) x_2761))
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (f_2748 (+ (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (f_2748 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_2761))
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                       (- 1)
                                                                                                                                                       (- 1)
                                                                                                                                                       (- 1)
                                                                                                                                                       (- 1)
                                                                                                                                                       (- 1…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                         (- 1)
                                                                                                                                                         (- 1)
                                                                                                                                                         (- 1)
                                                                                                                                                         (- 1)
                                                                                                                                                         (- 1…
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                           (- 1)
                                                                                                                                                           (- 1)
                                                                                                                                                           (- 1)
                                                                                                                                                           (- 1)
                                                                                                                                                           (- 1…
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                             (- 1)
                                                                                                                                                             (- 1)
                                                                                                                                                             (- 1)
                                                                                                                                                             (- 1)
                                                                                                                                                             (- 1…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                               (- 1)
                                                                                                                                                               (- 1)
                                                                                                                                                               (- 1)
                                                                                                                                                               (- 1)
                                                                                                                                                               (- 1…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                 (- 1)
                                                                                                                                                                 (- 1)
                                                                                                                                                                 (- 1)
                                                                                                                                                                 (- 1)
                                                                                                                                                                 (- 1…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                   (- 1)
                                                                                                                                                                   (- 1)
                                                                                                                                                                   (- 1)
                                                                                                                                                                   (- 1)
                                                                                                                                                                   (- 1…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                     (- 1)
                                                                                                                                                                     (- 1)
                                                                                                                                                                     (- 1)
                                                                                                                                                                     (- 1)
                                                                                                                                                                     (- 1…
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                       (- 1)
                                                                                                                                                                       (- 1)
                                                                                                                                                                       (- 1)
                                                                                                                                                                       (- 1)
                                                                                                                                                                       (- 1…
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                         (- 1)
                                                                                                                                                                         (- 1)
                                                                                                                                                                         (- 1)
                                                                                                                                                                         (- 1)
                                                                                                                                                                         (- 1…
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                           (- 1)
                                                                                                                                                                           (- 1)
                                                                                                                                                                           (- 1)
                                                                                                                                                                           (- 1)
                                                                                                                                                                           (- 1…
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                             (- 1)
                                                                                                                                                                             (- 1)
                                                                                                                                                                             (- 1)
                                                                                                                                                                             (- 1)
                                                                                                                                                                             (- 1…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                               (- 1)
                                                                                                                                                                               (- 1)
                                                                                                                                                                               (- 1)
                                                                                                                                                                               (- 1)
                                                                                                                                                                               (- 1…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                 (- 1)
                                                                                                                                                                                 (- 1)
                                                                                                                                                                                 (- 1)
                                                                                                                                                                                 (- 1)
                                                                                                                                                                                 (- 1…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                   (- 1)
                                                                                                                                                                                   (- 1)
                                                                                                                                                                                   (- 1)
                                                                                                                                                                                   (- 1)
                                                                                                                                                                                   (- 1…
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                     (- 1)
                                                                                                                                                                                     (- 1)
                                                                                                                                                                                     (- 1)
                                                                                                                                                                                     (- 1)
                                                                                                                                                                                     (- 1…
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                       (- 1)
                                                                                                                                                                                       (- 1)
                                                                                                                                                                                       (- 1)
                                                                                                                                                                                       (- 1)
                                                                                                                                                                                       (- 1…
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                         (- 1)
                                                                                                                                                                                         (- 1)
                                                                                                                                                                                         (- 1)
                                                                                                                                                                                         (- 1)
                                                                                                                                                                                         (- 1…
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                           (- 1)
                                                                                                                                                                                           (- 1)
                                                                                                                                                                                           (- 1)
                                                                                                                                                                                           (- 1)
                                                                                                                                                                                           (- 1…
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                             (- 1)
                                                                                                                                                                                             (- 1)
                                                                                                                                                                                             (- 1)
                                                                                                                                                                                             (- 1)
                                                                                                                                                                                             (- 1…
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                               (- 1)
                                                                                                                                                                                               (- 1)
                                                                                                                                                                                               (- 1)
                                                                                                                                                                                               (- 1)
                                                                                                                                                                                               (- 1…
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unroll
                                                                                                                                                                                            expr
                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                            expansions
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                    expr
                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                    expansions
                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                      expr
                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                      expansions
                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                        expr
                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                        expansions
                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                          expr
                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                          expansions
                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                            expr
                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                            expansions
                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                              expr
                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                              expansions
                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                expr
                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                            • unroll
                                                                                                                                                                                                                                                                                                              expr
                                                                                                                                                                                                                                                                                                              (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                                         (- 1)
                                                                                                                                                                                                                                                                                                                         (- 1…
                                                                                                                                                                                                                                                                                                              expansions
                                                                                                                                                                                                                                                                                                              • unroll
                                                                                                                                                                                                                                                                                                                expr
                                                                                                                                                                                                                                                                                                                (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                                           (- 1)
                                                                                                                                                                                                                                                                                                                           (- 1…
                                                                                                                                                                                                                                                                                                                expansions
                                                                                                                                                                                                                                                                                                                • unroll
                                                                                                                                                                                                                                                                                                                  expr
                                                                                                                                                                                                                                                                                                                  (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                                             (- 1)
                                                                                                                                                                                                                                                                                                                             (- 1…
                                                                                                                                                                                                                                                                                                                  expansions
                                                                                                                                                                                                                                                                                                                  • unroll
                                                                                                                                                                                                                                                                                                                    expr
                                                                                                                                                                                                                                                                                                                    (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                                               (- 1)
                                                                                                                                                                                                                                                                                                                               (- 1…
                                                                                                                                                                                                                                                                                                                    expansions
                                                                                                                                                                                                                                                                                                                    • unroll
                                                                                                                                                                                                                                                                                                                      expr
                                                                                                                                                                                                                                                                                                                      (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                                 (- 1)
                                                                                                                                                                                                                                                                                                                                 (- 1…
                                                                                                                                                                                                                                                                                                                      expansions
                                                                                                                                                                                                                                                                                                                      • unroll
                                                                                                                                                                                                                                                                                                                        expr
                                                                                                                                                                                                                                                                                                                        (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                                   (- 1)
                                                                                                                                                                                                                                                                                                                                   (- 1…
                                                                                                                                                                                                                                                                                                                        expansions
                                                                                                                                                                                                                                                                                                                        • unroll
                                                                                                                                                                                                                                                                                                                          expr
                                                                                                                                                                                                                                                                                                                          (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                                     (- 1)
                                                                                                                                                                                                                                                                                                                                     (- 1…
                                                                                                                                                                                                                                                                                                                          expansions
                                                                                                                                                                                                                                                                                                                          • unroll
                                                                                                                                                                                                                                                                                                                            expr
                                                                                                                                                                                                                                                                                                                            (f_2748 (+ (- 1)
                                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                                       (- 1)
                                                                                                                                                                                                                                                                                                                                       (- 1…
                                                                                                                                                                                                                                                                                                                            expansions
                                                                                                                                                                                                                                                                                                                            • unsat

                                                                                                                                                                                                                                                                                                                              (let ((a!1 (= (ite (<= x_2761 99) 1 (f_2748 (+ (- 100) x_2761))) 1))
                                                                                                                                                                                                                                                                                                                                    (a!3 (monotonicity (rewri…