• # StanBij.mws

• Referenced in 10 articles [sw06645]
• combinatorial proof of a partition identity of Andrews and Stanley In his paper ... certain partition identity analytically and asks for a combinatorial proof. This paper provides the requested...
• # Tame Graphs

• Referenced in 16 articles [sw28578]
• Proofs. [CUP 2012]. The values of the constants in the definition of tameness are identical ... refers to the original version of Hales’ proof, the ITP 2011 paper by Nipkow refers...
• # BijTools

• Referenced in 3 articles [sw12643]
• finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
• # Examples

• Referenced in 3 articles [sw12644]
• finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
• # Fibonacci

• Referenced in 3 articles [sw12645]
• finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
• # TransMethodZeck

• Referenced in 3 articles [sw12646]
• finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
• # ZeckFibBijections

• Referenced in 3 articles [sw12647]
• finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
• # OrientedSwaps

• Referenced in 2 articles [sw35044]
• Knuth and Burge correspondences. A second probabilistic identity, relating those two vectors to a vector ... give a computer-assisted proof of this identity for n≤6 after first reformulating...
• # MJ

• Referenced in 12 articles [sw24342]
• which are sufficiently small to facilitate formal proofs of key properties. However many ... compact, MJ models features such as object identity, field assignment, constructor methods and block structure ... operational semantics of MJ, and give a proof of type safety. In order to demonstrate...
• # Regular_Algebras

• Referenced in 3 articles [sw32237]
• regular expressions as induced by regular language identity. We use Isabelle/HOL for a detailed systematic ... relationships between these classes, formalise a soundness proof for the smallest class (Salomaa ... provide a large collection of regular identities in the general setting of Boffa’s axiom ... algebra hierarchy in the Archive of Formal Proofs; we have not aimed at an integration...
• # SicoTHEO

• Referenced in 8 articles [sw09982]
• exploited by competition: on each processor, an identical copy of SETHEO tries to prove ... soon as one processor finds a proof, the entire system is stopped. Three different versions...