lim+, δ+, and Non-Permutability of β-Steps

Using a human-oriented formal example proof of the lim+-theorem (that the sum of limits is the limit of the sum), we exhibit a non-permutability of β-steps and δ+-steps (according to Smullyan’s classification), which is not visible with non-liberalized δ-rules and dissolves into a problem of mere inefficiency with further liberalized δ-rules, such as the δ++-rules. Beside a careful presentation of the human-oriented search for a formal proof of (lim+), our main intention is to show where sequent and tableau calculi are in conflict with human-oriented proof construction.