Ops reversestack:2 nthstack:3 nilstackU:0 xGetHeap:2 xHeapStackToMerge:2 xLockReleased:1 xMerging:0 ifXx:2 nthheap:2 preparenthheap:2 monitorenter:0 xGetLock:2 xReleaseLock:2 xMonitorExit:1 monitorexit:0 outstack:2 Nil:0 appendrev:2 xappend:2 subseq:2 appendstring:2 Cons:2 nth:2 resultchar:1 substring:2 Str:2 resultcons:1 resultstring:2 pp23:0 FactoList2:0 IOException:0 InterruptedException:0 Next:0 val:0 in:0 out:0 Field:3 factorial:0 List:0 printList:0 println:0 AccDefault:0 read:0 charAt:0 TChar:0 concat:0 length:0 Substring:0 TInt:0 AccPublic:0 local0:0 local1:0 local2:0 local3:0 pp1:0 pp2:0 pp3:0 pp4:0 pp5:0 pp6:0 pp7:0 pp8:0 pp9:0 pp10:0 pp11:0 pp12:0 pp13:0 pp14:0 pp15:0 pp16:0 pp17:0 pp18:0 pp19:0 pp20:0 pp21:0 pp22:0 object0:0 object1:2 object2:0 object4:0 object5:0 object6:0 object7:0 object8:0 object9:0 object10:0 nilstack1:0 nilstack2:0 nilstack3:0 nilstack4:0 nilstack5:0 nilstack6:0 nilstack7:0 nilstack8:0 nilstack9:0 nilstack10:0 nillocal:0 lock:2 String:0 StringBuilder:0 Object:0 System:0 Exception:0 InputStream:0 io:0 PrintStream:0 java:0 lang:0 Thread:0 NilName:0 ConsName:2 Class:1 main:0 OType:1 AType:1 ConsType:2 nilstack0:0 object3:2 nilthreadlist:0 niloutstack:0 IO:3 initialJavaState:1 nilinstack:0 instack:2 instackExample:0 xTakeLock:2 xMonitorEnter:1 run:0 classloc:1 start:0 ifEqint:3 xJoin:2 xLeaveJoin:0 join:0 NilType:0 void:0 Method:3 threadloc:2 nilcallstack:0 insnew:1 insgoto:1 returnVoid:0 insreturn:0 nop:0 dup:0 dup2:0 pop:0 pop2:0 swap:0 push:1 aConstNull:0 ifNull:1 ifNonNull:1 load:1 store:1 iInc:2 neg:0 add:0 sub:0 mult:0 valnull:0 ifACmpEq:1 xIfACmpEq:4 eqCl:2 ifACmpNe:1 xIfACmpNe:4 ifCmpNe:1 ifCmpEq:1 ifCmpLt:1 ifCmpGt:1 ifCmpLe:1 ifCmpGe:1 ifNe:1 ifEq:1 ifLt:1 ifGt:1 ifLe:1 ifGe:1 instanceOf:1 result:1 xInstanceOf:1 locals:4 invokeVirtual:2 xInvokeVirtual:6 invokeStatic:2 xInvokeStatic:2 invokeSpecial:2 pprotected:0 orn:2 xInvokeSpecialCC:6 xCall:2 lookupSp2:2 pp0:0 nilstack:0 wait:0 storedframe:4 callstack:2 xInvokeSpecial:4 name:2 getField:1 xGetField:2 resultGetField:1 getStatic:1 putStatic:1 xGetHeapStack:2 putField:1 stack0:3 stack1:3 stack2:3 xMergeHeapStack:2 resultstack:2 xPutField:3 stack3:3 stack4:3 stack5:3 stack6:3 stack7:3 stack8:3 stack9:3 next:1 frame:4 stack10:3 resultstackmerge:1 resultPutField:1 xframe:5 thread:3 threadlist:2 heap:2 heaps:11 state:4 subclass:2 valfalse:0 isInit:1 AccNative:0 stack:2 loc:2 typeInstance:3 localCall:3 rmArgs:3 valtrue:0 accessibleMC:2 lookup:2 lookupIV:2 lookupSp1:2 init:0 clinit:0 AccStatic:0 AccAbstract:0 lookupF:1 Vars l0 l1 l2 l3 f0 f1 f2 f3 h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 x tl m pc s l f ntl h k tc y z sm ds i o lk n o1 lk1 o2 lk2 tid oid c a hs b sz r w s0 sz2 sz1 c1 c2 tl0 c0 a0 a1 m1 pc1 s1 ll b0 b1 e sf spc sl ca cam cc ic rc fx v TRS S initialJavaState(x) -> IO(state(threadlist(thread(threadloc(loc(Class(ConsName(FactoList2,NilName)),0),0),frame(name( Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))))), NilType),void),Class(ConsName(FactoList2,NilName))),pp0,nilstack,locals(nillocal,nillocal,nillocal, nillocal)),nilcallstack),nilthreadlist),heaps(heap(1,stack0(object0,lock(0,0),nilstack0)),heap(0, nilstack1),heap(1,stack2(object2,lock(0,0),nilstack2)),heap(0,nilstack3),heap(0,nilstack4),heap(0, nilstack5),heap(1,stack6(object6,lock(0,0),nilstack6)),heap(0,nilstack7),heap(0,nilstack8),heap(0, nilstack9),heap(0,nilstack10)),heaps(object0,object1(valnull,0),object2,object3(loc(Class(ConsName( java,ConsName(io,ConsName(InputStream,NilName)))),0),loc(Class(ConsName(java,ConsName(io,ConsName( PrintStream,NilName)))),0)),object4,object5,object6,object7,object8,object9,object10),1),x,niloutstack) state(threadlist(thread(tl,frame(name(Method(init,NilType,void),Class(ConsName(java,ConsName(lang, ConsName(Object,NilName))))),pp0,nilstack,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)), ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc) state(threadlist(thread(tl,frame(name(Method(init,NilType,void),Class(ConsName(java,ConsName(lang, ConsName(Thread,NilName))))),pp0,nilstack,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)), ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc) threadlist(thread(tl,frame(m,pc,s,l),f),threadlist(y,z)) -> threadlist(y,threadlist(thread(tl,frame(m,pc,s,l),f),z)) threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valfalse,sm)),m,pc,s,l),f),threadlist(y,z)) -> threadlist(y,threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valfalse,sm)),m,pc,s,l),f),z)) threadlist(thread(tl,xframe(returnVoid,m,pc,s,l),nilcallstack),threadlist(y,z)) -> threadlist(y,threadlist(thread(tl,xframe(returnVoid,m,pc,s,l),nilcallstack),z)) classloc(loc(x,y)) -> x xframe(result(x),m,pc,s,l) -> frame(m,next(pc),stack(x,s),l) nthstack(0,ds,s) -> resultstack(reversestack(ds,nilstackU),s) xMergeHeapStack(stack0(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack0(o,lk,n)) xMergeHeapStack(stack0(o1,lk1,stack0(o2,lk2,s)),n) -> stack0(o1,lk1,xMergeHeapStack(stack0(o2,lk2,s),n)) stack0(o,lk,resultstackmerge(n)) -> resultstackmerge(stack0(o,lk,n)) reversestack(stack0(o,lk,n),s) -> reversestack(n,stack0(o,lk,s)) xMergeHeapStack(stack1(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack1(o,lk,n)) xMergeHeapStack(stack1(o1,lk1,stack1(o2,lk2,s)),n) -> stack1(o1,lk1,xMergeHeapStack(stack1(o2,lk2,s),n)) stack1(o,lk,resultstackmerge(n)) -> resultstackmerge(stack1(o,lk,n)) reversestack(stack1(o,lk,n),s) -> reversestack(n,stack1(o,lk,s)) xMergeHeapStack(stack2(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack2(o,lk,n)) xMergeHeapStack(stack2(o1,lk1,stack2(o2,lk2,s)),n) -> stack2(o1,lk1,xMergeHeapStack(stack2(o2,lk2,s),n)) stack2(o,lk,resultstackmerge(n)) -> resultstackmerge(stack2(o,lk,n)) reversestack(stack2(o,lk,n),s) -> reversestack(n,stack2(o,lk,s)) xMergeHeapStack(stack3(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack3(o,lk,n)) xMergeHeapStack(stack3(o1,lk1,stack3(o2,lk2,s)),n) -> stack3(o1,lk1,xMergeHeapStack(stack3(o2,lk2,s),n)) stack3(o,lk,resultstackmerge(n)) -> resultstackmerge(stack3(o,lk,n)) reversestack(stack3(o,lk,n),s) -> reversestack(n,stack3(o,lk,s)) xMergeHeapStack(stack4(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack4(o,lk,n)) xMergeHeapStack(stack4(o1,lk1,stack4(o2,lk2,s)),n) -> stack4(o1,lk1,xMergeHeapStack(stack4(o2,lk2,s),n)) stack4(o,lk,resultstackmerge(n)) -> resultstackmerge(stack4(o,lk,n)) reversestack(stack4(o,lk,n),s) -> reversestack(n,stack4(o,lk,s)) xMergeHeapStack(stack5(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack5(o,lk,n)) xMergeHeapStack(stack5(o1,lk1,stack5(o2,lk2,s)),n) -> stack5(o1,lk1,xMergeHeapStack(stack5(o2,lk2,s),n)) stack5(o,lk,resultstackmerge(n)) -> resultstackmerge(stack5(o,lk,n)) reversestack(stack5(o,lk,n),s) -> reversestack(n,stack5(o,lk,s)) xMergeHeapStack(stack6(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack6(o,lk,n)) xMergeHeapStack(stack6(o1,lk1,stack6(o2,lk2,s)),n) -> stack6(o1,lk1,xMergeHeapStack(stack6(o2,lk2,s),n)) stack6(o,lk,resultstackmerge(n)) -> resultstackmerge(stack6(o,lk,n)) reversestack(stack6(o,lk,n),s) -> reversestack(n,stack6(o,lk,s)) xMergeHeapStack(stack7(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack7(o,lk,n)) xMergeHeapStack(stack7(o1,lk1,stack7(o2,lk2,s)),n) -> stack7(o1,lk1,xMergeHeapStack(stack7(o2,lk2,s),n)) stack7(o,lk,resultstackmerge(n)) -> resultstackmerge(stack7(o,lk,n)) reversestack(stack7(o,lk,n),s) -> reversestack(n,stack7(o,lk,s)) xMergeHeapStack(stack8(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack8(o,lk,n)) xMergeHeapStack(stack8(o1,lk1,stack8(o2,lk2,s)),n) -> stack8(o1,lk1,xMergeHeapStack(stack8(o2,lk2,s),n)) stack8(o,lk,resultstackmerge(n)) -> resultstackmerge(stack8(o,lk,n)) reversestack(stack8(o,lk,n),s) -> reversestack(n,stack8(o,lk,s)) xMergeHeapStack(stack9(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack9(o,lk,n)) xMergeHeapStack(stack9(o1,lk1,stack9(o2,lk2,s)),n) -> stack9(o1,lk1,xMergeHeapStack(stack9(o2,lk2,s),n)) stack9(o,lk,resultstackmerge(n)) -> resultstackmerge(stack9(o,lk,n)) reversestack(stack9(o,lk,n),s) -> reversestack(n,stack9(o,lk,s)) xMergeHeapStack(stack10(o,lk,nilstackU),n) -> xMergeHeapStack(nilstackU,stack10(o,lk,n)) xMergeHeapStack(stack10(o1,lk1,stack10(o2,lk2,s)),n) -> stack10(o1,lk1,xMergeHeapStack(stack10(o2,lk2,s),n)) stack10(o,lk,resultstackmerge(n)) -> resultstackmerge(stack10(o,lk,n)) reversestack(stack10(o,lk,n),s) -> reversestack(n,stack10(o,lk,s)) reversestack(nilstackU,s) -> s nthheap(i,heap(n,s)) -> nthstack(i,nilstackU,s) xMergeHeapStack(nilstackU,s) -> resultstackmerge(s) xGetHeap(Class(ConsName(FactoList2,NilName)),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> h0 xGetHeapStack(loc(Class(ConsName(FactoList2,NilName)),i),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(FactoList2,NilName)),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8, h9,h10))) xGetLock(tid,resultstack(ds,stack0(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack0(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack0(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack0(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack0(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(heap(a,hs),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(heap(a, xMergeHeapStack(ds,stack0(o,lock(oid,+(c,1)),n))),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(heap(a, resultstackmerge(hs)),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(heap(a,hs),h1,h2,h3,h4,h5,h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(heap(a, resultstackmerge(hs)),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(heap(a,hs),h1,h2,h3,h4,h5,h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(List,NilName)),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> h1 xGetHeapStack(loc(Class(ConsName(List,NilName)),i),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(List,NilName)),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9, h10))) xGetLock(tid,resultstack(ds,stack1(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack1(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack1(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack1(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack1(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,heap(a,hs),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,heap(a, xMergeHeapStack(ds,stack1(o,lock(oid,+(c,1)),n))),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,heap( a,resultstackmerge(hs)),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,heap(a,hs),h2,h3,h4,h5,h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,heap(a, resultstackmerge(hs)),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,heap(a,hs),h2,h3,h4,h5,h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),heaps(h0,h1,h2,h3,h4,h5, h6,h7,h8,h9,h10)) -> h2 xGetHeapStack(loc(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),i),heaps(h0,h1, h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),heaps( h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack2(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack2(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack2(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack2(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack2(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,heap(a,hs),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,heap(a, xMergeHeapStack(ds,stack2(o,lock(oid,+(c,1)),n))),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1, heap(a,resultstackmerge(hs)),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,heap(a,hs),h3,h4,h5,h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1, heap(a,resultstackmerge(hs)),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,heap(a,hs),h3,h4,h5,h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),heaps(h0,h1,h2,h3,h4,h5,h6, h7,h8,h9,h10)) -> h3 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),i),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),heaps(h0, h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack3(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack3(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack3(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack3(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack3(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,heap(a,hs),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,heap( a,xMergeHeapStack(ds,stack3(o,lock(oid,+(c,1)),n))),h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, heap(a,resultstackmerge(hs)),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,heap(a,hs),h4,h5,h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, heap(a,resultstackmerge(hs)),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,heap(a,hs),h4,h5,h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),heaps(h0,h1,h2,h3,h4,h5,h6, h7,h8,h9,h10)) -> h4 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),i),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),heaps(h0, h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack4(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack4(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack4(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack4(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack4(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,hs),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3, heap(a,xMergeHeapStack(ds,stack4(o,lock(oid,+(c,1)),n))),h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,heap(a,resultstackmerge(hs)),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,hs),h5,h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,heap(a,resultstackmerge(hs)),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,hs),h5,h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),heaps(h0,h1,h2,h3,h4,h5, h6,h7,h8,h9,h10)) -> h5 xGetHeapStack(loc(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),i),heaps(h0,h1, h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),heaps( h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack5(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack5(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack5(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack5(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack5(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,hs),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, heap(a,xMergeHeapStack(ds,stack5(o,lock(oid,+(c,1)),n))),h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,heap(a,resultstackmerge(hs)),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,hs),h6,h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,heap(a,resultstackmerge(hs)),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,hs),h6,h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),heaps(h0,h1,h2,h3,h4,h5, h6,h7,h8,h9,h10)) -> h6 xGetHeapStack(loc(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),i),heaps(h0,h1, h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),heaps( h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack6(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack6(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack6(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack6(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack6(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,hs),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,heap(a,xMergeHeapStack(ds,stack6(o,lock(oid,+(c,1)),n))),h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,heap(a,resultstackmerge(hs)),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,hs),h7, h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,heap(a,resultstackmerge(hs)),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,hs),h7, h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),heaps(h0,h1,h2,h3,h4,h5,h6, h7,h8,h9,h10)) -> h7 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),i),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),heaps(h0, h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack7(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack7(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack7(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack7(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack7(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,hs),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,heap(a,xMergeHeapStack(ds,stack7(o,lock(oid,+(c,1)),n))),h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,heap(a,resultstackmerge(hs)),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,hs), h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,heap(a,resultstackmerge(hs)),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,hs), h8,h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),heaps(h0,h1,h2,h3,h4, h5,h6,h7,h8,h9,h10)) -> h8 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),i),heaps(h0, h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))), heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack8(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack8(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack8(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack8(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack8(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a,hs),h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,heap(a,xMergeHeapStack(ds,stack8(o,lock(oid,+(c,1)),n))),h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,heap(a,resultstackmerge(hs)),h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a, hs),h9,h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,heap(a,resultstackmerge(hs)),h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a, hs),h9,h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),heaps(h0,h1,h2,h3,h4,h5,h6, h7,h8,h9,h10)) -> h9 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),i),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),heaps(h0, h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack9(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack9(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack9(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack9(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack9(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a,hs),h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,h8,heap(a,xMergeHeapStack(ds,stack9(o,lock(oid,+(c,1)),n))),h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,heap(a,resultstackmerge(hs)),h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a, hs),h10),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,heap(a,resultstackmerge(hs)),h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a, hs),h10),k,tc) xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,h10)) -> h10 xGetHeapStack(loc(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),i), heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10)) -> preparenthheap(i,xGetHeap(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException, NilName)))),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,h10))) xGetLock(tid,resultstack(ds,stack10(o,lock(oid,0),n))) -> xTakeLock(valtrue,xHeapStackToMerge(ds,stack10(o,lock(tid,0),n))) xReleaseLock(tid,resultstack(ds,stack10(o,lock(oid,c),n))) -> xLockReleased(xHeapStackToMerge(ds,stack10(o,lock(oid,c),n))) state(threadlist(thread(tl,xframe(xMonitorEnter(xTakeLock(valtrue,xHeapStackToMerge(ds,stack10(o, lock(oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,heap(a,hs)),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,h8,h9,heap(a,xMergeHeapStack(ds,stack10(o,lock(oid,+(c,1)),n)))),k,tc) state(threadlist(thread(tl,xframe(xMonitorEnter(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,heap(a,resultstackmerge(hs))),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9, heap(a,hs)),k,tc) state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,stack(x,s),l),f),ntl),heaps(h0,h1,h2, h3,h4,h5,h6,h7,h8,h9,heap(a,resultstackmerge(hs))),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9, heap(a,hs)),k,tc) xTakeLock(ifXx(b,x),s) -> xTakeLock(b,s) preparenthheap(result(i),h) -> nthheap(i,h) state(threadlist(thread(threadloc(r,tid),xframe(monitorenter,m,pc,stack(x,s),l),f),ntl),h,k,tc) -> state(threadlist(thread(threadloc(r,tid),xframe(xMonitorEnter(xGetLock(tid,xGetHeapStack(x,h))), m,pc,stack(x,s),l),f),ntl),h,k,tc) state(threadlist(thread(threadloc(r,tid),xframe(xMonitorEnter(xTakeLock(valfalse,w)),m,pc,stack(x, s),l),f),ntl),h,k,tc) -> state(threadlist(thread(threadloc(r,tid),xframe(xMonitorEnter(xGetLock(tid,xGetHeapStack(x,h))), m,pc,stack(x,s),l),f),ntl),h,k,tc) state(threadlist(thread(threadloc(r,tid),xframe(monitorexit,m,pc,stack(x,s),l),f),ntl),h,k,tc) -> state(threadlist(thread(threadloc(r,tid),xframe(xMonitorExit(xReleaseLock(tid,xGetHeapStack(x, h))),m,pc,stack(x,s),l),f),ntl),h,k,tc) IO(state(threadlist(thread(tl,frame(name(Method(read,NilType,TInt),Class(ConsName(java,ConsName(io, ConsName(InputStream,NilName))))),pp0,s0,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)),ntl), h,k,tc),instack(x,a),b) -> IO(state(threadlist(thread(tl,frame(m,next(pc),stack(x,s),l),f),ntl),h,k,tc),a,b) IO(state(threadlist(thread(tl,frame(name(Method(println,ConsType(TInt,NilType),void),Class(ConsName( java,ConsName(io,ConsName(PrintStream,NilName))))),pp0,s0,locals(l0,l1,l2,l3)),callstack(storedframe(m, pc,s,l),f)),ntl),h,k,tc),a,b) -> IO(state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc),a,outstack(l1,b)) IO(state(threadlist(thread(tl,frame(name(Method(println,ConsType(OType(Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))),NilType),void),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))),pp0,s0,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)),ntl),h,k,tc),a,b) -> IO(state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc),a,outstack(l1,b)) IO(state(threadlist(thread(tl,frame(name(Method(println,ConsType(TChar,NilType),void),Class( ConsName(java,ConsName(io,ConsName(PrintStream,NilName))))),pp0,s0,locals(l0,l1,l2,l3)),callstack( storedframe(m,pc,s,l),f)),ntl),h,k,tc),a,b) -> IO(state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc),a,outstack(l1,b)) nth(0,Cons(c,n)) -> resultchar(c) xappend(Nil,x) -> x xappend(Cons(x,y),z) -> appendrev(x,xappend(y,z)) appendrev(x,Cons(y,z)) -> Cons(x,Cons(y,z)) subseq(0,x) -> resultcons(x) appendstring(Str(sz1,c1),Str(sz2,c2)) -> resultstring(+(sz1,sz2),xappend(c1,c2)) substring(Str(sz,c1),i) -> resultstring(-(sz,i),subseq(i,c1)) state(threadlist(thread(tl,frame(name(Method(concat,ConsType(OType(Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))),NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),pp0,s0,locals(l0,l1,l2, l3)),callstack(storedframe(m,pc,s,l),f)),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(appendstring(l0,l1),m,pc,s,l),f),ntl),h,k,tc) state(threadlist(thread(tl,xframe(resultstring(result(sz),Cons(x,y)),m,pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(Str(sz,Cons(x,y)),s),l),f),ntl),h,k,tc) state(threadlist(thread(tl,frame(name(Method(charAt,ConsType(TInt,NilType),TChar),Class(ConsName( java,ConsName(lang,ConsName(String,NilName))))),pp0,s0,locals(Str(sz,x),l1,l2,l3)),callstack( storedframe(m,pc,s,l),f)),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(nth(l1,x),m,pc,s,l),f),ntl),h,k,tc) state(threadlist(thread(tl,xframe(resultchar(x),m,pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(x,s),l),f),ntl),h,k,tc) state(threadlist(thread(tl,frame(name(Method(length,NilType,TInt),Class(ConsName(java,ConsName(lang, ConsName(String,NilName))))),pp0,s0,locals(Str(sz,x),l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)), ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(sz,s),l),f),ntl),h,k,tc) state(threadlist(thread(tl,frame(name(Method(Substring,ConsType(TInt,NilType),OType(Class(ConsName( java,ConsName(lang,ConsName(String,NilName)))))),Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))),pp0,s0,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(substring(l0,l1),m,pc,s,l),f),ntl),h,k,tc) state(threadlist(thread(tl,xframe(resultstring(result(sz),resultcons(x)),m,pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(Str(sz,x),s),l),f),ntl),h,k,tc) state(threadlist(thread(tl,frame(name(Method(start,NilType,void),Class(ConsName(java,ConsName(lang, ConsName(Thread,NilName))))),pp0,nilstack,locals(l0,l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)), ntl),h,k,tc) -> state(threadlist(thread(threadloc(l0,tc),frame(name(Method(run,NilType,void),classloc(l0)),pp0, nilstack,locals(l0,l1,l2,l3)),nilcallstack),threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl)),h,k,+( tc,1)) state(threadlist(thread(tl0,frame(name(Method(join,NilType,void),Class(ConsName(java,ConsName(lang, ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2,l3)),callstack(storedframe(m,pc,s,l), f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid,m1,pc1,s1,ll),nilcallstack),ntl)),h, k,tc) -> state(threadlist(thread(tl0,xframe(xJoin(eqCl(c0,c1),ifEqint(wait,a0,a1)),name(Method(join, NilType,void),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc( c0,a0),l1,l2,l3)),callstack(storedframe(m,pc,s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid), xframe(returnVoid,m1,pc1,s1,ll),nilcallstack),ntl)),h,k,tc) state(threadlist(thread(tl0,xframe(xJoin(valfalse,ifEqint(wait,b0,b1)),name(Method(join,NilType, void),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1, l2,l3)),callstack(storedframe(m,pc,s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe( returnVoid,m1,pc1,s1,ll),nilcallstack),ntl)),h,k,tc) -> state(threadlist(thread(tl0,frame(name(Method(join,NilType,void),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2,l3)),callstack(storedframe(m,pc, s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid,m1,pc1,s1,ll),nilcallstack), ntl)),h,k,tc) state(threadlist(thread(tl0,xframe(xLeaveJoin,name(Method(join,NilType,void),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2,l3)),callstack( storedframe(m,pc,s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid,m1,pc1,s1,ll), nilcallstack),ntl)),h,k,tc) -> state(threadlist(thread(tl0,frame(m,next(pc),s,l),f),threadlist(thread(threadloc(loc(c1,a1),tid), xframe(returnVoid,m1,pc1,s1,ll),nilcallstack),ntl)),h,k,tc) frame(name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp0,s,l) -> xframe(load(local0),name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp0,s,l) frame(name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp1,s,l) -> xframe(invokeSpecial(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init, NilType,void)),name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp1,s,l) frame(name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp2,s,l) -> xframe(returnVoid,name(Method(init,NilType,void),Class(ConsName(FactoList2,NilName))),pp2,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp0,s, l) -> xframe(push(1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp0,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp1,s, l) -> xframe(store(local1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName( FactoList2,NilName))),pp1,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp2,s, l) -> xframe(push(2),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp2,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp3,s, l) -> xframe(store(local2),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName( FactoList2,NilName))),pp3,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp4,s, l) -> xframe(load(local2),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp4,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp5,s, l) -> xframe(load(local0),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp5,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp6,s, l) -> xframe(ifCmpGt(pp13),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName( FactoList2,NilName))),pp6,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp7,s, l) -> xframe(load(local1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp7,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp8,s, l) -> xframe(load(local2),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp8,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp9,s, l) -> xframe(mult,name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp9,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp10, s,l) -> xframe(store(local1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName( FactoList2,NilName))),pp10,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp11, s,l) -> xframe(iInc(local2,1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName( FactoList2,NilName))),pp11,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp12, s,l) -> xframe(insgoto(pp4),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp12,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp13, s,l) -> xframe(load(local1),name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp13,s,l) frame(name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2,NilName))),pp14, s,l) -> xframe(insreturn,name(Method(factorial,ConsType(TInt,NilType),TInt),Class(ConsName(FactoList2, NilName))),pp14,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp0,s,l) -> xframe(aConstNull,name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp0,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp1,s,l) -> xframe(store(local1),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp1,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp2,s,l) -> xframe(push(0),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName( String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp2,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp3,s,l) -> xframe(store(local2),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp3,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp4,s,l) -> xframe(load(local2),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp4,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp5,s,l) -> xframe(ifLt(pp21),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp5,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp6,s,l) -> xframe(getStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),in,OType( Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName))))))),name(Method(main,ConsType(AType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))))),NilType),void),Class(ConsName( FactoList2,NilName))),pp6,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp7,s,l) -> xframe(invokeVirtual(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method( read,NilType,TInt)),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName( String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp7,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp8,s,l) -> xframe(store(local2),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp8,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp9,s,l) -> xframe(insgoto(pp11),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp9,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp10,s,l) -> xframe(store(local3),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp10,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp11,s,l) -> xframe(load(local2),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp11,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp12,s,l) -> xframe(ifLt(pp4),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp12,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp13,s,l) -> xframe(insnew(Class(ConsName(List,NilName))),name(Method(main,ConsType(AType(OType(Class( ConsName(java,ConsName(lang,ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2, NilName))),pp13,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp14,s,l) -> xframe(dup,name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName( String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp14,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp15,s,l) -> xframe(load(local2),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp15,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp16,s,l) -> xframe(invokeStatic(Class(ConsName(FactoList2,NilName)),Method(factorial,ConsType(TInt,NilType), TInt)),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp16,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp17,s,l) -> xframe(load(local1),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp17,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp18,s,l) -> xframe(invokeSpecial(Class(ConsName(List,NilName)),Method(init,ConsType(TInt,ConsType(OType( Class(ConsName(List,NilName))),NilType)),void)),name(Method(main,ConsType(AType(OType(Class(ConsName( java,ConsName(lang,ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))), pp18,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp19,s,l) -> xframe(store(local1),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp19,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp20,s,l) -> xframe(insgoto(pp4),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp20,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp21,s,l) -> xframe(load(local1),name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp21,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp22,s,l) -> xframe(invokeVirtual(Class(ConsName(List,NilName)),Method(printList,NilType,void)),name(Method( main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))))),NilType), void),Class(ConsName(FactoList2,NilName))),pp22,s,l) frame(name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp23,s,l) -> xframe(returnVoid,name(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang, ConsName(String,NilName)))))),NilType),void),Class(ConsName(FactoList2,NilName))),pp23,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp0,s,l) -> xframe(load(local0),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp0,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp1,s,l) -> xframe(invokeSpecial(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init, NilType,void)),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)), void),Class(ConsName(List,NilName))),pp1,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp2,s,l) -> xframe(load(local0),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp2,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp3,s,l) -> xframe(load(local2),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp3,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp4,s,l) -> xframe(putField(Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName))))), name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void),Class( ConsName(List,NilName))),pp4,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp5,s,l) -> xframe(load(local0),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp5,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp6,s,l) -> xframe(load(local1),name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp6,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp7,s,l) -> xframe(putField(Field(Class(ConsName(List,NilName)),val,TInt)),name(Method(init,ConsType(TInt, ConsType(OType(Class(ConsName(List,NilName))),NilType)),void),Class(ConsName(List,NilName))),pp7,s,l) frame(name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void), Class(ConsName(List,NilName))),pp8,s,l) -> xframe(returnVoid,name(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))), NilType)),void),Class(ConsName(List,NilName))),pp8,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp0,s,l) -> xframe(load(local0),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp0,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp1,s,l) -> xframe(store(local1),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp1,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp2,s,l) -> xframe(load(local1),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp2,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp3,s,l) -> xframe(ifNull(pp12),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp3,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp4,s,l) -> xframe(getStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),out,OType( Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName))))))),name(Method(printList,NilType, void),Class(ConsName(List,NilName))),pp4,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp5,s,l) -> xframe(load(local1),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp5,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp6,s,l) -> xframe(getField(Field(Class(ConsName(List,NilName)),val,TInt)),name(Method(printList,NilType, void),Class(ConsName(List,NilName))),pp6,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp7,s,l) -> xframe(invokeVirtual(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method( println,ConsType(TInt,NilType),void)),name(Method(printList,NilType,void),Class(ConsName(List, NilName))),pp7,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp8,s,l) -> xframe(load(local1),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp8,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp9,s,l) -> xframe(getField(Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName))))), name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp9,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp10,s,l) -> xframe(store(local1),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp10,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp11,s,l) -> xframe(insgoto(pp2),name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp11,s,l) frame(name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp12,s,l) -> xframe(returnVoid,name(Method(printList,NilType,void),Class(ConsName(List,NilName))),pp12,s,l) next(pp0) -> pp1 next(pp1) -> pp2 next(pp2) -> pp3 next(pp3) -> pp4 next(pp4) -> pp5 next(pp5) -> pp6 next(pp6) -> pp7 next(pp7) -> pp8 next(pp8) -> pp9 next(pp9) -> pp10 next(pp10) -> pp11 next(pp11) -> pp12 next(pp12) -> pp13 next(pp13) -> pp14 next(pp14) -> pp15 next(pp15) -> pp16 next(pp16) -> pp17 next(pp17) -> pp18 next(pp18) -> pp19 next(pp19) -> pp20 next(pp20) -> pp21 next(pp21) -> pp22 next(pp22) -> pp23 state(threadlist(thread(tl,xframe(insnew(Class(ConsName(FactoList2,NilName))),m,pc,s,l),f),ntl), heaps(heap(a,h),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(FactoList2,NilName)),a),s), l),f),ntl),heaps(heap(+(a,1),stack0(object0,lock(0,0),h)),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(List,NilName))),m,pc,s,l),f),ntl),heaps(h0, heap(a,h),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(List,NilName)),a),s),l),f), ntl),heaps(h0,heap(+(a,1),stack1(object1(valnull,0),lock(0,0),h)),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,heap(a,h),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(io,ConsName( PrintStream,NilName)))),a),s),l),f),ntl),heaps(h0,h1,heap(+(a,1),stack2(object2,lock(0,0),h)),h3,h4,h5, h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName(System, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,heap(a,h),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( System,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,heap(+(a,1),stack3(object3(valnull,valnull),lock(0, 0),h)),h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName(Object, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,h),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( Object,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,heap(+(a,1),stack4(object4,lock(0,0),h)),h5,h6, h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(io,ConsName(IOException, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,h),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(io,ConsName( IOException,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(+(a,1),stack5(object5,lock(0,0),h)), h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(io,ConsName(InputStream, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,h),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(io,ConsName( InputStream,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(+(a,1),stack6(object6,lock(0,0), h)),h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,h),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( String,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(+(a,1),stack7(object7,lock(0,0), h)),h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a,h),h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( StringBuilder,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(+(a,1),stack8(object8, lock(0,0),h)),h9,h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName(Thread, NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a,h),h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( Thread,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(+(a,1),stack9(object9,lock(0, 0),h)),h10),k,tc) state(threadlist(thread(tl,xframe(insnew(Class(ConsName(java,ConsName(lang,ConsName( InterruptedException,NilName))))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,heap(a,h)),k, tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(loc(Class(ConsName(java,ConsName(lang,ConsName( InterruptedException,NilName)))),a),s),l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,heap(+(a,1), stack10(object10,lock(0,0),h))),k,tc) xframe(insgoto(x),m,pc,s,l) -> frame(m,x,s,l) state(threadlist(thread(tl,xframe(returnVoid,a,b,c,z),callstack(storedframe(m,pc,s,l),f)),ntl),h,k, tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,k,tc) state(threadlist(thread(tl,xframe(insreturn,a,b,stack(x,y),c),callstack(storedframe(m,pc,s,l),f)), ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(x,s),l),f),ntl),h,k,tc) xframe(nop,m,pc,s,l) -> frame(m,next(pc),s,l) xframe(dup,m,pc,stack(x,s),l) -> frame(m,next(pc),stack(x,stack(x,s)),l) xframe(dup2,m,pc,stack(x,stack(y,s)),l) -> frame(m,next(pc),stack(x,stack(y,stack(x,stack(y,s)))),l) xframe(pop,m,pc,stack(x,s),l) -> frame(m,next(pc),s,l) xframe(pop2,m,pc,stack(x,stack(y,s)),l) -> frame(m,next(pc),s,l) xframe(swap,m,pc,stack(x,stack(y,s)),l) -> frame(m,next(pc),stack(y,stack(x,s)),l) xframe(push(x),m,pc,s,l) -> frame(m,next(pc),stack(x,s),l) xframe(aConstNull,m,pc,s,l) -> frame(m,next(pc),stack(valnull,s),l) xframe(ifNull(x),m,pc,stack(loc(a,y),s),l) -> frame(m,next(pc),s,l) xframe(ifNull(x),m,pc,stack(valnull,s),l) -> frame(m,x,s,l) xframe(ifNonNull(x),m,pc,stack(loc(a,y),s),l) -> frame(m,x,s,l) xframe(ifNonNull(x),m,pc,stack(valnull,s),l) -> frame(m,next(pc),s,l) xframe(load(local0),m,pc,s,locals(l0,l1,l2,l3)) -> frame(m,next(pc),stack(l0,s),locals(l0,l1,l2,l3)) xframe(load(local1),m,pc,s,locals(l0,l1,l2,l3)) -> frame(m,next(pc),stack(l1,s),locals(l0,l1,l2,l3)) xframe(load(local2),m,pc,s,locals(l0,l1,l2,l3)) -> frame(m,next(pc),stack(l2,s),locals(l0,l1,l2,l3)) xframe(load(local3),m,pc,s,locals(l0,l1,l2,l3)) -> frame(m,next(pc),stack(l3,s),locals(l0,l1,l2,l3)) xframe(store(local0),m,pc,stack(x,s),locals(l0,l1,l2,l3)) -> frame(m,next(pc),s,locals(x,l1,l2,l3)) xframe(store(local1),m,pc,stack(x,s),locals(l0,l1,l2,l3)) -> frame(m,next(pc),s,locals(l0,x,l2,l3)) xframe(store(local2),m,pc,stack(x,s),locals(l0,l1,l2,l3)) -> frame(m,next(pc),s,locals(l0,l1,x,l3)) xframe(store(local3),m,pc,stack(x,s),locals(l0,l1,l2,l3)) -> frame(m,next(pc),s,locals(l0,l1,l2,x)) xframe(iInc(local0,x),m,pc,s,locals(l0,l1,l2,l3)) -> xframe(wait,m,pc,s,locals(+(l0,x),l1,l2,l3)) xframe(wait,m,pc,s,locals(x,l1,l2,l3)) -> frame(m,next(pc),s,locals(x,l1,l2,l3)) xframe(iInc(local1,x),m,pc,s,locals(l0,l1,l2,l3)) -> xframe(wait,m,pc,s,locals(l0,+(l1,x),l2,l3)) xframe(wait,m,pc,s,locals(l0,x,l2,l3)) -> frame(m,next(pc),s,locals(l0,x,l2,l3)) xframe(iInc(local2,x),m,pc,s,locals(l0,l1,l2,l3)) -> xframe(wait,m,pc,s,locals(l0,l1,+(l2,x),l3)) xframe(wait,m,pc,s,locals(l0,l1,x,l3)) -> frame(m,next(pc),s,locals(l0,l1,x,l3)) xframe(iInc(local3,x),m,pc,s,locals(l0,l1,l2,l3)) -> xframe(wait,m,pc,s,locals(l0,l1,l2,+(l3,x))) xframe(wait,m,pc,s,locals(l0,l1,l2,x)) -> frame(m,next(pc),s,locals(l0,l1,l2,x)) xframe(neg,m,pc,stack(a,s),l) -> xframe(result(-(0,a)),m,pc,s,l) xframe(add,m,pc,stack(b,stack(a,s)),l) -> xframe(result(+(a,b)),m,pc,s,l) xframe(sub,m,pc,stack(b,stack(a,s)),l) -> xframe(result(-(a,b)),m,pc,s,l) xframe(mult,m,pc,stack(b,stack(a,s)),l) -> xframe(result(*(a,b)),m,pc,s,l) eqCl(valnull,valnull) -> valtrue eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(FactoList2,NilName))) -> valtrue eqCl(Class(ConsName(FactoList2,NilName)),valnull) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(List,NilName))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(System, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Object, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(IOException, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(InputStream, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(StringBuilder, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Thread, NilName))))) -> valfalse eqCl(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName( InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(List,NilName))) -> valtrue eqCl(Class(ConsName(List,NilName)),valnull) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(FactoList2,NilName))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(IOException, NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(InputStream, NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(StringBuilder, NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(InterruptedException, NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(List, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(List,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName(io, ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName(io, ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName(io, ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(List,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName(io, ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName(io, ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName(io, ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(List, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(List, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(List,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName(io, ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName(io, ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName(io, ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(StringBuilder,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(List, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(List,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName(io, ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName(io, ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName(io, ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(InterruptedException,NilName))))) -> valtrue eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),valnull) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( FactoList2,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( List,NilName))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(System,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(Object,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(IOException,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(InputStream,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(String,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(StringBuilder,NilName))))) -> valfalse eqCl(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(Thread,NilName))))) -> valfalse xframe(ifACmpEq(x),m,pc,stack(loc(b,z),stack(loc(a,y),s)),l) -> xframe(xIfACmpEq(x,eqCl(a,b),y,z),m,pc,s,l) xframe(xIfACmpEq(x,valfalse,a,b),m,pc,s,l) -> frame(m,next(pc),s,l) xframe(ifACmpNe(x),m,pc,stack(loc(b,z),stack(loc(a,y),s)),l) -> xframe(xIfACmpNe(x,eqCl(a,b),y,z),m,pc,s,l) xframe(xIfACmpNe(x,valfalse,a,b),m,pc,s,l) -> frame(m,x,s,l) xframe(instanceOf(c),m,pc,stack(loc(x,y),s),l) -> xframe(xInstanceOf(subclass(x,c)),m,pc,s,l) xInstanceOf(valtrue) -> result(1) xInstanceOf(valfalse) -> result(0) state(threadlist(thread(tl,xframe(xCall(locals(l0,l1,l2,l3),nilstack),m,pc,s,wait),callstack( storedframe(sf,spc,wait,sl),f)),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,pc,s,locals(l0,l1,l2,l3)),callstack(storedframe(sf,spc, nilstack,sl),f)),ntl),h,k,tc) state(threadlist(thread(tl,xframe(xCall(locals(l0,l1,l2,l3),stack(a,b)),m,pc,s,wait),callstack( storedframe(sf,spc,wait,sl),f)),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,pc,s,locals(l0,l1,l2,l3)),callstack(storedframe(sf,spc,stack( a,b),sl),f)),ntl),h,k,tc) state(threadlist(thread(tl,xframe(invokeVirtual(ca,cam),name(m,cc),pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xInvokeVirtual(accessibleMC(name(ca,lookup(ca,cam)),cc), subclass(typeInstance(lookup(ca,cam),cam,s),ca),typeInstance(lookup(ca,cam),cam,s),cc,cam,lookupIV( typeInstance(lookup(ca,cam),cam,s),cam)),name(m,cc),pc,s,l),f),ntl),h,k,tc) xInvokeVirtual(pprotected,valtrue,ic,cc,cam,rc) -> xInvokeVirtual(subclass(ic,cc),valtrue,ic,cc,cam,rc) state(threadlist(thread(tl,xframe(xInvokeVirtual(valtrue,valtrue,ic,x,cam,rc),name(m,cc),pc,s,l),f), ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xCall(localCall(s,rc,cam),rmArgs(s,rc,cam)),name(cam,rc),pp0, nilstack,wait),callstack(storedframe(name(m,cc),pc,wait,l),f)),ntl),h,k,tc) state(threadlist(thread(tl,xframe(invokeStatic(ca,cam),name(m,cc),pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xInvokeStatic(lookup(ca,cam),cam),name(m,cc),pc,s,l),f),ntl),h, k,tc) state(threadlist(thread(tl,xframe(xInvokeStatic(rc,cam),name(m,cc),pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xCall(localCall(s,rc,cam),rmArgs(s,rc,cam)),name(cam,rc),pp0, nilstack,wait),callstack(storedframe(name(m,cc),pc,wait,l),f)),ntl),h,k,tc) orn(valtrue,valtrue) -> valtrue orn(valtrue,valfalse) -> valtrue orn(valfalse,valtrue) -> valfalse orn(valfalse,valfalse) -> valtrue state(threadlist(thread(tl,xframe(invokeSpecial(ca,cam),name(m,cc),pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xInvokeSpecialCC(accessibleMC(name(ca,lookup(ca,cam)),cc), subclass(typeInstance(lookup(ca,cam),cam,s),ca),cc,ca,cam,typeInstance(lookup(ca,cam),cam,s)),name(m, cc),pc,s,l),f),ntl),h,k,tc) xInvokeSpecialCC(pprotected,valtrue,cc,ca,cam,ic) -> xInvokeSpecialCC(subclass(ic,cc),valtrue,cc,ca,cam,ic) xInvokeSpecialCC(valtrue,valtrue,cc,ca,cam,ic) -> xInvokeSpecial(orn(isInit(cam),subclass(cc,lookup(ca,cam))),ca,cam,ic) state(threadlist(thread(tl,xframe(xInvokeSpecial(valtrue,ca,cam,ic),name(m,cc),pc,s,l),f),ntl),h,k, tc) -> state(threadlist(thread(tl,xframe(xCall(localCall(s,lookupSp1(ca,cam),cam),rmArgs(s,lookupSp1(ca, cam),cam)),name(cam,lookupSp1(ca,cam)),pp0,nilstack,wait),callstack(storedframe(name(m,cc),pc,wait,l), f)),ntl),h,k,tc) state(threadlist(thread(tl,xframe(xInvokeSpecial(valfalse,ca,cam,ic),name(m,cc),pc,s,l),f),ntl),h,k, tc) -> state(threadlist(thread(tl,xframe(xCall(localCall(s,lookupSp2(ic,cam),cam),rmArgs(s,lookupSp2(ic, cam),cam)),name(cam,lookupSp2(ic,cam)),pp0,nilstack,wait),callstack(storedframe(name(m,cc),pc,wait,l), f)),ntl),h,k,tc) state(threadlist(thread(tl,xframe(getField(fx),m,pc,stack(x,s),l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xGetField(lookupF(fx),xGetHeapStack(x,h)),m,pc,s,l),f),ntl),h, k,tc) xGetField(Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName)))), resultstack(ds,stack1(object1(f0,f1),lk,s))) -> resultGetField(f0) xGetField(Field(Class(ConsName(List,NilName)),val,TInt),resultstack(ds,stack1(object1(f0,f1),lk, s))) -> resultGetField(f1) xGetField(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),in,OType(Class( ConsName(java,ConsName(io,ConsName(InputStream,NilName)))))),resultstack(ds,stack3(object3(f2,f3),lk, s))) -> resultGetField(f2) xGetField(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),out,OType(Class( ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))))),resultstack(ds,stack3(object3(f2,f3),lk, s))) -> resultGetField(f3) state(threadlist(thread(tl,xframe(resultGetField(x),m,pc,s,l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(x,s),l),f),ntl),h,k,tc) state(threadlist(thread(tl,xframe(getStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System, NilName)))),in,OType(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName))))))),m,pc,s,l),f), ntl),h,heaps(h0,h1,h2,object3(f2,f3),h4,h5,h6,h7,h8,h9,h10),tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(f2,s),l),f),ntl),h,heaps(h0,h1,h2,object3(f2, f3),h4,h5,h6,h7,h8,h9,h10),tc) state(threadlist(thread(tl,xframe(getStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System, NilName)))),out,OType(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName))))))),m,pc,s,l),f), ntl),h,heaps(h0,h1,h2,object3(f2,f3),h4,h5,h6,h7,h8,h9,h10),tc) -> state(threadlist(thread(tl,frame(m,next(pc),stack(f3,s),l),f),ntl),h,heaps(h0,h1,h2,object3(f2, f3),h4,h5,h6,h7,h8,h9,h10),tc) state(threadlist(thread(tl,xframe(putStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System, NilName)))),in,OType(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName))))))),m,pc,stack(x, s),l),f),ntl),h,heaps(h0,h1,h2,object3(f2,f3),h4,h5,h6,h7,h8,h9,h10),tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,heaps(h0,h1,h2,object3(x,f3),h4,h5,h6, h7,h8,h9,h10),tc) state(threadlist(thread(tl,xframe(putStatic(Field(Class(ConsName(java,ConsName(lang,ConsName(System, NilName)))),out,OType(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName))))))),m,pc,stack(x, s),l),f),ntl),h,heaps(h0,h1,h2,object3(f2,f3),h4,h5,h6,h7,h8,h9,h10),tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),h,heaps(h0,h1,h2,object3(f2,x),h4,h5,h6, h7,h8,h9,h10),tc) state(threadlist(thread(tl,xframe(putField(fx),m,pc,stack(v,stack(x,s)),l),f),ntl),h,k,tc) -> state(threadlist(thread(tl,xframe(xPutField(lookupF(fx),xGetHeapStack(x,h),v),m,pc,s,l),f),ntl), h,k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack0(o,lk,hs))),m,pc,s,l),f), ntl),heaps(heap(a,h),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(heap(a,stack0(o,lk,hs)),h1,h2,h3, h4,h5,h6,h7,h8,h9,h10),k,tc) xPutField(Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName)))), resultstack(ds,stack1(object1(f0,f1),lk,s)),v) -> resultPutField(xMergeHeapStack(ds,stack1(object1(v,f1),lk,s))) xPutField(Field(Class(ConsName(List,NilName)),val,TInt),resultstack(ds,stack1(object1(f0,f1),lk,s)), v) -> resultPutField(xMergeHeapStack(ds,stack1(object1(f0,v),lk,s))) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack1(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,heap(a,h),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,heap(a,stack1(o,lk,hs)),h2,h3, h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack2(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,heap(a,h),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,heap(a,stack2(o,lk,hs)),h3, h4,h5,h6,h7,h8,h9,h10),k,tc) xPutField(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),in,OType(Class( ConsName(java,ConsName(io,ConsName(InputStream,NilName)))))),resultstack(ds,stack3(object3(f2,f3),lk, s)),v) -> resultPutField(xMergeHeapStack(ds,stack3(object3(v,f3),lk,s))) xPutField(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),out,OType(Class( ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))))),resultstack(ds,stack3(object3(f2,f3),lk, s)),v) -> resultPutField(xMergeHeapStack(ds,stack3(object3(f2,v),lk,s))) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack3(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,heap(a,h),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,heap(a,stack3(o,lk,hs)), h4,h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack4(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,heap(a,h),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,stack4(o,lk, hs)),h5,h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack5(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,heap(a,h),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,stack5(o,lk, hs)),h6,h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack6(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,h),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,stack6(o, lk,hs)),h7,h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack7(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,h),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a, stack7(o,lk,hs)),h8,h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack8(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a,h),h9,h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a, stack8(o,lk,hs)),h9,h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack9(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a,h),h10),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a, stack9(o,lk,hs)),h10),k,tc) state(threadlist(thread(tl,xframe(resultPutField(resultstackmerge(stack10(o,lk,hs))),m,pc,s,l),f), ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,heap(a,h)),k,tc) -> state(threadlist(thread(tl,frame(m,next(pc),s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9, heap(a,stack10(o,lk,hs))),k,tc) subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(FactoList2,NilName))) -> valtrue subclass(Class(ConsName(List,NilName)),Class(ConsName(FactoList2,NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName( FactoList2,NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(FactoList2, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( FactoList2,NilName))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(List,NilName))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(List,NilName))) -> valtrue subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(List, NilName))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( List,NilName))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(PrintStream,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(PrintStream,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(System, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(System, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(System,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Object, NilName))))) -> valtrue subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Object, NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(Object,NilName))))) -> valtrue subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(IOException, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(IOException, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(io,ConsName(IOException,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(IOException,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(io,ConsName(InputStream, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(io,ConsName(InputStream, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(io,ConsName(InputStream,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(String,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName( StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(StringBuilder, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(StringBuilder,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(StringBuilder,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Thread, NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName(Thread, NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))) -> valtrue subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(Thread,NilName))))) -> valfalse subclass(Class(ConsName(FactoList2,NilName)),Class(ConsName(java,ConsName(lang,ConsName( InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(List,NilName)),Class(ConsName(java,ConsName(lang,ConsName( InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Class(ConsName(java, ConsName(lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Class(ConsName(java,ConsName( lang,ConsName(InterruptedException,NilName))))) -> valfalse subclass(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Class(ConsName( java,ConsName(lang,ConsName(InterruptedException,NilName))))) -> valtrue isInit(Method(init,NilType,void)) -> valtrue isInit(Method(factorial,ConsType(TInt,NilType),TInt)) -> valfalse isInit(Method(main,ConsType(AType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName)))))),NilType),void)) -> valfalse isInit(Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void)) -> valtrue isInit(Method(printList,NilType,void)) -> valfalse isInit(Method(println,ConsType(TInt,NilType),void)) -> valfalse isInit(Method(println,ConsType(TChar,NilType),void)) -> valfalse isInit(Method(println,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))), NilType),void)) -> valfalse isInit(Method(read,NilType,TInt)) -> valfalse isInit(Method(charAt,ConsType(TInt,NilType),TChar)) -> valfalse isInit(Method(concat,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))), NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> valfalse isInit(Method(length,NilType,TInt)) -> valfalse isInit(Method(Substring,ConsType(TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName( String,NilName))))))) -> valfalse isInit(Method(join,NilType,void)) -> valfalse isInit(Method(start,NilType,void)) -> valfalse typeInstance(Class(ConsName(FactoList2,NilName)),Method(init,NilType,void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(FactoList2,NilName)),Method(init,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(FactoList2,NilName)),Method(init,NilType,void)) -> s localCall(stack(l0,s),Class(ConsName(FactoList2,NilName)),Method(factorial,ConsType(TInt,NilType), TInt)) -> locals(l0,nillocal,nillocal,nillocal) rmArgs(stack(l0,s),Class(ConsName(FactoList2,NilName)),Method(factorial,ConsType(TInt,NilType), TInt)) -> s localCall(stack(l0,s),Class(ConsName(FactoList2,NilName)),Method(main,ConsType(AType(OType(Class( ConsName(java,ConsName(lang,ConsName(String,NilName)))))),NilType),void)) -> locals(l0,nillocal,nillocal,nillocal) rmArgs(stack(l0,s),Class(ConsName(FactoList2,NilName)),Method(main,ConsType(AType(OType(Class( ConsName(java,ConsName(lang,ConsName(String,NilName)))))),NilType),void)) -> s typeInstance(Class(ConsName(List,NilName)),Method(init,ConsType(TInt,ConsType(OType(Class(ConsName( List,NilName))),NilType)),void),stack(l2,stack(l1,stack(loc(ic,x),s)))) -> ic localCall(stack(l2,stack(l1,stack(loc(ic,x),s))),Class(ConsName(List,NilName)),Method(init,ConsType( TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void)) -> locals(loc(ic,x),l1,l2,nillocal) rmArgs(stack(l2,stack(l1,stack(loc(ic,x),s))),Class(ConsName(List,NilName)),Method(init,ConsType( TInt,ConsType(OType(Class(ConsName(List,NilName))),NilType)),void)) -> s typeInstance(Class(ConsName(List,NilName)),Method(printList,NilType,void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(List,NilName)),Method(printList,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(List,NilName)),Method(printList,NilType,void)) -> s typeInstance(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println, ConsType(TInt,NilType),void),stack(l1,stack(loc(ic,x),s))) -> ic localCall(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(TInt,NilType),void)) -> locals(loc(ic,x),l1,nillocal,nillocal) rmArgs(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(TInt,NilType),void)) -> s typeInstance(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println, ConsType(TChar,NilType),void),stack(l1,stack(loc(ic,x),s))) -> ic localCall(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(TChar,NilType),void)) -> locals(loc(ic,x),l1,nillocal,nillocal) rmArgs(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(TChar,NilType),void)) -> s typeInstance(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println, ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),void),stack(l1, stack(loc(ic,x),s))) -> ic localCall(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))),NilType),void)) -> locals(loc(ic,x),l1,nillocal,nillocal) rmArgs(stack(l1,stack(loc(ic,x),s)),Class(ConsName(java,ConsName(io,ConsName(PrintStream, NilName)))),Method(println,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))),NilType),void)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init,NilType, void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method( init,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init, NilType,void)) -> s typeInstance(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method(read,NilType, TInt),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))), Method(read,NilType,TInt)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method( read,NilType,TInt)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(charAt,ConsType( TInt,NilType),TChar),s) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) localCall(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))), Method(charAt,ConsType(TInt,NilType),TChar)) -> locals(l0,l1,nillocal,nillocal) rmArgs(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method( charAt,ConsType(TInt,NilType),TChar)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(concat,ConsType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),OType(Class(ConsName( java,ConsName(lang,ConsName(String,NilName)))))),s) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) localCall(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))), Method(concat,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType), OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> locals(l0,l1,nillocal,nillocal) rmArgs(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method( concat,ConsType(OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),OType( Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length,NilType, TInt),s) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) localCall(stack(l0,s),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length, NilType,TInt)) -> locals(l0,nillocal,nillocal,nillocal) rmArgs(stack(l0,s),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length, NilType,TInt)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(Substring, ConsType(TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))))),s) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) localCall(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))), Method(Substring,ConsType(TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))))) -> locals(l0,l1,nillocal,nillocal) rmArgs(stack(l1,stack(l0,s)),Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method( Substring,ConsType(TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String, NilName))))))) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(init,NilType, void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method( init,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(init, NilType,void)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(join,NilType, void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method( join,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(join, NilType,void)) -> s typeInstance(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(start,NilType, void),stack(loc(ic,x),s)) -> ic localCall(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method( start,NilType,void)) -> locals(loc(ic,x),nillocal,nillocal,nillocal) rmArgs(stack(loc(ic,x),s),Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method( start,NilType,void)) -> s accessibleMC(x,y) -> valtrue lookup(Class(ConsName(FactoList2,NilName)),Method(init,NilType,void)) -> Class(ConsName(FactoList2,NilName)) lookup(Class(ConsName(FactoList2,NilName)),Method(factorial,ConsType(TInt,NilType),TInt)) -> Class(ConsName(FactoList2,NilName)) lookup(Class(ConsName(FactoList2,NilName)),Method(main,ConsType(AType(OType(Class(ConsName(java, ConsName(lang,ConsName(String,NilName)))))),NilType),void)) -> Class(ConsName(FactoList2,NilName)) lookup(Class(ConsName(List,NilName)),Method(init,ConsType(TInt,ConsType(OType(Class(ConsName(List, NilName))),NilType)),void)) -> Class(ConsName(List,NilName)) lookup(Class(ConsName(List,NilName)),Method(printList,NilType,void)) -> Class(ConsName(List,NilName)) lookup(Class(ConsName(List,NilName)),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TInt,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TChar,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(IOException,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method(read,NilType,TInt)) -> Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))) lookup(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(charAt,ConsType(TInt, NilType),TChar)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(concat,ConsType(OType( Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),OType(Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length,NilType,TInt)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(Substring,ConsType(TInt, NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(StringBuilder,NilName)))),Method(init,NilType, void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(join,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(start,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookup(Class(ConsName(java,ConsName(lang,ConsName(InterruptedException,NilName)))),Method(init, NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookupIV(Class(ConsName(List,NilName)),Method(printList,NilType,void)) -> Class(ConsName(List,NilName)) lookupIV(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TInt,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupIV(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TChar,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupIV(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupIV(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method(read,NilType, TInt)) -> Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(charAt,ConsType(TInt, NilType),TChar)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(concat,ConsType(OType( Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),OType(Class(ConsName(java, ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length,NilType,TInt)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(Substring,ConsType( TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(join,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookupIV(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(start,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookupSp1(Class(ConsName(FactoList2,NilName)),Method(init,NilType,void)) -> Class(ConsName(FactoList2,NilName)) lookupSp1(Class(ConsName(List,NilName)),Method(init,ConsType(TInt,ConsType(OType(Class(ConsName( List,NilName))),NilType)),void)) -> Class(ConsName(List,NilName)) lookupSp1(Class(ConsName(List,NilName)),Method(printList,NilType,void)) -> Class(ConsName(List,NilName)) lookupSp1(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TInt,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupSp1(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( TChar,NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupSp1(Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))),Method(println,ConsType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),void)) -> Class(ConsName(java,ConsName(io,ConsName(PrintStream,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Object,NilName)))) lookupSp1(Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))),Method(read,NilType, TInt)) -> Class(ConsName(java,ConsName(io,ConsName(InputStream,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(charAt,ConsType(TInt, NilType),TChar)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(concat,ConsType( OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))),NilType),OType(Class(ConsName( java,ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(length,NilType, TInt)) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))),Method(Substring,ConsType( TInt,NilType),OType(Class(ConsName(java,ConsName(lang,ConsName(String,NilName))))))) -> Class(ConsName(java,ConsName(lang,ConsName(String,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(init,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(join,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookupSp1(Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))),Method(start,NilType,void)) -> Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName)))) lookupF(Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName))))) -> Field(Class(ConsName(List,NilName)),Next,OType(Class(ConsName(List,NilName)))) lookupF(Field(Class(ConsName(List,NilName)),val,TInt)) -> Field(Class(ConsName(List,NilName)),val,TInt) lookupF(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),in,OType(Class(ConsName( java,ConsName(io,ConsName(InputStream,NilName))))))) -> Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),in,OType(Class(ConsName(java, ConsName(io,ConsName(InputStream,NilName)))))) lookupF(Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),out,OType(Class( ConsName(java,ConsName(io,ConsName(PrintStream,NilName))))))) -> Field(Class(ConsName(java,ConsName(lang,ConsName(System,NilName)))),out,OType(Class(ConsName( java,ConsName(io,ConsName(PrintStream,NilName)))))) nthstack(i,s,stack0(o,lk,n)) -> nthstack(-(i,1),stack0(o,lk,s),n) if >(i,0) nthstack(i,s,stack1(o,lk,n)) -> nthstack(-(i,1),stack1(o,lk,s),n) if >(i,0) nthstack(i,s,stack2(o,lk,n)) -> nthstack(-(i,1),stack2(o,lk,s),n) if >(i,0) nthstack(i,s,stack3(o,lk,n)) -> nthstack(-(i,1),stack3(o,lk,s),n) if >(i,0) nthstack(i,s,stack4(o,lk,n)) -> nthstack(-(i,1),stack4(o,lk,s),n) if >(i,0) nthstack(i,s,stack5(o,lk,n)) -> nthstack(-(i,1),stack5(o,lk,s),n) if >(i,0) nthstack(i,s,stack6(o,lk,n)) -> nthstack(-(i,1),stack6(o,lk,s),n) if >(i,0) nthstack(i,s,stack7(o,lk,n)) -> nthstack(-(i,1),stack7(o,lk,s),n) if >(i,0) nthstack(i,s,stack8(o,lk,n)) -> nthstack(-(i,1),stack8(o,lk,s),n) if >(i,0) nthstack(i,s,stack9(o,lk,n)) -> nthstack(-(i,1),stack9(o,lk,s),n) if >(i,0) nthstack(i,s,stack10(o,lk,n)) -> nthstack(-(i,1),stack10(o,lk,s),n) if >(i,0) xGetLock(tid,resultstack(ds,stack0(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack0(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack0(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(heap(a,hs),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(heap(a, xMergeHeapStack(ds,stack0(o,lock(oid,-(c,1)),n))),h1,h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack1(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack1(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack1(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,heap(a,hs),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,heap(a, xMergeHeapStack(ds,stack1(o,lock(oid,-(c,1)),n))),h2,h3,h4,h5,h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack2(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack2(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack2(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,heap(a,hs),h3,h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,heap(a, xMergeHeapStack(ds,stack2(o,lock(oid,-(c,1)),n))),h3,h4,h5,h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack3(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack3(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack3(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,heap(a,hs),h4,h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,heap(a, xMergeHeapStack(ds,stack3(o,lock(oid,-(c,1)),n))),h4,h5,h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack4(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack4(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack4(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,heap(a,hs),h5,h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3, heap(a,xMergeHeapStack(ds,stack4(o,lock(oid,-(c,1)),n))),h5,h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack5(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack5(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack5(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,heap(a,hs),h6,h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, heap(a,xMergeHeapStack(ds,stack5(o,lock(oid,-(c,1)),n))),h6,h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack6(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack6(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack6(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,heap(a,hs),h7,h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,heap(a,xMergeHeapStack(ds,stack6(o,lock(oid,-(c,1)),n))),h7,h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack7(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack7(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack7(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,heap(a,hs),h8,h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,heap(a,xMergeHeapStack(ds,stack7(o,lock(oid,-(c,1)),n))),h8,h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack8(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack8(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack8(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,heap(a,hs),h9,h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,heap(a,xMergeHeapStack(ds,stack8(o,lock(oid,-(c,1)),n))),h9,h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack9(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack9(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack9(o,lock(oid, c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,heap(a,hs),h10),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,h8,heap(a,xMergeHeapStack(ds,stack9(o,lock(oid,-(c,1)),n))),h10),k,tc)if >(c,0) xGetLock(tid,resultstack(ds,stack10(o,lock(oid,c),n))) -> xTakeLock(ifEqint(wait,tid,oid),xHeapStackToMerge(ds,stack10(o,lock(oid,c),n)))if >(c,0) state(threadlist(thread(tl,xframe(xMonitorExit(xLockReleased(xHeapStackToMerge(ds,stack10(o,lock( oid,c),n)))),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4,h5,h6,h7,h8,h9,heap(a,hs)),k,tc) -> state(threadlist(thread(tl,xframe(xMonitorExit(xMerging),m,pc,s,l),f),ntl),heaps(h0,h1,h2,h3,h4, h5,h6,h7,h8,h9,heap(a,xMergeHeapStack(ds,stack10(o,lock(oid,-(c,1)),n)))),k,tc)if >(c,0) preparenthheap(i,heap(sz,s)) -> preparenthheap(result(-(-(sz,1),i)),heap(-(sz,1),s))if >(sz,0) /\ >(i,0) preparenthheap(0,heap(sz,s)) -> preparenthheap(result(-(sz,1)),heap(-(sz,1),s)) if >(sz,0) nth(i,Cons(c,n)) -> nth(-(i,1),n) if >(i,0) subseq(i,Cons(x,y)) -> subseq(-(i,1),y) if >(i,0) xJoin(valtrue,ifEqint(wait,a0,a1)) -> xLeaveJoin if =(a0,a1) state(threadlist(thread(tl0,xframe(xJoin(e,ifEqint(wait,b0,b1)),name(Method(join,NilType,void), Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2, l3)),callstack(storedframe(m,pc,s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid, m1,pc1,s1,ll),nilcallstack),ntl)),h,k,tc) -> state(threadlist(thread(tl0,frame(name(Method(join,NilType,void),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2,l3)),callstack(storedframe(m,pc, s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid,m1,pc1,s1,ll),nilcallstack), ntl)),h,k,tc)if >(b0,b1) state(threadlist(thread(tl0,xframe(xJoin(e,ifEqint(wait,b0,b1)),name(Method(join,NilType,void), Class(ConsName(java,ConsName(lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2, l3)),callstack(storedframe(m,pc,s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid, m1,pc1,s1,ll),nilcallstack),ntl)),h,k,tc) -> state(threadlist(thread(tl0,frame(name(Method(join,NilType,void),Class(ConsName(java,ConsName( lang,ConsName(Thread,NilName))))),pp0,nilstack,locals(loc(c0,a0),l1,l2,l3)),callstack(storedframe(m,pc, s,l),f)),threadlist(thread(threadloc(loc(c1,a1),tid),xframe(returnVoid,m1,pc1,s1,ll),nilcallstack), ntl)),h,k,tc)if <(b0,b1) xframe(xIfACmpEq(x,valtrue,a,b),m,pc,s,l) -> frame(m,x,s,l) if =(a,b) xframe(xIfACmpEq(x,valtrue,a,b),m,pc,s,l) -> frame(m,next(pc),s,l) if >(a,b) xframe(xIfACmpEq(x,valtrue,a,b),m,pc,s,l) -> frame(m,next(pc),s,l) if <(a,b) xframe(xIfACmpNe(x,valtrue,a,b),m,pc,s,l) -> frame(m,x,s,l) if >(a,b) xframe(xIfACmpNe(x,valtrue,a,b),m,pc,s,l) -> frame(m,x,s,l) if <(a,b) xframe(xIfACmpNe(x,valtrue,a,b),m,pc,s,l) -> frame(m,next(pc),s,l) if =(a,b) xframe(ifCmpNe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if >(a,b) xframe(ifCmpNe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if <(a,b) xframe(ifCmpNe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if =(a,b) xframe(ifCmpEq(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if =(a,b) xframe(ifCmpEq(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if >(a,b) xframe(ifCmpEq(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if <(a,b) xframe(ifCmpLt(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if <(a,b) xframe(ifCmpLt(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if >=(a,b) xframe(ifCmpGt(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if >(a,b) xframe(ifCmpGt(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if <=(a,b) xframe(ifCmpLe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if <=(a,b) xframe(ifCmpLe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if >(a,b) xframe(ifCmpGe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,x,s,l) if >=(a,b) xframe(ifCmpGe(x),m,pc,stack(b,stack(a,s)),l) -> frame(m,next(pc),s,l) if <(a,b) xframe(ifNe(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if >(a,0) xframe(ifNe(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if <(a,0) xframe(ifNe(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if =(a,0) xframe(ifEq(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if =(a,0) xframe(ifEq(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if >(a,0) xframe(ifEq(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if <(a,0) xframe(ifLt(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if <(a,0) xframe(ifLt(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if >=(a,0) xframe(ifGt(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if >(a,0) xframe(ifGt(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if <=(a,0) xframe(ifLe(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if <=(a,0) xframe(ifLe(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if >(a,0) xframe(ifGe(x),m,pc,stack(a,s),l) -> frame(m,x,s,l) if >=(a,0) xframe(ifGe(x),m,pc,stack(a,s),l) -> frame(m,next(pc),s,l) if <(a,0) instackExample -> instack(2,instack(-1,nilinstack)) Automaton Init States q0 q1 q2 q3 q4 q5 q6 Final States q0 Transitions initialJavaState(q3) -> q0 instack(q2,q3) -> q3 [-oo;+oo] -> q2 nilinstack -> q3 SubPatterns outstack([-oo;0],_) Equations Approx Rules outstack(l0,l1)=l1 stack1(_,_,_)= stack1(_,_,_) +(l0,1)=l0 *(l0,5)=l0