x = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: sum = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == 0) #PREMISES FOR NEXT LINE: # (sum == 0) i = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == 0) # (sum == 0) assert (sum == (x * i)) # UNABLE TO VERIFY """{ 1.?? sum == x * i algebra }""" #PREMISES FOR NEXT LINE: # (sum == (x * i)) sum = sum + x #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == (sum_old + x)) # (sum_old == (x * i)) """{ 1.OK sum == sum_old + x premise 2.OK sum_old == x * i premise 3.OK sum == (x*i) + x algebra 2 1 }""" #PREMISES FOR NEXT LINE: # (sum == ((x * i) + x)) i = i + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == (i_old + 1)) # (sum == ((x * i_old) + x)) assert (sum == (x * i)) # UNABLE TO VERIFY """{ 1.OK i == i_old + 1 premise 2.OK sum == (x * i_old) + x premise 3.?? sum == x * i algebra 2 1 # doesn't work! Try this: 4.OK sum == x * (i_old + 1) algebra 2 5.OK sum == x * i subst 1 4 }""" #PREMISES FOR NEXT LINE: # (sum == (x * i))