val from_mech =
   (7 , --`((((arraySize(a)) > 0) ==> ((FromTo
                                           (0)
                                           (0)
                                           (((arraySize(a)) + 1)))
                                       /\
                                       ((F = (?j  . (FromTo
                                                        (j)
                                                        (0)
                                                        (0))
                                                    /\
                                                    (((a) ArrayApp (j) ) = x) ))
                                        /\
                                        ((F ==> (((a) ArrayApp (k) ) = x)) /\ (x = x)))))
            /\
            ((MARKER ["EC"]
              (((((FromTo
                      (i)
                      (0)
                      (((arraySize(a)) + 1)))
                  /\
                  ((found = (?j  . (FromTo
                                       (j)
                                       (0)
                                       (i))
                                   /\
                                   (((a) ArrayApp (j) ) = x__0) ))
                   /\
                   ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                 /\
                 (~(((~(found)) /\ (i < (arraySize(a)))))))
                ==>
                ((found = (?j  . (FromTo
                                     (j)
                                     (0)
                                     ((arraySize(a))))
                                 /\
                                 (((a) ArrayApp (j) ) = x__0) ))
                 /\
                 (found ==> (((a) ArrayApp (k) ) = x__0))))))
             /\
             ((MARKER ["TC2"]
               (((((FromTo
                       (i)
                       (0)
                       (((arraySize(a)) + 1)))
                   /\
                   ((found = (?j  . (FromTo
                                        (j)
                                        (0)
                                        (i))
                                    /\
                                    (((a) ArrayApp (j) ) = x__0) ))
                    /\
                    ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                  /\
                  ((~(found)) /\ (i < (arraySize(a)))))
                 ==>
                 ((((a) ArrayApp (i) ) = x) ==> (((arraySize(a)) - (i + 1)) < ((arraySize(a)) - i))))))
              /\
              ((MARKER ["IC"]
                (((((FromTo
                        (i)
                        (0)
                        (((arraySize(a)) + 1)))
                    /\
                    ((found = (?j  . (FromTo
                                         (j)
                                         (0)
                                         (i))
                                     /\
                                     (((a) ArrayApp (j) ) = x__0) ))
                     /\
                     ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                   /\
                   ((~(found)) /\ (i < (arraySize(a)))))
                  ==>
                  ((((a) ArrayApp (i) ) = x) ==> ((FromTo
                                                      ((i + 1))
                                                      (0)
                                                      (((arraySize(a)) + 1)))
                                                  /\
                                                  ((T = (?j  . (FromTo
                                                                   (j)
                                                                   (0)
                                                                   ((i + 1)))
                                                               /\
                                                               (((a) ArrayApp (j) ) = x__0) ))
                                                   /\
                                                   ((T ==> (((a) ArrayApp (i) ) = x__0)) /\ (x = x__0))))))))
               /\
               ((MARKER ["TC2"]
                 (((((FromTo
                         (i)
                         (0)
                         (((arraySize(a)) + 1)))
                     /\
                     ((found = (?j  . (FromTo
                                          (j)
                                          (0)
                                          (i))
                                      /\
                                      (((a) ArrayApp (j) ) = x__0) ))
                      /\
                      ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                    /\
                    ((~(found)) /\ (i < (arraySize(a)))))
                   ==>
                   ((~((((a) ArrayApp (i) ) = x))) ==> (((arraySize(a)) - (i + 1)) < ((arraySize(a)) - i))))))
                /\
                ((MARKER ["IC"]
                  (((((FromTo
                          (i)
                          (0)
                          (((arraySize(a)) + 1)))
                      /\
                      ((found = (?j  . (FromTo
                                           (j)
                                           (0)
                                           (i))
                                       /\
                                       (((a) ArrayApp (j) ) = x__0) ))
                       /\
                       ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                     /\
                     ((~(found)) /\ (i < (arraySize(a)))))
                    ==>
                    ((~((((a) ArrayApp (i) ) = x))) ==> ((FromTo
                                                             ((i + 1))
                                                             (0)
                                                             (((arraySize(a)) + 1)))
                                                         /\
                                                         ((found = (?j  . (FromTo
                                                                              (j)
                                                                              (0)
                                                                              ((i + 1)))
                                                                          /\
                                                                          (((a) ArrayApp (j) ) = x__0) ))
                                                          /\
                                                          ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))))))
                 /\
                 (MARKER ["TC1"]
                  (((((FromTo
                          (i)
                          (0)
                          (((arraySize(a)) + 1)))
                      /\
                      ((found = (?j  . (FromTo
                                           (j)
                                           (0)
                                           (i))
                                       /\
                                       (((a) ArrayApp (j) ) = x__0) ))
                       /\
                       ((found ==> (((a) ArrayApp (k) ) = x__0)) /\ (x = x__0))))
                     /\
                     ((~(found)) /\ (i < (arraySize(a)))))
                    ==>
                    (((arraySize(a)) - i) > 0))))))))))`-- ) ;