[PVS-HELP] about Inst. existential quantifiers

[fsong@xxxxxxxxxxxxxxx]

Dear Everyone:

I have a sequent as follow, I want to inst the quantifier the deepest one as  (EXISTS (s: State[Vars]) in the example.

How can I do? Thanks

 EXISTS (s_1: State[Vars]):
        (EXISTS (s_8: State[Vars]):
           (EXISTS (s_7: State[Vars]):
              (EXISTS (s_6: State[Vars]):
                 (EXISTS (s_5: State[Vars]):
                    (EXISTS (s_4: State[Vars]):
                       (EXISTS (s_3: State[Vars]):
                          (EXISTS (s_2: State[Vars]):
                             (EXISTS (s: State[Vars]):
                                intro(x)(Init_state, s) AND
                                 intro(y)(s, s_2))
                              AND intro(z)(s_2, s_3))
                           AND intro(max)(s_3, s_4))
                        AND intro(min)(s_4, s_5))
                     AND intro(aver)(s_5, s_6))
                  AND assign(x, 1)(s_6, s_7))
               AND assign(y, 3)(s_7, s_8))
            AND assign(z, 8)(s_8, s_1))
         AND
         (c(LAMBDA (s1_1, s2_1: State[Vars]):
              EXISTS (s_1: State[Vars]):
                assign(max, x)(s1_1, s_1) AND
                 (EXISTS (s: State[Vars]):
                    IFELSE((max > y), skip, assign(max, y))(s_1, s) AND
                     IFELSE((max > z), skip, assign(max, z))(s, s2_1)),
            LAMBDA (s1_1, s2_1: State[Vars]):
              EXISTS (s_1: State[Vars]):
                assign(min, x)(s1_1, s_1) AND
                 (EXISTS (s: State[Vars]):
                    IFELSE((min < y), skip, assign(min, y))(s_1, s) AND
                     IFELSE((min < z), skip, assign(min, z))(s, s2_1)))
           // assign(aver, exp(x, y, z)))
             (s_1, s_end)