• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
        • Lambda
        • Pseudo-termp
          • Pseudo-term-fty
            • Pseudo-term-lambda
            • Pseudo-term-call
            • Pseudo-term-fncall
            • Pseudo-lambda
            • Pseudo-term-var
            • Pseudo-term-quote
            • Pseudo-term-kind
            • Pseudo-term-null
            • Pseudo-fnsym
            • Pseudo-term-case
            • Pseudo-term-count
            • Def-ev-pseudo-term-fty-support
            • Def-ev-pseudo-term-congruence
            • Pseudo-term-fix
            • Pseudo-var
            • Pseudo-term-list-fix
            • Pseudo-fn
              • Pseudo-fn-fix
              • Pseudo-fn-p
          • Std/typed-lists/pseudo-term-listp
        • Term-order
        • Pseudo-term-listp
        • Guard-holders
        • Termp
        • Termify
        • L<
        • Kwote
        • Kwote-lst
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Pseudo-fn

Pseudo-fn-fix

Signature

(pseudo-fn-fix x) → new-x

Arguments

x — Guard (pseudo-fn-p x).

Returns

new-x — Type (pseudo-fn-p new-x).

Definitions and Theorems

Function: pseudo-fn-fix

(defun pseudo-fn-fix (x)
  (declare (xargs :guard (pseudo-fn-p x)))
  (let ((__function__ 'pseudo-fn-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (consp x)
             (pseudo-lambda-fix x)
           (pseudo-fnsym-fix x))
         :exec x)))

Theorem: pseudo-fn-p-of-pseudo-fn-fix

(defthm pseudo-fn-p-of-pseudo-fn-fix
  (b* ((new-x (pseudo-fn-fix x)))
    (pseudo-fn-p new-x))
  :rule-classes :rewrite)

Theorem: pseudo-fn-fix-when-pseudo-fn-p

(defthm pseudo-fn-fix-when-pseudo-fn-p
  (implies (pseudo-fn-p x)
           (equal (pseudo-fn-fix x) x)))

Theorem: pseudo-fn-fix-when-consp

(defthm pseudo-fn-fix-when-consp
  (implies (consp x)
           (equal (pseudo-fn-fix x)
                  (pseudo-lambda-fix x))))

Theorem: pseudo-fn-fix-when-not-consp

(defthm pseudo-fn-fix-when-not-consp
  (implies (not (consp x))
           (equal (pseudo-fn-fix x)
                  (pseudo-fnsym-fix x))))

Function: pseudo-fn-equiv$inline

(defun pseudo-fn-equiv$inline (x y)
  (declare (xargs :guard (and (pseudo-fn-p x) (pseudo-fn-p y))))
  (equal (pseudo-fn-fix x)
         (pseudo-fn-fix y)))

Theorem: pseudo-fn-equiv-is-an-equivalence

(defthm pseudo-fn-equiv-is-an-equivalence
  (and (booleanp (pseudo-fn-equiv x y))
       (pseudo-fn-equiv x x)
       (implies (pseudo-fn-equiv x y)
                (pseudo-fn-equiv y x))
       (implies (and (pseudo-fn-equiv x y)
                     (pseudo-fn-equiv y z))
                (pseudo-fn-equiv x z)))
  :rule-classes (:equivalence))

Theorem: pseudo-fn-equiv-implies-equal-pseudo-fn-fix-1

(defthm pseudo-fn-equiv-implies-equal-pseudo-fn-fix-1
  (implies (pseudo-fn-equiv x x-equiv)
           (equal (pseudo-fn-fix x)
                  (pseudo-fn-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: pseudo-fn-fix-under-pseudo-fn-equiv

(defthm pseudo-fn-fix-under-pseudo-fn-equiv
  (pseudo-fn-equiv (pseudo-fn-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: pseudo-fn-fix-of-pseudo-fn-fix-x

(defthm pseudo-fn-fix-of-pseudo-fn-fix-x
  (equal (pseudo-fn-fix (pseudo-fn-fix x))
         (pseudo-fn-fix x)))

Theorem: pseudo-fn-fix-pseudo-fn-equiv-congruence-on-x

(defthm pseudo-fn-fix-pseudo-fn-equiv-congruence-on-x
  (implies (pseudo-fn-equiv x x-equiv)
           (equal (pseudo-fn-fix x)
                  (pseudo-fn-fix x-equiv)))
  :rule-classes :congruence)