def succ(x) : """{ pre x > 0 post y > x and y > 0 return y }""" #PREMISES FOR NEXT LINE: # (x > 0) y = x + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (y == (x + 1)) # (x > 0) #PREMISES FOR NEXT LINE: # (y == (x + 1)) # (x > 0) return y #PREMISES FOR NEXT LINE: # ((y > x) and (y > 0)) #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) """{ 1.OK a > 1 premise 2.OK a > 0 algebra 1 }""" #PREMISES FOR NEXT LINE: # (a > 0) # (a > 1) b = succ(a) #PREMISES FOR ATTACHED PROOF, IF ANY: # ((b > a) and (b > 0)) # (a > 0) # (a > 1) """{ 1.OK b > a and b > 0 premise # from post_succ 2.OK b > a ande 1 }""" #PREMISES FOR NEXT LINE: # (b > a) # ((b > a) and (b > 0)) # (a > 0) # (a > 1)