Definitions: Mathlib.ModelTheory

field axiom (from the name)

The field axioms are a basic type.

the additive associator (from the name)

The additive associator is a field axiom.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the additive associator and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero sum and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{negAddCancel}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the multiplicative associator and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $5$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{mulComm}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one product and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $6$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{existsInv}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $7$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{leftDistrib}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{existsPairNE}$.

$\operatorname{existsInv}$ is a field axiom.

$\operatorname{existsPairNE}$ is a field axiom.

$\operatorname{leftDistrib}$ is a field axiom.

the multiplicative associator (from the name)

The multiplicative associator is a field axiom.

$\operatorname{mulComm}$ is a field axiom.

$\operatorname{negAddCancel}$ is a field axiom.

the one product (from the name)

The one product is a field axiom.

Let $K$ be a set. Let $x_{5}$ be a field axiom. Then we can say that $\operatorname{toProp}$ holds for $K$ and $x_{5}$.

the sentence of x (from the name)

Let $x$ be a field axiom. Then the sentence of $x$ is a sentence of the ring.

the zero sum (from the name)

The zero sum is a field axiom.

the field (from the name)

The field is a theory of the ring defined as the range of $\operatorname{toSentence}$.

Let $n$ be a natural number. Then $\operatorname{eqZero}$ applied to $n$ is a sentence of the ring defined as the equal of $\operatorname{termOfFreeCommRing}$ applied to $n$ and $0$.

the field of p (from the name)

Let $p$ be an element of $\Natural$. Then the field of $p$ is a theory of the ring defined as $\UnionunionMACRoAB {\operatorname{field}}{(\iteMACRoG {\mathrm{Eq} (p , 0)}{\operatorname{image} (\lambda q . \operatorname{not} (\operatorname{eqZero} (q)), \operatorname{ofPred} (\lambda q_{1} . \mathrm{prime} (q_{1})))}{(\iteMACRoG {\mathrm{prime} (p)}{\operatorname{singleton} (\operatorname{eqZero} (p))}{\operatorname{singleton} (\operatorname{bot})})})}$.

the generic monic polynomial of n (from the name)

Let $n$ be a natural number. Then the generic monic polynomial of $n$ is a free commutative ring of $\mathrm{Fin}$ applied to $n + 1$ defined as $\operatorname{of} (\operatorname{last} (n))^ {n}+ \FinsetSum {\FinsetunivMACRoAC}{i}{(\operatorname{of} (\operatorname{castSucc} (i))\times \operatorname{of} (\operatorname{last} (n))^ {\operatorname{val} (i)})}$.

Let $n$ be a natural number. Then $\operatorname{genericMonicPolyHasRoot}$ applied to $n$ is a sentence of the ring defined as $\operatorname{alls}$ applied to $\operatorname{ex}$ applied to $\operatorname{bdEqual}$ applied to $\operatorname{relabel}$ applied to $\operatorname{inr}$ and $\operatorname{termOfFreeCommRing}$ applied to the generic monic polynomial of $n$ and $0$.

Let $p$ be a natural number. Then $\operatorname{ACF}$ applied to $p$ is a theory of the ring defined as the union of the field of $p$ and the image of $\operatorname{genericMonicPolyHasRoot}$ and $\operatorname{ofPred}$ applied to the function that maps $n$ to $\mathrm{Lt} (0 , n)$.

the ring (from the name)

The ring is a language defined as $\operatorname{mk}$ applied to the set of elements of $\operatorname{ringFunc}$ and the function that maps $x$ to $\mathrm{Empty}$.

R is a compatible ring (from the name)

Let $R$ be a set. Then we can say that $R$ is a compatible ring.

the additive function (from the name)

The additive function is a function of the ring and $2$ defined as the sum.

the language equivalence equivalence ring isomorphism (from the name)

The language equivalence equivalence ring isomorphism is an equivalence from the set of equivalences of $R$ and $S$ to the set of ring isomorphisms of $R$ and $S$.

the multiplicative function (from the name)

The multiplicative function is a function of the ring and $2$ defined as the product.

the negation function (from the name)

The negation function is a function of the ring and $1$ defined as the negation.

the one function (from the name)

The one function is a function of the ring and $0$ defined as the one.

the zero function (from the name)

The zero function is a function of the ring and $0$ defined as the zero.

ring function of x (from the name)

Let $x$ be a natural number. Then the ring functions of $x$ are a basic type.

the sum (from the name)

The sum is a ring function of $2$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $2$ and the sum and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $2$ and the product and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $1$ and the negation and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $0$ and the zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $0$ and the one.

the product (from the name)

The product is a ring function of $2$.

the negation (from the name)

The negation is a ring function of $1$.

the one (from the name)

The one is a ring function of $0$.

the zero (from the name)

The zero is a ring function of $0$.

$\operatorname{presburger}$ is a language defined as $\operatorname{mk}$ applied to $\operatorname{presburgerFunc}$ and the function that maps $x$ to $\mathrm{Empty}$.

the sum of s and f (from the name)

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to terms of $\operatorname{presburger}$ and $x$. Then the sum of $s$ and $f$ is a term of $\operatorname{presburger}$ and $x$ defined as $\operatorname{sum}$ applied to $\operatorname{map}$ applied to $f$ and the list of $s$.

Let $x$ be a natural number. Then the elements of $\operatorname{presburgerFunc}$ applied to $x$ are a basic type.

the sum (from the name)

The sum is an element of $\operatorname{presburgerFunc}$ applied to $2$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $0$ and the zero and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $0$ and the one and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $2$ and the sum.

the one (from the name)

The one is an element of $\operatorname{presburgerFunc}$ applied to $0$.

the zero (from the name)

The zero is an element of $\operatorname{presburgerFunc}$ applied to $0$.

s is linear (from the docstring)

Let $s$ be an element of $\wp M$. Then $s$ is linear, if there exists an element $a$ of $M$, such that there exists an element $t$ of $\wp M$, such that $t$ is finite and $s$ is equal to the sum of $a$ and the closure of $t$.

s is proper (from the docstring)

Let $s$ be an element of $\wp M$. Then $s$ is proper, if there exists an element $a$ of $M$, such that there exists an element $t$ of $\wp M$, such that $t$ is finite, $\mathrm{LinearIndepOn}$ holds for $\Natural$, $\mathrm{id}$ and $t$ and $s$ is equal to the sum of $a$ and the closure of $t$.

s is proper (from the docstring)

Let $s$ be an element of $\wp M$. Then $s$ is proper, if there exists an element $S$ of $\wp (\wp M)$, such that $S$ is finite, for all elements $t$ of $\wp M$, if $t$ is an element of $S$, then $t$ is proper and $s$ is equal to the union of $S$.

s is semilinear (from the docstring)

Let $s$ be an element of $\wp M$. Then $s$ is semilinear, if there exists an element $S$ of $\wp (\wp M)$, such that $S$ is finite, for all elements $t$ of $\wp M$, if $t$ is an element of $S$, then $t$ is linear and $s$ is equal to the union of $S$.

the induced structure equivalence of e (from the name)

Let $e$ be an equivalence from $M$ to $N$. Then the induced structure equivalence of $e$ is an equivalence of $M$ and $N$.

language (from the name)

The languages are a basic type.

constant of L (from the name)

Let $L$ be a language. Then a constant of $L$ is an element of the function that maps $L$ to the set of functions of $L$ and $0$.

