Consider this Python function r. #Pre-condition: m and n are natural numbers with n < 2**m. n-1 # Post-condition: return a tuple of m bits b with n= Em- b[i].2. def r(m, n): i=0 if m == 0: return () else: return (n % 2,) + r(m - 1, n // 2) Prove r is correct. Make sure to first express precisely which claim you are proving inductively. You may use Post(m, n) to conveniently refer to the post-condition.