TRACE OF subst PREDICATE
                                      ------------------------


          Script started on Thu Oct 27 13:42:21 1994
          vestavia% sbprolog
          SB-Prolog Version 3.1
          | ?- consult('coreas.pro').
          yes
          | ?- trace(subst/4).
          yes
          | ?- pre_condition(P), program(S), post_condition(Q), loop_invariant(I),
                   verify(P, S, Q).
             (1) Call: subst(and(x = q * y + r,r >= 0),r - y,r,_1393344) ?
             (2) Call: subst(x = q * y + r,r - y,r,_1393636) ?
             (3) Call: subst(x,r - y,r,_1393928) ?
             (3) Exit: subst(x,r - y,r,x)
             (4) Call: subst(q * y + r,r - y,r,_1394420) ?
             (5) Call: subst(q * y,r - y,r,_1394712) ?
             (6) Call: subst(q,r - y,r,_1395004) ?
             (6) Exit: subst(q,r - y,r,q)
             (7) Call: subst(y,r - y,r,_1395496) ?
             (7) Exit: subst(y,r - y,r,y)
             (5) Exit: subst(q * y,r - y,r,q * y)
             (8) Call: subst(r,r - y,r,_1396212) ?
             (8) Exit: subst(r,r - y,r,r - y)
             (4) Exit: subst(q * y + r,r - y,r,q * y + (r - y))
             (2) Exit: subst(x = q * y + r,r - y,r,x = q * y + (r - y))
             (9) Call: subst(r >= 0,r - y,r,_1397124) ?
             (10) Call: subst(r,r - y,r,_1397416) ?
             (10) Exit: subst(r,r - y,r,r - y)
             (11) Call: subst(0,r - y,r,_1397880) ?
             (11) Exit: subst(0,r - y,r,0)
             (9) Exit: subst(r >= 0,r - y,r,r - y >= 0)
             (1) Exit: subst(and(x = q * y + r,r >= 0),r - y,r,and(x = q * y + (r - y),r - y >= 0))
             (12) Call: subst(and(x = q * y + (r - y),r - y >= 0),q + 1,q,and(and(x = q * y + r,r >= 0),r >= y)) ?
             (13) Call: subst(x = q * y + (r - y),q + 1,q,and(x = q * y + r,r >= 0)) ?
             (13) Fail: subst(x = q * y + (r - y),q + 1,q,and(x = q * y + r,r >= 0)) ?
             (12) Fail: subst(and(x = q * y + (r - y),r - y >= 0),q + 1,q,and(and(x = q * y + r,r >= 0),r >= y)) ?
             (14) Call: subst(and(x = q * y + (r - y),r - y >= 0),q + 1,q,and(x = (q + 1) * y + (r - y),r - y >= 0)) ?
             (15) Call: subst(x = q * y + (r - y),q + 1,q,x = (q + 1) * y + (r - y)) ?
             (16) Call: subst(x,q + 1,q,x) ?
             (16) Exit: subst(x,q + 1,q,x)
             (17) Call: subst(q * y + (r - y),q + 1,q,(q + 1) * y + (r - y)) ?
             (18) Call: subst(q * y,q + 1,q,(q + 1) * y) ?
             (19) Call: subst(q,q + 1,q,q + 1) ?
             (19) Exit: subst(q,q + 1,q,q + 1)
             (20) Call: subst(y,q + 1,q,y) ?
             (20) Exit: subst(y,q + 1,q,y)
             (18) Exit: subst(q * y,q + 1,q,(q + 1) * y)
             (21) Call: subst(r - y,q + 1,q,r - y) ?
             (22) Call: subst(r,q + 1,q,r) ?
             (22) Exit: subst(r,q + 1,q,r)
             (23) Call: subst(y,q + 1,q,y) ?
             (23) Exit: subst(y,q + 1,q,y)
             (21) Exit: subst(r - y,q + 1,q,r - y)
             (17) Exit: subst(q * y + (r - y),q + 1,q,(q + 1) * y + (r - y))
             (15) Exit: subst(x = q * y + (r - y),q + 1,q,x = (q + 1) * y + (r - y))
             (24) Call: subst(r - y >= 0,q + 1,q,r - y >= 0) ?
             (25) Call: subst(r - y,q + 1,q,r - y) ?
             (26) Call: subst(r,q + 1,q,r) ?
             (26) Exit: subst(r,q + 1,q,r)
             (27) Call: subst(y,q + 1,q,y) ?
             (27) Exit: subst(y,q + 1,q,y)
             (25) Exit: subst(r - y,q + 1,q,r - y)
             (28) Call: subst(0,q + 1,q,0) ?
             (28) Exit: subst(0,q + 1,q,0)
             (24) Exit: subst(r - y >= 0,q + 1,q,r - y >= 0)
             (14) Exit: subst(and(x = q * y + (r - y),r - y >= 0),q + 1,q,and(x = (q + 1) * y + (r - y),r - y >= 0))
             (29) Call: subst(and(x = q * y + r,r >= 0),x,r,_1406356) ?
             (30) Call: subst(x = q * y + r,x,r,_1406648) ?
             (31) Call: subst(x,x,r,_1406940) ?
             (31) Exit: subst(x,x,r,x)
             (32) Call: subst(q * y + r,x,r,_1407432) ?
             (33) Call: subst(q * y,x,r,_1407724) ?
             (34) Call: subst(q,x,r,_1408016) ?
             (34) Exit: subst(q,x,r,q)
             (35) Call: subst(y,x,r,_1408508) ?
             (35) Exit: subst(y,x,r,y)
             (33) Exit: subst(q * y,x,r,q * y)
             (36) Call: subst(r,x,r,_1409224) ?
             (36) Exit: subst(r,x,r,x)
             (32) Exit: subst(q * y + r,x,r,q * y + x)
             (30) Exit: subst(x = q * y + r,x,r,x = q * y + x)
             (37) Call: subst(r >= 0,x,r,_1410136) ?
             (38) Call: subst(r,x,r,_1410428) ?
             (38) Exit: subst(r,x,r,x)
             (39) Call: subst(0,x,r,_1410892) ?
             (39) Exit: subst(0,x,r,0)
             (37) Exit: subst(r >= 0,x,r,x >= 0)
             (29) Exit: subst(and(x = q * y + r,r >= 0),x,r,and(x = q * y + x,x >= 0))
             (40) Call: subst(and(x = q * y + x,x >= 0),0,q,and(x >= 0,y > 0)) ?
             (41) Call: subst(x = q * y + x,0,q,x >= 0) ?
             (41) Fail: subst(x = q * y + x,0,q,x >= 0) ?
             (40) Fail: subst(and(x = q * y + x,x >= 0),0,q,and(x >= 0,y > 0)) ?
             (42) Call: subst(and(x = q * y + x,x >= 0),0,q,and(x = 0 * y + x,x >= 0)) ?
             (43) Call: subst(x = q * y + x,0,q,x = 0 * y + x) ?
             (44) Call: subst(x,0,q,x) ?
             (44) Exit: subst(x,0,q,x)
             (45) Call: subst(q * y + x,0,q,0 * y + x) ?
             (46) Call: subst(q * y,0,q,0 * y) ?
             (47) Call: subst(q,0,q,0) ?
             (47) Exit: subst(q,0,q,0)
             (48) Call: subst(y,0,q,y) ?
             (48) Exit: subst(y,0,q,y)
             (46) Exit: subst(q * y,0,q,0 * y)
             (49) Call: subst(x,0,q,x) ?
             (49) Exit: subst(x,0,q,x)
             (45) Exit: subst(q * y + x,0,q,0 * y + x)
             (43) Exit: subst(x = q * y + x,0,q,x = 0 * y + x)
             (50) Call: subst(x >= 0,0,q,x >= 0) ?
             (51) Call: subst(x,0,q,x) ?
             (51) Exit: subst(x,0,q,x)
             (52) Call: subst(0,0,q,0) ?
             (52) Exit: subst(0,0,q,0)
             (50) Exit: subst(x >= 0,0,q,x >= 0)
             (42) Exit: subst(and(x = q * y + x,x >= 0),0,q,and(x = 0 * y + x,x >= 0))

          P = and(x >= 0,y > 0)
          S = :(:(:=(q,0),:=(r,x)),while_loop(r >= y,:(:=(q,q + 1),:=(r,r - y))))
          Q = and(x = q * y + r,not r >= y)
          I = and(x = q * y + r,r >= 0)
          yes
          | ?- ^D
          Halt. Program terminated normally
          vestavia% ^D
          script done on Thu Oct 27 13:47:15 1994