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. When verifying a formula that doesn't depend on function parameters, verify (<expr>) is a shorthand for verify (fun () -> <expr>)

  • 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.040s
details
Expand
smt_stats
rlimit count10
mk bool var5
num allocs1354308917
memory25.040000
max memory27.740000
Expand
  • start[0.040s] (: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.038s):
       let x = (-1)
       let y = 5
      
      Instance
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.038s
      details
      Expand
      smt_stats
      num checks1
      eliminated vars1
      rlimit count120
      mk bool var7
      eliminated applications2
      num allocs1460995864
      final checks1
      memory25.260000
      max memory27.740000
      Expand
      • start[0.038s] :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.028s
          details
          Expand
          smt_stats
          rlimit count20
          mk bool var5
          num allocs1540727088
          memory25.610000
          max memory27.740000
          Expand
          • start[0.028s] (: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.028s):
               let n = 99
              
              Refuted
              proof attempt
              ground_instances0
              definitions0
              inductions0
              search_time
              0.028s
              details
              Expand
              smt_stats
              eliminated vars1
              rlimit count29
              mk bool var5
              num allocs1622004690
              memory25.810000
              max memory27.740000
              Expand
              • start[0.028s] 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.183s).
                  
                  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.339s
                  Expand
                  • start[0.339s, "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.339s, "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.049s, "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.049s, "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.061s
                      details
                      Expand
                      smt_stats
                      rlimit count357
                      mk bool var5
                      num allocs2161422749
                      memory32.340000
                      max memory32.640000
                      Expand
                      • start[0.061s]
                          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.022s).
                          
                          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.123s
                          Expand
                          • start[0.123s, "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.123s, "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.055s, "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.055s, "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.071s
                              details
                              Expand
                              smt_stats
                              rlimit count450
                              mk bool var5
                              num allocs2937416450
                              memory33.720000
                              max memory34.020000
                              Expand
                              • start[0.071s] 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.062s).
                                
                                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.157s
                                Expand
                                • start[0.157s, "Goal"] List.append :var_0: [] = :var_0:
                                • subproof

                                  List.append x [] = x
                                  • start[0.157s, "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.070s, "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.070s, "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.233s):
                                         let x = [2328]
                                         let y = [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)]
                                        
                                        Instance
                                        proof attempt
                                        ground_instances31
                                        definitions0
                                        inductions0
                                        search_time
                                        0.233s
                                        details
                                        Expand
                                        smt_stats
                                        arith offset eqs9
                                        num checks63
                                        arith assert lower377
                                        arith pivots202
                                        rlimit count64515
                                        mk clause580
                                        datatype occurs check647
                                        mk bool var2583
                                        arith assert upper280
                                        datatype splits375
                                        decisions1144
                                        arith add rows1263
                                        arith bound prop9
                                        propagations1688
                                        interface eqs36
                                        conflicts106
                                        arith fixed eqs294
                                        datatype accessor ax340
                                        minimized lits2
                                        arith conflicts29
                                        arith assert diseq94
                                        datatype constructor ax386
                                        num allocs3283951672
                                        final checks132
                                        added eqs4040
                                        del clause506
                                        arith eq adapter330
                                        memory35.910000
                                        max memory38.530000
                                        Expand
                                        • start[0.233s]
                                            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 = [2328] let y = [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)] )

                                                                                                          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.052s
                                                                                                          details
                                                                                                          Expand
                                                                                                          smt_stats
                                                                                                          num checks3
                                                                                                          arith assert lower8
                                                                                                          arith pivots2
                                                                                                          rlimit count65542
                                                                                                          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 allocs3346866764
                                                                                                          final checks1
                                                                                                          added eqs6
                                                                                                          del clause4
                                                                                                          arith eq adapter2
                                                                                                          memory38.850000
                                                                                                          max memory38.850000
                                                                                                          Expand
                                                                                                          • start[0.052s]
                                                                                                              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.973s
                                                                                                                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 allocs3450078633
                                                                                                                final checks100
                                                                                                                added eqs300
                                                                                                                del clause297
                                                                                                                memory41.170000
                                                                                                                max memory41.170000
                                                                                                                Expand
                                                                                                                • start[0.973s] :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…