Homological Perturbation Theory [11, 13] is a well-known general method for computing homology, but its main algorithm, the Basic Perturbation Lemma, presents, in general, high com...
While implementing a proof for the Basic Perturbation Lemma (a central result in Homological Algebra) in the theorem prover Isabelle one faces problems such as the implementation o...