#P1 = (think, lambda1).P1'; #P1' = (get1, g).P1''; #P1'' = (use, mu1).P1'''; #P1''' = (rel, r).P1; #P2 = (think, lambda2).P2'; #P2' = (get2, g).P2''; #P2'' = (use, mu2).P2'''; #P2''' = (rel, r).P2; #Mem1 = (get2, infty).Mem1'; #Mem1' = (use, infty).Mem1''; #Mem1'' = (rel, infty).Mem2; #Mem2 = (get1, infty).Mem2'; #Mem2' = (use, infty).Mem2''; #Mem2'' = (rel, infty).Mem1; ((P1 <> P2) Mem1)