Need help in TLAPM

pls help me to find mistake in this code for this problem

thanks in advance

pls help