ProofRule

java.lang.Object
- java.lang.Enum<ProofRule>
- - io.github.cvc5.ProofRule

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<ProofRule>
```
public enum ProofRule
extends java.lang.Enum<ProofRule>
```

Enum Constant Summary

Enum Constants
Enum Constant and Description
`ABSORB` Builtin theory – absorb \[ \inferrule{- \mid t = z}{t = z} \] where $t$ contains $z$ as a subterm, where $z$ is a zero element.
`ACI_NORM` Builtin theory – associative/commutative/idempotency/identity \ normalization \[ \inferrule{- \mid t = s}{t = s} \] where $t$ and $s$ are equivalent modulo associativity and identity elements, and (optionally) commutativity and idempotency.
`ALETHE_RULE` External – Alethe Place holder for Alethe rules.
`ALPHA_EQUIV` Quantifiers – Alpha equivalence \[ \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} \] Notice that this rule is correct only when $z_1,\dots,z_n$ are not contained in $FV(F) \setminus \{ y_1,\dots, y_n \}$, where $FV(F)$ are the free variables of $F$.
`AND_ELIM` Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
`AND_INTRO` Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
`ARITH_MULT_ABS_COMPARISON` Arithmetic – Non-linear multiply absolute value comparison \[ \inferrule{F_1 \dots F_n \mid -}{F} \] where $F$ is of the form $\left\| t_1 \cdot t_n \right\| \diamond \left\| s_1 \cdot s_n \right\|$.
`ARITH_MULT_NEG` Arithmetic – Multiplication with negative factor \[ \inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r} \] where $\diamond$ is a relation symbol and $\diamond_{inv}$ the inverted relation symbol.
`ARITH_MULT_POS` Arithmetic – Multiplication with positive factor \[ \inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r} \] where $\diamond$ is a relation symbol.
`ARITH_MULT_SIGN` Arithmetic – Sign inference \[ \inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0} \] where $f_1 \dots f_k$ are variables compared to zero (less, greater or not equal), $m$ is a monomial from these variables and $\diamond$ is the comparison (less or greater) that results from the signs of the variables.
`ARITH_MULT_TANGENT` Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid x, y, a, b, \sigma}{(t \leq tplane) = ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = \bot$} \inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) = ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = \top$} \] where $x,y$ are real terms (variables or extended terms), $t = x \cdot y$, $a,b$ are real constants, $\sigma \in \{ \top, \bot\}$ and $tplane := b \cdot x + a \cdot y - a \cdot b$ is the tangent plane of $x \cdot y$ at $(a,b)$.
`ARITH_POLY_NORM` Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top$.
`ARITH_POLY_NORM_REL` Arithmetic – Polynomial normalization for relations ..
`ARITH_REDUCTION` Arithmetic – Reduction \[ \inferrule{- \mid t}{F} \] where $t$ is an application of an extended arithmetic operator (e.g.
`ARITH_SUM_UB` Arithmetic – Sum upper bounds \[ \inferrule{P_1 \dots P_n \mid -}{L \diamond R} \] where $P_i$ has the form $L_i \diamond_i R_i$ and $\diamond_i \in \{<, \leq, =\}$.
`ARITH_TRANS_EXP_APPROX_ABOVE_NEG` Arithmetic – Transcendentals – Exp is approximated from above for \ negative values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$.
`ARITH_TRANS_EXP_APPROX_ABOVE_POS` Arithmetic – Transcendentals – Exp is approximated from above for \ positive values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$.
`ARITH_TRANS_EXP_APPROX_BELOW` Arithmetic – Transcendentals – Exp is approximated from below \[ \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)} \] where $d$ is a non-negative number, $t$ an arithmetic term and $\texttt{maclaurin}(\exp, n+1, c)$ is the $(n+1)$'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at $c$ where $n$ is $2 \cdot d$.
`ARITH_TRANS_EXP_NEG` Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
`ARITH_TRANS_EXP_POSITIVITY` Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
`ARITH_TRANS_EXP_SUPER_LIN` Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
`ARITH_TRANS_EXP_ZERO` Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
`ARITH_TRANS_PI` Arithmetic – Transcendentals – Assert bounds on Pi \[ \inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u} \] where $l,u$ are valid lower and upper bounds on $\pi$.
`ARITH_TRANS_SINE_APPROX_ABOVE_NEG` Arithmetic – Transcendentals – Sine is approximated from above for\ negative values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$.
`ARITH_TRANS_SINE_APPROX_ABOVE_POS` Arithmetic – Transcendentals – Sine is approximated from above for \ positive values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$).
`ARITH_TRANS_SINE_APPROX_BELOW_NEG` Arithmetic – Transcendentals – Sine is approximated from below for \ negative values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$).
`ARITH_TRANS_SINE_APPROX_BELOW_POS` Arithmetic – Transcendentals – Sine is approximated from below for \ positive values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$.
`ARITH_TRANS_SINE_BOUNDS` Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
`ARITH_TRANS_SINE_SHIFT` Arithmetic – Transcendentals – Sine is shifted to -pi...pi \[ \inferrule{- \mid x}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})} \] where $x$ is the argument to sine, $y$ is a new real skolem that is $x$ shifted into $-\pi \dots \pi$ and $s$ is a new integer skolem that is the number of phases $y$ is shifted.
`ARITH_TRANS_SINE_SYMMETRY` Arithmetic – Transcendentals – Sine is symmetric with respect to \ negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
`ARITH_TRANS_SINE_TANGENT_PI` Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..
`ARITH_TRANS_SINE_TANGENT_ZERO` Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..
`ARITH_TRICHOTOMY` Arithmetic – Trichotomy of the reals \[ \inferrule{A, B \mid -}{C} \] where $\neg A, \neg B, C$ are $x < c, x = c, x > c$ in some order.
`ARRAYS_EXT` Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where $k$ is the $\texttt{ARRAY_DEQ_DIFF}$ skolem for `(a, b)`.
`ARRAYS_READ_OVER_WRITE` Arrays – Read over write \[ \inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)} \]
`ARRAYS_READ_OVER_WRITE_1` Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
`ARRAYS_READ_OVER_WRITE_CONTRA` Arrays – Read over write, contrapositive \[ \inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2} \]
`ASSUME` Assumption (a leaf) \[ \inferrule{- \mid F}{F} \] This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified.
`BV_BITBLAST_STEP` Bit-vectors – Bitblast bit-vector constant, variable, and terms For constant and variables: \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] For terms: \[ \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)} \] where $t$ is $k(t_1,\dots,t_n)$.
`BV_EAGER_ATOM` Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where $F$ is of kind `BITVECTOR_EAGER_ATOM`.
`BV_POLY_NORM` Bit-vectors – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top$.
`BV_POLY_NORM_EQ` Bit-vectors – Polynomial normalization for relations ..
`CHAIN_RESOLUTION` Boolean – N-ary Resolution \[ \inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C} \] where let $C_1 \dots C_n$ be nodes viewed as clauses, as defined above let $C_1 \diamond_{L,pol} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined above let $C_1' = C_1$, for each $i > 1$, let $C_i' = C_{i-1} \diamond_{L_{i-1}, pol_{i-1}} C_i'$ Note the list of polarities and pivots are provided as s-expressions.
`CNF_AND_NEG` Boolean – CNF – And Negative \[ \inferrule{- \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n} \]
`CNF_AND_POS` Boolean – CNF – And Positive \[ \inferrule{- \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i} \]
`CNF_EQUIV_NEG1` Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]
`CNF_EQUIV_NEG2` Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]
`CNF_EQUIV_POS1` Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]
`CNF_EQUIV_POS2` Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]
`CNF_IMPLIES_NEG1` Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]
`CNF_IMPLIES_NEG2` Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]
`CNF_IMPLIES_POS` Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]
`CNF_ITE_NEG1` Boolean – CNF – ITE Negative 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1} \]
`CNF_ITE_NEG2` Boolean – CNF – ITE Negative 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2} \]
`CNF_ITE_NEG3` Boolean – CNF – ITE Negative 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2} \]
`CNF_ITE_POS1` Boolean – CNF – ITE Positive 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1} \]
`CNF_ITE_POS2` Boolean – CNF – ITE Positive 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2} \]
`CNF_ITE_POS3` Boolean – CNF – ITE Positive 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2} \]
`CNF_OR_NEG` Boolean – CNF – Or Negative \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i} \]
`CNF_OR_POS` Boolean – CNF – Or Positive \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n} \]
`CNF_XOR_NEG1` Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]
`CNF_XOR_NEG2` Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]
`CNF_XOR_POS1` Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]
`CNF_XOR_POS2` Boolean – CNF – XOR Positive 2 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2} \]
`CONCAT_CPROP` Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1 \cdot w_1 \cdot \ldots \cdot t_n) = (w_2 \cdot s_2 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)} \] where $w_1,\,w_2$ are words, $t_3$ is $\mathit{pre}(w_2,p)$, $p$ is $\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)$, and $r$ is the purification skolem for $\mathit{suf}(t_1,\mathit{len}(w_3))$.
`CONCAT_CSPLIT` Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (c \cdot t_2 \ldots \cdot s_m),\,\mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)} \] where $r$ is the purification skolem for $\mathit{suf}(t_1,1)$.
`CONCAT_EQ` Strings – Core rules – Concatenation equality \[ \inferrule{(t_1 \cdot \ldots \cdot t_n \cdot t) = (t_1 \cdot \ldots \cdot t_n \cdot s)\mid \bot}{t = s} \] Alternatively for the reverse: \inferrule{(t \cdot t_1 \cdot \ldots \cdot t_n) = (s \cdot t_1 \cdot \ldots \cdot t_n)\mid \top}{t = s} Notice that $t$ or $s$ may be empty, in which case they are implicit in the concatenation above.
`CONCAT_LPROP` Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)} \] where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$.
`CONCAT_SPLIT` Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid \bot}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0} \] where $r$ is the purification skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$ and $\epsilon$ is the empty string (or sequence).
`CONCAT_UNIFY` Strings – Core rules – Concatenation unification \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1} \] Alternatively for the reverse: \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) = \mathit{len}(s_m)\mid \top}{t_n = s_m} \]
`CONG` Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used when the kind of $f(t_1,\dots, t_n)$ has a fixed arity.
`CONTRA` Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
`DISTINCT_VALUES` Builtin theory – Distinct values \[ \inferrule{- \mid t, s}{\neg t = s} \] where $t$ and $s$ are distinct values.
`DRAT_REFUTATION` DRAT Refutation \[ \inferrule{F_1 \dots F_n \mid D, P}{\bot} \] where $F_1 \dots F_n$ correspond to the clauses in the DIMACS file given by filename `D` and `P` is a filename of a file storing a DRAT proof.
`DSL_REWRITE` Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where `id` is a ProofRewriteRule whose definition in the RARE DSL is \(\forall x_1 \dots x_n.
`DT_SPLIT` Datatypes – Split \[ \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)} \] where $C_1,\dots,C_n$ are all the constructors of the type of $t$.
`ENCODE_EQ_INTRO` Builtin theory – Encode equality introduction \[ \inferrule{- \mid t}{t=t'} \] where $t$ and $t'$ are equivalent up to their encoding in an external proof format.
`EQ_RESOLVE` Boolean – Equality resolution \[ \inferrule{F_1, (F_1 = F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for EQUIV_ELIM1 <cvc5.`EQUIV_ELIM1`> + RESOLUTION <cvc5.`RESOLUTION`>.
`EQUIV_ELIM1` Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
`EQUIV_ELIM2` Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
`EVALUATE` Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{evaluate}(t)} \] where $\texttt{evaluate}$ is implemented by calling the method $\texttt{Evalutor::evaluate}$ in :cvc5src:`theory/evaluator.h` with an empty substitution.
`EXISTS_STRING_LENGTH` Quantifiers – Exists string length \[ \inferrule{-\mid T n i} {\mathit{len}(k) = n} \] where $k$ is a skolem of string or sequence type $T$ and $n$ is a non-negative integer.
`FACTORING` Boolean – Factoring \[ \inferrule{C_1 \mid -}{C_2} \] where $C_2$ is the clause $C_1$, but every occurrence of a literal after its first occurrence is omitted.
`FALSE_ELIM` Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]
`FALSE_INTRO` Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]
`HO_APP_ENCODE` Equality – Higher-order application encoding \[ \inferrule{-\mid t}{t=t'} \] where `t'` is the higher-order application that is equivalent to `t`, as implemented by `uf.TheoryUfRewriter.getHoApplyForApplyUf`.
`HO_CONG` Equality – Higher-order congruence \[ \inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)} \] Notice that this rule is only used when the application kind $k$ is either `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.
`IMPLIES_ELIM` Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]
`INSTANTIATE` Quantifiers – Instantiation \[ \inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The list of terms to instantiate $(t_1 \dots t_n)$ is provided as an s-expression as the first argument.
`INT_TIGHT_LB` Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where $i$ has integer type.
`INT_TIGHT_UB` Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where $i$ has integer type.
`ITE_ELIM1` Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
`ITE_ELIM2` Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
`ITE_EQ` Processing rules – If-then-else equivalence \[ \inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}} \]
`LFSC_RULE` External – LFSC Place holder for LFSC rules.
`MACRO_ARITH_SCALE_SUM_UB` Arithmetic – Adding inequalities An arithmetic literal is a term of the form $p \diamond c$ where $\diamond \in \{ <, \leq, =, \geq, > \}$, $p$ a polynomial and $c$ a rational constant.
`MACRO_BV_BITBLAST` Bit-vectors – (Macro) Bitblast \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] where $\texttt{bitblast}$ represents the result of the bit-blasted term as a bit-vector consisting of the output bits of the bit-blasted circuit representation of the term.
`MACRO_RESOLUTION` Boolean – N-ary Resolution + Factoring + Reordering \[ \inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C} \] where let $C_1 \dots C_n$ be nodes viewed as clauses, as defined in RESOLUTION <cvc5.`RESOLUTION`> let $C_1 \diamond_{L,\mathit{pol}} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined in RESOLUTION <cvc5.`RESOLUTION`> let $C_1'$ be equal, in its set representation, to $C_1$, for each $i > 1$, let $C_i'$ be equal, in its set representation, to $C_{i-1} \diamond_{L_{i-1},\mathit{pol}_{i-1}} C_i'$ The result of the chain resolution is $C$, which is equal, in its set representation, to $C_n'$
`MACRO_RESOLUTION_TRUST` Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as MACRO_RESOLUTION <cvc5.`MACRO_RESOLUTION`>, but not checked by the internal proof checker.
`MACRO_REWRITE` Builtin theory – Rewrite \[ \inferrule{- \mid t, idr}{t = \texttt{rewrite}_{idr}(t)} \] where $idr$ is a MethodId identifier, which determines the kind of rewriter to apply, e.g., Rewriter.rewrite.
`MACRO_SR_EQ_INTRO` Builtin theory – Substitution + Rewriting equality introduction In this rule, we provide a term $t$ and conclude that it is equal to its rewritten form under a (proven) substitution.
`MACRO_SR_PRED_ELIM` Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))} \] where $ids$ and $idr$ are method identifiers.
`MACRO_SR_PRED_INTRO` Builtin theory – Substitution + Rewriting predicate introduction In this rule, we provide a formula $F$ and conclude it, under the condition that it rewrites to true under a proven substitution.
`MACRO_SR_PRED_TRANSFORM` Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G} \] where \[ \texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ\cdots \circ \sigma_{ids, ida}(F_1)) =\\ \texttt{rewrite}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) \] More generally, this rule also holds when: $\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))$ where $F'$ and $G'$ are the result of each side of the equation above.
`MACRO_STRING_INFERENCE` Strings – (Macro) String inference \[ \inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F} \] used to bookkeep an inference that has not yet been converted via $\texttt{strings::InferProofCons::convert}$.
`MODUS_PONENS` Boolean – Modus Ponens \[ \inferrule{F_1, (F_1 \rightarrow F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for IMPLIES_ELIM <cvc5.`IMPLIES_ELIM`> + RESOLUTION <cvc5.`RESOLUTION`>.
`NARY_CONG` Equality – N-ary Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used for terms $f(t_1,\dots, t_n)$ whose kinds $k$ have variadic arity, such as `cvc5.Kind.AND`, `cvc5.Kind.PLUS` and so on.
`NOT_AND` Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
`NOT_EQUIV_ELIM1` Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
`NOT_EQUIV_ELIM2` Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
`NOT_IMPLIES_ELIM1` Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
`NOT_IMPLIES_ELIM2` Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
`NOT_ITE_ELIM1` Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
`NOT_ITE_ELIM2` Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
`NOT_NOT_ELIM` Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
`NOT_OR_ELIM` Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
`NOT_XOR_ELIM1` Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
`NOT_XOR_ELIM2` Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
`QUANT_VAR_REORDERING` Quantifiers – Variable reordering \[ \inferrule{-\mid (\forall X.\> F) = (\forall Y.\> F)} {(\forall X.\> F) = (\forall Y.\> F)} \] where $Y$ is a reordering of $X$.
`RE_CONCAT` Strings – Regular expressions – Concatenation \[ \inferrule{t_1\in R_1,\,\ldots,\,t_n\in R_n\mid -}{\text{str.++}(t_1, \ldots, t_n)\in \text{re.++}(R_1, \ldots, R_n)} \]
`RE_INTER` Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{re.inter}(R_1,R_2)} \]
`RE_UNFOLD_NEG` Strings – Regular expressions – Negative Unfold \[ \inferrule{t \not \in \mathit{re}.\text{*}(R) \mid -}{t \neq \ \epsilon \ \wedge \forall L.
`RE_UNFOLD_NEG_CONCAT_FIXED` Strings – Regular expressions – Unfold negative concatenation, fixed ..
`RE_UNFOLD_POS` Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{F} \] where $F$ corresponds to the one-step unfolding of the premise.
`REFL` Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
`REORDERING` Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the multiset representations of $C_1$ and $C_2$ are the same.
`RESOLUTION` Boolean – Resolution \[ \inferrule{C_1, C_2 \mid pol, L}{C} \] where $C_1$ and $C_2$ are nodes viewed as clauses, i.e., either an `OR` node with each children viewed as a literal or a node viewed as a literal.
`SAT_EXTERNAL_PROVE` SAT external prove Refutation \[ \inferrule{F_1 \dots F_n \mid D}{\bot} \] where $F_1 \dots F_n$ correspond to the input clauses in the DIMACS file `D`.
`SAT_REFUTATION` SAT Refutation for assumption-based unsat cores \[ \inferrule{F_1 \dots F_n \mid -}{\bot} \] where $F_1 \dots F_n$ correspond to the unsat core determined by the SAT solver.
`SCOPE` Scope (a binder for assumptions) \[ \inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$} \] This rule has a dual purpose with ASSUME <cvc5.`ASSUME`>.
`SETS_EXT` Sets – Sets extensionality \[ \inferrule{a \neq b\mid -} {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)} \] where $k$ is the $\texttt{SETS_DEQ_DIFF}$ skolem for `(a, b)`.
`SETS_FILTER_DOWN` Sets – Sets filter down \[ \inferrule{\mathit{set.member}(x,\mathit{set.filter}(P, a))\mid -} {\mathit{set.member}(x,a) \wedge P(x)} \]
`SETS_FILTER_UP` Sets – Sets filter up \[ \inferrule{\mathit{set.member}(x,a)\mid P} {\mathit{set.member}(x, \mathit{set.filter}(P, a)) = P(x)} \]
`SETS_SINGLETON_INJ` Sets – Singleton injectivity \[ \inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid -}{t=s} \]
`SKOLEM_INTRO` Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where $t$ is the unpurified form of skolem $k$.
`SKOLEMIZE` Quantifiers – Skolemization \[ \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} \] where $\sigma$ maps $x_1,\dots,x_n$ to their representative skolems, which are skolems $k_1,\dots,k_n$.
`SPLIT` Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
`STRING_CODE_INJ` Strings – Code points \[ \inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t = s} \]
`STRING_DECOMPOSE` Strings – Core rules – String decomposition \[ \inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n} \] where $w_1$ is the purification skolem for $\mathit{pre}(t,n)$ and $w_2$ is the purification skolem for $\mathit{suf}(t,n)$.
`STRING_EAGER_REDUCTION` Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where $R$ is $\texttt{TermRegistry::eagerReduce}(t)$.
`STRING_EXT` Strings – Extensionality \[ \inferrule{s \neq t\mid -} {\mathit{seq.len}(s) \neq \mathit{seq.len}(t) \vee (\mathit{seq.nth}(s,k)\neq\mathit{set.nth}(t,k) \wedge 0 \leq k \wedge k < \mathit{seq.len}(s))} \] where $s,t$ are terms of sequence type, $k$ is the $\texttt{STRINGS_DEQ_DIFF}$ skolem for $s,t$.
`STRING_LENGTH_NON_EMPTY` Strings – Core rules – Length non-empty \[ \inferrule{t\neq \epsilon\mid -}{\mathit{len}(t) \neq 0} \]
`STRING_LENGTH_POS` Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= \epsilon)\vee \mathit{len}(t) > 0} \]
`STRING_REDUCTION` Strings – Extended functions – Reduction \[ \inferrule{-\mid t}{R\wedge t = w} \] where $w$ is $\texttt{StringsPreprocess::reduce}(t, R, \dots)$.
`STRING_SEQ_UNIT_INJ` Strings – Sequence unit \[ \inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y} \] Also applies to the case where $\mathit{unit}(y)$ is a constant sequence of length one.
`SUBS` Builtin theory – Substitution \[ \inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)} \] where $\sigma_{ids}(F_i)$ are substitutions, which notice are applied in reverse order.
`SYMM` Equality – Symmetry \[ \inferrule{t_1 = t_2\mid -}{t_2 = t_1} \] or \[ \inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1} \]
`THEORY_REWRITE` Other theory rewrite rules \[ \inferrule{- \mid id, t = t'}{t = t'} \] where `id` is the ProofRewriteRule of the theory rewrite rule which transforms $t$ to $t'$.
`TRANS` Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
`TRUE_ELIM` Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
`TRUE_INTRO` Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
`TRUST` Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where $tid$ is an identifier and $F$ is a formula.
`TRUST_THEORY_REWRITE` Trusted rules – Theory rewrite \[ \inferrule{- \mid F, tid, rid}{F} \] where $F$ is an equality of the form $t = t'$ where $t'$ is obtained by applying the kind of rewriting given by the method identifier $rid$, which is one of: `RW_REWRITE_THEORY_PRE`, `RW_REWRITE_THEORY_POST`, `RW_REWRITE_EQ_EXT`.
`UNKNOWN` External – Alethe Place holder for Alethe rules.
`XOR_ELIM1` Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]
`XOR_ELIM2` Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`static ProofRule`	`fromInt(int value)`
`int`	`getValue()`
`static ProofRule`	`valueOf(java.lang.String name)` Returns the enum constant of this type with the specified name.
`static ProofRule[]`	`values()` Returns an array containing the constants of this enum type, in the order they are declared.