embedding of M and N (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the embeddings of $M$ and $N$ are a basic type.

the composition of hnp and hmn (from the name)

Let $\mathrm{hnp}$ be an embedding of $N$ and $P$. Let $\mathrm{hmn}$ be an embedding of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an embedding of $M$ and $P$.

the embedding of hf (from the name)

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the embedding of $\mathrm{hf}$ is an embedding of $M$ and $N$.

the identity embedding of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the identity embedding of $L$ and $M$ is an embedding of $M$ and $M$.

the homomorphism of x2 (from the name)

Let $x_{2}$ be an embedding of $M$ and $N$. Then the homomorphism of $x_{2}$ is a homomorphism of $M$ and $N$ defined as the homomorphism of $x_{2}$.

equivalence of M and N (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the equivalences of $M$ and $N$ are a basic type.

the composition of hnp and hmn (from the name)

Let $\mathrm{hnp}$ be an equivalence of $N$ and $P$. Let $\mathrm{hmn}$ be an equivalence of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an equivalence of $M$ and $P$.

the identity equivalence of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the identity equivalence of $L$ and $M$ is an equivalence of $M$ and $M$.

the inverse of f (from the docstring)

Let $f$ be an equivalence of $M$ and $N$. Then the inverse of $f$ is an equivalence of $N$ and $M$.

the embedding of x2 (from the name)

Let $x_{2}$ be an equivalence of $M$ and $N$. Then the embedding of $x_{2}$ is an embedding of $M$ and $N$ defined as the embedding of $x_{2}$.

the homomorphism of x2 (from the name)

Let $x_{2}$ be an equivalence of $M$ and $N$. Then the homomorphism of $x_{2}$ is a homomorphism of $M$ and $N$ defined as the homomorphism of $x_{2}$.

function of self and x (from the name)

Let $\mathrm{self}$ be a language. Let $x$ be a natural number. Then a function of $\mathrm{self}$ and $x$ is an element of the function that maps $\mathrm{self}$ and $x$ to $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

homomorphism of M and N (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the homomorphisms of $M$ and $N$ are a basic type.

the composition of hnp and hmn (from the name)

Let $\mathrm{hnp}$ be a homomorphism of $N$ and $P$. Let $\mathrm{hmn}$ be a homomorphism of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is a homomorphism of $M$ and $P$.

the identity map of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the identity map of $L$ and $M$ is a homomorphism of $M$ and $M$.

the underlying function of self and x2 (from the docstring)

Let $\mathrm{self}$ be a homomorphism of $M$ and $N$. Let $x_{2}$ be an element of $M$. Then the underlying function of $\mathrm{self}$ and $x_{2}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Let $L$ be an element of $\mathrm{outParam}$ applied to the set of languages. Let $F$ be a set. Let $M$ and $N$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\operatorname{HomClass}$ holds for $L$, $F$, $M$ and $N$.

the homomorphism of x3 (from the name)

Let $x_{3}$ be an element of $F$. Then the homomorphism of $x_{3}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $x_{3}$, the function that maps $x_{4}$ to $\mathrm{FirstOrder\_\_Language\_\_HomClass\_\_map\_fun}$ applied to $x_{3}$ and the function that maps $x_{5}$ to $\mathrm{FirstOrder\_\_Language\_\_HomClass\_\_map\_rel}$ applied to $x_{3}$.

L is algebraic (from the name)

Let $L$ be a language. Then $L$ is algebraic, if for all natural numbers $n$, the set of relations of $L$ and $n$ is empty.

L is relational (from the name)

Let $L$ be a language. Then $L$ is relational, if for all natural numbers $n$, the set of functions of $L$ and $n$ is empty.

relation of self and x (from the name)

Let $\mathrm{self}$ be a language. Let $x$ be a natural number. Then a relation of $\mathrm{self}$ and $x$ is an element of the function that maps $\mathrm{self}$ and $x$ to $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.

Let $L$ be an element of $\mathrm{outParam}$ applied to the set of languages. Let $F$ be a set. Let $M$ and $N$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\operatorname{StrongHomClass}$ holds for $L$, $F$, $M$ and $N$.

the embedding of x3 (from the name)

Let $x_{3}$ be an element of $F$. Then the embedding of $x_{3}$ is an embedding of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $x_{3}$ and $\operatorname{injective}$ applied to $x_{3}$, the function that maps $x_{4}$ to $\mathrm{FirstOrder\_\_Language\_\_StrongHomClass\_\_map\_fun}$ applied to $x_{3}$ and the function that maps $x_{5}$ to $\mathrm{FirstOrder\_\_Language\_\_StrongHomClass\_\_map\_rel}$ applied to $x_{3}$.

the equivalence of x3 (from the name)

Let $x_{3}$ be an element of $F$. Then the equivalence of $x_{3}$ is an equivalence of $M$ and $N$.

L is a structure (from the name)

Let $L$ be a language. Let $M$ be a set. Then we can say that $L$ is a structure.

Let $x$ be a relation of $L$ and $n$. Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$. Then $\operatorname{RelMap}$ holds for $x$ and $x_{1}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$, $x$ and $x_{1}$.

the function map of x and x1 (from the name)

Let $x$ be a function of $L$ and $n$. Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$. Then the function map of $x$ and $x_{1}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

symbol of L (from the name)

Let $L$ be a language. Then a symbol of $L$ is an element of the function that maps $L$ to $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $l$ to the set of functions of $L$ and $l$ and $\Sigma$ applied to the function that maps $l_{1}$ to the set of relations of $L$ and $l_{1}$.

the cardinality of L (from the docstring)

Let $L$ be a language. Then the cardinality of $L$ is a cardinal defined as $\operatorname{mk}$ applied to the set of symbols of $L$.

the constant map of c (from the name)

Let $c$ be a constant of $L$. Then the constant map of $c$ is an element of $M$ defined as the function map of $c$ and $\operatorname{default}$.

$\operatorname{empty}$ is a language defined as $\operatorname{mk}$ applied to the function that maps $x$ to $\mathrm{Empty}$ and the function that maps $x_{1}$ to $\mathrm{Empty}$.

the sum of L and #2 (from the name)

Let $L$ and $\mathrm{L'}$ be languages. Then the sum of $L$ and $\mathrm{L'}$ is a language defined as $\operatorname{mk}$ applied to the function that maps $n$ to $\mathrm{Sum}$ applied to the set of functions of $L$ and $n$ and the set of functions of $\mathrm{L'}$ and $n$ and the function that maps $n_{1}$ to $\mathrm{Sum}$ applied to the set of relations of $L$ and $n_{1}$ and the set of relations of $\mathrm{L'}$ and $n_{1}$.

the empty homomorphism of f (from the name)

Let $f$ be a function from elements of $M$ to elements of $N$. Then the empty homomorphism of $f$ is a homomorphism of $M$ and $N$.

Let $L$ be a language. Let $g$ be an equivalence from $M$ to $N$. Then $\operatorname{bundledInduced}$ applied to $L$ and $g$ is an element of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure defined as $\operatorname{mk}$ applied to $N$ and $\operatorname{inducedStructure}$ applied to $g$.

the bundled induced equivalence of L and g (from the name)

Let $L$ be a language. Let $g$ be an equivalence from $M$ to $N$. Then the bundled induced equivalence of $L$ and $g$ is an equivalence of $M$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $\operatorname{bundledInduced}$ applied to $L$ and $g$ defined as the induced structure equivalence of $g$.

the model of T and h (from the name)

the model of T and S (from the name)

Let $T$ be a theory of $L$. Let $S$ be an elementary substructure of $L$ and the set of carriers of $M$. Then the model of $T$ and $S$ is a model type of $T$.

Assume that $T$ is a model. Then $\operatorname{bundled}$ applied to $h$ is a model type of $T$ defined as $\operatorname{of}$ applied to $T$ and $M$.

model type of T (from the name)

Let $T$ be a theory of $L$. Then the model types of $T$ are a basic type.

carrier of self (from the name)

Let $\mathrm{self}$ be a model type of $T$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the default expansion of h and M (from the name)

Assume that $x$ is injective. Let $M$ be a model type of $T$. Then the default expansion of $h$ and $M$ is a model type of $\operatorname{onTheory}$ applied to $x$ and $T$ defined as $\operatorname{mk}$ applied to the set of carriers of $M$.

Let $e$ be an equivalence from the set of carriers of $M$ to $N$. Then $\operatorname{equivInduced}$ applied to $e$ is a model type of $T$ defined as $\operatorname{mk}$ applied to $N$.

Let $T$ be a theory of $L$. Let $M$ be a set. Then $\operatorname{of}$ applied to $T$ and $M$ is a model type of $T$ defined as $\operatorname{mk}$ applied to $M$.

Let $x$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $M$ be a model type of $\operatorname{onTheory}$ applied to $x$ and $T$. Then $\operatorname{reduct}$ applied to $x$ and $M$ is a model type of $T$ defined as $\operatorname{mk}$ applied to the set of carriers of $M$.

the shrink of M (from the name)

Let $M$ be a model type of $T$. Then the shrink of $M$ is a model type of $T$ defined as $\operatorname{equivInduced}$ applied to the equivalence shrink of the set of carriers of $M$.

Let $M$ be a model type of $T$. Assume that $\mathrm{T'} \leq T$. Then $\operatorname{subtheoryModel}$ applied to $M$ and $h$ is a model type of $\mathrm{T'}$ defined as $\operatorname{mk}$ applied to the set of carriers of $M$.

the lift of M (from the name)

Let $M$ be a model type of $T$. Then the lift of $M$ is a model type of $T$ defined as $\operatorname{equivInduced}$ applied to the inverse of the lift.

x1 is atomic (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then we can say that $x_{1}$ is atomic.

x1 is existential (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then we can say that $x_{1}$ is existential.

Assume that $x_{1}$ is existential. Then we can say that $\operatorname{below}$ holds for $t$.

x1 is a prenex (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then we can say that $x_{1}$ is a prenex.

Assume that $x_{1}$ is a prenex. Then we can say that $\operatorname{below}$ holds for $t$.

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then we can say that $\operatorname{IsQF}$ holds for $x_{1}$.

Assume that $\operatorname{IsQF}$ holds for $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

x1 is universal (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then we can say that $x_{1}$ is universal.

Assume that $x_{1}$ is universal. Then we can say that $\operatorname{below}$ holds for $t$.

the prenex of x1 (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then the prenex of $x_{1}$ is a bounded formula of $x$ and $n$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_toPrenex\_\_\_f}$.

T is universal (from the name)

Let $T$ be a theory of $L$. Then we can say that $T$ is universal.

definable set of A and x1 (from the name)

Let $L$ be a language. Let $A$ be an element of $\wp M$. Let $x_{1}$ be a set. Then a definable set of $A$ and $x_{1}$ is an element of the function that maps $L$, $A$ and $x_{1}$ to $\SubtypeSet {s}{\operatorname{Definable} (A , L , s)}$.

Let $A$ be an element of $\wp M$. Let $L$ be a language. Let $s$ be an element of $\wp (\mathrm{Elem} (x_{1})\rightarrow M)$. Then $\operatorname{Definable}$ holds for $A$, $L$ and $s$, if there exists a formula $x_{2}$ of $\operatorname{withConstants}$ applied to $L$ and the set of elements of $A$ and $x_{1}$, such that $\EqtMACRoH {s}{\operatorname{ofPred} (\operatorname{Realize} (x_{2}))}$.

Let $L$ be a language. Let $A$ be an element of $\wp M$. Let $f$ be a function from functions from elements of $x_{1}$ to elements of $M$ to elements of $M$. Then $\operatorname{DefinableFun}$ holds for $L$, $A$ and $f$, if $\operatorname{Definable}$ holds for $A$, $L$ and the tuple graph of $f$.

Let $L$ be a language. Let $A$ be an element of $\wp M$. Let $F$ be a function from functions from elements of $x_{1}$ to elements of $M$ and elements of $x_{2}$ to elements of $M$. Then $\operatorname{DefinableMap}$ holds for $L$, $A$ and $F$, if for all elements $i$ of $x_{2}$, $\operatorname{DefinableFun}$ holds for $L$, $A$ and the function that maps $x_{3}$ to $F$ applied to $x_{3}$ and $i$.

Let $A$ and $s$ be elements of $\wp M$. Let $L$ be a language. Then $\mathrm{Set\_\_Definable\_u2081\_}$ holds for $A$, $L$ and $s$, if $\operatorname{Definable}$ holds for $A$, $L$ and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1} (0)}$.

Let $A$ be an element of $\wp M$. Let $L$ be a language. Let $s$ be an element of $\wp \mathrm{Prod} (M , M)$. Then $\mathrm{Set\_\_Definable\_u2082\_}$ holds for $A$, $L$ and $s$, if $\operatorname{Definable}$ holds for $A$, $L$ and $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{(\ProdmkMACRoU {x_{1} (0)}{x_{1} (1)})}$.

Let $A$ be an element of $\wp M$. Let $L$ be a language. Let $f$ be a function from functions from elements of $x_{1}$ to elements of $M$ to elements of $M$. Then $\operatorname{TermDefinable}$ holds for $A$, $L$ and $f$, if there exists a term $x_{2}$ of $\operatorname{withConstants}$ applied to $L$ and the set of elements of $A$ and $x_{1}$, such that $\EqtMACRoH {f}{\lambda v . \operatorname{realize} (v , x_{2})}$.

Let $L$ be a language. Let $f$ be a function from elements of $M$ to elements of $M$. Then $\mathrm{Set\_\_TermDefinable\_u2081\_}$ holds for $L$ and $f$, if $\operatorname{TermDefinable}$ holds for $A$, $L$ and the function that maps $x_{1}$ to $f$ applied to $x_{1}$ applied to $\operatorname{unit}$.

direct limit of G and f (from the name)

Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to embeddings of $G$ applied to $i$ and $G$ applied to $j$. Then a direct limit of $G$ and $i$ is an element of the function that maps $G$, $f$, $j$ and $f$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $G$ and $i$, $j$ and $f$.

the equivalence supremum of S (from the name)

Let $S$ be an order homomorphism of $x$ and the set of substructures of $L$ and $M$. Then the equivalence supremum of $S$ is an equivalence of the set of direct limits of the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S (i)}{x_{3}})}$ and the function that maps $x_{4}$, $x_{5}$ and $h_{2}$ to the inclusion of $\operatorname{monotone}$ applied to $S$, $x_{4}$, $x_{5}$ and $h_{2}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{iSup} (\operatorname{coe} (S))}{x_{6}})}$.

the equivalence lift of j2 and i2 (from the name)

Let $L$ be a language. Let $x$ be a set. Let $G$ and $\mathrm{G'}$ be functions from elements of $x$ to sets. Let $f$ be a function from elements $i_{3}$ of $x$ and elements $j_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{3} , j_{2})$ to embeddings of $G$ applied to $i_{3}$ and $G$ applied to $j_{2}$. Let $\mathrm{f'}$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to embeddings of $\mathrm{G'}$ applied to $i_{2}$ and $\mathrm{G'}$ applied to $j_{1}$. Let $g$ be a function from elements $i_{1}$ of $x$ to equivalences of $G$ applied to $i_{1}$ and $\mathrm{G'}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{4}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{4}))}{\mathrm{f'} (i , j , \mathrm{hij} , g (i , x_{4}))}$. Then the equivalence lift of $f$ and $\mathrm{G'}$ is an equivalence of the set of direct limits of $G$ and $f$ and the set of direct limits of $\mathrm{G'}$ and $\mathrm{f'}$.

the lift of f and i2 (from the name)

Let $L$ be a language. Let $x$ be a set. Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to embeddings of $G$ applied to $i_{2}$ and $G$ applied to $j_{1}$. Let $g$ be a function from elements $i_{1}$ of $x$ to embeddings of $G$ applied to $i_{1}$ and $P$ such that for all elements $i$ and $j$ of $x$, for all elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{4}$ of $G$ applied to $i$, $\EqtMACRoH {g (j , f (i , j , \mathrm{hij} , x_{4}))}{g (i , x_{4})}$. Then the lift of $i_{2}$ and $j_{1}$ is an embedding of the set of direct limits of $G$ and $f$ and $P$.

the lift inclusion of S (from the name)

Let $S$ be an order homomorphism of $x$ and the set of substructures of $L$ and $M$. Then the lift inclusion of $S$ is an embedding of the set of direct limits of the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S (i)}{x_{3}})}$ and the function that maps $x_{4}$, $x_{5}$ and $h_{2}$ to the inclusion of $\operatorname{monotone}$ applied to $S$, $x_{4}$, $x_{5}$ and $h_{2}$ and $M$.

