init infinite
edits
edits
valid
add proof of first lemma