Kruskal-Fan
by DmxLarchey
The Fan theorem for inductive bars and a constructive variant of König's lemma
AI summary
Proof framework
A Coq proof framework for Fan theorem and König's lemma
- stars
- 1
- forks
- 0
- watching
- 1
Similar projects
Found by comparing what the projects do, not just their names.
Kruskal proof library
A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts.
Tree embedding theorems
Provides theorem results for tree embeddings in inductive type theory
Almost Full relation library
A formalization of ground results about Almost Full relations in Coq 8.14+, including closure properties and Dickson's lemma.
Tree theorem proof
Provides a constructive account of Wim Veldman's proof of a variant of Kruskal's tree theorem for rose trees in Coq.
Data analysis tools
Tools for determining and working with finite data structures in a proof assistant.
Tree embedding library
An inductive proof of Higman's theorem for unary trees and lists, providing a constructive basis for Kruskal's theorem
Relation algebra library
A collection of lemmas and tactics about lists and binary relations for a proof assistant
Rose tree library
A Coq library formalizing rose trees for mathematical proof and theorem proving
Galois theorem formalizer
Formalization of mathematical theorems about solvability and Galois theory for polynomials
Proof automation library
A Coq library demonstrating design patterns for automated proof automation and canonical structures
Quasi morphism library
A Coq library providing tools and definitions for quasi-morphisms in the context of Almost Full relations
Symmetric functions library
An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions.
Relevance logic proof
Mechanization of a proof for the decidability of Implicational Relevance Logic
Tree function
A Coq implementation of Harvey Friedman's tree(n) function and its properties related to homeomorphic embedding.
Graph algorithm formalization
Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs.