Methods inherited from class java.lang.Enum
clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait

- Enum Constant Detail
  - ASSUME
```
public static final ProofRule ASSUME
```
    Assumption (a leaf) \[ \inferrule{- \mid F}{F} \] This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified. An assume leaf is analogous to a free variable in a term, where we say "F is a free assumption in proof P" if it contains an application of F that is not bound by SCOPE <cvc5.SCOPE> (see below).
  - SCOPE
```
public static final ProofRule SCOPE
```
    Scope (a binder for assumptions) \[ \inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$} \] This rule has a dual purpose with ASSUME <cvc5.ASSUME>. It is a way to close assumptions in a proof. We require that $F_1 \dots F_n$ are free assumptions in P and say that $F_1 \dots F_n$ are not free in (SCOPE P). In other words, they are bound by this application. For example, the proof node: (SCOPE (ASSUME F) :args F) has the conclusion $F \Rightarrow F$ and has no free assumptions. More generally, a proof with no free assumptions always concludes a valid formula.
  - SUBS
```
public static final ProofRule SUBS
```
    Builtin theory – Substitution \[ \inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)} \] where $\sigma_{ids}(F_i)$ are substitutions, which notice are applied in reverse order. Notice that $ids$ is a MethodId identifier, which determines how to convert the formulas $F_1 \dots F_n$ into substitutions. It is an optional argument, where by default the premises are equalities of the form `(= x y)` and converted into substitutions $x\mapsto y$.
  - MACRO_REWRITE
