some corrections and fixes
improved the control clock axioms
added the input entrance axioms, changed neg() to not()