0{}n0 1{x1}n1 2{x2}n2 3{x1,x2}n3 ; 0(,,deposit?x1)1 1(,[x2:=x1],withdraw!x2)0 1(,[x2:=x1],deposit?x1)3 2(,,withdraw!x2)0 2(,,deposit?x1)3 3(,,withdraw!x2)1 ;; _A _G [ _A _G[{deposit?x[]}_true] ]