val from_mech =
   (9 , --`((((0 < (arraySize(a))) /\ ((allRWB) (a) )) ==> (((allRWB) (a) ) /\ ((!k  . (FromTo
                                                                                           (k)
                                                                                           ((arraySize(a)))
                                                                                           ((arraySize(a))))
                                                                                       ==>
                                                                                       ((isRed) (((a) ArrayApp (k) )) ) )
                                                                                /\
                                                                                ((!k  . (FromTo
                                                                                            (k)
                                                                                            (0)
                                                                                            (0))
                                                                                        ==>
                                                                                        ((isWhite) (((a) ArrayApp (k) )) ) )
                                                                                 /\
                                                                                 ((!k  . (FromTo
                                                                                             (k)
                                                                                             (0)
                                                                                             (0))
                                                                                         ==>
                                                                                         ((isBlue) (((a) ArrayApp (k) )) ) )
                                                                                  /\
                                                                                  ((FromTo
                                                                                       (0)
                                                                                       (0)
                                                                                       ((0 + 1)))
                                                                                   /\
                                                                                   ((0 <= (arraySize(a))) /\ ((arraySize(a)) <= (arraySize(a))))))))))
            /\
            ((MARKER ["EC"]
              ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                 (k)
                                                 (r)
                                                 ((arraySize(a))))
                                             ==>
                                             ((isRed) (((a) ArrayApp (k) )) ) )
                                      /\
                                      ((!k  . (FromTo
                                                  (k)
                                                  (b)
                                                  (i))
                                              ==>
                                              ((isWhite) (((a) ArrayApp (k) )) ) )
                                       /\
                                       ((!k  . (FromTo
                                                   (k)
                                                   (0)
                                                   (b))
                                               ==>
                                               ((isBlue) (((a) ArrayApp (k) )) ) )
                                        /\
                                        ((FromTo
                                             (b)
                                             (0)
                                             ((i + 1)))
                                         /\
                                         ((i <= r) /\ (r <= (arraySize(a)))))))))
                 /\
                 (~((i < r))))
                ==>
                ((dutchSorted) (a) ))))
             /\
             ((MARKER ["TC2"]
               ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                  (k)
                                                  (r)
                                                  ((arraySize(a))))
                                              ==>
                                              ((isRed) (((a) ArrayApp (k) )) ) )
                                       /\
                                       ((!k  . (FromTo
                                                   (k)
                                                   (b)
                                                   (i))
                                               ==>
                                               ((isWhite) (((a) ArrayApp (k) )) ) )
                                        /\
                                        ((!k  . (FromTo
                                                    (k)
                                                    (0)
                                                    (b))
                                                ==>
                                                ((isBlue) (((a) ArrayApp (k) )) ) )
                                         /\
                                         ((FromTo
                                              (b)
                                              (0)
                                              ((i + 1)))
                                          /\
                                          ((i <= r) /\ (r <= (arraySize(a)))))))))
                  /\
                  (i < r))
                 ==>
                 ((((a) ArrayApp (i) ) = 2) ==> ((r - (i + 1)) < (r - i))))))
              /\
              ((MARKER ["IC"]
                ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                   (k)
                                                   (r)
                                                   ((arraySize(a))))
                                               ==>
                                               ((isRed) (((a) ArrayApp (k) )) ) )
                                        /\
                                        ((!k  . (FromTo
                                                    (k)
                                                    (b)
                                                    (i))
                                                ==>
                                                ((isWhite) (((a) ArrayApp (k) )) ) )
                                         /\
                                         ((!k  . (FromTo
                                                     (k)
                                                     (0)
                                                     (b))
                                                 ==>
                                                 ((isBlue) (((a) ArrayApp (k) )) ) )
                                          /\
                                          ((FromTo
                                               (b)
                                               (0)
                                               ((i + 1)))
                                           /\
                                           ((i <= r) /\ (r <= (arraySize(a)))))))))
                   /\
                   (i < r))
                  ==>
                  ((((a) ArrayApp (i) ) = 2) ==> (((allRWB) ((ArrayUpdate
                                                                 (ArrayUpdate
                                                                     a
                                                                     i
                                                                     ((a) ArrayApp (b) ))
                                                                 b
                                                                 ((a) ArrayApp (i) ))) )
                                                  /\
                                                  ((!k  . (FromTo
                                                              (k)
                                                              (r)
                                                              ((arraySize((ArrayUpdate
                                                                              (ArrayUpdate
                                                                                  a
                                                                                  i
                                                                                  ((a) ArrayApp (b) ))
                                                                              b
                                                                              ((a) ArrayApp (i) ))))))
                                                          ==>
                                                          ((isRed) ((((ArrayUpdate
                                                                          (ArrayUpdate
                                                                              a
                                                                              i
                                                                              ((a) ArrayApp (b) ))
                                                                          b
                                                                          ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                   /\
                                                   ((!k  . (FromTo
                                                               (k)
                                                               ((b + 1))
                                                               ((i + 1)))
                                                           ==>
                                                           ((isWhite) ((((ArrayUpdate
                                                                             (ArrayUpdate
                                                                                 a
                                                                                 i
                                                                                 ((a) ArrayApp (b) ))
                                                                             b
                                                                             ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                    /\
                                                    ((!k  . (FromTo
                                                                (k)
                                                                (0)
                                                                ((b + 1)))
                                                            ==>
                                                            ((isBlue) ((((ArrayUpdate
                                                                             (ArrayUpdate
                                                                                 a
                                                                                 i
                                                                                 ((a) ArrayApp (b) ))
                                                                             b
                                                                             ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                     /\
                                                     ((FromTo
                                                          ((b + 1))
                                                          (0)
                                                          (((i + 1) + 1)))
                                                      /\
                                                      (((i + 1) <= r) /\ (r <= (arraySize((ArrayUpdate
                                                                                              (ArrayUpdate
                                                                                                  a
                                                                                                  i
                                                                                                  ((a) ArrayApp (b) ))
                                                                                              b
                                                                                              ((a) ArrayApp (i) )))))))))))))))
               /\
               ((MARKER ["TC2"]
                 ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                    (k)
                                                    (r)
                                                    ((arraySize(a))))
                                                ==>
                                                ((isRed) (((a) ArrayApp (k) )) ) )
                                         /\
                                         ((!k  . (FromTo
                                                     (k)
                                                     (b)
                                                     (i))
                                                 ==>
                                                 ((isWhite) (((a) ArrayApp (k) )) ) )
                                          /\
                                          ((!k  . (FromTo
                                                      (k)
                                                      (0)
                                                      (b))
                                                  ==>
                                                  ((isBlue) (((a) ArrayApp (k) )) ) )
                                           /\
                                           ((FromTo
                                                (b)
                                                (0)
                                                ((i + 1)))
                                            /\
                                            ((i <= r) /\ (r <= (arraySize(a)))))))))
                    /\
                    (i < r))
                   ==>
                   ((~((((a) ArrayApp (i) ) = 2))) ==> ((((a) ArrayApp (i) ) = 1) ==> ((r - (i + 1)) < (r - i)))))))
                /\
                ((MARKER ["IC"]
                  ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                     (k)
                                                     (r)
                                                     ((arraySize(a))))
                                                 ==>
                                                 ((isRed) (((a) ArrayApp (k) )) ) )
                                          /\
                                          ((!k  . (FromTo
                                                      (k)
                                                      (b)
                                                      (i))
                                                  ==>
                                                  ((isWhite) (((a) ArrayApp (k) )) ) )
                                           /\
                                           ((!k  . (FromTo
                                                       (k)
                                                       (0)
                                                       (b))
                                                   ==>
                                                   ((isBlue) (((a) ArrayApp (k) )) ) )
                                            /\
                                            ((FromTo
                                                 (b)
                                                 (0)
                                                 ((i + 1)))
                                             /\
                                             ((i <= r) /\ (r <= (arraySize(a)))))))))
                     /\
                     (i < r))
                    ==>
                    ((~((((a) ArrayApp (i) ) = 2))) ==> ((((a) ArrayApp (i) ) = 1) ==> (((allRWB) (a) ) /\ ((!k  . (FromTo
                                                                                                                       (k)
                                                                                                                       (r)
                                                                                                                       ((arraySize(a))))
                                                                                                                   ==>
                                                                                                                   ((isRed) (((a) ArrayApp (k) )) ) )
                                                                                                            /\
                                                                                                            ((!k  . (FromTo
                                                                                                                        (k)
                                                                                                                        (b)
                                                                                                                        ((i + 1)))
                                                                                                                    ==>
                                                                                                                    ((isWhite) (((a) ArrayApp (k) )) ) )
                                                                                                             /\
                                                                                                             ((!k  . (FromTo
                                                                                                                         (k)
                                                                                                                         (0)
                                                                                                                         (b))
                                                                                                                     ==>
                                                                                                                     ((isBlue) (((a) ArrayApp (k) )) ) )
                                                                                                              /\
                                                                                                              ((FromTo
                                                                                                                   (b)
                                                                                                                   (0)
                                                                                                                   (((i + 1) + 1)))
                                                                                                               /\
                                                                                                               (((i + 1) <= r) /\ (r <= (arraySize(a))))))))))))))
                 /\
                 ((MARKER ["TC2"]
                   ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                      (k)
                                                      (r)
                                                      ((arraySize(a))))
                                                  ==>
                                                  ((isRed) (((a) ArrayApp (k) )) ) )
                                           /\
                                           ((!k  . (FromTo
                                                       (k)
                                                       (b)
                                                       (i))
                                                   ==>
                                                   ((isWhite) (((a) ArrayApp (k) )) ) )
                                            /\
                                            ((!k  . (FromTo
                                                        (k)
                                                        (0)
                                                        (b))
                                                    ==>
                                                    ((isBlue) (((a) ArrayApp (k) )) ) )
                                             /\
                                             ((FromTo
                                                  (b)
                                                  (0)
                                                  ((i + 1)))
                                              /\
                                              ((i <= r) /\ (r <= (arraySize(a)))))))))
                      /\
                      (i < r))
                     ==>
                     ((~((((a) ArrayApp (i) ) = 2))) ==> ((~((((a) ArrayApp (i) ) = 1))) ==> (((r - 1) - i) < (r - i)))))))
                  /\
                  ((MARKER ["IC"]
                    ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                       (k)
                                                       (r)
                                                       ((arraySize(a))))
                                                   ==>
                                                   ((isRed) (((a) ArrayApp (k) )) ) )
                                            /\
                                            ((!k  . (FromTo
                                                        (k)
                                                        (b)
                                                        (i))
                                                    ==>
                                                    ((isWhite) (((a) ArrayApp (k) )) ) )
                                             /\
                                             ((!k  . (FromTo
                                                         (k)
                                                         (0)
                                                         (b))
                                                     ==>
                                                     ((isBlue) (((a) ArrayApp (k) )) ) )
                                              /\
                                              ((FromTo
                                                   (b)
                                                   (0)
                                                   ((i + 1)))
                                               /\
                                               ((i <= r) /\ (r <= (arraySize(a)))))))))
                       /\
                       (i < r))
                      ==>
                      ((~((((a) ArrayApp (i) ) = 2))) ==> ((~((((a) ArrayApp (i) ) = 1))) ==> (((allRWB) ((ArrayUpdate
                                                                                                              (ArrayUpdate
                                                                                                                  a
                                                                                                                  i
                                                                                                                  ((a) ArrayApp ((r - 1)) ))
                                                                                                              (r - 1)
                                                                                                              ((a) ArrayApp (i) ))) )
                                                                                               /\
                                                                                               ((!k  . (FromTo
                                                                                                           (k)
                                                                                                           ((r - 1))
                                                                                                           ((arraySize((ArrayUpdate
                                                                                                                           (ArrayUpdate
                                                                                                                               a
                                                                                                                               i
                                                                                                                               ((a) ArrayApp ((r - 1)) ))
                                                                                                                           (r - 1)
                                                                                                                           ((a) ArrayApp (i) ))))))
                                                                                                       ==>
                                                                                                       ((isRed) ((((ArrayUpdate
                                                                                                                       (ArrayUpdate
                                                                                                                           a
                                                                                                                           i
                                                                                                                           ((a) ArrayApp ((r - 1)) ))
                                                                                                                       (r - 1)
                                                                                                                       ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                                                                /\
                                                                                                ((!k  . (FromTo
                                                                                                            (k)
                                                                                                            (b)
                                                                                                            (i))
                                                                                                        ==>
                                                                                                        ((isWhite) ((((ArrayUpdate
                                                                                                                          (ArrayUpdate
                                                                                                                              a
                                                                                                                              i
                                                                                                                              ((a) ArrayApp ((r - 1)) ))
                                                                                                                          (r - 1)
                                                                                                                          ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                                                                 /\
                                                                                                 ((!k  . (FromTo
                                                                                                             (k)
                                                                                                             (0)
                                                                                                             (b))
                                                                                                         ==>
                                                                                                         ((isBlue) ((((ArrayUpdate
                                                                                                                          (ArrayUpdate
                                                                                                                              a
                                                                                                                              i
                                                                                                                              ((a) ArrayApp ((r - 1)) ))
                                                                                                                          (r - 1)
                                                                                                                          ((a) ArrayApp (i) ))) ArrayApp (k) )) ) )
                                                                                                  /\
                                                                                                  ((FromTo
                                                                                                       (b)
                                                                                                       (0)
                                                                                                       ((i + 1)))
                                                                                                   /\
                                                                                                   ((i <= (r - 1)) /\ ((r - 1) <= (arraySize((ArrayUpdate
                                                                                                                                                 (ArrayUpdate
                                                                                                                                                     a
                                                                                                                                                     i
                                                                                                                                                     ((a) ArrayApp ((r - 1)) ))
                                                                                                                                                 (r - 1)
                                                                                                                                                 ((a) ArrayApp (i) ))))))))))))))))
                   /\
                   (MARKER ["TC1"]
                    ((((((allRWB) (a) ) /\ ((!k  . (FromTo
                                                       (k)
                                                       (r)
                                                       ((arraySize(a))))
                                                   ==>
                                                   ((isRed) (((a) ArrayApp (k) )) ) )
                                            /\
                                            ((!k  . (FromTo
                                                        (k)
                                                        (b)
                                                        (i))
                                                    ==>
                                                    ((isWhite) (((a) ArrayApp (k) )) ) )
                                             /\
                                             ((!k  . (FromTo
                                                         (k)
                                                         (0)
                                                         (b))
                                                     ==>
                                                     ((isBlue) (((a) ArrayApp (k) )) ) )
                                              /\
                                              ((FromTo
                                                   (b)
                                                   (0)
                                                   ((i + 1)))
                                               /\
                                               ((i <= r) /\ (r <= (arraySize(a)))))))))
                       /\
                       (i < r))
                      ==>
                      ((r - i) > 0))))))))))))`-- ) ;