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.2.tar.gz
sha256=fcaae51f970d68be837dac59520d0aae0bbaba1d522d9e25466580c3f1c2646d

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: 24 Nov 2024

Dev Dependencies

None

Conflicts

None