• 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
        • Block-headerp
        • Ctrex-rule
        • Execution-environmentp
        • Glmc-fsm-p
        • Transactionp
        • Eqbylbp-config-p
        • Proof-obligation
          • Proof-obligation-fix
          • Proof-obligation-equiv
          • Make-proof-obligation
          • Proof-obligation->source-expression
          • Proof-obligation->variables
          • Proof-obligation->hypotheses
          • Proof-obligation->conclusion
          • Change-proof-obligation
          • Proof-obligationp
        • Cgraph-edge
        • Wcp-instance-rule-p
        • Fgl-casesplit-config
        • Wcp-witness-rule-p
        • Obligation-hyp
        • Vl-parsestate
        • Ecutnames-p
        • Te-args
        • Fgl-satlink-monolithic-sat-config
        • Fn-info-elt-p
        • Wcp-template-p
        • Truth-idx
        • Polarity4
        • Phase-fsm-params
        • Propiso-info-p
        • Cutscore
        • Vl-rhs
        • Truth6
        • Constraint-tuple
        • Truth5
        • Truth4
        • Truth3
        • Svexl-node
        • Ringosc3
        • Prof-entry-p
        • Constraint-tuple-p
        • Fgl-rune
        • Stv-spec-p
        • Run-snippet-file-info
        • Svex-scc-consts
        • Fsm
        • Machine-statep
        • Run-snippet-info
        • Svtv-precompose-data
        • Pipeline-setup
        • Maybe-svar-p
        • Svl-module
        • Maybe-fgl-generic-rule
        • Frames
        • Maybe-snippet-mismatch
        • Cpuid-info-p
        • Vl-warningtree
        • Maybe-proof-obligation
        • Svtv-override-check
        • Maybe-svtv-chase-evaldata
        • Fty-info
        • Prof-entry
        • Substatep
        • Vl-maybe-rhs
        • Vl-parsed-ports
        • Svex-context
        • Account-statep
        • Maybe-simpcode
        • Maybe-rational
        • Maybe-svex
        • Flatten-res
        • Svex-reduce-config
        • Fty-type
        • Rewrite
        • Snippet-info
        • Addnames-indices
        • Svtv*-phase
        • Segment-driver
        • Satlink-parser-state
        • Fgl-binder-rune
        • Congruence-rule
        • Snippet-mismatch
        • Vl-ctxexpr
        • Rsh-of-concat-table
        • Chase-position
        • Hyp-tuple-p
        • Glcp-obj-ctrex-p
        • Glcp-bit-ctrex-p
        • Block$-p
        • Boundrw-subst-p
        • Svtv-cyclephase
        • Svar-split
        • Scopetree
        • Flatnorm-res
        • Fgl-rule
        • Constraint-rule
        • Vl-user-paramsetting
        • Svtv-override-triple
        • Svtv-evaldata
        • 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-chase-evaldata
        • 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
        • Fe-list-listp
        • 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
        • Svex-envs-1mask-equiv
        • U32arr
        • Litarr
        • Aigtrans
        • Svexlist-eval-equiv
        • N-outputs-unreachability-config
        • Svex-eval-equiv
        • Unreachability-config
        • Keys-equiv
        • Vl-maybe-exprtype-list-p
        • Svex-alistlist
        • Svar-overridetype-p
        • Fty::flexprod-listp
        • Fty::flexprod-field-listp
        • 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
        • 4v-equiv
        • Sdm-instruction-table
        • 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
        • Byte-list
        • 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
        • Segment-driver-map
        • 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
        • Named-lit-list-map
        • 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
        • Calist
        • Bvar-db-consistency-errorlist
        • Var-counts-alist
        • Pseudo-var-list
        • Equiv-contextslist
        • Nat-val-alistp
        • Id-neg-alist
        • String-keyed-alist-p
        • Snippet-table
        • Snippet-mismatch-list
        • 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-overridetypelist
        • Svar-override-triplelist
        • Segment-driverlist
        • 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
        • Symbol-pseudoeventform-alist
        • Inst-list
        • Vl-user-paramsettings-mode-p
        • Svtv-data$c-field-p
        • Ctrex-ruletype-p
        • String-stringlist-alist
        • Ipasir-status-p
        • Fgl-toplevel-sat-check-mode-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
      • Defxdoc+
      • Save-rendered
      • Add-resource-directory
      • 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
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Proof-obligation