```
public static final ProofRule MACRO_REWRITE
```
    Builtin theory – Rewrite \[ \inferrule{- \mid t, idr}{t = \texttt{rewrite}_{idr}(t)} \] where $idr$ is a MethodId identifier, which determines the kind of rewriter to apply, e.g., Rewriter.rewrite.
  - EVALUATE
```
public static final ProofRule EVALUATE
```
    Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{evaluate}(t)} \] where $\texttt{evaluate}$ is implemented by calling the method $\texttt{Evalutor::evaluate}$ in :cvc5src:`theory/evaluator.h` with an empty substitution. Note this is equivalent to: (REWRITE t {@link MethodId#RW_EVALUATE)}. Note this proof rule only applies to atomic sorts, that is, operators on Int, Real, String, Bool or BitVector.
  - DISTINCT_VALUES
```
public static final ProofRule DISTINCT_VALUES
```
    Builtin theory – Distinct values \[ \inferrule{- \mid t, s}{\neg t = s} \] where $t$ and $s$ are distinct values. Note that cvc5 internally has a notion of which terms denote "values". This property is implemented for any sort that can appear in equalities. A term denotes a value if and only if it is the canonical representation of a value of that sort. For example, set values are a chain of unions of singleton sets whose elements are also values, where this chain is sorted. Any two distinct values are semantically disequal in all models. In practice, we use this rule only to show the distinctness of non-atomic sort, e.g. Sets, Sequences, Datatypes, Arrays, etc. Note that internally, the notion of value is implemented by the Node.isConst method.
  - ACI_NORM
```
public static final ProofRule ACI_NORM
```
    Builtin theory – associative/commutative/idempotency/identity \ normalization \[ \inferrule{- \mid t = s}{t = s} \] where $t$ and $s$ are equivalent modulo associativity and identity elements, and (optionally) commutativity and idempotency. This method normalizes currently based on two kinds of operators: (1) those that are associative, commutative, idempotent, and have an identity element (examples are or, and, bvand), (2) those that are associative, commutative and have an identity element (bvxor), (3) those that are associative and have an identity element (examples are concat, str.++, re.++). This is implemented internally by checking that $\texttt{expr::isACINorm(t, s)} = \top$. For details, see :cvc5src:`expr/aci_norm.h`.
  - ABSORB
```
public static final ProofRule ABSORB
```
    Builtin theory – absorb \[ \inferrule{- \mid t = z}{t = z} \] where $t$ contains $z$ as a subterm, where $z$ is a zero element. In particular, $t$ is expected to be an application of a function with a zero element $z$, and $z$ is contained as a subterm of $t$ beneath applications of that function. For example, this may show that $(A \wedge ( B \wedge \bot)) = \bot$. This is implemented internally by checking that $\texttt{expr::isAbsorb(t, z)} = \top$. For details, see :cvc5src:`expr/aci_norm.h`.
  - MACRO_SR_EQ_INTRO
```
public static final ProofRule MACRO_SR_EQ_INTRO
```
    Builtin theory – Substitution + Rewriting equality introduction In this rule, we provide a term $t$ and conclude that it is equal to its rewritten form under a (proven) substitution. \[ \inferrule{F_1 \dots F_n \mid t, (ids (ida (idr)?)?)?}{t = \texttt{rewrite}_{idr}(t \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))} \] In other words, from the point of view of Skolem forms, this rule transforms $t$ to $t'$ by standard substitution + rewriting. The arguments $ids$, $ida$ and $idr$ are optional and specify the identifier of the substitution, the substitution application and rewriter respectively to be used. For details, see :cvc5src:`theory/builtin/proof_checker.h`.
  - MACRO_SR_PRED_INTRO
```
public static final ProofRule MACRO_SR_PRED_INTRO
```
    Builtin theory – Substitution + Rewriting predicate introduction In this rule, we provide a formula $F$ and conclude it, under the condition that it rewrites to true under a proven substitution. \[ \inferrule{F_1 \dots F_n \mid F, (ids (ida (idr)?)?)?}{F} \] where $\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \top$ and $ids$ and $idr$ are method identifiers. More generally, this rule also holds when $\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \top$ where $F'$ is the result of the left hand side of the equality above. Here, notice that we apply rewriting on the original form of $F'$, meaning that this rule may conclude an $F$ whose Skolem form is justified by the definition of its (fresh) Skolem variables. For example, this rule may justify the conclusion $k = t$ where $k$ is the purification Skolem for $t$, e.g. where the original form of $k$ is $t$. Furthermore, notice that the rewriting and substitution is applied only within the side condition, meaning the rewritten form of the original form of $F$ does not escape this rule.
  - MACRO_SR_PRED_ELIM
```
public static final ProofRule MACRO_SR_PRED_ELIM
```
    Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))} \] where $ids$ and $idr$ are method identifiers. We rewrite only on the Skolem form of $F$, similar to MACRO_SR_EQ_INTRO <cvc5.MACRO_SR_EQ_INTRO>.
  - MACRO_SR_PRED_TRANSFORM
