def succ(x) : 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: #PREMISES FOR NEXT LINE: a = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: assert a > 1 #PREMISES FOR NEXT LINE: # (a > 1) b = succ(a) #PREMISES FOR ATTACHED PROOF, IF ANY: # True # (a > 1) #PREMISES FOR NEXT LINE: # (a > 1)