Let $L$ be a language. Let $x$ be a set. Let $G$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to embeddings of $G$ applied to $i_{1}$ and $G$ applied to $j$. Let $i$ be an element of $x$. Then $\operatorname{of}$ applied to $L$, $x$, $G$, $i_{1}$, $j$, $f$ and $i$ is an embedding of $G$ applied to $i$ and the set of direct limits of $G$ and $f$.

Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to embeddings of $G$ applied to $i_{1}$ and $G$ applied to $j$. Let $x_{4}$ be a function from elements of $x_{3}$ to sigmas of $f$. Let $i$ be an element of $x$ such that $i$ is an element of the upper bound of the range of $\operatorname{comp}$ applied to $\operatorname{fst}$ and $x_{4}$. Let $a$ be an element of $x_{3}$. Then $\operatorname{unify}$ applied to $i_{1}$, $j$, $f$, $x_{4}$, $i$, $h$ and $a$ is an element of $G$ applied to $i$.

Let $\mathrm{f'}$ be a function from natural numbers $n_{1}$ to embeddings of $\mathrm{G'}$ applied to $n_{1}$ and $\mathrm{G'}$ applied to $n_{1} + 1$. Let $m$ and $n$ be natural numbers such that $m \leq n$. Then $\operatorname{natLERec}$ applied to $n_{1}$, $\mathrm{f'}$, $m$, $n$ and $h$ is an embedding of $\mathrm{G'}$ applied to $m$ and $\mathrm{G'}$ applied to $n$ defined as the function that maps $h$ to $\operatorname{leRecOn}$ applied to $n$, the function that maps $k$ and $g$ to the composition of $n_{1}$ applied to $k$ and $g$, the identity embedding of $L$ and $\mathrm{G'}$ applied to $\mathrm{f'}$ and $h$.

sigma of f (from the name)

Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to embeddings of $G$ applied to $i$ and $G$ applied to $j$. Then a sigma of $i$ is an element of the function that maps $f$, $j$ and $f$ to $\Sigma$ applied to the function that maps $i$ to $G$ applied to $i$, $j$ and $f$.

Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to embeddings of $G$ applied to $i_{1}$ and $G$ applied to $j$. Let $i$ be an element of $x$. Let $x_{3}$ be an element of $G$ applied to $i$. Then $\operatorname{mk}$ applied to $i_{1}$, $j$, $f$, $i$ and $x_{3}$ is a sigma of $f$ defined as the function that maps $i$ and $x_{3}$ to $\operatorname{mk}$ applied to $j$, $f$, $i$ and $x_{3}$.

elementary embedding of M and N (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the elementary embeddings of $M$ and $N$ are a basic type.

the composition of hnp and hmn (from the name)

Let $\mathrm{hnp}$ be an elementary embedding of $N$ and $P$. Let $\mathrm{hmn}$ be an elementary embedding of $M$ and $N$. Then the composition of $\mathrm{hnp}$ and $\mathrm{hmn}$ is an elementary embedding of $M$ and $P$.

the lift with constant of f and A (from the name)

Let $f$ be an elementary embedding of $M$ and $N$. Let $A$ be an element of $\wp M$. Then the lift with constant of $f$ and $A$ is an elementary embedding of $M$ and $\operatorname{withConstants}$ applied to the embedding of $f$ and $A$.

the elementary embedding of L (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the elementary embedding of $L$ is an elementary embedding of $M$ and $N$.

the identity elementary embedding of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the identity elementary embedding of $L$ and $M$ is an elementary embedding of $M$ and $M$.

the embedding of f (from the name)

Let $f$ be an elementary embedding of $M$ and $N$. Then the embedding of $f$ is an embedding of $M$ and $N$.

the underlying embedding of self and x2 (from the docstring)

Let $\mathrm{self}$ be an elementary embedding of $M$ and $N$. Let $x_{2}$ be an element of $M$. Then the underlying embedding of $\mathrm{self}$ and $x_{2}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

the homomorphism of f (from the name)

Let $f$ be an elementary embedding of $M$ and $N$. Then the homomorphism of $f$ is a homomorphism of $M$ and $N$.

the elementary embedding of f and htv (from the name)

Let $f$ be an embedding of $M$ and $N$ such that for all natural numbers $n$, for all bounded formulas $x_{2}$ of $\mathrm{Empty}$ and $n + 1$, for all functions $x_{3}$ from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$, for all elements $a$ of $N$, if $\operatorname{Realize}$ holds for $x_{2}$, $\operatorname{default}$ and $\operatorname{snoc}$ applied to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $f$ and $x_{3}$ and $a$, then there exists an element $b$ of $M$, such that $\operatorname{Realize}$ holds for $x_{2}$, $\operatorname{default}$ and $\operatorname{snoc}$ applied to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $f$ and $x_{3}$ and $f$ applied to $b$. Then the elementary embedding of $f$ and $\mathrm{htv}$ is an elementary embedding of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and the function that maps $x_{2}$ to $\mathrm{FirstOrder\_\_Language\_\_Embedding\_\_isElementary\_of\_exists}$ applied to $f$ and $\mathrm{htv}$.

the elementary embedding of f (from the name)

Let $f$ be an equivalence of $M$ and $N$. Then the elementary embedding of $f$ is an elementary embedding of $M$ and $N$.

the elementary diagram of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the elementary diagram of $L$ and $M$ is a theory of $\operatorname{withConstants}$ applied to $L$ and $M$ defined as the complete theory of $\operatorname{withConstants}$ applied to $L$ and $M$ and $M$.

elementary substructure of L and M (from the name)

Let $L$ be a language. Let $M$ be a set. Then the elementary substructures of $L$ and $M$ are a basic type.

the subtype of S (from the name)

Let $S$ be an elementary substructure of $L$ and $M$. Then the subtype of $S$ is an elementary embedding of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $M$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to $\MembershipmemMACRoT {S}{x_{1}}$ and $\operatorname{isElementary}$ applied to $S$.

the underlying substructure of self (from the docstring)

Let $\mathrm{self}$ be an elementary substructure of $L$ and $M$. Then the underlying substructure of $\mathrm{self}$ is a substructure of $L$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $A$ be an element of $\wp M$. Then $\operatorname{MeetsDefinable}$ holds for $A$, if for all elements $D$ of $\wp M$, if $D$ is nonempty, then if $\mathrm{Set\_\_Definable\_u2081\_}$ holds for $A$, $L$ and $D$, then $\operatorname{inter}$ applied to $D$ and $A$ is nonempty.

the elementary substructure of hA (from the name)

Assume that $\operatorname{MeetsDefinable}$ holds for $A$. Then the elementary substructure of $\mathrm{hA}$ is an elementary substructure of $L$ and $M$ defined as $\operatorname{mk}$ applied to the lower adjoint of the closure of $L$ and $A$ and $\mathrm{FirstOrder\_\_Language\_\_MeetsDefinable\_\_isElementary\_closure}$ applied to $\mathrm{hA}$.

S is elementary (from the name)

Let $S$ be a substructure of $L$ and $M$. Then $S$ is elementary, if for all natural numbers $n$, for all formulas $x_{1}$ of $L$ and $\mathrm{Fin}$ applied to $n$, for all functions $x_{2}$ from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, $\operatorname{Realize}$ holds for $x_{1}$ and $\operatorname{comp}$ applied to the function that maps $x_{3}$ to $\MembershipmemMACRoT {S}{x_{3}}$ and $x_{2}$, if and only if $\operatorname{Realize}$ holds for $x_{1}$ and $x_{2}$.

the elementary substructure of S and htv (from the name)

Let $S$ be a substructure of $L$ and $M$ such that for all natural numbers $n$, for all bounded formulas $x_{1}$ of $\mathrm{Empty}$ and $n + 1$, for all functions $x_{2}$ from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$, for all elements $a$ of $M$, if $\operatorname{Realize}$ holds for $x_{1}$, $\operatorname{default}$ and $\operatorname{snoc}$ applied to $\operatorname{comp}$ applied to the function that maps $x_{5}$ to $\MembershipmemMACRoT {S}{x_{5}}$ and $x_{2}$ and $a$, then there exists an element $b$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$, such that $\operatorname{Realize}$ holds for $x_{1}$, $\operatorname{default}$ and $\operatorname{snoc}$ applied to $\operatorname{comp}$ applied to the function that maps $x_{3}$ to $\MembershipmemMACRoT {S}{x_{3}}$ and $x_{2}$ and $b$. Then the elementary substructure of $S$ and $\mathrm{htv}$ is an elementary substructure of $L$ and $M$ defined as $\operatorname{mk}$ applied to $S$ and $\mathrm{FirstOrder\_\_Language\_\_Substructure\_\_isElementary\_of\_exists}$ applied to $S$ and $\mathrm{htv}$.

the encoding (from the name)

The encoding is an encoding of $\Sigma$ applied to the function that maps $n$ to the set of bounded formulas of $x$ and $n$ and $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $k$ to the set of terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $k$ and $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $n_{1}$ to the set of relations of $L$ and $n_{1}$ and $\Natural$.

the list decode of x1 (from the name)

Let $x_{1}$ be a list of elements of $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $k$ to the set of terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $k$ and $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $n_{1}$ to the set of relations of $L$ and $n_{1}$ and $\Natural$. Then the list decode of $x_{1}$ is a list of elements of $\Sigma$ applied to the function that maps $n$ to the set of bounded formulas of $x$ and $n$.

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{listEncode}$ applied to $x_{1}$ is a list of elements of $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $k$ to the set of terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $k$ and $\mathrm{Sum}$ applied to $\Sigma$ applied to the function that maps $n_{1}$ to the set of relations of $L$ and $n_{1}$ and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_listEncode\_\_\_f}$.

Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $n_{1}$ to the set of bounded formulas of $x$ and $n_{1}$. Then $\operatorname{sigmaAll}$ applied to $x_{1}$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bounded formulas of $x$ and $n$.

Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $n_{2}$ to the set of bounded formulas of $x$ and $n_{2}$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $n_{1}$ to the set of bounded formulas of $x$ and $n_{1}$. Then $\operatorname{sigmaImp}$ applied to $x_{1}$ and $x_{2}$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bounded formulas of $x$ and $n$.

the encoding (from the name)

The encoding is an encoding of the set of terms of $L$ and $x$ and $\mathrm{Sum}$ applied to $x$ and $\Sigma$ applied to the function that maps $i$ to the set of functions of $L$ and $i$.

the list decode of x1 (from the name)

Let $x_{1}$ be a list of elements of $\mathrm{Sum}$ applied to $x$ and $\Sigma$ applied to the function that maps $i$ to the set of functions of $L$ and $i$. Then the list decode of $x_{1}$ is a list of terms of $L$ and $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_listDecode\_\_\_f}$.

Let $x_{1}$ be a term of $L$ and $x$. Then $\operatorname{listEncode}$ applied to $x_{1}$ is a list of elements of $\mathrm{Sum}$ applied to $x$ and $\Sigma$ applied to the function that maps $i$ to the set of functions of $L$ and $i$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_listEncode\_\_\_f}$.

Let $T$ be a theory of $L$. Let $x_{1}$ and $x_{2}$ be bounded formulas of $x$ and $n$. Then $\operatorname{Iff}$ holds for $T$, $x_{1}$ and $x_{2}$, if $\operatorname{ModelsBoundedFormula}$ holds for $T$ and $\operatorname{iff}$ applied to $x_{1}$ and $x_{2}$.

Let $T$ be a theory of $L$. Let $x_{1}$ and $x_{2}$ be bounded formulas of $x$ and $n$. Then $\operatorname{Imp}$ holds for $T$, $x_{1}$ and $x_{2}$, if $\operatorname{ModelsBoundedFormula}$ holds for $T$ and $\operatorname{imp}$ applied to $x_{1}$ and $x_{2}$.