```
public static final ProofRule MACRO_SR_PRED_TRANSFORM
```
    Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G} \] where \[ \texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ\cdots \circ \sigma_{ids, ida}(F_1)) =\\ \texttt{rewrite}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) \] More generally, this rule also holds when: $\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))$ where $F'$ and $G'$ are the result of each side of the equation above. Here, original forms are used in a similar manner to MACRO_SR_PRED_INTRO <cvc5.MACRO_SR_PRED_INTRO> above.
  - ENCODE_EQ_INTRO
```
public static final ProofRule ENCODE_EQ_INTRO
```
    Builtin theory – Encode equality introduction \[ \inferrule{- \mid t}{t=t'} \] where $t$ and $t'$ are equivalent up to their encoding in an external proof format. More specifically, it is the case that $\texttt{RewriteDbNodeConverter::postConvert}(t) = t;$. This conversion method for instance may drop user patterns from quantified formulas or change the representation of $t$ in a way that is a no-op in external proof formats. Note this rule can be treated as a REFL <cvc5.REFL> when appropriate in external proof formats.
  - DSL_REWRITE
```
public static final ProofRule DSL_REWRITE
```
    Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where `id` is a ProofRewriteRule whose definition in the RARE DSL is $\forall x_1 \dots x_n. (G_1 \wedge G_n) \Rightarrow G$ where for $i=1, \dots n$, we have that $F_i = \sigma(G_i)$ and $F = \sigma(G)$ where $\sigma$ is the substitution $\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}$. Notice that the application of the substitution takes into account the possible list semantics of variables $x_1 \ldots x_n$. If $x_i$ is a variable with list semantics, then $t_i$ denotes a list of terms. The substitution implemented by $\texttt{expr::narySubstitute}$ (for details, see :cvc5src:`expr/nary_term_util.h`) which replaces each $x_i$ with the list $t_i$ in its place.
  - THEORY_REWRITE
```
public static final ProofRule THEORY_REWRITE
```
    Other theory rewrite rules \[ \inferrule{- \mid id, t = t'}{t = t'} \] where `id` is the ProofRewriteRule of the theory rewrite rule which transforms $t$ to $t'$. In contrast to DSL_REWRITE, theory rewrite rules used by this proof rule are not necessarily expressible in RARE. Each rule that can be used in this proof rule are documented explicitly in cases within the ProofRewriteRule enum.
  - ITE_EQ
```
public static final ProofRule ITE_EQ
```
    Processing rules – If-then-else equivalence \[ \inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}} \]
  - TRUST
```
public static final ProofRule TRUST
```
    Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where $tid$ is an identifier and $F$ is a formula. This rule is used when a formal justification of an inference step cannot be provided. The formulas $F_1 \dots F_n$ refer to a set of formulas that entail $F$, which may or may not be provided.
  - TRUST_THEORY_REWRITE
```
public static final ProofRule TRUST_THEORY_REWRITE
```
    Trusted rules – Theory rewrite \[ \inferrule{- \mid F, tid, rid}{F} \] where $F$ is an equality of the form $t = t'$ where $t'$ is obtained by applying the kind of rewriting given by the method identifier $rid$, which is one of: RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT. Notice that the checker for this rule does not replay the rewrite to ensure correctness, since theory rewriter methods are not static. For example, the quantifiers rewriter involves constructing new bound variables that are not guaranteed to be consistent on each call.
  - SAT_REFUTATION
```
public static final ProofRule SAT_REFUTATION
```
    SAT Refutation for assumption-based unsat cores \[ \inferrule{F_1 \dots F_n \mid -}{\bot} \] where $F_1 \dots F_n$ correspond to the unsat core determined by the SAT solver.
  - DRAT_REFUTATION
```
public static final ProofRule DRAT_REFUTATION
```
    DRAT Refutation \[ \inferrule{F_1 \dots F_n \mid D, P}{\bot} \] where $F_1 \dots F_n$ correspond to the clauses in the DIMACS file given by filename `D` and `P` is a filename of a file storing a DRAT proof.
  - SAT_EXTERNAL_PROVE
```
public static final ProofRule SAT_EXTERNAL_PROVE
```
    SAT external prove Refutation \[ \inferrule{F_1 \dots F_n \mid D}{\bot} \] where $F_1 \dots F_n$ correspond to the input clauses in the DIMACS file `D`.
  - RESOLUTION
```
public static final ProofRule RESOLUTION
```
    Boolean – Resolution \[ \inferrule{C_1, C_2 \mid pol, L}{C} \] where
    - $C_1$ and $C_2$ are nodes viewed as clauses, i.e., either an OR node with each children viewed as a literal or a node viewed as a literal. Note that an OR node could also be a literal.
    - $pol$ is either true or false, representing the polarity of the pivot on the first clause
    - $L$ is the pivot of the resolution, which occurs as is (resp. under a NOT) in $C_1$ and negatively (as is) in $C_2$ if $pol = \top$ ($pol = \bot$).
    $C$ is a clause resulting from collecting all the literals in $C_1$, minus the first occurrence of the pivot or its negation, and $C_2$, minus the first occurrence of the pivot or its negation, according to the policy above. If the resulting clause has a single literal, that literal itself is the result; if it has no literals, then the result is false; otherwise it's an OR node of the resulting literals. Note that it may be the case that the pivot does not occur in the clauses. In this case the rule is not unsound, but it does not correspond to resolution but rather to a weakening of the clause that did not have a literal eliminated.
  - CHAIN_RESOLUTION
```
public static final ProofRule CHAIN_RESOLUTION
```
    Boolean – N-ary Resolution \[ \inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C} \] where
    - let $C_1 \dots C_n$ be nodes viewed as clauses, as defined above
    - let $C_1 \diamond_{L,pol} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined above
    - let $C_1' = C_1$,
    - for each $i > 1$, let $C_i' = C_{i-1} \diamond_{L_{i-1}, pol_{i-1}} C_i'$
    Note the list of polarities and pivots are provided as s-expressions. The result of the chain resolution is $C = C_n'$
  - FACTORING
```
public static final ProofRule FACTORING
```
    Boolean – Factoring \[ \inferrule{C_1 \mid -}{C_2} \] where $C_2$ is the clause $C_1$, but every occurrence of a literal after its first occurrence is omitted.
  - REORDERING
```
public static final ProofRule REORDERING
```
    Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the multiset representations of $C_1$ and $C_2$ are the same.
  - MACRO_RESOLUTION
```
public static final ProofRule MACRO_RESOLUTION
```
    Boolean – N-ary Resolution + Factoring + Reordering \[ \inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C} \] where
    - let $C_1 \dots C_n$ be nodes viewed as clauses, as defined in RESOLUTION <cvc5.RESOLUTION>
    - let $C_1 \diamond_{L,\mathit{pol}} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined in RESOLUTION <cvc5.RESOLUTION>
    - let $C_1'$ be equal, in its set representation, to $C_1$,
    - for each $i > 1$, let $C_i'$ be equal, in its set representation, to $C_{i-1} \diamond_{L_{i-1},\mathit{pol}_{i-1}} C_i'$
    The result of the chain resolution is $C$, which is equal, in its set representation, to $C_n'$
  - MACRO_RESOLUTION_TRUST
```
public static final ProofRule MACRO_RESOLUTION_TRUST
```
    Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as MACRO_RESOLUTION <cvc5.MACRO_RESOLUTION>, but not checked by the internal proof checker.
  - SPLIT
```
public static final ProofRule SPLIT
```
    Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
  - EQ_RESOLVE
```
public static final ProofRule EQ_RESOLVE
```
    Boolean – Equality resolution \[ \inferrule{F_1, (F_1 = F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for EQUIV_ELIM1 <cvc5.EQUIV_ELIM1> + RESOLUTION <cvc5.RESOLUTION>.
  - MODUS_PONENS
```
public static final ProofRule MODUS_PONENS
```
    Boolean – Modus Ponens \[ \inferrule{F_1, (F_1 \rightarrow F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for IMPLIES_ELIM <cvc5.IMPLIES_ELIM> + RESOLUTION <cvc5.RESOLUTION>.
  - NOT_NOT_ELIM
```
public static final ProofRule NOT_NOT_ELIM
```
    Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
  - CONTRA
```
public static final ProofRule CONTRA
```
    Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
  - AND_ELIM
```
public static final ProofRule AND_ELIM
```
    Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
  - AND_INTRO
```
public static final ProofRule AND_INTRO
```
    Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
  - NOT_OR_ELIM
```
public static final ProofRule NOT_OR_ELIM
```
    Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
  - IMPLIES_ELIM
```
public static final ProofRule IMPLIES_ELIM
```
    Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]
  - NOT_IMPLIES_ELIM1
```
public static final ProofRule NOT_IMPLIES_ELIM1
```
    Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
  - NOT_IMPLIES_ELIM2
```
public static final ProofRule NOT_IMPLIES_ELIM2
```
    Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
  - EQUIV_ELIM1
```
public static final ProofRule EQUIV_ELIM1
```
    Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
  - EQUIV_ELIM2
```
public static final ProofRule EQUIV_ELIM2
```
    Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
  - NOT_EQUIV_ELIM1
```
public static final ProofRule NOT_EQUIV_ELIM1
```
    Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
  - NOT_EQUIV_ELIM2
```
public static final ProofRule NOT_EQUIV_ELIM2
```
    Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
  - XOR_ELIM1
```
public static final ProofRule XOR_ELIM1
```
    Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]
  - XOR_ELIM2
```
public static final ProofRule XOR_ELIM2
```
    Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
  - NOT_XOR_ELIM1
```
public static final ProofRule NOT_XOR_ELIM1
```
    Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
  - NOT_XOR_ELIM2
```
public static final ProofRule NOT_XOR_ELIM2
```
    Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
  - ITE_ELIM1
```
public static final ProofRule ITE_ELIM1
```
    Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
  - ITE_ELIM2
```
public static final ProofRule ITE_ELIM2
```
    Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
  - NOT_ITE_ELIM1
```
public static final ProofRule NOT_ITE_ELIM1
```
    Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
  - NOT_ITE_ELIM2
```
public static final ProofRule NOT_ITE_ELIM2
```
    Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
  - NOT_AND
```
public static final ProofRule NOT_AND
```
    Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
  - CNF_AND_POS
```
public static final ProofRule CNF_AND_POS
```
    Boolean – CNF – And Positive \[ \inferrule{- \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i} \]
  - CNF_AND_NEG
```
public static final ProofRule CNF_AND_NEG
```
    Boolean – CNF – And Negative \[ \inferrule{- \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n} \]
  - CNF_OR_POS
```
public static final ProofRule CNF_OR_POS
```
    Boolean – CNF – Or Positive \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n} \]
  - CNF_OR_NEG
```
public static final ProofRule CNF_OR_NEG
```
    Boolean – CNF – Or Negative \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i} \]
  - CNF_IMPLIES_POS
