robot named Wall$-$E wanders around a two$-$dimensional grid. He starts out at $(0,0)$ and is allowed to take four different types of steps:$1.(+2,1)2.(1,+2)3.(+1,+1)4.(3,+0)$Thus$,$ for example, Wall$-$E might walk as follows. The types of his steps are listed above the arrows:$(0,0)1(2,1)3(3,0)2(2,2)4(1,2)$Wall$-$Es true love, the fashionable and high$-$powered robot, Eve, awaits at $(0,2)($A$)$ Let Wall$-$Es movements be modeled by a state machine M $=\{,$ S$,,$ s$0,$ F$\}.$ is the set of four actions defined above. Recall that : $($s$1,)$ s$2,$ where s$1,$ s$2$ S and $.$ And since well define success as Wall$-$E getting to Eve, well say that F $=\{(0,2)\}.$ Provide definitions for the state space S$,$ and the transition relation $,$ and s$0.($For $,$ you may have multiple cases.$)($B$)$ Sadly, you can see that Wall$-$E will never be able to reach Eve. But Wall$-$E doesnt believe it$.$ What preserved invariant could you use to prove to Wall$-$E that he can never reach Eve at $(0,2)?$ Hint: The value x y is not invariant, but how does it change?$($C$)$ Prove to Wall$-$E that he cannot reach Eve using your preserved invariant and Floyds invariant principle