arprove(A&B,E1,E3) <- arprove(A,E1,E2) & arprove(B,E2,E3). arprove(G,E1,E2) <- (G <= B) & arprove(B,E1,E2). arprove(true,E,E). arprove((V is Exp),E1,E1) <- eval(Exp,V,E1). arprove(assign(X,Exp),E1,E2) <- eval(Exp,Val,E1) & update(X,Val,E1,E2). arprove(X > Y,E1,E1) <- eval(X,XV,E1) & eval(Y,YV,E1) & XV > YV.