Let $L$ be a language. Let $M$ be a set. Then we can say that $\operatorname{CG}$ holds for $L$ and $M$.

Let $L$ be a language. Let $M$ be a set. Then we can say that $\operatorname{FG}$ holds for $L$ and $M$.

Let $N$ be a substructure of $L$ and $M$. Then $\operatorname{CG}$ holds for $N$, if there exists an element $S$ of $\wp M$, such that $S$ is countable and the lower adjoint of the closure of $L$ and $S$ is equal to $N$.

Let $N$ be a substructure of $L$ and $M$. Then $\operatorname{FG}$ holds for $N$, if there exists a finite set $S$ of $M$, such that the lower adjoint of the closure of $L$ and $S$ is equal to $N$.

K is a amalgamation (from the name)

Let $K$ be an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure. Then $K$ is an amalgamation, if for all elements $M$, $N$ and $P$ of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure, for all embeddings $\mathrm{MN}$ of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $M$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $N$, for all embeddings $\mathrm{MP}$ of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $M$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $P$, if $M$ is an element of $K$, then if $N$ is an element of $K$, then if $P$ is an element of $K$, then there exists an element $Q$ of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure, such that there exists an embedding $\mathrm{NQ}$ of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $N$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $Q$, such that there exists an embedding $\mathrm{PQ}$ of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $P$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $Q$, such that $Q$ is an element of $K$ and the composition of $\mathrm{NQ}$ and $\mathrm{MN}$ is equal to the composition of $\mathrm{PQ}$ and $\mathrm{MP}$.

K is hereditary (from the name)

Let $K$ be an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure. Then $K$ is hereditary, if for all elements $M$ of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure, if $M$ is an element of $K$, then the age of $L$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $M$ is less than or equal to $K$.

Let $K$ be an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure. Then we can say that $\operatorname{IsFraisse}$ holds for $K$.

Let $K$ be an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure. Let $M$ be a set. Then we can say that $\operatorname{IsFraisseLimit}$ holds for $K$ and $M$.

Let $L$ be a language. Let $M$ be a set. Then $\operatorname{IsUltrahomogeneous}$ holds for $L$ and $M$, if for all substructures $S$ of $L$ and $M$, if $\operatorname{FG}$ holds for $S$, then for all embeddings $f$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ and $M$, there exists an equivalence $g$ of $M$ and $M$, such that $f$ is equal to the composition of the embedding of $g$ and the subtype of $S$.

K is a joint embedding (from the name)

Let $K$ be an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure. Then $K$ is a joint embedding, if $\mathrm{DirectedOn}$ holds for the function that maps $M$ and $N$ to $\mathrm{Nonempty}$ applied to the set of embeddings of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $M$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $N$ and $K$.

the age of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the age of $L$ and $M$ is an element of the power set of $\operatorname{Bundled}$ applied to the proposition that $L$ is a structure defined as $\operatorname{ofPred}$ applied to the function that maps $N$ to the proposition that $\operatorname{FG}$ holds for $L$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $N$ and $\mathrm{Nonempty}$ holds for the set of embeddings of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $N$ and $M$.

the simple graph (from the name)

The simple graph is a theory of the graph defined as $\operatorname{insert}$ applied to $\operatorname{irreflexive}$ applied to the adjoint and $\operatorname{singleton}$ applied to $\operatorname{symmetric}$ applied to the adjoint.

the adjoint (from the name)

The adjoint is a relation of the graph and $2$ defined as the adjoint.

the graph (from the name)

The graph is a language defined as $\operatorname{mk}$ applied to the function that maps $x$ to $\mathrm{Empty}$ and the set of elements of $\operatorname{graphRel}$.

graph relation of x (from the name)

Let $x$ be a natural number. Then the graph relations of $x$ are a basic type.

the adjoint (from the name)

The adjoint is a graph relation of $2$.

the simple graph of V (from the name)

Let $V$ be a set. Then the simple graph of $V$ is a simple graph of $V$.

the lift with constant of A and f (from the name)

Let $A$ be an element of $\wp M$. Let $f$ be an embedding of $M$ and $N$. Then the lift with constant of $A$ and $f$ is an embedding of $M$ and $\operatorname{withConstants}$ applied to $f$ and $A$.

Let $\mathrm{\_f}$ be an embedding of $M$ and $N$. Let $\mathrm{\_A}$ be an element of $\wp M$. Then an element of $\operatorname{withConstants}$ applied to $\mathrm{\_f}$ and $\mathrm{\_A}$ is an element of the function that maps $\mathrm{\_f}$ and $\mathrm{\_A}$ to $N$.

equivalence of L and #2 (from the name)

Let $L$ and $\mathrm{L'}$ be languages. Then the equivalences of $L$ and $\mathrm{L'}$ are a basic type.

the additive empty constant of L and x (from the name)

Let $L$ be a language. Let $x$ be a set. Then the additive empty constant of $L$ and $x$ is an equivalence of $L$ and $\operatorname{withConstants}$ applied to $L$ and $x$.

the inverse language homomorphism of self (from the docstring)

Let $\mathrm{self}$ be an equivalence of $L$ and $\mathrm{L'}$. Then the inverse language homomorphism of $\mathrm{self}$ is a homomorphism of $\mathrm{L'}$ and $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the identity equivalence of L (from the docstring)

Let $L$ be a language. Then the identity equivalence of $L$ is an equivalence of $L$ and $L$.

the inverse of e (from the docstring)

Let $e$ be an equivalence of $L$ and $\mathrm{L'}$. Then the inverse of $e$ is an equivalence of $\mathrm{L'}$ and $L$ defined as $\operatorname{mk}$ applied to the inverse language homomorphism of $e$, the forward language homomorphism of $e$, $\mathrm{FirstOrder\_\_Language\_\_LEquiv\_\_right\_inv}$ applied to $e$ and $\mathrm{FirstOrder\_\_Language\_\_LEquiv\_\_left\_inv}$ applied to $e$.

the forward language homomorphism of self (from the docstring)

