• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
        • Two-nats-measure
        • Impossible
        • Bytep
        • Nat-list-measure
        • Maybe-posp
        • Nibblep
        • Organize-symbols-by-pkg
        • Organize-symbols-by-name
        • Lnfix
        • Good-valuep
        • Streqv
        • Chareqv
        • Symbol-package-name-non-cl
        • Arith-equivs
        • Induction-schemes
          • Dec-dec-induct
          • Cdr-dec-induct
          • Cdr-cdr-induct
            • Dec-induct
            • Cdr-induct
          • Maybe-integerp
          • Char-fix
          • Pos-fix
          • Symbol-package-name-lst
          • Mbt$
          • Maybe-bitp
          • Good-pseudo-termp
          • Str-fix
          • Maybe-string-fix
          • Nonkeyword-listp
          • Lifix
          • Bfix
          • Std/basic/if*
          • Impliez
          • Tuplep
          • Std/basic/intern-in-package-of-symbol
          • Lbfix
          • Std/basic/symbol-name-lst
          • True
          • Std/basic/rfix
          • Std/basic/realfix
          • Std/basic/member-symbol-name
          • Std/basic/fix
          • False
          • Std/basic/nfix
          • Std/basic/ifix
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Induction-schemes

    Cdr-cdr-induct

    (cdr-cdr-induct x y) inducts by simultaneously cdr'ing x and y until we reach the end of either.

    Definitions and Theorems

    Function: cdr-cdr-induct

    (defun cdr-cdr-induct (x y)
      (if (or (atom x) (atom y))
          nil
        (cdr-cdr-induct (cdr x) (cdr y))))