x = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: y = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: if x > y : #PREMISES FOR THEN-ARM: # (x > y) """{ 1.OK x > y premise }""" #PREMISES FOR NEXT LINE: # (x > y) max = x #PREMISES FOR ATTACHED PROOF, IF ANY: # (max == x) # (x > y) """{ 1.OK max == x premise 2.OK x > y premise 3.OK max >= x algebra 1 4.OK max >= y algebra 3 2 5.OK max >= x and max >= y andi 3 4 6.OK return 2 1 5 }""" #PREMISES FOR NEXT LINE: # (x > y) # (max == x) # ((max >= x) and (max >= y)) # andi means ``and introduction'' else : #PREMISES FOR ELSE-ARM: # not (x > y) max = y #PREMISES FOR ATTACHED PROOF, IF ANY: # (max == y) # not (x > y) """{ 1.OK not x > y premise 2.OK y >= x algebra 1 4.OK max == y premise 5.OK max >= x algebra 2 4 3.OK max >= x or (0 == 1) ori 5 6.OK max >= y algebra 4 7.OK max >= x and max >= y andi 5 6 8.OK return 2 4 7 }""" #PREMISES FOR NEXT LINE: # (y >= x) # (max == y) # ((max >= x) and (max >= y)) #PREMISES FOR NEXT LINE: # (((x > y) and (max == x)) or ((y >= x) and (max == y))) # ((max >= x) and (max >= y)) """{ 1.OK max >= x and max >= y premise 2.OK (((x > y) and (max == x)) or ((y >= x) and (max == y))) premise 3.OK max == x or max == y ore 2 4.OK (max == x or max == y) and (max >= x and max >= y) andi 3 1 }""" #PREMISES FOR NEXT LINE: # (((max == x) or (max == y)) and ((max >= x) and (max >= y)))