Let $\mathrm{self}$ be an equivalence of $L$ and $\mathrm{L'}$. Then the forward language homomorphism of $\mathrm{self}$ is a homomorphism of $L$ and $\mathrm{L'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition of e and #2 (from the name)

Let $e$ be an equivalence of $L$ and $\mathrm{L'}$. Let $\mathrm{e'}$ be an equivalence of $\mathrm{L'}$ and $\mathrm{L''}$. Then the composition of $e$ and $\mathrm{e'}$ is an equivalence of $L$ and $\mathrm{L''}$.

homomorphism of L and #2 (from the name)

Let $L$ and $\mathrm{L'}$ be languages. Then the homomorphisms of $L$ and $\mathrm{L'}$ are a basic type.

x is injective (from the name)

Let $x$ be a homomorphism of $L$ and $\mathrm{L'}$. Then we can say that $x$ is injective.

x is an expansion (from the docstring)

Let $x$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $M$ be a set. Then we can say that $x$ is an expansion.

the additive constant of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a homomorphism of $L$ and $\mathrm{L'}$. Then the additive constant of $x$ and $x_{1}$ is a homomorphism of $\operatorname{withConstants}$ applied to $L$ and $x$ and $\operatorname{withConstants}$ applied to $\mathrm{L'}$ and $x$ defined as the sum map of $x_{1}$ and the identity language homomorphism of $\operatorname{constantsOn}$ applied to $x$.

the composition of g and f (from the name)

Let $g$ be a homomorphism of $\mathrm{L'}$ and $\mathrm{L''}$. Let $f$ be a homomorphism of $L$ and $\mathrm{L'}$. Then the composition of $g$ and $f$ is a homomorphism of $L$ and $\mathrm{L''}$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ and $F$ to $\operatorname{onFunction}$ applied to $g$ and $\operatorname{onFunction}$ applied to $f$ and $F$ and the function that maps $x$ and $R$ to $\operatorname{onRelation}$ applied to $g$ and $\operatorname{onRelation}$ applied to $f$ and $R$.

the constant on map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the constant on map of $f$ is a homomorphism of $\operatorname{constantsOn}$ applied to $x$ and $\operatorname{constantsOn}$ applied to $x_{1}$.

the identity language homomorphism of L (from the docstring)

Let $L$ be a language. Then the identity language homomorphism of $L$ is a homomorphism of $L$ and $L$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ to $\mathrm{id}$ and the function that maps $\mathrm{\_n1}$ to $\mathrm{id}$.

the inclusion of L and #2 (from the docstring)

Let $L$ and $\mathrm{L'}$ be languages. Then the inclusion of $L$ and $\mathrm{L'}$ is a homomorphism of $L$ and $\mathrm{L'}$ defined as $\operatorname{mk}$ applied to the function that maps $n$ and $a$ to $\mathrm{isEmptyElim}$ applied to $a$ and the function that maps $n_{1}$ and $a_{1}$ to $\mathrm{isEmptyElim}$ applied to $a_{1}$.

Let $\mathrm{self}$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x$ be a function of $L$ and $n$. Then $\operatorname{onFunction}$ applied to $\mathrm{self}$ and $x$ is a function of $\mathrm{L'}$ and $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

Let $\mathrm{self}$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x$ be a relation of $L$ and $n$. Then $\operatorname{onRelation}$ applied to $\mathrm{self}$ and $x$ is a relation of $\mathrm{L'}$ and $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.

the sum eliminator of x and x1 (from the name)

Let $x$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{1}$ be a homomorphism of $\mathrm{L''}$ and $\mathrm{L'}$. Then the sum eliminator of $x$ and $x_{1}$ is a homomorphism of the sum of $L$ and $\mathrm{L''}$ and $\mathrm{L'}$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ to $\operatorname{elim}$ applied to the function that maps $f$ to $\operatorname{onFunction}$ applied to $x$ and $f$ and the function that maps $f_{1}$ to $\operatorname{onFunction}$ applied to $x_{1}$ and $f_{1}$ and the function that maps $\mathrm{\_n1}$ to $\operatorname{elim}$ applied to the function that maps $f_{2}$ to $\operatorname{onRelation}$ applied to $x$ and $f_{2}$ and the function that maps $f_{3}$ to $\operatorname{onRelation}$ applied to $x_{1}$ and $f_{3}$.

the inclusion of the left factor into the sum of two languages (from the docstring)

The inclusion of the left factor into the sum of two languages is a homomorphism of $L$ and the sum of $L$ and $\mathrm{L'}$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ to $\operatorname{inl}$ and the function that maps $\mathrm{\_n1}$ to $\operatorname{inl}$.

the inclusion of the right factor into the sum of two languages (from the docstring)

The inclusion of the right factor into the sum of two languages is a homomorphism of $\mathrm{L'}$ and the sum of $L$ and $\mathrm{L'}$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ to $\operatorname{inr}$ and the function that maps $\mathrm{\_n1}$ to $\operatorname{inr}$.

the sum map of x and x3 (from the name)

Let $x$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{3}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then the sum map of $x$ and $x_{3}$ is a homomorphism of the sum of $L$ and $x_{1}$ and the sum of $\mathrm{L'}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the function that maps $\mathrm{\_n}$ to $\operatorname{map}$ applied to the function that maps $f$ to $\operatorname{onFunction}$ applied to $x$ and $f$ and the function that maps $f_{1}$ to $\operatorname{onFunction}$ applied to $x_{3}$ and $f_{1}$ and the function that maps $\mathrm{\_n1}$ to $\operatorname{map}$ applied to the function that maps $f_{2}$ to $\operatorname{onRelation}$ applied to $x$ and $f_{2}$ and the function that maps $f_{3}$ to $\operatorname{onRelation}$ applied to $x_{3}$ and $f_{3}$.

the congruence relation of L and a (from the name)

Let $L$ be a language. Let $a$ be an element of $x$. Then the congruence relation of $L$ and $a$ is a constant of $\operatorname{withConstants}$ applied to $L$ and $x$ defined as $\operatorname{inr}$ applied to $a$.

Let $x$ be a set. Then $\operatorname{constantsOn}$ applied to $x$ is a language defined as $\operatorname{mk}$ applied to the set of elements of $\operatorname{constantsOnFunc}$ applied to $x$ and the function that maps $x_{1}$ to $\mathrm{Empty}$.

constant on function of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a natural number. Then the constants on function of $x$ and $x_{1}$ are a basic type.

Let $L$ be a language. Let $x$ be a set. Then $\operatorname{lhomWithConstants}$ applied to $L$ and $x$ is a homomorphism of $L$ and $\operatorname{withConstants}$ applied to $L$ and $x$ defined as the inclusion of the left factor into the sum of two languages.

Let $L$ be a language. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{lhomWithConstantsMap}$ applied to $L$ and $f$ is a homomorphism of $\operatorname{withConstants}$ applied to $L$ and $x$ and $\operatorname{withConstants}$ applied to $L$ and $x_{1}$ defined as the sum map of the identity language homomorphism of $L$ and the constant on map of $f$.

Let $L$ be a language. Let $x$ be a set. Then $\operatorname{withConstants}$ applied to $L$ and $x$ is a language defined as the sum of $L$ and $\operatorname{constantsOn}$ applied to $x$.

L is ordered (from the docstring)

Let $L$ be a language. Then we can say that $L$ is ordered.

the relation symbol representing (from the docstring)

The relation symbol representing is a relation of $L$ and $2$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

L is ordered (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then we can say that $L$ is ordered.

Let $x_{2}$ and $x_{3}$ be terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{le}$ applied to $x_{2}$ and $x_{3}$ is a bounded formula of $x$ and $n$ defined as the bounded formula of $x_{2}$ and $x_{3}$.

Let $x_{2}$ and $x_{3}$ be terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{lt}$ applied to $x_{2}$ and $x_{3}$ is a bounded formula of $x$ and $n$ defined as $\MinminMACRoAG {\operatorname{le} (x_{2} , x_{3})}{\operatorname{not} (\operatorname{le} (x_{3} , x_{2}))}$.

the densely ordered sentence of L (from the name)

the linear order theory of L (from the name)

Let $L$ be a language. Then the linear order theory of $L$ is a theory of $L$ defined as $\operatorname{insert}$ applied to $\operatorname{total}$ applied to the relation symbol representing and the partial order theory of $L$.

Let $L$ be a language. Then $\operatorname{noBotOrderSentence}$ applied to $L$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{ex}$ applied to $\operatorname{not}$ applied to $\operatorname{le}$ applied to $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$.

Let $L$ be a language. Then $\operatorname{noTopOrderSentence}$ applied to $L$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{ex}$ applied to $\operatorname{not}$ applied to $\operatorname{le}$ applied to $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$.

the order (from the name)

The order is a language defined as $\operatorname{mk}$ applied to the function that maps $x$ to $\mathrm{Empty}$ and the set of elements of $\operatorname{orderRel}$.

the order homomorphism of L (from the name)

Let $L$ be a language. Then the order homomorphism of $L$ is a homomorphism of the order and $L$.

order relation of x (from the name)

Let $x$ be a natural number. Then the order relations of $x$ are a basic type.

$\operatorname{le}$ is an order relation of $2$.

the partial order theory of L (from the name)

Let $L$ be a language. Then the partial order theory of $L$ is a theory of $L$ defined as $\operatorname{insert}$ applied to $\operatorname{antisymmetric}$ applied to the relation symbol representing and the preorder theory of $L$.

the preorder theory of L (from the name)

Let $L$ be a language. Then the preorder theory of $L$ is a theory of $L$ defined as $\operatorname{insert}$ applied to $\operatorname{reflexive}$ applied to the relation symbol representing and $\operatorname{singleton}$ applied to $\operatorname{transitive}$ applied to the relation symbol representing.

the limit of S (from the docstring)

Let $S$ be an order homomorphism of $x_{2}$ and the set of partial equivalences of $M$ and $N$. Then the limit of $S$ is a partial equivalence of $M$ and $N$.

the partial equivalence of f (from the name)

Let $f$ be an embedding of $M$ and $N$. Then the partial equivalence of $f$ is a partial equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to the top, the range of the homomorphism of $f$ and the composition of the equivalence between the domain and the range of $f$ and the equivalence between the maximal substructure.

Let $L$ be a language. Let $M$ and $N$ be sets. Then an element of $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$ is an element of the function that maps $L$, $M$ and $N$ to $\SubtypeSet {f}{\operatorname{FG} (\operatorname{dom} (f))}$.

the inverse of f (from the name)

Let $f$ be an element of $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$. Then the inverse of $f$ is an element of $\operatorname{FGEquiv}$ applied to $L$, $N$ and $M$ defined as the inverse of $f$.

L is a extension pair (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then $L$ is an extension pair, if for all elements $f$ of $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$, for all elements $m$ of $M$, there exists an element $g$ of $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$, such that $m$ is an element of the domain of $g$ and $f \leq g$.

Assume that $L$ is an extension pair. Let $m$ be an element of $M$. Then $\operatorname{definedAtLeft}$ applied to $h$ and $m$ is an element of $\operatorname{Cofinal}$ applied to $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $m$ is an element of the domain of $f$ and the function that maps $f_{1}$ to $h$ applied to $f_{1}$ and $m$.

Assume that $L$ is an extension pair. Let $n$ be an element of $N$. Then $\operatorname{definedAtRight}$ applied to $h$ and $n$ is an element of $\operatorname{Cofinal}$ applied to $\operatorname{FGEquiv}$ applied to $L$, $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $n$ is an element of the codomain of $f$ and the function that maps $f_{1}$ to $\operatorname{cod}$ applied to $h$, $f_{1}$ and $n$.

partial equivalence of M and N (from the name)

Let $L$ be a language. Let $M$ and $N$ be sets. Then the partial equivalences of $M$ and $N$ are a basic type.

the codomain of self (from the name)

Let $\mathrm{self}$ be a partial equivalence of $M$ and $N$. Then the codomain of $\mathrm{self}$ is a substructure of $L$ and $N$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $f$ be a partial equivalence of $M$ and $N$ such that $A$ is less than or equal to the codomain of $f$. Then $\operatorname{codRestrict}$ applied to $f$ and $h$ is a partial equivalence of $M$ and $N$ defined as the inverse of $\operatorname{domRestrict}$ applied to the inverse of $f$ and $h$.

the domain of self (from the name)

Let $\mathrm{self}$ be a partial equivalence of $M$ and $N$. Then the domain of $\mathrm{self}$ is a substructure of $L$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $f$ be a partial equivalence of $M$ and $N$ such that $A$ is less than or equal to the domain of $f$. Then $\operatorname{domRestrict}$ applied to $f$ and $h$ is a partial equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $A$, the range of the homomorphism of the composition of the subtype of the codomain of $f$ and the composition of the embedding of the equivalence of $f$ and the inclusion of $h$ and the equivalence between the domain and the range of the composition of the subtype of the codomain of $f$ and the composition of the embedding of the equivalence of $f$ and the inclusion of $h$.

the inverse of f (from the name)

Let $f$ be a partial equivalence of $M$ and $N$. Then the inverse of $f$ is a partial equivalence of $N$ and $M$ defined as $\operatorname{mk}$ applied to the codomain of $f$, the domain of $f$ and the inverse of the equivalence of $f$.

the embedding of f (from the name)

Let $f$ be a partial equivalence of $M$ and $N$. Then the embedding of $f$ is an embedding of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{dom} (f)}{x_{2}})}$ and $N$ defined as the composition of the subtype of the codomain of $f$ and the embedding of the equivalence of $f$.

the embedding of h (from the name)

Assume that the domain of $f$ is equal to the top. Then the embedding of $h$ is an embedding of $M$ and $N$.

the equivalence of self (from the name)

Let $\mathrm{self}$ be a partial equivalence of $M$ and $N$. Then the equivalence of $\mathrm{self}$ is an equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{dom} (\mathrm{self})}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{cod} (\mathrm{self})}{x_{3}})}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the equivalence of h_dom and h_cod (from the name)

Assume that the domain of $f$ is equal to the top. Assume that the codomain of $f$ is equal to the top. Then the equivalence of $\mathrm{h\_dom}$ and $\mathrm{h\_cod}$ is an equivalence of $M$ and $N$.

Let $L$ be a language. Assume that $\mathrm{Setoid}$ holds for $M$. Then we can say that $\operatorname{Prestructure}$ holds for $L$ and $s$.

Let $x$ be a cardinal. Let $T$ be a theory of $L$. Then $\operatorname{Categorical}$ holds for $x$ and $T$, if for all model types $M$ and $N$ of $T$, if $\operatorname{mk}$ applied to the set of carriers of $M$ is equal to $x$, then if $\operatorname{mk}$ applied to the set of carriers of $N$ is equal to $x$, then $\mathrm{Nonempty}$ holds for the set of equivalences of the set of carriers of $M$ and the set of carriers of $N$.

T is complete (from the name)

Let $T$ be a theory of $L$. Then $T$ is complete, if $T$ is satisfiable and for all sentences $x$ of $L$, $\operatorname{ModelsBoundedFormula}$ holds for $T$ and $x$ or $\operatorname{ModelsBoundedFormula}$ holds for $T$ and $\operatorname{not}$ applied to $x$.

Let $T$ be a theory of $L$. Then $\operatorname{IsFinitelySatisfiable}$ holds for $T$, if for all finite sets $T_{0}$ of the set of sentences of $L$, if $T_{0} \leq T$, then $T_{0}$ is satisfiable.

T is maximal (from the name)

Let $T$ be a theory of $L$. Then $T$ is maximal, if $T$ is satisfiable and for all sentences $x$ of $L$, $x$ is an element of $T$ or $\MembershipmemMACRoT {T}{\operatorname{not} (x)}$.

T is satisfiable (from the docstring)

Let $T$ be a theory of $L$. Then $T$ is satisfiable, if $\mathrm{Nonempty}$ holds for the set of model types of $T$.

Let $T$ be a theory of $L$. Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{ModelsBoundedFormula}$ holds for $T$ and $x_{1}$, if for all model types $M$ of $T$, for all functions $v$ from elements of $x$ to carriers of $M$, for all functions $\mathrm{xs}$ from elements of $\mathrm{Fin}$ applied to $n$ to carriers of $M$, $\operatorname{Realize}$ holds for $x_{1}$, $v$ and $\mathrm{xs}$.

Let $\mathrm{\_f}$ be a bounded formula of $x_{1}$ and $l$. Let $\mathrm{\_v}$ be a function from elements of $x_{1}$ to elements of $M$. Let $\mathrm{\_xs}$ be a function from elements of $\mathrm{Fin}$ applied to $l$ to elements of $M$. Then $\operatorname{Realize}$ holds for $\mathrm{\_f}$, $\mathrm{\_v}$ and $\mathrm{\_xs}$, if $\operatorname{brecOn}$ holds for $\mathrm{\_f}$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_Realize\_\_\_f}$, $\mathrm{\_v}$ and $\mathrm{\_xs}$.

L is elementarily equivalent (from the name)

Let $x_{2}$ be a formula of $L$ and $x_{1}$. Let $v$ be a function from elements of $x_{1}$ to elements of $M$. Then $\operatorname{Realize}$ holds for $x_{2}$ and $v$, if $\operatorname{Realize}$ holds for $x_{2}$, $v$ and $\operatorname{default}$.

Let $M$ be a set. Let $x_{1}$ be a sentence of $L$. Then $\operatorname{Realize}$ holds for $M$ and $x_{1}$, if $\operatorname{Realize}$ holds for $x_{1}$ and $\operatorname{default}$.

Let $v$ be a function from elements of $x_{1}$ to elements of $M$. Let $\mathrm{\_t}$ be a term of $L$ and $x_{1}$. Then $\operatorname{realize}$ applied to $v$ and $\mathrm{\_t}$ is an element of $M$ defined as $\operatorname{brecOn}$ applied to $\mathrm{\_t}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_realize\_\_\_f}$ applied to $v$.

