Isabelle/Isar provides named cases to structure proofs. This article contains an implementation of a proof method casify, which can be used to easily extend proof tools with suppo...
This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides im...
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are...
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers...
In this work, we prove the lower bound ln(Hn)−ln(5 3 ) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series n p=1[p p...
Based on existing libraries for matrices, factorization of rational polynomials, and Sturm’s theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as ...