Typos and minor lemma clean-up (#2611)

* cleanup

* lemmas

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

@@ -38,8 +38,8 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's
     rule word2Bool( W ) => true  requires W =/=Int 0
 ```
 
--   `sgn` gives the twos-complement interperetation of the sign of a word.
--   `abs` gives the twos-complement interperetation of the magnitude of a word.
+-   `sgn` gives the twos-complement interpretation of the sign of a word.
+-   `abs` gives the twos-complement interpretation of the magnitude of a word.
 
 ```k
     syntax Int ::= sgn ( Int ) [symbol(sgn), function, total]
@@ -114,7 +114,7 @@ The helper `powmod` is a totalization of the operator `_^%Int__` (which comes wi
     rule [powmod.zero]:    powmod( _,  _, W2) => 0               requires W2  ==Int 0 [concrete]
 ```
 
-`/sWord` and `%sWord` give the signed interperetations of `/Word` and `%Word`.
+`/sWord` and `%sWord` give the signed interpretations of `/Word` and `%Word`.
 
 ```k
     syntax Int ::= Int "/sWord" Int [function]
@@ -144,7 +144,7 @@ The `<op>Word` comparisons similarly lift K operators to EVM ones:
     rule W0 ==Word W1 => bool2Word(W0 ==Int W1)
 ```
 
--   `s<Word` implements a less-than for `Word` (with signed interperetation).
+-   `s<Word` implements a less-than for `Word` (with signed interpretation).
 
 ```k
     syntax Int ::= Int "s<Word" Int [function, total]
@@ -333,8 +333,8 @@ A cons-list is used for the EVM wordstack.
 Bytes helper functions
 ----------------------
 
--   `#asWord` will interperet a stack of bytes as a single word (with MSB first).
--   `#asInteger` will interperet a stack of bytes as a single arbitrary-precision integer (with MSB first).
+-   `#asWord` will interpret a stack of bytes as a single word (with MSB first).
+-   `#asInteger` will interpret a stack of bytes as a single arbitrary-precision integer (with MSB first).
 -   `#asAccount` will interpret a stack of bytes as a single account id (with MSB first).
     Differs from `#asWord` only in that an empty stack represents the empty account, not account zero.
 -   `#asByteStack` will split a single word up into a `Bytes`.

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -463,7 +463,7 @@ Here we load the correct number of arguments from the `wordStack` based on the s
     rule <k> #exec [ SO:StackOp ] => #gas [ SO , SO WS ] ~> SO WS ... </k> <wordStack> WS </wordStack>
 ```
 
-The `CallOp` opcodes all interperet their second argument as an address.
+The `CallOp` opcodes all interpret their second argument as an address.
 
 ```k
     syntax InternalOp ::= CallSixOp Int Int     Int Int Int Int
@@ -2344,21 +2344,21 @@ EVM Program Representations
 
 EVM programs are represented algebraically in K, but programs can load and manipulate program data directly.
 The opcodes `CODECOPY` and `EXTCODECOPY` rely on the assembled form of the programs being present.
-The opcode `CREATE` relies on being able to interperet EVM data as a program.
+The opcode `CREATE` relies on being able to interpret EVM data as a program.
 
 This is a program representation dependence, which we might want to avoid.
 Perhaps the only program representation dependence we should have is the hash of the program; doing so achieves:
 
--   Program representation independence (different analysis tools on the language don't have to ensure they have a common representation of programs, just a common interperetation of the data-files holding programs).
--   Programming language independence (we wouldn't even have to commit to a particular language or interperetation of the data-file).
+-   Program representation independence (different analysis tools on the language don't have to ensure they have a common representation of programs, just a common interpretation of the data-files holding programs).
+-   Programming language independence (we wouldn't even have to commit to a particular language or interpretation of the data-file).
 -   Only depending on the hash allows us to know that we have *exactly* the correct data-file (program), and nothing more.
 
 Disassembler
 ------------
 
 After interpreting the strings representing programs as a `WordStack`, it should be changed into an `OpCodes` for use by the EVM semantics.
 
--   `#dasmOpCode` interperets a `Int` as an `OpCode`.
+-   `#dasmOpCode` interprets a `Int` as an `OpCode`.
 
 ```k
     syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [symbol(#dasmOpCode), function, memo, total]

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md

@@ -149,7 +149,7 @@ Here we provide some standard parser/unparser functions for that format.
 Parsing
 -------
 
-These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s.
+These parsers can interpret hex-encoded strings as `Int`s, `Bytes`s, and `Map`s.
 
 -   `#parseHexWord` interprets a string as a single hex-encoded `Word`.
 -   `#parseHexBytes` interprets a string as a hex-encoded stack of bytes.
@@ -207,7 +207,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s
 
 Unparsing
 ---------
--   `#padByte` ensures that the `String` interperetation of a `Int` is wide enough.
+-   `#padByte` ensures that the `String` interpretation of a `Int` is wide enough.
 
 ```k
     syntax String ::= #padByte ( String ) [symbol(#padByte), function]
@@ -396,7 +396,7 @@ Decoding
 --------
 
 -   `#rlpDecode` RLP decodes a single `Bytes` into a `JSON`.
--   `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpereting the input as the RLP encoding of a list.
+-   `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpreting the input as the RLP encoding of a list.
 
 ```k
     syntax JSON ::= #rlpDecode ( Bytes )               [symbol(#rlpDecode   ), function]