val from_mech =
   (5 , --`(((((arraySize(a)) = n) /\ (n >= 0)) ==> ((FromTo
                                                         (0)
                                                         (0)
                                                         (((arraySize(a)) + 1)))
                                                     /\
                                                     ((!j  . (FromTo
                                                                 (j)
                                                                 (0)
                                                                 (0))
                                                             ==>
                                                             (((a) ArrayApp (j) ) = x) )
                                                      /\
                                                      (x = x))))
            /\
            ((MARKER ["EC"]
              (((((FromTo
                      (i)
                      (0)
                      (((arraySize(a)) + 1)))
                  /\
                  ((!j  . (FromTo
                              (j)
                              (0)
                              (i))
                          ==>
                          (((a) ArrayApp (j) ) = x__0) )
                   /\
                   (x = x__0)))
                 /\
                 (~((i < (arraySize(a))))))
                ==>
                T)))
             /\
             ((MARKER ["TC2"]
               (((((FromTo
                       (i)
                       (0)
                       (((arraySize(a)) + 1)))
                   /\
                   ((!j  . (FromTo
                               (j)
                               (0)
                               (i))
                           ==>
                           (((a) ArrayApp (j) ) = x__0) )
                    /\
                    (x = x__0)))
                  /\
                  (i < (arraySize(a))))
                 ==>
                 (((arraySize((ArrayUpdate
                                  a
                                  i
                                  x)))
                   -
                   (i + 1))
                  <
                  ((arraySize(a)) - i)))))
              /\
              ((MARKER ["IC"]
                (((((FromTo
                        (i)
                        (0)
                        (((arraySize(a)) + 1)))
                    /\
                    ((!j  . (FromTo
                                (j)
                                (0)
                                (i))
                            ==>
                            (((a) ArrayApp (j) ) = x__0) )
                     /\
                     (x = x__0)))
                   /\
                   (i < (arraySize(a))))
                  ==>
                  ((FromTo
                       ((i + 1))
                       (0)
                       (((arraySize((ArrayUpdate
                                        a
                                        i
                                        x)))
                         +
                         1)))
                   /\
                   ((!j  . (FromTo
                               (j)
                               (0)
                               ((i + 1)))
                           ==>
                           ((((ArrayUpdate
                                  a
                                  i
                                  x)) ArrayApp (j) )
                            =
                            x__0) )
                    /\
                    (x = x__0))))))
               /\
               (MARKER ["TC1"]
                (((((FromTo
                        (i)
                        (0)
                        (((arraySize(a)) + 1)))
                    /\
                    ((!j  . (FromTo
                                (j)
                                (0)
                                (i))
                            ==>
                            (((a) ArrayApp (j) ) = x__0) )
                     /\
                     (x = x__0)))
                   /\
                   (i < (arraySize(a))))
                  ==>
                  (((arraySize(a)) - i) > 0))))))))`-- ) ;