original.name="Property_Valid_13"
======
>>> main.whiley
property sum(int n, int[] xs, int i) -> (bool r):
   return (i >= |xs| && n == 0) ||
          (i >= 0 && i < |xs| && sum(n-xs[i],xs,i+1))

function fsum(int[] xs, int s, int[] ys) -> (int r)
requires sum(s,xs,0) && sum(s,ys,0)
ensures r == 0:
    //
    return 0

function f() -> (int r):
    return 0

public export method test():
    int x = f()
    assert fsum([x,x],2*x,[x,x]) == 0
---