An Example of Separating Implication Suppose p holds for Rest Store:x:a,..· 3 of Heap:a:3,a+1:4,. 4 Heap Then (x3,4)-*p holds for Rest Store x:a,.. X一→ of Heap:.· Heap and x1,2 ((x3,4)-*p)holds for Rest Store:x:a,.. of Heap:a:1,a+1:2,.. Heap