tweaked statement and definition

change statement to allow the clock to change, and change definition so
the case split on whether a call is clocked happens later.
started updating proof for new statement.