qualif Nat(v:int) : (0 <= v)
qualif N10(v:int) : (10 = v)
qualif N20(v:int) : (20 = v)
bind 0 x0 : {v: int | [$k0]}
bind 1 x1 : {v: int | [$k1]}
cut $k0
constraint:
env [ ]
lhs {v : int | [v = 10]}
rhs {v : int | [$k0]}
id 1 tag [0]
constraint:
env [ ]
lhs {v : int | [v = 20]}
rhs {v : int | [$k0]}
id 2 tag [0]
constraint:
env [ 0 ]
lhs {v : int | [v = x0 + 7]}
rhs {v : int | [$k1]}
id 3 tag [0]
constraint:
env [ 1 ]
lhs {v : int | [v = x1 + 9]}
rhs {v : int | [$k0]}
id 4 tag [0]
constraint:
env [ 1 ]
lhs {v : int | [v = x1]}
rhs {v : int | [0 <= v]}
id 5 tag [0]
wf:
env [ ]
reft {v: int | [$k0]}
wf:
env [ ]
reft {v: int | [$k1]}