claim G(c) = ForAll x in [0,1] Exists y in [0,1]: x*y + (1-x)*(1-y^2) >= c A specification of an algorithm: Write a program which takes an x as input and produces a y as output so that the above condition holds. G(1/2) winning strategy for verifier: f(x,y) = x*y + (1-x)*(1-y^2) if x>1-x : y=1. f(x,y)=x > 1/2 1-x>x : y=0. f(x,y)=1-x > 1/2 1-x=x : y=1. f(x,y)=1/2 formal debate: falsifier x=0.75 verifier y=1 0.75>0.5 verifier wins G(0.615) winning strategy for verifier: Choose y=x. Result: x^3-x+1 minimize x^3-x+1 local minimum at x=1/sqrt(3) = min{x^3-x+1}~~0.6151 at x~~0.57735 formal debate: falsifier x=0.58 verifier y=0.58 x^3-x+1 where x = 0.58 Result: 0.615112 > 0.615 G(0.616) formal debate 1: falsifier x=0.3 verifier y=0.3 Result 0.727 verifier wins formal debate 2: x=0.57735 y=0.57735 Result 0.6151 < g(0.616) verifier loses!!!!!!!!!!!!!!! Question: Is G(0.616) really true? What is the winning strategy? The winning strategy is an algorithm which maps an x to a y such that f(x,y)>=0.616 holds for all x in [0,1]. Homework: Find such an algorithm.