Finish proving the validRanges and validRangesCmd predicates and adding them to all other soundness proofs