start updating bytecodeProof

prove ImplodeCode_correct
prove ExplodeCode_correct
update bytecodeProofTheory