mem(A,_), mem(A,_) <=> fail prog(L,_,_,_), prog(L,_,_,_) <=> fail pc(_), pc(_) <=> fail prog(L,"add",B,A), mem(B,Y) \ mem(A,X), pc(L) <=> mem(A,X+Y), pc(L+1) prog(L,"sub",B,A), mem(B,Y) \ mem(A,X), pc(L) <=> mem(A,X-Y), pc(L+1) prog(L,"mult",B,A), mem(B,Y) \ mem(A,X), pc(L) <=> mem(A,X*Y), pc(L+1) prog(L,"div",B,A), mem(B,Y) \ mem(A,X), pc(L) <=> mem(A,X/Y), pc(L+1) prog(L,"move",B,A), mem(B,X) \ mem(A,_), pc(L) <=> mem(A,X), pc(L+1) prog(L,"i_mov",B,A), mem(B,C), mem(C,X) \ mem(A,_), pc(L) <=> mem(A,X), pc(L+1) prog(L,"mov_i",B,A), mem(B,X), mem(A,C) \ mem(C,_), pc(L) <=> mem(C,X), pc(L+1) prog(L,"const",B,A) \ mem(A,_), pc(L) <=> mem(A,B), pc(L+1) prog(L,"init",A,_), mem(A,B) \ pc(L) <=> mem(B,0), pc(L+1) prog(L,"jump",_,A) \ pc(L) <=> pc(A) prog(L,"cjmp",R,A), mem(R,X) \ pc(L) <=> X == 0 | pc(A) prog(L,"cjmp",R,_), mem(R,X) \ pc(L) <=> X != 0 | pc(L+1) prog(L,"halt",_,_) \ pc(L) <=> true pc(_) <=> fail