x = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: if x < 0: #PREMISES FOR THEN-ARM: # (x < 0) """{ 1.OK x < 0 premise }""" #PREMISES FOR NEXT LINE: # (x < 0) x = 0 - x #PREMISES FOR ATTACHED PROOF, IF ANY: # (x == (0 - x_old)) # (x_old < 0) """{ 1.OK x == 0 - x_old premise 2.OK x_old < 0 premise 3.OK x > 0 algebra 1 2 }""" #PREMISES FOR NEXT LINE: # (x > 0) else: #PREMISES FOR ELSE-ARM: # not (x < 0) """{ 1.OK not(x < 0) premise 2.OK x >= 0 algebra 1 }""" #PREMISES FOR NEXT LINE: # (x >= 0) pass #PREMISES FOR NEXT LINE: # (x >= 0) """{ 1.OK x >= 0 premise }""" #PREMISES FOR NEXT LINE: # (x >= 0) #PREMISES FOR NEXT LINE: # ((x > 0) or (x >= 0)) # prove here that x >= 0 : """{ 1.OK (x > 0) or (x >= 0) premise 2.OK x >= 0 ore 1 }""" #PREMISES FOR NEXT LINE: # (x >= 0)