T is a model (from the name)

Let $M$ be a set. Let $T$ be a theory of $L$. Then we can say that $T$ is a model.

the complete theory of L and M (from the docstring)

Let $L$ be a language. Let $M$ be a set. Then the complete theory of $L$ and $M$ is a theory of $L$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\operatorname{Realize}$ applied to $M$ and $x_{1}$.

Let $S$ be a substructure of the sum of $L$ and $\mathrm{FirstOrder\_\_Language\_\_skolem\_u2081\_}$ applied to $L$ and $M$. Then $\mathrm{FirstOrder\_\_Language\_\_Substructure\_\_elementarySkolem\_u2081\_Reduct}$ applied to $S$ is an elementary substructure of $L$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{substructureReduct}$ applied to the inclusion of the left factor into the sum of two languages and $S$ and $\mathrm{FirstOrder\_\_Language\_\_Substructure\_\_skolem\_u2081\_\_reduct\_isElementary}$ applied to $S$.

Let $L$ be a language. Then $\mathrm{FirstOrder\_\_Language\_\_skolem\_u2081\_}$ applied to $L$ is a language defined as $\operatorname{mk}$ applied to the function that maps $n$ to the set of bounded formulas of $\mathrm{Empty}$ and $n + 1$ and the function that maps $x$ to $\mathrm{Empty}$.

Let $f$ be a function of $L$ and $n$. Let $s$ be an element of $\wp M$. Then $\operatorname{ClosedUnder}$ holds for $f$ and $s$, if for all functions $x_{1}$ from elements of $\mathrm{Fin}$ applied to $n$ to elements of $M$, if for all elements $i$ of $\mathrm{Fin}$ applied to $n$, $\MembershipmemMACRoT {s}{x_{1} (i)}$, then the function map of $f$ and $x_{1}$ is an element of $s$.

Let $p$ be a substructure of $L$ and $N$. Let $f$ be an embedding of $M$ and $N$ such that for all elements $c$ of $M$, $\MembershipmemMACRoT {p}{f (c)}$. Then $\operatorname{codRestrict}$ applied to $p$, $f$ and $h$ is an embedding of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$.

the restriction of f and p (from the docstring)

Let $f$ be an embedding of $M$ and $N$. Let $p$ be a substructure of $L$ and $M$. Then the restriction of $f$ and $p$ is an embedding of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$ and $N$ defined as the composition of $f$ and the subtype of $p$.

the equivalence between the domain and the range of f (from the docstring)

Let $f$ be an embedding of $M$ and $N$. Then the equivalence between the domain and the range of $f$ is an equivalence of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toHom} (f))}{x_{2}})}$.

the substructure equivalence map of f and s (from the name)

Let $f$ be an embedding of $M$ and $N$. Let $s$ be a substructure of $L$ and $M$. Then the substructure equivalence map of $f$ and $s$ is an equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toHom} (f), s)}{x_{3}})}$.

Let $p$ be a substructure of $L$ and $N$. Let $f$ be a homomorphism of $M$ and $N$ such that for all elements $c$ of $M$, $\MembershipmemMACRoT {p}{f (c)}$. Then $\operatorname{codRestrict}$ applied to $p$, $f$ and $h$ is a homomorphism of $M$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$.

the restriction of f and p (from the docstring)

Let $f$ be a homomorphism of $M$ and $N$. Let $p$ be a substructure of $L$ and $M$. Then the restriction of $f$ and $p$ is a homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$ and $N$ defined as the composition of $f$ and the homomorphism of the subtype of $p$.

Let $f$ and $g$ be homomorphisms of $M$ and $N$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is a substructure of $L$ and $M$.

the range of f (from the docstring)

Let $f$ be a homomorphism of $M$ and $N$. Then the range of $f$ is a substructure of $L$ and $N$.

Let $x_{2}$ be a homomorphism of $L$ and $\mathrm{L'}$. Then $\operatorname{substructureReduct}$ applied to $x_{2}$ is an order embedding of the set of substructures of $\mathrm{L'}$ and $M$ and the set of substructures of $L$ and $M$.

substructure of L and M (from the name)

Let $L$ be a language. Let $M$ be a set. Then the substructures of $L$ and $M$ are a basic type.

the carrier of self (from the name)

Let $\mathrm{self}$ be a substructure of $L$ and $M$. Then the carrier of $\mathrm{self}$ is an element of $\wp M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the closure of L (from the name)

Let $L$ be a language. Then the closure of $L$ is a lower adjoint of $\operatorname{instSetLike}$.

the preimage of x2 and S (from the docstring)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Let $S$ be a substructure of $L$ and $N$. Then the preimage of $x_{2}$ and $S$ is a substructure of $L$ and $M$.

the copy of S and s (from the name)

Let $S$ be a substructure of $L$ and $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{S}$. Then the copy of $S$ and $s$ is a substructure of $L$ and $M$.

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{gciMapComap}$ applied to $\mathrm{hf}$ is a Galois coinsertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

Let $L$ be a language. Let $M$ be a set. Then $\operatorname{gi}$ applied to $L$ and $M$ is a Galois insertion of $\operatorname{toFun}$ applied to the closure of $L$ and $\operatorname{instSetLike}$.

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{giMapComap}$ applied to $\mathrm{hf}$ is a Galois insertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

the inclusion of h (from the name)

Assume that $S \leq T$. Then the inclusion of $h$ is an embedding of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$.

the map of x2 and S (from the name)

Let $x_{2}$ be a homomorphism of $M$ and $N$. Let $S$ be a substructure of $L$ and $M$. Then the map of $x_{2}$ and $S$ is a substructure of $L$ and $N$.

the subtype of S (from the name)

Let $S$ be a substructure of $L$ and $M$. Then the subtype of $S$ is an embedding of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$ and $M$.

the equivalence between the maximal substructure (from the docstring)

The equivalence between the maximal substructure is an equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{1}})}$ and $M$.

Let $S$ be a substructure of $L$ and $M$ such that $A \leq S$. Then $\operatorname{withConstants}$ applied to $S$ and $h$ is a substructure of $\operatorname{withConstants}$ applied to $L$ and the set of elements of $A$ and $M$.

bounded formula of x and x1 (from the name)

Let $L$ be a language. Let $x$ be a set. Let $x_{1}$ be a natural number. Then the bounded formulas of $x$ and $x_{1}$ are a basic type.

Let $f$ be a bounded formula of $x$ and $n + 1$. Then $\operatorname{all}$ applied to $f$ is a bounded formula of $x$ and $n$.

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{alls}$ applied to $x_{1}$ is a formula of $L$ and $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_alls\_\_\_f}$ and $x_{1}$.

Assume that $m \leq n$. Let $x_{1}$ be a bounded formula of $x$ and $m$. Then $\operatorname{castLE}$ applied to $\mathrm{\_h}$ and $x_{1}$ is a bounded formula of $x$ and $n$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_castLE\_\_\_f}$, $n$ and $\mathrm{\_h}$.

$\operatorname{constantsVarsEquiv}$ is an equivalence from the set of bounded formulas of $x$ and $n$ to the set of bounded formulas of $\mathrm{Sum}$ applied to $x_{1}$ and $x$ and $n$ defined as the map term relative equivalence of the function that maps $x_{2}$ to $\operatorname{constantsVarsEquivLeft}$ and the function that maps $x_{3}$ to $\operatorname{sumEmpty}$ applied to the set of relations of $L$ and $x_{3}$ and the set of relations of $\operatorname{constantsOn}$ applied to $x_{1}$ and $x_{3}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from natural numbers $n$ to elements of $\mathrm{motive}$ applied to $n$ and $\operatorname{falsum}$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{1}$ and terms $x_{1}$ of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n_{1}$ and terms $x_{2}$ of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n_{1}$ to elements of $\mathrm{motive}$ applied to $n_{1}$ and the equal of $x_{1}$ and $x_{2}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{2}$ and natural numbers $l$ and relations $R$ of $L$ and $l$ and functions $\mathrm{ts}$ from elements of $\mathrm{Fin}$ applied to $l$ to terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n_{2}$ to elements of $\mathrm{motive}$ applied to $n_{2}$ and the relation of $R$ and $\mathrm{ts}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{3}$ and bounded formulas $x_{4}$ of $x$ and $n_{3}$ and bounded formulas $x_{5}$ of $x$ and $n_{3}$ to elements of $\mathrm{motive}$ applied to $n_{3}$ and $\operatorname{imp}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{4}$ and bounded formulas $f$ of $x$ and $n_{4} + 1$ to elements of $\mathrm{motive}$ applied to $n_{4}$ and $\operatorname{all}$ applied to $f$.

the equal of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then the equal of $x_{1}$ and $x_{2}$ is a bounded formula of $x$ and $n$.

Let $x_{1}$ be a bounded formula of $x$ and $n + 1$. Then $\operatorname{ex}$ applied to $x_{1}$ is a bounded formula of $x$ and $n$ defined as $\operatorname{not}$ applied to $\operatorname{all}$ applied to $\operatorname{not}$ applied to $x_{1}$.

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{exs}$ applied to $x_{1}$ is a formula of $L$ and $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_exs\_\_\_f}$ and $x_{1}$.

$\operatorname{falsum}$ is a bounded formula of $x$ and $n$.

the free variable finite set of x2 (from the name)

Let $x_{2}$ be a bounded formula of $x$ and $n$. Then the free variable finite set of $x_{2}$ is a finite set of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_freeVarFinset\_\_\_f}$.

the infimum of f (from the name)

Let $f$ be a function from elements of $x_{1}$ to bounded formulas of $x$ and $n$. Then the infimum of $f$ is a bounded formula of $x$ and $n$ defined as $\operatorname{foldr}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\MinminMACRoAG {x_{2}}{x_{3}}$, the top and $\operatorname{map}$ applied to $f$ and the list of the universal set.

the supremum of f (from the name)

Let $f$ be a function from elements of $x_{1}$ to bounded formulas of $x$ and $n$. Then the supremum of $f$ is a bounded formula of $x$ and $n$ defined as $\operatorname{foldr}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\MaxmaxMACRoAF {x_{2}}{x_{3}}$, the bottom and $\operatorname{map}$ applied to $f$ and the list of the universal set.

Let $x_{1}$ and $x_{2}$ be bounded formulas of $x$ and $n$. Then $\operatorname{iff}$ applied to $x_{1}$ and $x_{2}$ is a bounded formula of $x$ and $n$ defined as $\MinminMACRoAG {\operatorname{imp} (x_{1} , x_{2})}{\operatorname{imp} (x_{2} , x_{1})}$.

Let $x_{1}$ and $x_{2}$ be bounded formulas of $x$ and $n$. Then $\operatorname{imp}$ applied to $x_{1}$ and $x_{2}$ is a bounded formula of $x$ and $n$.

Let $\mathrm{n'}$ and $\mathrm{\_m}$ be natural numbers. Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{liftAt}$ applied to $\mathrm{n'}$, $\mathrm{\_m}$ and $x_{1}$ is a bounded formula of $x$ and $n + \mathrm{n'}$.

the map term relation of fr and n2 (from the name)

Let $\mathrm{ft}$ be a function from natural numbers $n_{3}$ and terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n_{3}$ to terms of $\mathrm{L'}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $\mathrm{Fin}$ applied to $g$ applied to $n_{3}$. Let $\mathrm{fr}$ be a function from natural numbers $n_{2}$ and relations of $L$ and $n_{2}$ to relations of $\mathrm{L'}$ and $n_{2}$. Let $h$ be a function from natural numbers $n_{1}$ and bounded formulas of $x_{1}$ and $g$ applied to $n_{1} + 1$ to bounded formulas of $x_{1}$ and $g (n_{1})+ 1$. Let $x_{2}$ be a bounded formula of $x$ and $n$. Then the map term relation of $n_{2}$ and $\mathrm{fr}$ is a bounded formula of $x_{1}$ and $g$ applied to $n$ defined as the function that maps $n_{1}$, $h$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $\mathrm{fr}$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_mapTermRel\_\_\_f}$ applied to $n_{3}$, $\mathrm{ft}$ and $n_{2}$, $n_{1}$, $h$ and $x_{2}$.

