• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
      • Apt
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Prime-field-constraint-systems
      • Proof-checker-array
      • Soft
      • Rp-rewriter
      • Farray
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
        • Leftist-tree-sort
          • Ltree-to-list
          • How-many-ltree-sort
          • True-listp-ltree-sort
          • Orderedp-ltree-sort
        • Leftist-tree-fns
        • Leftist-tree-thms
        • How-many-lt
        • Ltree-sort
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Bigmem
      • Regex
      • ACL2-programming-language
      • Java
      • C
      • Jfkr
      • X86isa
      • Equational
      • Cryptography
      • Where-do-i-place-my-book
      • Json
      • Built-ins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Leftist-trees

Leftist-tree-sort

Functions and theorems about leftist tree-based heapsort.

There are three functions related to heapsort, the most important being ltree-sort, which works just like the other sorting functions in the books/sorting contribution, except it uses leftist trees to sort its input. There are a number of theorems provided that prove the heapsort algorithm correct.

------------------------------------------------------------ Functions and Constants ------------------------------------------------------------

Function/Constant Name Result (supporting function) Type ---------------------- ---- LTREE-TO-LIST list LTREE-SORT list HOW-MANY-LT natural

Subtopics

Ltree-to-list
Convert a leftist tree to a list
How-many-ltree-sort
Ltree-sort preserves how-many
True-listp-ltree-sort
Ltree-sort produces a true-listp
Orderedp-ltree-sort
Ltree-sort produces an ordered list