package coq-kruskal-theorems

  1. Overview
  2. No Docs
Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. D
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Maintainers

  1. D
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Sources

v1.0.tar.gz
sha256=22744c15e1066dcbba024e1d93f7158d09ab9892b77c8a851a0e27af90a31572

Description

This library formalizes the high-level variants of Higman's theorem (for trees of bounded arity) and Kruskal's theorem (for rose trees), depending on how these datatypes are implemented. Also, Vazsonyi's conjecture to illustrate the expressive power of Kruskal's and Higman's theorem.

Tags

category:Computer Science/Data Types and Data Structures date:2024-04-15 logpath:KruskalThmProp logpath:KruskalThmType

Published: 15 Apr 2024

Dependencies (2)

  1. coq-kruskal-veldman >= "1.0"
  2. coq-kruskal-almostfull >= "1.0"

Dev Dependencies

None

Conflicts

None