Proof-obligation-fix

Fixing function for proof-obligation structures.

Signature

(proof-obligation-fix x) → new-x

Arguments

x — Guard (proof-obligationp x).

Returns

new-x — Type (proof-obligationp new-x).

Definitions and Theorems

Function: proof-obligation-fix$inline

(defun proof-obligation-fix$inline (x)
 (declare (xargs :guard (proof-obligationp x)))
 (let ((__function__ 'proof-obligation-fix))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b*
     ((variables (typed-variable-list-fix (cdr (std::da-nth 0 x))))
      (hypotheses (obligation-hyp-list-fix (cdr (std::da-nth 1 x))))
      (conclusion (expression-fix (cdr (std::da-nth 2 x))))
      (source-expression (expression-fix (cdr (std::da-nth 3 x)))))
     (list (cons 'variables variables)
           (cons 'hypotheses hypotheses)
           (cons 'conclusion conclusion)
           (cons 'source-expression
                 source-expression)))
    :exec x)))

Theorem: proof-obligationp-of-proof-obligation-fix

(defthm proof-obligationp-of-proof-obligation-fix
  (b* ((new-x (proof-obligation-fix$inline x)))
    (proof-obligationp new-x))
  :rule-classes :rewrite)

Theorem: proof-obligation-fix-when-proof-obligationp

(defthm proof-obligation-fix-when-proof-obligationp
  (implies (proof-obligationp x)
           (equal (proof-obligation-fix x) x)))

Function: proof-obligation-equiv$inline

(defun proof-obligation-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (proof-obligationp acl2::x)
                              (proof-obligationp acl2::y))))
  (equal (proof-obligation-fix acl2::x)
         (proof-obligation-fix acl2::y)))

Theorem: proof-obligation-equiv-is-an-equivalence

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

Theorem: proof-obligation-equiv-implies-equal-proof-obligation-fix-1

(defthm proof-obligation-equiv-implies-equal-proof-obligation-fix-1
  (implies (proof-obligation-equiv acl2::x x-equiv)
           (equal (proof-obligation-fix acl2::x)
                  (proof-obligation-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: proof-obligation-fix-under-proof-obligation-equiv

(defthm proof-obligation-fix-under-proof-obligation-equiv
  (proof-obligation-equiv (proof-obligation-fix acl2::x)
                          acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-proof-obligation-fix-1-forward-to-proof-obligation-equiv

(defthm
  equal-of-proof-obligation-fix-1-forward-to-proof-obligation-equiv
  (implies (equal (proof-obligation-fix acl2::x)
                  acl2::y)
           (proof-obligation-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-proof-obligation-fix-2-forward-to-proof-obligation-equiv

(defthm
  equal-of-proof-obligation-fix-2-forward-to-proof-obligation-equiv
  (implies (equal acl2::x (proof-obligation-fix acl2::y))
           (proof-obligation-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: proof-obligation-equiv-of-proof-obligation-fix-1-forward

(defthm proof-obligation-equiv-of-proof-obligation-fix-1-forward
  (implies (proof-obligation-equiv (proof-obligation-fix acl2::x)
                                   acl2::y)
           (proof-obligation-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: proof-obligation-equiv-of-proof-obligation-fix-2-forward

(defthm proof-obligation-equiv-of-proof-obligation-fix-2-forward
 (implies
     (proof-obligation-equiv acl2::x (proof-obligation-fix acl2::y))
     (proof-obligation-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)