"Cleans up" a proof by permuting weakenings downward as far as possible.
"Cleans up" a proof by permuting weakenings downward as far as possible.
Value parameters
proof
The LKProof to be transformed.
reductive
Whether the algorithm is allowed to discard "unnecessary" subproofs. True by default.
Attributes
Returns
A proof of the same end sequent (up to a permutation) in which all weakenings are performed as late as possible; and an SequentConnector relating the end sequents of the old and new proofs.