```
public static final ProofRule CNF_IMPLIES_POS
```
    Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]
  - CNF_IMPLIES_NEG1
```
public static final ProofRule CNF_IMPLIES_NEG1
```
    Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]
  - CNF_IMPLIES_NEG2
```
public static final ProofRule CNF_IMPLIES_NEG2
```
    Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]
  - CNF_EQUIV_POS1
```
public static final ProofRule CNF_EQUIV_POS1
```
    Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]
  - CNF_EQUIV_POS2
```
public static final ProofRule CNF_EQUIV_POS2
```
    Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]
  - CNF_EQUIV_NEG1
```
public static final ProofRule CNF_EQUIV_NEG1
```
    Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]
  - CNF_EQUIV_NEG2
```
public static final ProofRule CNF_EQUIV_NEG2
```
    Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]
  - CNF_XOR_POS1
```
public static final ProofRule CNF_XOR_POS1
```
    Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]
  - CNF_XOR_POS2
```
public static final ProofRule CNF_XOR_POS2
```
    Boolean – CNF – XOR Positive 2 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2} \]
  - CNF_XOR_NEG1
```
public static final ProofRule CNF_XOR_NEG1
```
    Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]
  - CNF_XOR_NEG2
```
public static final ProofRule CNF_XOR_NEG2
```
    Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]
  - CNF_ITE_POS1
```
public static final ProofRule CNF_ITE_POS1
```
    Boolean – CNF – ITE Positive 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1} \]
  - CNF_ITE_POS2
```
public static final ProofRule CNF_ITE_POS2
```
    Boolean – CNF – ITE Positive 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2} \]
  - CNF_ITE_POS3
```
public static final ProofRule CNF_ITE_POS3
```
    Boolean – CNF – ITE Positive 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2} \]
  - CNF_ITE_NEG1
```
public static final ProofRule CNF_ITE_NEG1
```
    Boolean – CNF – ITE Negative 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1} \]
  - CNF_ITE_NEG2
```
public static final ProofRule CNF_ITE_NEG2
```
    Boolean – CNF – ITE Negative 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2} \]
  - CNF_ITE_NEG3
```
public static final ProofRule CNF_ITE_NEG3
```
    Boolean – CNF – ITE Negative 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2} \]
  - REFL
```
public static final ProofRule REFL
```
    Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
  - SYMM
```
public static final ProofRule SYMM
```
    Equality – Symmetry \[ \inferrule{t_1 = t_2\mid -}{t_2 = t_1} \] or \[ \inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1} \]
  - TRANS
```
public static final ProofRule TRANS
```
    Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
  - CONG
```
public static final ProofRule CONG
```
    Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used when the kind of $f(t_1,\dots, t_n)$ has a fixed arity. This includes kinds such as cvc5.Kind.ITE, cvc5.Kind.EQUAL, as well as indexed functions such as cvc5.Kind.BITVECTOR_EXTRACT. It is also used for cvc5.Kind.APPLY_UF, where $f$ is an uninterpreted function. It is not used for kinds with variadic arity, or for kind cvc5.Kind.HO_APPLY, which respectively use the rules NARY_CONG <cvc5.NARY_CONG> and HO_CONG <cvc5.HO_CONG> below.
  - NARY_CONG
```
public static final ProofRule NARY_CONG
```
    Equality – N-ary Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used for terms $f(t_1,\dots, t_n)$ whose kinds $k$ have variadic arity, such as cvc5.Kind.AND, cvc5.Kind.PLUS and so on.
  - TRUE_INTRO
```
public static final ProofRule TRUE_INTRO
```
    Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
  - TRUE_ELIM
```
public static final ProofRule TRUE_ELIM
```
    Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
  - FALSE_INTRO
```
public static final ProofRule FALSE_INTRO
```
    Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]
  - FALSE_ELIM
```
public static final ProofRule FALSE_ELIM
```
    Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]
  - HO_APP_ENCODE
```
public static final ProofRule HO_APP_ENCODE
```
    Equality – Higher-order application encoding \[ \inferrule{-\mid t}{t=t'} \] where `t'` is the higher-order application that is equivalent to `t`, as implemented by uf.TheoryUfRewriter.getHoApplyForApplyUf. For details see :cvc5src:`theory/uf/theory_uf_rewriter.h` For example, this rule concludes $f(x,y) = @( @(f,x), y)$, where $@$ is the HO_APPLY kind. Note this rule can be treated as a REFL <cvc5.REFL> when appropriate in external proof formats.
  - HO_CONG
```
public static final ProofRule HO_CONG
```
    Equality – Higher-order congruence \[ \inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)} \] Notice that this rule is only used when the application kind $k$ is either `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.
  - ARRAYS_READ_OVER_WRITE
```
public static final ProofRule ARRAYS_READ_OVER_WRITE
```
    Arrays – Read over write \[ \inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)} \]
  - ARRAYS_READ_OVER_WRITE_CONTRA
```
public static final ProofRule ARRAYS_READ_OVER_WRITE_CONTRA
```
    Arrays – Read over write, contrapositive \[ \inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2} \]
  - ARRAYS_READ_OVER_WRITE_1
```
public static final ProofRule ARRAYS_READ_OVER_WRITE_1
```
    Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
  - ARRAYS_EXT
```
public static final ProofRule ARRAYS_EXT
```
    Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where $k$ is the $\texttt{ARRAY_DEQ_DIFF}$ skolem for `(a, b)`.
  - MACRO_BV_BITBLAST
```
public static final ProofRule MACRO_BV_BITBLAST
```
    Bit-vectors – (Macro) Bitblast \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] where $\texttt{bitblast}$ represents the result of the bit-blasted term as a bit-vector consisting of the output bits of the bit-blasted circuit representation of the term. Terms are bit-blasted according to the strategies defined in :cvc5src:`theory/bv/bitblast/bitblast_strategies_template.h`.
  - BV_BITBLAST_STEP
```
public static final ProofRule BV_BITBLAST_STEP
```
    Bit-vectors – Bitblast bit-vector constant, variable, and terms For constant and variables: \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] For terms: \[ \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)} \] where $t$ is $k(t_1,\dots,t_n)$.
  - BV_EAGER_ATOM
```
public static final ProofRule BV_EAGER_ATOM
```
    Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where $F$ is of kind BITVECTOR_EAGER_ATOM.
  - BV_POLY_NORM
```
public static final ProofRule BV_POLY_NORM
```
    Bit-vectors – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top$. This method normalizes polynomials $s$ and $t$ over bitvectors.
  - BV_POLY_NORM_EQ
```
public static final ProofRule BV_POLY_NORM_EQ
```
    Bit-vectors – Polynomial normalization for relations .. math. \inferrule{c_x \cdot (x_1 - x_2) = c_y \cdot (y_1 - y_2) \mid (x_1 = x_2) = (y_1 = y_2)} {(x_1 = x_2) = (y_1 = y_2)} $c_x$ and $c_y$ are scaling factors, currently required to be one.
  - DT_SPLIT
```
public static final ProofRule DT_SPLIT
```
    Datatypes – Split \[ \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)} \] where $C_1,\dots,C_n$ are all the constructors of the type of $t$.
  - SKOLEM_INTRO
```
public static final ProofRule SKOLEM_INTRO
```
    Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where $t$ is the unpurified form of skolem $k$.
  - SKOLEMIZE
```
public static final ProofRule SKOLEMIZE
```
    Quantifiers – Skolemization \[ \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} \] where $\sigma$ maps $x_1,\dots,x_n$ to their representative skolems, which are skolems $k_1,\dots,k_n$. For each $k_i$, its skolem identifier is QUANTIFIERS_SKOLEMIZE <cvc5.SkolemId.QUANTIFIERS_SKOLEMIZE>, and its indices are $(\forall x_1\dots x_n.\> F)$ and $x_i$.
  - INSTANTIATE
```
public static final ProofRule INSTANTIATE
```
    Quantifiers – Instantiation \[ \inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The list of terms to instantiate $(t_1 \dots t_n)$ is provided as an s-expression as the first argument. The optional argument $id$ indicates the inference id that caused the instantiation. The term $t$ indicates an additional term (e.g. the trigger) associated with the instantiation, which depends on the id. If the id has prefix QUANTIFIERS_INST_E_MATCHING, then $t$ is the trigger that generated the instantiation.
  - ALPHA_EQUIV
```
public static final ProofRule ALPHA_EQUIV
```
    Quantifiers – Alpha equivalence \[ \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} \] Notice that this rule is correct only when $z_1,\dots,z_n$ are not contained in $FV(F) \setminus \{ y_1,\dots, y_n \}$, where $FV(F)$ are the free variables of $F$. The internal quantifiers proof checker does not currently check that this is the case.
  - QUANT_VAR_REORDERING