the map term relative equivalence of ft and n2 (from the name)

Let $\mathrm{ft}$ be a function from natural numbers $n_{2}$ to equivalences from the set of terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n_{2}$ to the set of terms of $\mathrm{L'}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $\mathrm{Fin}$ applied to $n_{2}$. Let $\mathrm{fr}$ be a function from natural numbers $n_{1}$ to equivalences from the set of relations of $L$ and $n_{1}$ to the set of relations of $\mathrm{L'}$ and $n_{1}$. Then the map term relative equivalence of $n_{2}$ and $\mathrm{ft}$ is an equivalence from the set of bounded formulas of $x$ and $n$ to the set of bounded formulas of $x_{1}$ and $n$.

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then $\operatorname{not}$ applied to $x_{1}$ is a bounded formula of $x$ and $n$ defined as $\operatorname{imp}$ applied to $x_{1}$ and the bottom.

the relation of R and ts (from the name)

Let $R$ be a relation of $L$ and $l$. Let $\mathrm{ts}$ be a function from elements of $\mathrm{Fin}$ applied to $l$ to terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then the relation of $R$ and $\mathrm{ts}$ is a bounded formula of $x$ and $n$.

Let $g$ be a function from elements of $x$ to elements of $\mathrm{Sum}$ applied to $x_{1}$ and $\mathrm{Fin}$ applied to $n$. Let $x_{2}$ be a bounded formula of $x$ and $k$. Then $\operatorname{relabel}$ applied to $g$ and $x_{2}$ is a bounded formula of $x_{1}$ and $n + k$.

Let $g$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{relabelEquiv}$ applied to $g$ is an equivalence from the set of bounded formulas of $x$ and $k$ to the set of bounded formulas of $x_{1}$ and $k$ defined as the map term relative equivalence of the function that maps $\mathrm{\_n}$ to $\operatorname{relabelEquiv}$ applied to the sum congruence of $g$ and the identity of $\mathrm{Fin}$ applied to $\mathrm{\_n}$ and the function that maps $\mathrm{\_n1}$ to the identity of the set of relations of $L$ and $\mathrm{\_n1}$.

Let $x_{3}$ be a bounded formula of $x$ and $n$. Let $\mathrm{\_f}$ be a function from elements of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{freeVarFinset} (x_{3})}{x_{5}})}$ to elements of $x_{1}$. Then $\operatorname{restrictFreeVar}$ applied to $x_{3}$ and $\mathrm{\_f}$ is a bounded formula of $x_{1}$ and $n$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_restrictFreeVar\_\_\_f}$ and $\mathrm{\_f}$.

the substitution of x2 and f (from the name)

Let $x_{2}$ be a bounded formula of $x$ and $n$. Let $f$ be a function from elements of $x$ to terms of $L$ and $x_{1}$. Then the substitution of $x_{2}$ and $f$ is a bounded formula of $x_{1}$ and $n$ defined as the map term relation of the function that maps $x_{5}$ to $\mathrm{id}$ and $x_{2}$.

the formula of x1 (from the name)

Let $x_{1}$ be a bounded formula of $x$ and $n$. Then the formula of $x_{1}$ is a formula of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_BoundedFormula\_\_toFormula\_\_\_f}$.

formula of L and x (from the name)

Let $L$ be a language. Let $x$ be a set. Then a formula of $L$ and $x$ is an element of the function that maps $L$ and $x$ to the set of bounded formulas of $x$ and $0$.

the equivalence sentence (from the name)

The equivalence sentence is an equivalence from the set of formulas of $L$ and $x$ to the set of sentences of $\operatorname{withConstants}$ applied to $L$ and $x$ defined as the inverse of the composition of $\operatorname{constantsVarsEquiv}$ and $\operatorname{relabelEquiv}$ applied to $\operatorname{sumEmpty}$ applied to $x$ and $\mathrm{Empty}$.

Let $x_{2}$ be a formula of $L$ and $x$. Then $\operatorname{exClosure}$ applied to $x_{2}$ is a sentence of $L$ defined as $\operatorname{iExs}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{freeVarFinset} (x_{2})}{x_{3}})}$ and $\operatorname{relabel}$ applied to $\operatorname{inr}$ and $\operatorname{restrictFreeVar}$ applied to $x_{2}$ and $\mathrm{id}$.

the graph of f (from the docstring)

Let $f$ be a function of $L$ and $n$. Then the graph of $f$ is a formula of $L$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the equal of the variable of $0$ and the function of $f$ and the function that maps $i$ to the variable of $\operatorname{succ}$ applied to $i$.

Let $x_{1}$ be a set. Let $x_{2}$ be a formula of $L$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{iAlls}$ applied to $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$.

Let $x_{1}$ be a set. Let $x_{2}$ be a formula of $L$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{iExs}$ applied to $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$.

Let $x_{1}$ be a set. Let $x_{2}$ be a formula of $L$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{iExsUnique}$ applied to $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$ defined as $\operatorname{iExs}$ applied to $x_{1}$ and the minimum of $x_{2}$ and $\operatorname{iAlls}$ applied to $x_{1}$ and $\operatorname{imp}$ applied to $\operatorname{relabel}$ applied to the function that maps $a$ to $\operatorname{elim}$ applied to $\operatorname{comp}$ applied to $\operatorname{inl}$ and $\operatorname{inl}$, $\operatorname{inr}$ and $a$ and $x_{2}$ and the infimum of the function that maps $g$ to the equal of the variable of $\operatorname{inr}$ applied to $g$ and the variable of $\operatorname{inl}$ applied to $\operatorname{inr}$ applied to $g$.

the infimum of f (from the name)

Let $f$ be a function from elements of $x$ to formulas of $L$ and $x_{1}$. Then the infimum of $f$ is a formula of $L$ and $x_{1}$ defined as the infimum of $f$.

the supremum of f (from the name)

Let $f$ be a function from elements of $x$ to formulas of $L$ and $x_{1}$. Then the supremum of $f$ is a formula of $L$ and $x_{1}$ defined as the supremum of $f$.

Let $x_{1}$ and $x_{2}$ be formulas of $L$ and $x$. Then $\operatorname{iff}$ applied to $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$ defined as $\operatorname{iff}$ applied to $x_{1}$ and $x_{2}$.

Let $x_{1}$ and $x_{2}$ be formulas of $L$ and $x$. Then $\operatorname{imp}$ applied to $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$ defined as $\operatorname{imp}$ applied to $x_{1}$ and $x_{2}$.

Let $x_{1}$ be a formula of $L$ and $x$. Then $\operatorname{not}$ applied to $x_{1}$ is a formula of $L$ and $x$ defined as $\operatorname{not}$ applied to $x_{1}$.

Let $g$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a formula of $L$ and $x$. Then $\operatorname{relabel}$ applied to $g$ and $x_{2}$ is a formula of $L$ and $x_{1}$ defined as $\operatorname{relabel}$ applied to $\operatorname{comp}$ applied to $\operatorname{inl}$ and $g$ and $x_{2}$.

Let $f$ be a function of $L$ and $1$. Let $t$ be a term of $L$ and $x$. Then $\mathrm{FirstOrder\_\_Language\_\_Functions\_\_apply\_u2081\_}$ applied to $f$ and $t$ is a term of $L$ and $x$ defined as the function of $f$ and $\operatorname{vecCons}$ applied to $t$ and $\operatorname{vecEmpty}$.

Let $f$ be a function of $L$ and $2$. Let $x_{1}$ and $x_{2}$ be terms of $L$ and $x$. Then $\mathrm{FirstOrder\_\_Language\_\_Functions\_\_apply\_u2082\_}$ applied to $f$, $x_{1}$ and $x_{2}$ is a term of $L$ and $x$ defined as the function of $f$ and $\operatorname{vecCons}$ applied to $x_{1}$ and $\operatorname{vecCons}$ applied to $x_{2}$ and $\operatorname{vecEmpty}$.

