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()