g = [0,0]
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (g == [0, 0])
#PREMISES FOR NEXT LINE: 
# (g == [0, 0])
def f() :
    """{ pre len(g) == 2  post g[0] == g_in[0] + 1 return ans }"""
    global g
    g_in = [ _v for _v in g ]
    #PREMISES FOR NEXT LINE: 
    # (len(g) == 2)
    # forall 0 <= _i < len(g), (g[_i] == g_in[_i])
    # (len(g) == len(g_in))
    g[0] = g[0] + 1
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (g[0] == (g_old[0] + 1))
    # (len(g_old) == 2)
    # forall 0 <= _i < len(g_old), (g_old[_i] == g_in[_i])
    # (len(g_old) == len(g_in))
    # (len(g) == len(g_old))
    # forall 0 <= _i < len(g), ((_i == 0) or (g_old[_i] == g[_i]))
    # forall (0 + 1) <= _i < len(g), (g[_i] == g_in[_i])
    """{ 1.OK g[0] == g_old[0] + 1    premise
         2.OK forall 0 <= _i < len(g_old), (g_old[_i] == g_in[_i])  premise
         6.OK g_old[0] == g_in[0]    foralle 0 2
         3.OK g[0] == g_in[0] + 1     subst 6 1
    }"""
    #PREMISES FOR NEXT LINE: 
    # (g[0] == (g_in[0] + 1))
    return ans
    #PREMISES FOR NEXT LINE: 
    # (g[0] == (g_in[0] + 1))
#PREMISES FOR NEXT LINE: 
# (g == [0, 0])

#x = f()