Research

Git repositories: Formalization of Combinatorics on Words in Isabelle/HOL; Axiomatic theory of hereditarily finite sets and its fragments

Archive of Formal Proofs entries: Axiomatic theory of hereditarily finite sets and its fragments; Power Operator for Lists; Binary codes that do not preserve primitivity; Intersection of two monoids generated by two element codes; Combinatorics on Words Basics; Graph Lemma; Lyndon words

Visualization of an algoritm for fixed points of morphisms and its its description