• Top
    • Documentation
      • Xdoc
        • Undocumented
          • Interp-flags
          • Simpcode
          • Npn4
          • Cutinfo
          • Glcp-config-p
          • Glmc-config-p
          • Defsvtv-args
          • Vl-renaming-alist-p
          • Vcd-pathmap-p
          • Vcd-idxhash-p
          • *atc-exec-binary-strict-pure-rules*
          • Ecut-wirename-alistp
          • Context
          • Incremental-extremize-config-p
          • Ctrex-rule
          • Glmc-fsm-p
          • Eqbylbp-config-p
          • Proof-obligation
          • Cgraph-edge
          • Wcp-instance-rule-p
          • Wcp-witness-rule-p
          • Obligation-hyp
          • Vl-parsestate
          • Ecutnames-p
          • Te-args
          • Fn-info-elt-p
          • Wcp-template-p
          • Truth-idx
          • Polarity4
          • Phase-fsm-params
          • Fgl-casesplit-config
          • Propiso-info-p
          • Cutscore
          • Vl-rhs
          • Truth6
          • Fgl-satlink-monolithic-sat-config
          • Constraint-tuple
          • Truth5
          • Truth4
          • Truth3
          • Svexl-node
          • Ringosc3
          • Prof-entry-p
          • Constraint-tuple-p
          • Fgl-rune
          • Stv-spec-p
          • Svex-scc-consts
          • Base-fsm
          • Svtv-precompose-data
          • Pipeline-setup
          • Maybe-svar-p
          • Svl-module
          • Maybe-fgl-generic-rule
          • Frames
          • Vl-warningtree
          • Maybe-proof-obligation
          • Svtv-override-check
          • Fty-info
          • Prof-entry
          • Vl-maybe-rhs
          • Vl-parsed-ports
          • Svex-context
          • Maybe-svtv-evaldata
          • Maybe-svex
          • Maybe-simpcode
          • Maybe-rational
          • Flatten-res
          • Svex-reduce-config
          • Fty-type
          • Rewrite
          • Addnames-indices
          • Svtv*-phase
          • Fgl-binder-rune
          • Congruence-rule
          • Vl-ctxexpr
          • Rsh-of-concat-table
          • Chase-position
          • Hyp-tuple-p
          • Glcp-obj-ctrex-p
          • Glcp-bit-ctrex-p
          • Boundrw-subst-p
          • Svtv-evaldata
          • Svtv-cyclephase
          • Svar-split
          • Scopetree
          • Flatnorm-res
          • Fgl-rule
          • Constraint-rule
          • Vl-user-paramsetting
          • Svtv-override-triple
          • Svtv-composedata
          • Width-of-svex-extn
          • Array-fieldinfo-p
          • Wcp-example-app-p
          • Svtv*-input
          • Svex-override-triple
          • Svar-override-triple
          • 3col4vecline
          • Constraint-rule-p
          • Vl-parsed-ports
          • Svtv-assigns-override-config
          • Svex/index
          • Svl-env
          • Svl-aliasdb
          • Inverter
          • Fgl-binder-rule
          • Bvar-db-consistency-error
          • Wcp-lit-actions-p
          • Vcd-multivector-p
          • Svtv-fsm
          • Svexl
          • Constraint-instance
          • Vl-parsestate
          • Partsum-comp
          • Classname/params
          • Vcd-vector-p
          • Tmp-occ
          • Svl-occ
          • Svexllist
          • Svexl-alist
          • Integerp-of-svex-extn
          • Uninterpreted
          • Rw-pair
          • Vl-echar-raw
          • Vl-echar-raw
          • Use-set
          • Svtv-probe
          • Svex-phase-varname
          • Svex-cycle-varname
          • Range
          • Phase-fsm-config
          • Overridekey-syntaxcheck-data
          • Constraint
          • Alias
          • Sig
          • Sandwich
          • Cgraph-derivstate
          • Candidate-assign
          • Svex-alist-eval-equiv!
          • Svex-alist-eval-equiv
          • Scalar-fieldinfo-p
          • Fgl-ev-congruence-rulelist-correct-p
          • N-outputs-dom-supergates-sweep-config
          • Svex-envlists-equivalent
          • Svex-alistlist-eval-equiv
          • Flatnorm-setup
          • G-map-tag
          • Obs-sdom-array
          • Dom-supergates-sweep-config
          • Truth4arr
          • Npn4arr
          • Syndef::acid4
          • Svex-envlists-similar
          • Svex-alist-compose-equiv
          • Sym-prod
          • Fgl-congruence-rune
          • U32arr
          • Litarr
          • Aigtrans
          • Svexlist-eval-equiv
          • N-outputs-unreachability-config
          • Svex-eval-equiv
          • Unreachability-config
          • Keys-equiv
          • Vl-maybe-exprtype-list-p
          • Svex-alistlist
          • Vcd-indexlist-p
          • Alternative-spec-listp
          • Variable-listp
          • Vcd-vectorlist-p
          • Vcd-multivectorlist-p
          • Field-spec-listp
          • Neteval-ordering
          • Prof-entrylist-p
          • Hyp-tuplelist-p
          • Glcp-obj-ctrexlist-p
          • Symbol-path-list-p
          • Pseudo-input-listp
          • Input-listp
          • Ecutname-list-p
          • Boundrw-substlist-p
          • Constraintlist
          • Fgl-object-bindings
          • Fgl-generic-rule
          • Nonkeyword-listp
          • 4v-equiv
          • Svexl-node-array
          • Sig-path
          • Func-alist
          • Fgl-generic-rune
          • Fgl-ev-iff-equiv
          • Pseudo-term-subst
          • Nth-lit-equiv
          • Frames-equiv
          • Eval-formula-equiv
          • Svex-s4env
          • Svex-env-keys-equiv
          • Svex-alist-keys-equiv
          • Pseudo-term-alist
          • Fgl-ev-equiv
          • Lits-equiv
          • Nth-nat-equiv
          • Faig-const-equiv
          • Bdd-equiv
          • Vl-user-paramsettings
          • Classname/params-unparam-map
          • Obligation-hyp-list
          • Svtv*-output-alist
          • Svtv*-input-alist
          • Svtv-probealist
          • Svtv-override-triplemap
          • Svtv-cyclephaselist
          • Svex/index-maybenat-alist
          • Svex-context-alist
          • Rangemap
          • Fnsym-svexlistlist-alist
          • Tmp-occ-alist
          • Svl-module-alist
          • Svexl-node-alist
          • Occ-name-alist
          • Integerp-of-svex-extn-list
          • Alias-alist
          • Special-char-alist
          • Fty-info-alist
          • Bfr-updates
          • Term-equivs
          • Term-bvars
          • Sig-table
          • Fgl-function-mode-alist
          • Ctrex-ruletable
          • Constraint-db
          • Congruence-rule-table
          • Cgraph-derivstates
          • Cgraph-alist
          • Cgraph
          • Casesplit-alist
          • Truthmap
          • Axi-map
          • Nth-equiv
          • Faig-fix-equiv
          • Vl-string/int-alist
          • Vl-reservedtable
          • Vl-echarlist
          • Vl-ctxexprlist
          • Vl-coredatatype-infolist
          • Vl-usertypes
          • Vl-coredatatype-infolist
          • Proof-obligation-list
          • Use-set-summaries
          • Svtv-rev-probealist
          • Svex/index-nat-alist
          • Svex/index-key-alist
          • Svex-key-alist
          • Svex-envlist
          • Svar-widths
          • Svar-width-map
          • Svar-splittab
          • Svar-proplist
          • Svar-key-alist
          • Rsh-of-concat-alist
          • Path-alist
          • Name-alist
          • Address-alist
          • Width-of-svex-extn-list
          • Svl-occ-alist
          • Svex-to-natp-alist
          • Symbol-string-alist
          • Symbol-integer-alist
          • Sym-nat-alist
          • String-string-alist
          • Fty-types
          • Fty-field-alist
          • Any-table
          • Obj-alist
          • Nat-nat-alist
          • Constraint-instancelist
          • Congruence-rulelist
            • Congruence-rulelist-fix
              • Congruence-rulelist-equiv
              • Congruence-rulelist-p
            • Calist
            • Bvar-db-consistency-errorlist
            • Var-counts-alist
            • Pseudo-var-list
            • Equiv-contextslist
            • Nat-val-alistp
            • Id-neg-alist
            • String-keyed-alist-p
            • Vl-reportcardkeylist
            • Partsumlist
            • Partsum-elt
            • Classname/paramslist
            • Vl-reportcardkeylist
            • Vl-locationlist
            • Vl-echarlist
            • Perm4-list
            • Svtv*-phaselist
            • Svtv-override-triplemaplist
            • Svtv-override-triplelist
            • Svtv-override-checklist
            • Svtv-name-lhs-map-list
            • Svex/indexlist
            • Svexlistlist
            • Svex-override-triplelist
            • Svex-contextlist
            • Svarlist-list
            • Svar-widthslist
            • Svar-override-triplelist
            • Rangelist
            • Chase-stack
            • Addresslist
            • 4veclistlist
            • 3col4vecs
            • Occ-name-list
            • Alias-lst
            • Word-list
            • Sig-path-list
            • Function-option-name-lst
            • Any-trace
            • Bfr-varnamelist
            • Aig-varlist
            • Scratch-nontagidxlist
            • Prof-entrylist
            • Interp-st-field-p
            • Fgl-runelist
            • Fgl-rulelist
            • Fgl-object-bindingslist
            • Fgl-congruence-runelist
            • Fgl-binder-runelist
            • Fgl-binder-rulelist
            • Ctrex-rulelist
            • Constraint-tuplelist
            • Cgraph-edgelist
            • Candidate-assigns
            • Rw-pairlist
            • Rewritelist
            • Equiv-contexts
            • Bindinglist
            • Pos-list
            • Obs-sdom-info-list
            • Cutinfolist
            • Bit-list
            • Axi-termlist
            • Axi-litlist
            • Symbol-pseudoterm-alist
            • Vl-user-paramsettings-mode-p
            • Svtv-data$c-field-p
            • Ctrex-ruletype-p
            • String-stringlist-alist
            • Svar-overridetype-p
            • Ipasir-status-p
            • Axi-op-p
            • Vl-opacity-p
            • St-hyp-method-p
            • Scratchobj-kind-p
            • Logicman-field-p
            • Env$-field-p
            • Axi
            • *smt-architecture*
            • *vl-directions-kwds*
            • *vl-directions-kwd-alist*
            • Rlp-trees
          • Save
          • Defsection
          • Markup
          • Preprocessor
          • Terminal
          • Emacs-links
          • Defxdoc
          • Katex-integration
          • Constructors
          • Entities
          • Save-rendered
          • Add-resource-directory
          • Defxdoc+
          • Testing
          • Order-subtopics
          • Save-rendered-event
          • Archive-matching-topics
          • Archive-xdoc
          • Xdoc-extend
          • Set-default-parents
          • Missing-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Recursion-and-induction
        • Loop$-primer
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
      • Books
      • Boolean-reasoning
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Congruence-rulelist

    Congruence-rulelist-fix

    (congruence-rulelist-fix x) is a usual ACL2::fty list fixing function.

    Signature
    (congruence-rulelist-fix x) → fty::newx
    Arguments
    x — Guard (congruence-rulelist-p x).
    Returns
    fty::newx — Type (congruence-rulelist-p fty::newx).

    In the logic, we apply cmr::congruence-rule-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

    Definitions and Theorems

    Function: congruence-rulelist-fix$inline

    (defun congruence-rulelist-fix$inline (x)
      (declare (xargs :guard (congruence-rulelist-p x)))
      (let ((__function__ 'congruence-rulelist-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 nil
               (cons (cmr::congruence-rule-fix (car x))
                     (congruence-rulelist-fix (cdr x))))
             :exec x)))

    Theorem: congruence-rulelist-p-of-congruence-rulelist-fix

    (defthm congruence-rulelist-p-of-congruence-rulelist-fix
      (b* ((fty::newx (congruence-rulelist-fix$inline x)))
        (congruence-rulelist-p fty::newx))
      :rule-classes :rewrite)

    Theorem: congruence-rulelist-fix-when-congruence-rulelist-p

    (defthm congruence-rulelist-fix-when-congruence-rulelist-p
      (implies (congruence-rulelist-p x)
               (equal (congruence-rulelist-fix x) x)))

    Function: congruence-rulelist-equiv$inline

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

    Theorem: congruence-rulelist-equiv-is-an-equivalence

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

    Theorem: congruence-rulelist-equiv-implies-equal-congruence-rulelist-fix-1

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

    Theorem: congruence-rulelist-fix-under-congruence-rulelist-equiv

    (defthm congruence-rulelist-fix-under-congruence-rulelist-equiv
      (congruence-rulelist-equiv (congruence-rulelist-fix x)
                                 x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-congruence-rulelist-fix-1-forward-to-congruence-rulelist-equiv

    (defthm
     equal-of-congruence-rulelist-fix-1-forward-to-congruence-rulelist-equiv
     (implies (equal (congruence-rulelist-fix x) y)
              (congruence-rulelist-equiv x y))
     :rule-classes :forward-chaining)

    Theorem: equal-of-congruence-rulelist-fix-2-forward-to-congruence-rulelist-equiv

    (defthm
     equal-of-congruence-rulelist-fix-2-forward-to-congruence-rulelist-equiv
     (implies (equal x (congruence-rulelist-fix y))
              (congruence-rulelist-equiv x y))
     :rule-classes :forward-chaining)

    Theorem: congruence-rulelist-equiv-of-congruence-rulelist-fix-1-forward

    (defthm
         congruence-rulelist-equiv-of-congruence-rulelist-fix-1-forward
      (implies (congruence-rulelist-equiv (congruence-rulelist-fix x)
                                          y)
               (congruence-rulelist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: congruence-rulelist-equiv-of-congruence-rulelist-fix-2-forward

    (defthm
         congruence-rulelist-equiv-of-congruence-rulelist-fix-2-forward
      (implies (congruence-rulelist-equiv x (congruence-rulelist-fix y))
               (congruence-rulelist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: car-of-congruence-rulelist-fix-x-under-congruence-rule-equiv

    (defthm car-of-congruence-rulelist-fix-x-under-congruence-rule-equiv
      (cmr::congruence-rule-equiv (car (congruence-rulelist-fix x))
                                  (car x)))

    Theorem: car-congruence-rulelist-equiv-congruence-on-x-under-congruence-rule-equiv

    (defthm
     car-congruence-rulelist-equiv-congruence-on-x-under-congruence-rule-equiv
     (implies (congruence-rulelist-equiv x x-equiv)
              (cmr::congruence-rule-equiv (car x)
                                          (car x-equiv)))
     :rule-classes :congruence)

    Theorem: cdr-of-congruence-rulelist-fix-x-under-congruence-rulelist-equiv

    (defthm
       cdr-of-congruence-rulelist-fix-x-under-congruence-rulelist-equiv
      (congruence-rulelist-equiv (cdr (congruence-rulelist-fix x))
                                 (cdr x)))

    Theorem: cdr-congruence-rulelist-equiv-congruence-on-x-under-congruence-rulelist-equiv

    (defthm
     cdr-congruence-rulelist-equiv-congruence-on-x-under-congruence-rulelist-equiv
     (implies (congruence-rulelist-equiv x x-equiv)
              (congruence-rulelist-equiv (cdr x)
                                         (cdr x-equiv)))
     :rule-classes :congruence)

    Theorem: cons-of-congruence-rule-fix-x-under-congruence-rulelist-equiv

    (defthm
          cons-of-congruence-rule-fix-x-under-congruence-rulelist-equiv
      (congruence-rulelist-equiv (cons (cmr::congruence-rule-fix x) y)
                                 (cons x y)))

    Theorem: cons-congruence-rule-equiv-congruence-on-x-under-congruence-rulelist-equiv

    (defthm
     cons-congruence-rule-equiv-congruence-on-x-under-congruence-rulelist-equiv
     (implies (cmr::congruence-rule-equiv x x-equiv)
              (congruence-rulelist-equiv (cons x y)
                                         (cons x-equiv y)))
     :rule-classes :congruence)

    Theorem: cons-of-congruence-rulelist-fix-y-under-congruence-rulelist-equiv

    (defthm
      cons-of-congruence-rulelist-fix-y-under-congruence-rulelist-equiv
      (congruence-rulelist-equiv (cons x (congruence-rulelist-fix y))
                                 (cons x y)))

    Theorem: cons-congruence-rulelist-equiv-congruence-on-y-under-congruence-rulelist-equiv

    (defthm
     cons-congruence-rulelist-equiv-congruence-on-y-under-congruence-rulelist-equiv
     (implies (congruence-rulelist-equiv y y-equiv)
              (congruence-rulelist-equiv (cons x y)
                                         (cons x y-equiv)))
     :rule-classes :congruence)

    Theorem: consp-of-congruence-rulelist-fix

    (defthm consp-of-congruence-rulelist-fix
      (equal (consp (congruence-rulelist-fix x))
             (consp x)))

    Theorem: congruence-rulelist-fix-under-iff

    (defthm congruence-rulelist-fix-under-iff
      (iff (congruence-rulelist-fix x)
           (consp x)))

    Theorem: congruence-rulelist-fix-of-cons

    (defthm congruence-rulelist-fix-of-cons
      (equal (congruence-rulelist-fix (cons a x))
             (cons (cmr::congruence-rule-fix a)
                   (congruence-rulelist-fix x))))

    Theorem: len-of-congruence-rulelist-fix

    (defthm len-of-congruence-rulelist-fix
      (equal (len (congruence-rulelist-fix x))
             (len x)))

    Theorem: congruence-rulelist-fix-of-append

    (defthm congruence-rulelist-fix-of-append
      (equal (congruence-rulelist-fix (append std::a std::b))
             (append (congruence-rulelist-fix std::a)
                     (congruence-rulelist-fix std::b))))

    Theorem: congruence-rulelist-fix-of-repeat

    (defthm congruence-rulelist-fix-of-repeat
      (equal (congruence-rulelist-fix (acl2::repeat n x))
             (acl2::repeat n (cmr::congruence-rule-fix x))))

    Theorem: list-equiv-refines-congruence-rulelist-equiv

    (defthm list-equiv-refines-congruence-rulelist-equiv
      (implies (acl2::list-equiv x y)
               (congruence-rulelist-equiv x y))
      :rule-classes :refinement)

    Theorem: nth-of-congruence-rulelist-fix

    (defthm nth-of-congruence-rulelist-fix
      (equal (nth n (congruence-rulelist-fix x))
             (if (< (nfix n) (len x))
                 (cmr::congruence-rule-fix (nth n x))
               nil)))

    Theorem: congruence-rulelist-equiv-implies-congruence-rulelist-equiv-append-1

    (defthm
     congruence-rulelist-equiv-implies-congruence-rulelist-equiv-append-1
     (implies (congruence-rulelist-equiv x fty::x-equiv)
              (congruence-rulelist-equiv (append x y)
                                         (append fty::x-equiv y)))
     :rule-classes (:congruence))

    Theorem: congruence-rulelist-equiv-implies-congruence-rulelist-equiv-append-2

    (defthm
     congruence-rulelist-equiv-implies-congruence-rulelist-equiv-append-2
     (implies (congruence-rulelist-equiv y fty::y-equiv)
              (congruence-rulelist-equiv (append x y)
                                         (append x fty::y-equiv)))
     :rule-classes (:congruence))

    Theorem: congruence-rulelist-equiv-implies-congruence-rulelist-equiv-nthcdr-2

    (defthm
     congruence-rulelist-equiv-implies-congruence-rulelist-equiv-nthcdr-2
     (implies (congruence-rulelist-equiv l l-equiv)
              (congruence-rulelist-equiv (nthcdr n l)
                                         (nthcdr n l-equiv)))
     :rule-classes (:congruence))

    Theorem: congruence-rulelist-equiv-implies-congruence-rulelist-equiv-take-2

    (defthm
     congruence-rulelist-equiv-implies-congruence-rulelist-equiv-take-2
     (implies (congruence-rulelist-equiv l l-equiv)
              (congruence-rulelist-equiv (take n l)
                                         (take n l-equiv)))
     :rule-classes (:congruence))