Proof of `Callable reductions between the algorithmic problems` (6th statement)
groundedproofs/Lax350013Proofs/Certificates.lean · lax-350013
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The original upstream proof of the callable contract. Its uses of other exposed contracts go through concept statements.