[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Stack Overflow Error



I want to prove the next formula

  inv_aux2: LEMMA
            LET a = (LAMBDA (i:nat) : IF i <= N THEN 1 ELSE 0 ENDIF) ,
                g = polynom(a,N),
                c = (LAMBDA (i:nat) : IF N = 0 THEN 0 ELSE b(i)/b(0) ENDIF),
                t = polynom(c,N),
                p = polynom(b,N),
            s1 = (t(x)^N+1)/(1 - t(x)),
            s2 = - (y/p(x))/(1 + y/p(x))
             IN  p(x) /= 0
             AND p(0) /= 0 and y ## Y
             IMPLIES 1/(p(x) + y) = polynom(comp(a,c,N),N*N)(x) +
                         (s1 + s1*s2 + s2*polynom(comp(a,c,N),N*N)(x))/p(0)

but at a few steps almost all commands that I use done the following error

  Error: Stack overflow (signal 1000)
    [condition type: synchronous-operating-system-signal]
 
    Restart actions (select using :continue):
    0: continue computation
    1: Return to Top Level (an "abort" restart).
    2: Abort entirely from this process.
    [1c] pvs(256):

Any idea?