a) wp(a:a+1;b:=a/2, b≥0) == wp(a:=a+1wp(b:=a/2, b≥0)) == wp(a:=a+1, a/2 ≥ 0) == (a+1)/2 ≥ 0

b) wp(a:= A[i] +1;b := aa, b ≠ 2) == wp(a:= A[i] +1,wp(b := aa, b ≠ 2)) == wp(a:= A[i] +1, aa ≠ 2) == 0 ≤ i < |A| ^L (A[i]+1)(A[i]+1) ≠ 2 (se agrega def A[i]+1)

c) wp(a:= A[i] +1;a := bb, a ≥ 0) == wp(a:= A[i] +1wp(a := bb, a ≥ 0)) == wp(a:= A[i] +1,wp(bb ≥ 0)) == bb ≥ 0 (ya que no hay apariciones libres de a)

d)wp(a:=a-b;b:=a+b,a≥0 ^ b ≥ 0) == wp(a:=a-b,wp(b:=a+b,a≥0 ^ b ≥ 0)) == wp(a:=a-b,a≥0 ^ a+b≥0) == a-b ≥ 0 ^ a-b+b≥0 == a ≥ b ^ a ≥0