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

Kruskal-Theorems-1.1.tar.gz
sha256=1298e558236c8f760cfd8e93720c2b12a0c7b1773ddf25412220b75f20c0347a

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-08-28 logpath:KruskalThmProp logpath:KruskalThmType

Published: 28 Aug 2024

Dev Dependencies

None

Conflicts

None