```
public static final ProofRule QUANT_VAR_REORDERING
```
    Quantifiers – Variable reordering \[ \inferrule{-\mid (\forall X.\> F) = (\forall Y.\> F)} {(\forall X.\> F) = (\forall Y.\> F)} \] where $Y$ is a reordering of $X$.
  - EXISTS_STRING_LENGTH
```
public static final ProofRule EXISTS_STRING_LENGTH
```
    Quantifiers – Exists string length \[ \inferrule{-\mid T n i} {\mathit{len}(k) = n} \] where $k$ is a skolem of string or sequence type $T$ and $n$ is a non-negative integer. The argument $i$ is an identifier for $k$. These three arguments are the indices of $k$, whose skolem identifier is WITNESS_STRING_LENGTH <cvc5.SkolemId.WITNESS_STRING_LENGTH>.
  - SETS_SINGLETON_INJ
```
public static final ProofRule SETS_SINGLETON_INJ
```
    Sets – Singleton injectivity \[ \inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid -}{t=s} \]
  - SETS_EXT
```
public static final ProofRule SETS_EXT
```
    Sets – Sets extensionality \[ \inferrule{a \neq b\mid -} {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)} \] where $k$ is the $\texttt{SETS_DEQ_DIFF}$ skolem for `(a, b)`.
  - SETS_FILTER_UP
```
public static final ProofRule SETS_FILTER_UP
```
    Sets – Sets filter up \[ \inferrule{\mathit{set.member}(x,a)\mid P} {\mathit{set.member}(x, \mathit{set.filter}(P, a)) = P(x)} \]
  - SETS_FILTER_DOWN
```
public static final ProofRule SETS_FILTER_DOWN
```
    Sets – Sets filter down \[ \inferrule{\mathit{set.member}(x,\mathit{set.filter}(P, a))\mid -} {\mathit{set.member}(x,a) \wedge P(x)} \]
  - CONCAT_EQ
```
public static final ProofRule CONCAT_EQ
```
    Strings – Core rules – Concatenation equality \[ \inferrule{(t_1 \cdot \ldots \cdot t_n \cdot t) = (t_1 \cdot \ldots \cdot t_n \cdot s)\mid \bot}{t = s} \] Alternatively for the reverse: \inferrule{(t \cdot t_1 \cdot \ldots \cdot t_n) = (s \cdot t_1 \cdot \ldots \cdot t_n)\mid \top}{t = s} Notice that $t$ or $s$ may be empty, in which case they are implicit in the concatenation above. For example, if the premise is $x\cdot z = x$, then this rule, with argument $\bot$, concludes $z = \epsilon$.
  - CONCAT_UNIFY
```
public static final ProofRule CONCAT_UNIFY
```
    Strings – Core rules – Concatenation unification \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1} \] Alternatively for the reverse: \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) = \mathit{len}(s_m)\mid \top}{t_n = s_m} \]
  - CONCAT_SPLIT
```
public static final ProofRule CONCAT_SPLIT
```
    Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid \bot}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0} \] where $r$ is the purification skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$ and $\epsilon$ is the empty string (or sequence). \[ \inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) \neq \mathit{len}(s_m)\mid \top}{((t_n = r \cdot s_m) \vee (s_m = r \cdot t_n)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0} \] where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_n) >= \mathit{len}(s_m), \mathit{pre}(t_n,\mathit{len}(t_n) - \mathit{len}(s_m)), \mathit{pre}(s_m,\mathit{len}(s_m) - \mathit{len}(t_n)))$ and $\epsilon$ is the empty string (or sequence). Above, $\mathit{suf}(x,y)$ is shorthand for $\mathit{substr}(x,y, \mathit{len}(x) - y)$ and $\mathit{pre}(x,y)$ is shorthand for $\mathit{substr}(x,0,y)$.
  - CONCAT_CSPLIT
```
public static final ProofRule CONCAT_CSPLIT
```
    Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (c \cdot t_2 \ldots \cdot s_m),\,\mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)} \] where $r$ is the purification skolem for $\mathit{suf}(t_1,1)$. Alternatively for the reverse: \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots s_{m-1} \cdot c),\,\mathit{len}(t_n) \neq 0\mid \top}{(t_n = r\cdot c)} \] where $r$ is the purification skolem for $\mathit{pre}(t_n,\mathit{len}(t_n) - 1)$.
  - CONCAT_LPROP
```
public static final ProofRule CONCAT_LPROP
```
    Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)} \] where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$. Alternatively for the reverse: \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m)),\, \mathit{len}(t_n) > \mathit{len}(s_m)\mid \top}{(t_n = r \cdot s_m)} \] where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_n) >= \mathit{len}(s_m), \mathit{pre}(t_n,\mathit{len}(t_n) - \mathit{len}(s_m)), \mathit{pre}(s_m,\mathit{len}(s_m) - \mathit{len}(t_n)))$
  - CONCAT_CPROP
```
public static final ProofRule CONCAT_CPROP
```
    Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1 \cdot w_1 \cdot \ldots \cdot t_n) = (w_2 \cdot s_2 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)} \] where $w_1,\,w_2$ are words, $t_3$ is $\mathit{pre}(w_2,p)$, $p$ is $\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)$, and $r$ is the purification skolem for $\mathit{suf}(t_1,\mathit{len}(w_3))$. Note that $\mathit{suf}(w_2,p)$ is the largest suffix of $\mathit{suf}(w_2,1)$ that can contain a prefix of $w_1$; since $t_1$ is non-empty, $w_3$ must therefore be contained in $t_1$. Alternatively for the reverse: \[ \inferrule{(t_1 \cdot \ldots \cdot w_1 \cdot t_n) = (s_1 \cdot \ldots \cdot w_2),\, \mathit{len}(t_n) \neq 0\mid \top}{(t_n = r\cdot t_3)} \] where $w_1,\,w_2$ are words, $t_3$ is $\mathit{substr}(w_2, \mathit{len}(w_2) - p, p)$, $p$ is $\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2) - 1), w_1)$, and $r$ is the purification skolem for $\mathit{pre}(t_n,\mathit{len}(t_n) - \mathit{len}(w_3))$. Note that $\mathit{pre}(w_2, \mathit{len}(w_2) - p)$ is the largest prefix of $\mathit{pre}(w_2, \mathit{len}(w_2) - 1)$ that can contain a suffix of $w_1$; since $t_n$ is non-empty, $w_3$ must therefore be contained in $t_n$.
  - STRING_DECOMPOSE
```
public static final ProofRule STRING_DECOMPOSE
```
    Strings – Core rules – String decomposition \[ \inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n} \] where $w_1$ is the purification skolem for $\mathit{pre}(t,n)$ and $w_2$ is the purification skolem for $\mathit{suf}(t,n)$. Or alternatively for the reverse: \[ \inferrule{\mathit{len}(t) \geq n\mid \top}{t = w_1\cdot w_2 \wedge \mathit{len}(w_2) = n} \] where $w_1$ is the purification skolem for $\mathit{pre}(t,n)$ and $w_2$ is the purification skolem for $\mathit{suf}(t,n)$.
  - STRING_LENGTH_POS
```
public static final ProofRule STRING_LENGTH_POS
```
    Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= \epsilon)\vee \mathit{len}(t) > 0} \]
  - STRING_LENGTH_NON_EMPTY
```
public static final ProofRule STRING_LENGTH_NON_EMPTY
```
    Strings – Core rules – Length non-empty \[ \inferrule{t\neq \epsilon\mid -}{\mathit{len}(t) \neq 0} \]
  - STRING_REDUCTION
```
public static final ProofRule STRING_REDUCTION
```
    Strings – Extended functions – Reduction \[ \inferrule{-\mid t}{R\wedge t = w} \] where $w$ is $\texttt{StringsPreprocess::reduce}(t, R, \dots)$. For details, see :cvc5src:`theory/strings/theory_strings_preprocess.h`. In other words, $R$ is the reduction predicate for extended term $t$, and $w$ is the purification skolem for $t$. Notice that the free variables of $R$ are $w$ and the free variables of $t$.
  - STRING_EAGER_REDUCTION
```
public static final ProofRule STRING_EAGER_REDUCTION
```
    Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where $R$ is $\texttt{TermRegistry::eagerReduce}(t)$. For details, see :cvc5src:`theory/strings/term_registry.h`.
  - RE_INTER
```
public static final ProofRule RE_INTER
```
    Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{re.inter}(R_1,R_2)} \]
  - RE_CONCAT
```
public static final ProofRule RE_CONCAT
```
    Strings – Regular expressions – Concatenation \[ \inferrule{t_1\in R_1,\,\ldots,\,t_n\in R_n\mid -}{\text{str.++}(t_1, \ldots, t_n)\in \text{re.++}(R_1, \ldots, R_n)} \]
  - RE_UNFOLD_POS
```
public static final ProofRule RE_UNFOLD_POS
```
    Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{F} \] where $F$ corresponds to the one-step unfolding of the premise. This is implemented by $\texttt{RegExpOpr::reduceRegExpPos}(t\in R)$.
  - RE_UNFOLD_NEG
```
public static final ProofRule RE_UNFOLD_NEG
```
    Strings – Regular expressions – Negative Unfold \[ \inferrule{t \not \in \mathit{re}.\text{*}(R) \mid -}{t \neq \ \epsilon \ \wedge \forall L. L \leq 0 \vee \mathit{str.len}(t) < L \vee \mathit{pre}(t, L) \not \in R \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{*}(R)} \] Or alternatively for regular expression concatenation: \[ \inferrule{t \not \in \mathit{re}.\text{++}(R_1, \ldots, R_n)\mid -}{\forall L. L < 0 \vee \mathit{str.len}(t) < L \vee \mathit{pre}(t, L) \not \in R_1 \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{++}(R_2, \ldots, R_n)} \] Note that in either case the varaible $L$ has type $Int$ and name `"@var.str_index"`.
  - RE_UNFOLD_NEG_CONCAT_FIXED
