• 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
        • Leftist-tree-fns
        • Leftist-tree-thms
          • Leftist-tree-misc-thms
            • Member-insert-lt
            • Size-is-natp-lt
            • Rank-is-natp-lt
            • Ltn-equals-rank-lt
            • Lrt-equals-rank-lt
          • Leftist-tree-structure-thms
          • Leftist-tree-rank-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-tree-thms

Leftist-tree-misc-thms

Miscellaneous theorems

Includes proofs that the rank, length of right spine, and length of the shortest path to an empty node are all equal. We also prove that the rank and size of a tree are always natp, as this is helpful in a later theorem.

Subtopics

Member-insert-lt
Size-is-natp-lt
Rank-is-natp-lt
Ltn-equals-rank-lt
Lrt-equals-rank-lt