# t13
# C4B:    2|[0,x]| + |[0,y]|
# eocimp: 1/2·[x | x ≥ 0] + [x·y | x ≥ 0 ∧  y ≥ 0] + 1/2·[x^2 | x ≥ 0]

def startT13():
  var x, y

  while x > 0:
    tick 1
    x = x - 1
    nondet:
      y = y + 1
    else:
      while y > 0:
        tick 1
        y = y - 1