```
public static final ProofRule RE_UNFOLD_NEG_CONCAT_FIXED
```
    Strings – Regular expressions – Unfold negative concatenation, fixed .. math. \inferrule{t\not\in \mathit{re}.\text{re.++}(r_1, \ldots, r_n) \mid \bot}{ \mathit{pre}(t, L) \not \in r_1 \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{re.++}(r_2, \ldots, r_n)} where $r_1$ has fixed length $L$. or alternatively for the reverse: \[ \inferrule{t \not \in \mathit{re}.\text{re.++}(r_1, \ldots, r_n) \mid \top}{ \mathit{suf}(t, str.len(t) - L) \not \in r_n \vee \mathit{pre}(t, str.len(t) - L) \not \in \mathit{re}.\text{re.++}(r_1, \ldots, r_{n-1})} \] where $r_n$ has fixed length $L$.
  - STRING_CODE_INJ
```
public static final ProofRule STRING_CODE_INJ
```
    Strings – Code points \[ \inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t = s} \]
  - STRING_SEQ_UNIT_INJ
```
public static final ProofRule STRING_SEQ_UNIT_INJ
```
    Strings – Sequence unit \[ \inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y} \] Also applies to the case where $\mathit{unit}(y)$ is a constant sequence of length one.
  - STRING_EXT
```
public static final ProofRule STRING_EXT
```
    Strings – Extensionality \[ \inferrule{s \neq t\mid -} {\mathit{seq.len}(s) \neq \mathit{seq.len}(t) \vee (\mathit{seq.nth}(s,k)\neq\mathit{set.nth}(t,k) \wedge 0 \leq k \wedge k < \mathit{seq.len}(s))} \] where $s,t$ are terms of sequence type, $k$ is the $\texttt{STRINGS_DEQ_DIFF}$ skolem for $s,t$. Alternatively, if $s,t$ are terms of string type, we use $\mathit{seq.substr}(s,k,1)$ instead of $\mathit{seq.nth}(s,k)$ and similarly for $t$.
  - MACRO_STRING_INFERENCE
```
public static final ProofRule MACRO_STRING_INFERENCE
```
    Strings – (Macro) String inference \[ \inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F} \] used to bookkeep an inference that has not yet been converted via $\texttt{strings::InferProofCons::convert}$.
  - MACRO_ARITH_SCALE_SUM_UB
```
public static final ProofRule MACRO_ARITH_SCALE_SUM_UB
```
    Arithmetic – Adding inequalities An arithmetic literal is a term of the form $p \diamond c$ where $\diamond \in \{ <, \leq, =, \geq, > \}$, $p$ a polynomial and $c$ a rational constant. \[ \inferrule{l_1 \dots l_n \mid k_1 \dots k_n}{t_1 \diamond t_2} \] where $k_i \in \mathbb{R}, k_i \neq 0$, $\diamond$ is the fusion of the $\diamond_i$ (flipping each if its $k_i$ is negative) such that $\diamond_i \in \{ <, \leq \}$ (this implies that lower bounds have negative $k_i$ and upper bounds have positive $k_i$), $t_1$ is the sum of the scaled polynomials and $t_2$ is the sum of the scaled constants: \[ t_1 \colon= k_1 \cdot p_1 + \cdots + k_n \cdot p_n t_2 \colon= k_1 \cdot c_1 + \cdots + k_n \cdot c_n \]
  - ARITH_MULT_ABS_COMPARISON
```
public static final ProofRule ARITH_MULT_ABS_COMPARISON
```
    Arithmetic – Non-linear multiply absolute value comparison \[ \inferrule{F_1 \dots F_n \mid -}{F} \] where $F$ is of the form $\left| t_1 \cdot t_n \right| \diamond \left| s_1 \cdot s_n \right|$. If $\diamond$ is $=$, then each $F_i$ is $\left| t_i \right| = \left| s_i \right|$. If $\diamond$ is $>$, then each $F_i$ is either $\left| t_i \right| > \left| s_i \right|$ or $\left| t_i \right| = \left| s_i \right| \land t_i \neq 0$, and $F_1$ is of the former form.
  - ARITH_SUM_UB
```
public static final ProofRule ARITH_SUM_UB
```
    Arithmetic – Sum upper bounds \[ \inferrule{P_1 \dots P_n \mid -}{L \diamond R} \] where $P_i$ has the form $L_i \diamond_i R_i$ and $\diamond_i \in \{<, \leq, =\}$. Furthermore $\diamond = <$ if $\diamond_i = <$ for any $i$ and $\diamond = \leq$ otherwise, $L = L_1 + \cdots + L_n$ and $R = R_1 + \cdots + R_n$.
  - INT_TIGHT_UB
```
public static final ProofRule INT_TIGHT_UB
```
    Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where $i$ has integer type.
  - INT_TIGHT_LB
```
public static final ProofRule INT_TIGHT_LB
```
    Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where $i$ has integer type.
  - ARITH_TRICHOTOMY
```
public static final ProofRule ARITH_TRICHOTOMY
```
    Arithmetic – Trichotomy of the reals \[ \inferrule{A, B \mid -}{C} \] where $\neg A, \neg B, C$ are $x < c, x = c, x > c$ in some order. Note that $\neg$ here denotes arithmetic negation, i.e., flipping $\geq$ to $<$ etc.
  - ARITH_REDUCTION
```
public static final ProofRule ARITH_REDUCTION
```
    Arithmetic – Reduction \[ \inferrule{- \mid t}{F} \] where $t$ is an application of an extended arithmetic operator (e.g. division, modulus, cosine, sqrt, is_int, to_int) and $F$ is the reduction predicate for $t$. In other words, $F$ is a predicate that is used to reduce reasoning about $t$ to reasoning about the core operators of arithmetic. In detail, $F$ is implemented by $\texttt{arith::OperatorElim::getAxiomFor(t)}$, see :cvc5src:`theory/arith/operator_elim.h`.
  - ARITH_POLY_NORM
```
public static final ProofRule ARITH_POLY_NORM
```
    Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top$. This method normalizes polynomials $s$ and $t$ over arithmetic.
  - ARITH_POLY_NORM_REL
```
public static final ProofRule ARITH_POLY_NORM_REL
```
    Arithmetic – Polynomial normalization for relations .. math. \inferrule{c_x \cdot (x_1 - x_2) = c_y \cdot (y_1 - y_2) \mid (x_1 \diamond x_2) = (y_1 \diamond y_2)} {(x_1 \diamond x_2) = (y_1 \diamond y_2)} where $\diamond \in \{<, \leq, =, \geq, >\}$. $c_x$ and $c_y$ are scaling factors. For $<, \leq, \geq, >$, the scaling factors have the same sign. If $c_x$ has type $Real$ and $x_1, x_2$ are of type $Int$, then $(x_1 - x_2)$ is wrapped in an application of `to_real`, similarly for $(y_1 - y_2)$.
  - ARITH_MULT_SIGN
```
public static final ProofRule ARITH_MULT_SIGN
```
    Arithmetic – Sign inference \[ \inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0} \] where $f_1 \dots f_k$ are variables compared to zero (less, greater or not equal), $m$ is a monomial from these variables and $\diamond$ is the comparison (less or greater) that results from the signs of the variables. In particular, $\diamond$ is :math`<` if $f_1 \dots f_k$ contains an odd number of :math`<`. Otherwise $\diamond$ is :math`>`. All variables with even exponent in $m$ are given as not equal to zero while all variables with odd exponent in $m$ should be given as less or greater than zero.
  - ARITH_MULT_POS
```
public static final ProofRule ARITH_MULT_POS
```
    Arithmetic – Multiplication with positive factor \[ \inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r} \] where $\diamond$ is a relation symbol.
  - ARITH_MULT_NEG
```
public static final ProofRule ARITH_MULT_NEG
```
    Arithmetic – Multiplication with negative factor \[ \inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r} \] where $\diamond$ is a relation symbol and $\diamond_{inv}$ the inverted relation symbol.
  - ARITH_MULT_TANGENT
```
public static final ProofRule ARITH_MULT_TANGENT
```
    Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid x, y, a, b, \sigma}{(t \leq tplane) = ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = \bot$} \inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) = ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = \top$} \] where $x,y$ are real terms (variables or extended terms), $t = x \cdot y$, $a,b$ are real constants, $\sigma \in \{ \top, \bot\}$ and $tplane := b \cdot x + a \cdot y - a \cdot b$ is the tangent plane of $x \cdot y$ at $(a,b)$.
  - ARITH_TRANS_PI
```
public static final ProofRule ARITH_TRANS_PI
```
    Arithmetic – Transcendentals – Assert bounds on Pi \[ \inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u} \] where $l,u$ are valid lower and upper bounds on $\pi$.
  - ARITH_TRANS_EXP_NEG
```
public static final ProofRule ARITH_TRANS_EXP_NEG
```
    Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
  - ARITH_TRANS_EXP_POSITIVITY
```
public static final ProofRule ARITH_TRANS_EXP_POSITIVITY
```
    Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
  - ARITH_TRANS_EXP_SUPER_LIN
```
public static final ProofRule ARITH_TRANS_EXP_SUPER_LIN
```
    Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
  - ARITH_TRANS_EXP_ZERO
```
public static final ProofRule ARITH_TRANS_EXP_ZERO
```
    Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
  - ARITH_TRANS_EXP_APPROX_ABOVE_NEG
