def succ(x) :
    """{ pre True
         post y > x
         return y
    }"""
    #PREMISES FOR NEXT LINE: 
    # True
    x = x - 1
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (x == (x_old - 1))
    # True
    #PREMISES FOR NEXT LINE: 
    y = x + 1
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (y == (x + 1))
    #PREMISES FOR NEXT LINE: 
    # (y == (x + 1))
    return y
    #PREMISES FOR NEXT LINE: 
    # (y > x)
# ERROR: sorry: cannot assign to input parameter x
#PREMISES FOR NEXT LINE: 


a = succ(2)
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (a > 2)
#PREMISES FOR NEXT LINE: 
# (a > 2)