Let $x_{1}$ be an equivalence of $L$ and $\mathrm{L'}$. Then $\operatorname{onBoundedFormula}$ applied to $x_{1}$ is an equivalence from the set of bounded formulas of $x$ and $n$ to the set of bounded formulas of $x$ and $n$.

Let $x_{1}$ be an equivalence of $L$ and $\mathrm{L'}$. Then $\operatorname{onFormula}$ applied to $x_{1}$ is an equivalence from the set of formulas of $L$ and $x$ to the set of formulas of $\mathrm{L'}$ and $x$ defined as $\operatorname{onBoundedFormula}$ applied to $x_{1}$.

Let $x$ be an equivalence of $L$ and $\mathrm{L'}$. Then $\operatorname{onSentence}$ applied to $x$ is an equivalence from the set of sentences of $L$ to the set of sentences of $\mathrm{L'}$ defined as $\operatorname{onFormula}$ applied to $x$.

Let $x_{1}$ be an equivalence of $L$ and $\mathrm{L'}$. Then $\operatorname{onTerm}$ applied to $x_{1}$ is an equivalence from the set of terms of $L$ and $x$ to the set of terms of $\mathrm{L'}$ and $x$.

Let $g$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{1}$ be a bounded formula of $x$ and $k$. Then $\operatorname{onBoundedFormula}$ applied to $g$ and $x_{1}$ is a bounded formula of $x$ and $k$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{FirstOrder\_\_Language\_\_LHom\_\_onBoundedFormula\_\_\_f}$ applied to $g$.

Let $g$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{1}$ be a formula of $L$ and $x$. Then $\operatorname{onFormula}$ applied to $g$ and $x_{1}$ is a formula of $\mathrm{L'}$ and $x$ defined as $\operatorname{onBoundedFormula}$ applied to $g$ and $x_{1}$.

Let $g$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x$ be a sentence of $L$. Then $\operatorname{onSentence}$ applied to $g$ and $x$ is a sentence of $\mathrm{L'}$ defined as $\operatorname{onFormula}$ applied to $g$ and $x$.

Let $x_{1}$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{2}$ be a term of $L$ and $x$. Then $\operatorname{onTerm}$ applied to $x_{1}$ and $x_{2}$ is a term of $\mathrm{L'}$ and $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_LHom\_\_onTerm\_\_\_f}$ applied to $x_{1}$.

Let $g$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $T$ be a theory of $L$. Then $\operatorname{onTheory}$ applied to $g$ and $T$ is a theory of $\mathrm{L'}$ defined as the image of $\operatorname{onSentence}$ applied to $g$ and $T$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{antisymmetric}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{all}$ applied to $\operatorname{imp}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{imp}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{bdEqual}$ applied to $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$.

the bounded formula of R and ts (from the name)

Let $R$ be a relation of $L$ and $n$. Let $\mathrm{ts}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $l$. Then the bounded formula of $R$ and $\mathrm{ts}$ is a bounded formula of $x$ and $l$ defined as the relation of $R$ and $\mathrm{ts}$.

the bounded formula of r and t (from the name)

Let $r$ be a relation of $L$ and $1$. Let $t$ be a term of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then the bounded formula of $r$ and $t$ is a bounded formula of $x$ and $n$ defined as the bounded formula of $r$ and $\operatorname{vecCons}$ applied to $t$ and $\operatorname{vecEmpty}$.

the bounded formula of x1 and x2 (from the name)

Let $r$ be a relation of $L$ and $2$. Let $x_{1}$ and $x_{2}$ be terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then the bounded formula of $x_{1}$ and $x_{2}$ is a bounded formula of $x$ and $n$ defined as the bounded formula of $r$ and $\operatorname{vecCons}$ applied to $x_{1}$ and $\operatorname{vecCons}$ applied to $x_{2}$ and $\operatorname{vecEmpty}$.

the formula of R and ts (from the name)

Let $R$ be a relation of $L$ and $n$. Let $\mathrm{ts}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to terms of $L$ and $x$. Then the formula of $R$ and $\mathrm{ts}$ is a formula of $L$ and $x$ defined as the bounded formula of $R$ and the function that maps $i$ to $\operatorname{relabel}$ applied to $\operatorname{inl}$ and $\mathrm{ts}$ applied to $i$.

the formula of r and t (from the name)

Let $r$ be a relation of $L$ and $1$. Let $t$ be a term of $L$ and $x$. Then the formula of $r$ and $t$ is a formula of $L$ and $x$ defined as the formula of $r$ and $\operatorname{vecCons}$ applied to $t$ and $\operatorname{vecEmpty}$.

the formula of x1 and x2 (from the name)

Let $r$ be a relation of $L$ and $2$. Let $x_{1}$ and $x_{2}$ be terms of $L$ and $x$. Then the formula of $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$ defined as the formula of $r$ and $\operatorname{vecCons}$ applied to $x_{1}$ and $\operatorname{vecCons}$ applied to $x_{2}$ and $\operatorname{vecEmpty}$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{irreflexive}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{not}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{reflexive}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{symmetric}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{all}$ applied to $\operatorname{imp}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{total}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{all}$ applied to the maximum of the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$.

Let $r$ be a relation of $L$ and $2$. Then $\operatorname{transitive}$ applied to $r$ is a sentence of $L$ defined as $\operatorname{all}$ applied to $\operatorname{all}$ applied to $\operatorname{all}$ applied to $\operatorname{imp}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{imp}$ applied to the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $1$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $2$ and the bounded formula of $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $0$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $2$.

sentence of L (from the name)

Let $L$ be a language. Then a sentence of $L$ is an element of the function that maps $L$ to the set of formulas of $L$ and $\mathrm{Empty}$.

Let $L$ be a language. Let $n$ be a natural number. Then $\operatorname{cardGe}$ applied to $L$ and $n$ is a sentence of $L$ defined as $\operatorname{exs}$ applied to $\operatorname{foldr}$ applied to the function that maps $x$ and $x_{1}$ to $\MinminMACRoAG {x}{x_{1}}$, the top and $\operatorname{map}$ applied to the function that maps $\mathrm{ij}$ to $\operatorname{not}$ applied to $\operatorname{bdEqual}$ applied to $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $\ProdfstMACRoZ {\mathrm{ij}}$ and $\operatorname{comp}$ applied to $\operatorname{var}$, $\operatorname{inr}$ and $\ProdsndMACRoAA {\mathrm{ij}}$ and $\operatorname{filter}$ applied to the function that maps $\mathrm{ij1}$ to $\operatorname{decide}$ applied to $\mathrm{Neq} (\ProdfstMACRoZ {\mathrm{ij1}}, \ProdsndMACRoAA {\mathrm{ij1}})$ and $\operatorname{sprod}$ applied to $\operatorname{finRange}$ applied to $n$ and $\operatorname{finRange}$ applied to $n$.

term of L and x (from the name)

Let $L$ be a language. Let $x$ be a set. Then the terms of $L$ and $x$ are a basic type.

Let $x_{1}$ and $x_{2}$ be terms of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{bdEqual}$ applied to $x_{1}$ and $x_{2}$ is a bounded formula of $x$ and $n$ defined as the equal of $x_{1}$ and $x_{2}$.

Let $x_{2}$ be a term of $\operatorname{withConstants}$ applied to $L$ and $x_{1}$ and $x$. Then $\operatorname{constantsToVars}$ applied to $x_{2}$ is a term of $L$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_constantsToVars\_\_\_f}$.

$\operatorname{constantsVarsEquiv}$ is an equivalence from the set of terms of $\operatorname{withConstants}$ applied to $L$ and $x_{1}$ and $x$ to the set of terms of $L$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x$.

$\operatorname{constantsVarsEquivLeft}$ is an equivalence from the set of terms of $\operatorname{withConstants}$ applied to $L$ and $x_{2}$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to the set of terms of $L$ and $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $x_{2}$ and $x$ and $x_{1}$ defined as the composition of $\operatorname{constantsVarsEquiv}$ and the inverse of $\operatorname{relabelEquiv}$ applied to the sum associator of $x$ and $x_{1}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to the variable of $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $l$ and functions $\mathrm{\_f}$ of $L$ and $l$ and functions $\mathrm{\_ts}$ from elements of $\mathrm{Fin}$ applied to $l$ to terms of $L$ and $x$ to elements of $\mathrm{motive}$ applied to the function of $\mathrm{\_f}$ and $\mathrm{\_ts}$.

the equal of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be terms of $L$ and $x$. Then the equal of $x_{1}$ and $x_{2}$ is a formula of $L$ and $x$ defined as $\operatorname{bdEqual}$ applied to $\operatorname{relabel}$ applied to $\operatorname{inl}$ and $x_{1}$ and $\operatorname{relabel}$ applied to $\operatorname{inl}$ and $x_{2}$.

the function of _f and _ts (from the name)

Let $\mathrm{\_f}$ be a function of $L$ and $l$. Let $\mathrm{\_ts}$ be a function from elements of $\mathrm{Fin}$ applied to $l$ to terms of $L$ and $x$. Then the function of $\mathrm{\_f}$ and $\mathrm{\_ts}$ is a term of $L$ and $x$.

Let $\mathrm{n'}$ and $m$ be natural numbers. Let $x_{1}$ be a term of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{liftAt}$ applied to $\mathrm{n'}$, $m$ and $x_{1}$ is a term of $L$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Fin}$ applied to $n + \mathrm{n'}$ defined as $\operatorname{relabel}$ applied to $\operatorname{map}$ applied to $\mathrm{id}$ and the function that maps $i$ to $\iteMACRoG {\mathrm{Lt} (\operatorname{val} (i), m)}{\operatorname{castAdd} (\mathrm{n'} , i)}{\operatorname{addNat} (i , \mathrm{n'})}$ and $x_{1}$.

Let $g$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a term of $L$ and $x$. Then $\operatorname{relabel}$ applied to $g$ and $x_{2}$ is a term of $L$ and $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_relabel\_\_\_f}$ applied to $g$.

Let $g$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{relabelEquiv}$ applied to $g$ is an equivalence from the set of terms of $L$ and $x$ to the set of terms of $L$ and $x_{1}$.

Let $t$ be a term of $L$ and $x$. Let $\mathrm{\_f}$ be a function from elements of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{varFinset} (t)}{x_{4}})}$ to elements of $x_{1}$. Then $\operatorname{restrictVar}$ applied to $t$ and $\mathrm{\_f}$ is a term of $L$ and $x_{1}$ defined as $\operatorname{brecOn}$ applied to $t$, $\mathrm{FirstOrder\_\_Language\_\_Term\_\_restrictVar\_\_\_f}$ and $\mathrm{\_f}$.

Let $t$ be a term of $L$ and $\mathrm{Sum}$ applied to $x$ and $x_{3}$. Let $\mathrm{\_f}$ be a function from elements of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{varFinsetLeft} (t)}{x_{5}})}$ to elements of $x_{1}$. Then $\operatorname{restrictVarLeft}$ applied to $t$ and $\mathrm{\_f}$ is a term of $L$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{3}$ defined as $\operatorname{brecOn}$ applied to $t$, $\mathrm{FirstOrder\_\_Language\_\_Term\_\_restrictVarLeft\_\_\_f}$ and $\mathrm{\_f}$.

the substitution of x2 and x3 (from the name)

Let $x_{2}$ be a term of $L$ and $x$. Let $x_{3}$ be a function from elements of $x$ to terms of $L$ and $x_{1}$. Then the substitution of $x_{2}$ and $x_{3}$ is a term of $L$ and $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{FirstOrder\_\_Language\_\_Term\_\_subst\_\_\_f}$ and $x_{3}$.

the substitution function of x1 and x2 (from the name)

Let $x_{1}$ be a term of $L$ and $x$. Let $x_{2}$ be a function from natural numbers $n$ and functions of $L$ and $n$ to terms of $\mathrm{L'}$ and $\mathrm{Fin}$ applied to $n$. Then the substitution function of $x_{1}$ and $n$ is a term of $\mathrm{L'}$ and $x$ defined as the function that maps $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{FirstOrder\_\_Language\_\_Term\_\_substFunc\_\_\_f}$, $n$ and $x_{2}$.

the variable of x1 (from the name)

Let $x_{1}$ be an element of $x$. Then the variable of $x_{1}$ is a term of $L$ and $x$.

the variable finite set of x2 (from the name)

Let $x_{2}$ be a term of $L$ and $x$. Then the variable finite set of $x_{2}$ is a finite set of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_varFinset\_\_\_f}$.

the left variable finite set of x3 (from the name)

Let $x_{3}$ be a term of $L$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then the left variable finite set of $x_{3}$ is a finite set of $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_varFinsetLeft\_\_\_f}$.

Let $x_{2}$ be a term of $L$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x$. Then $\operatorname{varsToConstants}$ applied to $x_{2}$ is a term of $\operatorname{withConstants}$ applied to $L$ and $x_{1}$ and $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FirstOrder\_\_Language\_\_Term\_\_varsToConstants\_\_\_f}$.

theory of L (from the name)

Let $L$ be a language. Then a theory of $L$ is an element of the function that maps $L$ to the power set of the set of sentences of $L$.

the distinct constant theory of L and s (from the name)

Let $L$ be a language. Let $s$ be an element of $\wp x$. Then the distinct constant theory of $L$ and $s$ is a theory of $\operatorname{withConstants}$ applied to $L$ and $x$ defined as the image of the function that maps $\mathrm{ab}$ to $\operatorname{not}$ applied to the equal of $\operatorname{term}$ applied to the congruence relation of $L$ and $\ProdfstMACRoZ {\mathrm{ab}}$ and $\operatorname{term}$ applied to the congruence relation of $L$ and $\ProdsndMACRoAA {\mathrm{ab}}$ and $\operatorname{inter}$ applied to $\operatorname{sprod}$ applied to $s$ and $s$ and the complement of the diagonal of $x$.

the infinite theory of L (from the name)

Let $L$ be a language. Then the infinite theory of $L$ is a theory of $L$ defined as the range of $\operatorname{cardGe}$ applied to $L$.

the nonempty theory of L (from the name)

Let $L$ be a language. Then the nonempty theory of $L$ is a theory of $L$ defined as $\operatorname{singleton}$ applied to $\operatorname{cardGe}$ applied to $L$ and $1$.

complete type of T and x (from the name)

Let $T$ be a theory of $L$. Let $x$ be a set. Then the complete types of $T$ and $x$ are a basic type.

the underlying theory of self (from the docstring)

Let $\mathrm{self}$ be a complete type of $T$ and $x$. Then the underlying theory of $\mathrm{self}$ is a theory of $\operatorname{withConstants}$ applied to $L$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $T$ be a theory of $L$. Let $M$ and $x_{1}$ be sets. Then $\operatorname{realizedTypes}$ applied to $T$, $M$ and $x_{1}$ is an element of the power set of the set of complete types of $T$ and $x_{1}$ defined as the range of $\operatorname{typeOf}$ applied to $T$.

the type of T and v (from the name)

Let $T$ be a theory of $L$. Let $v$ be a function from elements of $x$ to elements of $M$. Then the type of $T$ and $v$ is a complete type of $T$ and $x$.

Let $T$ be a theory of $L$. Let $x_{1}$ be a sentence of $\operatorname{withConstants}$ applied to $L$ and $x$. Then $\operatorname{typesWith}$ applied to $T$ and $x_{1}$ is an element of the power set of the set of complete types of $T$ and $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that $x_{1}$ is an element of the underlying theory of $p$.