```
public static final ProofRule ARITH_TRANS_EXP_APPROX_ABOVE_NEG
```
    Arithmetic – Transcendentals – Exp is approximated from above for \ negative values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$. Let $p$ be the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function. $\texttt{secant}(\exp, l, u, t)$ denotes the secant of $p$ from $(l, \exp(l))$ to $(u, \exp(u))$ evaluated at $t$, calculated as follows: \[ \frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l) \] The lemma states that if $t$ is between $l$ and $u$, then $\exp(t$ is below the secant of $p$ from $l$ to $u$.
  - ARITH_TRANS_EXP_APPROX_ABOVE_POS
```
public static final ProofRule ARITH_TRANS_EXP_APPROX_ABOVE_POS
```
    Arithmetic – Transcendentals – Exp is approximated from above for \ positive values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$. Let $p^*$ be a modification of the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function as follows where $p(d-1)$ is the regular Maclaurin series of degree $d-1$: \[ p^* := p(d-1) \cdot \frac{1 + t^n}{n!} \] $\texttt{secant-pos}(\exp, l, u, t)$ denotes the secant of $p$ from $(l, \exp(l))$ to $(u, \exp(u))$ evaluated at $t$, calculated as follows: \[ \frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l) \] The lemma states that if $t$ is between $l$ and $u$, then $\exp(t$ is below the secant of $p$ from $l$ to $u$.
  - ARITH_TRANS_EXP_APPROX_BELOW
```
public static final ProofRule ARITH_TRANS_EXP_APPROX_BELOW
```
    Arithmetic – Transcendentals – Exp is approximated from below \[ \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)} \] where $d$ is a non-negative number, $t$ an arithmetic term and $\texttt{maclaurin}(\exp, n+1, c)$ is the $(n+1)$'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at $c$ where $n$ is $2 \cdot d$. The Maclaurin series for the exponential function is the following: \[ \exp(x) = \sum_{i=0}^{\infty} \frac{x^i}{i!} \] This rule furthermore requires that $1 > c^{n+1}/(n+1)!$
  - ARITH_TRANS_SINE_BOUNDS
```
public static final ProofRule ARITH_TRANS_SINE_BOUNDS
```
    Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
  - ARITH_TRANS_SINE_SHIFT
```
public static final ProofRule ARITH_TRANS_SINE_SHIFT
```
    Arithmetic – Transcendentals – Sine is shifted to -pi...pi \[ \inferrule{- \mid x}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})} \] where $x$ is the argument to sine, $y$ is a new real skolem that is $x$ shifted into $-\pi \dots \pi$ and $s$ is a new integer skolem that is the number of phases $y$ is shifted. In particular, $y$ is the TRANSCENDENTAL_PURIFY_ARG <cvc5.SkolemId.TRANSCENDENTAL_PURIFY_ARG> skolem for $\sin(x)$ and $s$ is the TRANSCENDENTAL_SINE_PHASE_SHIFT <cvc5.SkolemId.TRANSCENDENTAL_SINE_PHASE_SHIFT> skolem for $x$.
  - ARITH_TRANS_SINE_SYMMETRY
```
public static final ProofRule ARITH_TRANS_SINE_SYMMETRY
```
    Arithmetic – Transcendentals – Sine is symmetric with respect to \ negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
  - ARITH_TRANS_SINE_TANGENT_ZERO
```
public static final ProofRule ARITH_TRANS_SINE_TANGENT_ZERO
```
    Arithmetic – Transcendentals – Sine is bounded by the tangent at zero .. math. \inferrule{- \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0 \rightarrow \sin(t) > t)}
  - ARITH_TRANS_SINE_TANGENT_PI
```
public static final ProofRule ARITH_TRANS_SINE_TANGENT_PI
```
    Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi .. math. \inferrule{- \mid t}{(t > -\pi \rightarrow \sin(t) > -\pi - t) \land (t < \pi \rightarrow \sin(t) < \pi - t)}
  - ARITH_TRANS_SINE_APPROX_ABOVE_NEG
```
public static final ProofRule ARITH_TRANS_SINE_APPROX_ABOVE_NEG
```
    Arithmetic – Transcendentals – Sine is approximated from above for\ negative values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$. Let $p$ be the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the sine function. $\texttt{secant}(\sin, l, u, t)$ denotes the secant of $p$ from $(l, \sin(l))$ to $(u, \sin(u))$ evaluated at $t$, calculated as follows: \[ \frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l) \] The lemma states that if $t$ is between $l$ and $u$, then $\sin(t)$ is below the secant of $p$ from $l$ to $u$.
  - ARITH_TRANS_SINE_APPROX_ABOVE_POS
```
public static final ProofRule ARITH_TRANS_SINE_APPROX_ABOVE_POS
```
    Arithmetic – Transcendentals – Sine is approximated from above for \ positive values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$). Let $p$ be the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the sine function. $\texttt{upper}(\sin, c)$ denotes the upper bound on $\sin(c)$ given by $p$ and $lb,up$ such that $\sin(t)$ is the maximum of the sine function on $(lb,ub)$.
  - ARITH_TRANS_SINE_APPROX_BELOW_NEG
```
public static final ProofRule ARITH_TRANS_SINE_APPROX_BELOW_NEG
```
    Arithmetic – Transcendentals – Sine is approximated from below for \ negative values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$). Let $p$ be the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the sine function. $\texttt{lower}(\sin, c)$ denotes the lower bound on $\sin(c)$ given by $p$ and $lb,up$ such that $\sin(t)$ is the minimum of the sine function on $(lb,ub)$.
  - ARITH_TRANS_SINE_APPROX_BELOW_POS
```
public static final ProofRule ARITH_TRANS_SINE_APPROX_BELOW_POS
```
    Arithmetic – Transcendentals – Sine is approximated from below for \ positive values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb \land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$. Let $p$ be the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the sine function. $\texttt{secant}(\sin, l, u, t)$ denotes the secant of $p$ from $(l, \sin(l))$ to $(u, \sin(u))$ evaluated at $t$, calculated as follows: \[ \frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l) \] The lemma states that if $t$ is between $l$ and $u$, then $\sin(t)$ is above the secant of $p$ from $l$ to $u$.
  - LFSC_RULE
```
public static final ProofRule LFSC_RULE
```
    External – LFSC Place holder for LFSC rules. \[ \inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, A_1,\dots, A_m}{Q} \] Note that the premises and arguments are arbitrary. It's expected that $\texttt{id}$ refer to a proof rule in the external LFSC calculus.
  - ALETHE_RULE
```
public static final ProofRule ALETHE_RULE
```
    External – Alethe Place holder for Alethe rules. \[ \inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q} \] Note that the premises and arguments are arbitrary. It's expected that $\texttt{id}$ refer to a proof rule in the external Alethe calculus, and that $Q'$ be the representation of Q to be printed by the Alethe printer.
  - UNKNOWN
```
public static final ProofRule UNKNOWN
```
    External – Alethe Place holder for Alethe rules. \[ \inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q} \] Note that the premises and arguments are arbitrary. It's expected that $\texttt{id}$ refer to a proof rule in the external Alethe calculus, and that $Q'$ be the representation of Q to be printed by the Alethe printer.
- Method Detail
  - values
```
public static ProofRule[] values()
```
    Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:
```
for (ProofRule c : ProofRule.values())
    System.out.println(c);
```
    Returns:
    
    an array containing the constants of this enum type, in the order they are declared
  - valueOf
```
public static ProofRule valueOf(java.lang.String name)
```
    Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
    
    Parameters:
    
    name - the name of the enum constant to be returned.
    
    Returns:
    
    the enum constant with the specified name
    
    Throws:
    
    java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
    
    java.lang.NullPointerException - if the argument is null
  - fromInt
```
public static ProofRule fromInt(int value)
                         throws CVC5ApiException
```
    Throws:
    
    CVC5ApiException
  - getValue
```
public int getValue()
```

Enum ProofRule

Enum Constant Summary

Method Summary

Methods inherited from class java.lang.Enum

Methods inherited from class java.lang.Object

Enum Constant Detail

ASSUME

SCOPE

SUBS

MACRO_REWRITE

EVALUATE

DISTINCT_VALUES

ACI_NORM

ABSORB

MACRO_SR_EQ_INTRO

MACRO_SR_PRED_INTRO

MACRO_SR_PRED_ELIM

MACRO_SR_PRED_TRANSFORM

ENCODE_EQ_INTRO

DSL_REWRITE

THEORY_REWRITE

ITE_EQ

TRUST

TRUST_THEORY_REWRITE

SAT_REFUTATION

DRAT_REFUTATION

SAT_EXTERNAL_PROVE

RESOLUTION

CHAIN_RESOLUTION

FACTORING

REORDERING

MACRO_RESOLUTION

MACRO_RESOLUTION_TRUST

SPLIT

EQ_RESOLVE

MODUS_PONENS

NOT_NOT_ELIM

CONTRA

AND_ELIM

AND_INTRO

NOT_OR_ELIM

IMPLIES_ELIM

NOT_IMPLIES_ELIM1

NOT_IMPLIES_ELIM2

EQUIV_ELIM1

EQUIV_ELIM2

NOT_EQUIV_ELIM1

NOT_EQUIV_ELIM2

XOR_ELIM1

XOR_ELIM2

NOT_XOR_ELIM1

NOT_XOR_ELIM2

ITE_ELIM1

ITE_ELIM2

NOT_ITE_ELIM1

NOT_ITE_ELIM2

NOT_AND

CNF_AND_POS

CNF_AND_NEG

CNF_OR_POS

CNF_OR_NEG

CNF_IMPLIES_POS

CNF_IMPLIES_NEG1

CNF_IMPLIES_NEG2

CNF_EQUIV_POS1

CNF_EQUIV_POS2

CNF_EQUIV_NEG1

CNF_EQUIV_NEG2

CNF_XOR_POS1

CNF_XOR_POS2

CNF_XOR_NEG1

CNF_XOR_NEG2

CNF_ITE_POS1

CNF_ITE_POS2

CNF_ITE_POS3

CNF_ITE_NEG1

CNF_ITE_NEG2

CNF_ITE_NEG3

REFL

SYMM