Definitions: Mathlib.Computability, part 1 of 2

Let $x$ be a natural number. Then $\operatorname{pappAck}$ applied to $x$ is a code defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_Partrec\_\_Code\_\_pappAck\_\_\_f}$.

the step of c (from the name)

Let $c$ be a code. Then the step of $c$ is a code defined as the curry of $\operatorname{prec}$ applied to the composition of $c$ and the constant of $1$ and the composition of $c$ and the composition of the right and the right and $0$.

Let $x$ and $x_{1}$ be natural numbers. Then $\mathrm{ack}$ applied to $x$ and $x_{1}$ is a natural number defined as $\mathrm{ack\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $x$ and $x_{1}$.

Let $f$ be a function from real numbers to real numbers. Then $\operatorname{GrowsPolynomially}$ holds for $f$, if for all real numbers $b$, if $b$ is an element of the open interval of $0$ and $1$, then there exists a real number $x$, such that $x > 0$ and there exists a real number $x_{1}$ such that $x_{1} > 0$ and $\operatorname{Eventually}$ holds for the function that maps $x_{2}$ to the proposition that for all real numbers $u$, if $u$ is an element of $\SetIccMACRoP {(b \times x_{2})}{x_{2}}$, then $\MembershipmemMACRoT {\SetIccMACRoP {(x \times f (x_{2}))}{(x_{1} \times f (x_{2}))}}{f (u)}$ and $\operatorname{atTop}$.

Let $T$ be a function from natural numbers to real numbers. Let $g$ be a function from real numbers to real numbers. Let $a$ and $b$ be functions from elements of $x$ to real numbers. Let $r$ be a function from elements of $x$ and natural numbers to natural numbers. Then the elements of $\mathrm{AkraBazziRecurrence}$ applied to $T$, $g$, $a$, $b$ and $r$ are a basic type.

Let $g$ be a function from real numbers to real numbers. Let $a$ and $b$ be functions from elements of $x$ to real numbers. Let $n$ be a natural number. Then $\operatorname{asympBound}$ applied to $g$, $a$, $b$ and $n$ is a real number defined as the sum of $n ^ {\operatorname{p} (a , b)}$ and the sum transform of $0$ and $n$.

Let $b$ be a function from elements of $x$ to real numbers. Then $\mathrm{AkraBazziRecurrence\_\_max\_bi}$ applied to $b$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Finite\_\_exists\_max}$ applied to $b$.

Let $b$ be a function from elements of $x$ to real numbers. Then $\mathrm{AkraBazziRecurrence\_\_min\_bi}$ applied to $b$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Finite\_\_exists\_min}$ applied to $b$.

Let $\mathrm{self}$ be an element of $\mathrm{AkraBazziRecurrence}$ applied to $T$, $g$, $a$, $b$ and $r$. Then $\mathrm{AkraBazziRecurrence\_\_n\_u2080\_}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $a$ and $b$ be functions from elements of $x$ to real numbers. Then $\operatorname{p}$ applied to $a$ and $b$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{AkraBazziRecurrence\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Computability\_\_AkraBazzi\_\_SumTransform\_\_2571614175\_\_\_hygCtx\_\_\_hyg\_\_54}$, $a$ and $b$.

Let $n$ be a real number. Then $\operatorname{smoothingFn}$ applied to $n$ is a real number defined as the quotient of $1$ and the logarithm of $n$.

the sum transform of x and n (from the name)

Let $p$ be a real number. Let $g$ be a function from real numbers to real numbers. Let $x$ and $n$ be natural numbers. Then the sum transform of $x$ and $n$ is a real number defined as $n ^ {p}\times \FinsetSum {(\FinsetIcoMACRoO {x}{n})}{u}{(\frac{ g (u)}{u ^ {(p + 1)}})}$.

context free grammar of T (from the name)

Let $T$ be a set. Then the context free grammars of $T$ are a basic type.

Let $g$ be a context free grammar of $T$. Let $x$ and $x_{1}$ be lists of symbols of $T$ and $\operatorname{NT}$ applied to $g$. Then $\operatorname{Derives}$ holds for $g$, $x$ and $x_{1}$, if $\operatorname{ReflTransGen}$ holds for $\operatorname{Produces}$ applied to $g$, $x$ and $x_{1}$.

Let $g$ be a context free grammar of $T$. Let $s$ be a list of symbols of $T$ and $\operatorname{NT}$ applied to $g$. Then $\operatorname{Generates}$ holds for $g$ and $s$, if $\operatorname{Derives}$ holds for $g$, $\operatorname{cons}$ applied to $\operatorname{nonterminal}$ applied to $\operatorname{initial}$ applied to $g$ and $\operatorname{nil}$ and $s$.

Let $\mathrm{self}$ be a context free grammar of $T$. Then an element of $\operatorname{NT}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $g$ be a context free grammar of $T$. Let $u$ and $v$ be lists of symbols of $T$ and $\operatorname{NT}$ applied to $g$. Then $\operatorname{Produces}$ holds for $g$, $u$ and $v$, if there exists a context free rule $r$ of $T$ and $\operatorname{NT}$ applied to $g$, such that $r$ is an element of the rule of $g$ and $\operatorname{Rewrites}$ holds for $r$, $u$ and $v$.

Let $\mathrm{self}$ be a context free grammar of $T$. Then $\operatorname{initial}$ applied to $\mathrm{self}$ is an element of $\operatorname{NT}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the language of g (from the name)

Let $g$ be a context free grammar of $T$. Then the language of $g$ is a language of $T$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to $\operatorname{Generates}$ applied to $g$ and $\operatorname{map}$ applied to $\operatorname{terminal}$ and $w$.

the reverse of g (from the name)

Let $g$ be a context free grammar of $T$. Then the reverse of $g$ is a context free grammar of $T$.

the rule of self (from the name)

Let $\mathrm{self}$ be a context free grammar of $T$. Then the rule of $\mathrm{self}$ is a finite set of the set of context free rules of $T$ and $\operatorname{NT}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

context free rule of T and N (from the name)

Let $T$ and $N$ be sets. Then the context free rules of $T$ and $N$ are a basic type.

Let $r$ be a context free rule of $T$ and $N$. Let $x$ and $x_{1}$ be lists of symbols of $T$ and $N$. Then we can say that $\operatorname{Rewrites}$ holds for $r$, $x$ and $x_{1}$.

Assume that $\operatorname{Rewrites}$ holds for $r$, $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

the input of self (from the name)

Let $\mathrm{self}$ be a context free rule of $T$ and $N$. Then the input of $\mathrm{self}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the output of self (from the name)

Let $\mathrm{self}$ be a context free rule of $T$ and $N$. Then the output of $\mathrm{self}$ is a list of symbols of $T$ and $N$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the reverse of r (from the name)

Let $r$ be a context free rule of $T$ and $N$. Then the reverse of $r$ is a context free rule of $T$ and $N$ defined as $\operatorname{mk}$ applied to the input of $r$ and $\operatorname{reverse}$ applied to the output of $r$.

L is a context free (from the name)

Let $L$ be a language of $T$. Then $L$ is a context free, if there exists a context free grammar $g$ of $T$, such that the language of $g$ is equal to $L$.

the representation of x4 and x5 (from the name)

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{DFA}$ applied to $x$ and $x_{1}$ are a basic type.

Let $\mathrm{self}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{accept}$ applied to $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{accepts}$ applied to $M$ is a language of $x$ defined as $\operatorname{acceptsFrom}$ applied to $M$ and the start of $M$.

Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $s$ be an element of $x_{1}$. Then $\operatorname{acceptsFrom}$ applied to $M$ and $s$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {\operatorname{accept} (M)}{\operatorname{evalFrom} (M , s , x_{2})}$.

the preimage of f and M (from the name)

Let $f$ be a function from elements of $x_{2}$ to elements of $x$. Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Then the preimage of $f$ and $M$ is an element of $\mathrm{DFA}$ applied to $x_{2}$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to the step of $s$ and $f$ applied to $a$, the start of $M$ and $\operatorname{accept}$ applied to $M$.

the evaluation of M and x2 (from the name)

Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then the evaluation of $M$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{evalFrom}$ applied to $M$, the start of $M$ and $x_{2}$.

Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $s$ be an element of $x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{evalFrom}$ applied to $M$, $s$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{foldl}$ applied to $\operatorname{step}$, $s$ and $x_{2}$.

the intersection of M1 and M2 (from the name)

Let $M_{1}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $M_{2}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{2}$. Then the intersection of $M_{1}$ and $M_{2}$ is an element of $\mathrm{DFA}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to $\ProdmkMACRoU {\operatorname{step} (\ProdfstMACRoZ {s}, a)}{\operatorname{step} (\ProdsndMACRoAA {s}, a)}$, $\ProdmkMACRoU {\operatorname{start} (M_{1})}{\operatorname{start} (M_{2})}$ and $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to the proposition that $\MembershipmemMACRoT {\operatorname{accept} (M_{1})}{\ProdfstMACRoZ {s_{1}}}$ and $\MembershipmemMACRoT {\operatorname{accept} (M_{2})}{\ProdsndMACRoAA {s_{1}}}$.

the reindexing of g (from the name)

Let $g$ be an equivalence from $x_{1}$ to $x_{2}$. Then the reindexing of $g$ is an element of $\EquivMACRoAE {\mathrm{DFA} (x , x_{1})}{\mathrm{DFA} (x , x_{2})}$.

the start of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Then the start of $\mathrm{self}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the step of x2 and x3 (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Let $x_{3}$ be an element of $x$. Then the step of $x_{2}$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the union of M1 and M2 (from the name)

Let $M_{1}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Let $M_{2}$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{2}$. Then the union of $M_{1}$ and $M_{2}$ is an element of $\mathrm{DFA}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to $\ProdmkMACRoU {\operatorname{step} (\ProdfstMACRoZ {s}, a)}{\operatorname{step} (\ProdsndMACRoAA {s}, a)}$, $\ProdmkMACRoU {\operatorname{start} (M_{1})}{\operatorname{start} (M_{2})}$ and $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to the proposition that $\MembershipmemMACRoT {\operatorname{accept} (M_{1})}{\ProdfstMACRoZ {s_{1}}}$ or $\MembershipmemMACRoT {\operatorname{accept} (M_{2})}{\ProdsndMACRoAA {s_{1}}}$.

L is a regular (from the name)

Let $L$ be a language of $T$. Then $L$ is a regular, if there exists a set $x$, such that there exists an element $x_{1}$ of $\mathrm{Fintype}$ applied to $x$, such that there exists an element $M$ of $\mathrm{DFA}$ applied to $T$ and $x$, such that $\EqtMACRoH {\operatorname{accepts} (M)}{L}$.

encoding of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the encodings of $x$ and $x_{1}$ are a basic type.

the decode of self and x2 (from the name)

Let $\mathrm{self}$ be an encoding of $x$ and $x_{1}$. Let $x_{2}$ be a list of elements of $x_{1}$. Then the decode of $\mathrm{self}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

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

Let $\mathrm{self}$ be an encoding of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then the encoding function of $\mathrm{self}$ and $x_{2}$ is a list of elements of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

the decode bool of x (from the name)

Let $x$ be a list of elements of $\mathrm{Bool}$. Then the decode bool of $x$ is an element of $\mathrm{Bool}$.

the decode natural number of x (from the name)

Let $x$ be a list of elements of $\mathrm{Bool}$. Then the decode natural number of $x$ is a natural number defined as the cast numerator of the decode numerator of $x$.

the decode numerator of x (from the name)

Let $x$ be a list of elements of $\mathrm{Bool}$. Then the decode numerator of $x$ is a numerator defined as $\iteMACRoG {(\EqtMACRoH {x}{\operatorname{nil}})}{\operatorname{zero}}{\mathrm{castPosNum} (\operatorname{decodePosNum} (x))}$.

the decode positive part numerator of x (from the name)

Let $x$ be a list of elements of $\mathrm{Bool}$. Then the decode positive part numerator of $x$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Computability\_\_decodePosNum\_\_\_f}$.

Let $x$ be an element of $\mathrm{Bool}$. Then $\operatorname{encodeBool}$ applied to $x$ is a list of elements of $\mathrm{Bool}$ defined as $\operatorname{pure}$ applied to $x$.

Let $n$ be a natural number. Then $\operatorname{encodeNat}$ applied to $n$ is a list of elements of $\mathrm{Bool}$ defined as $\operatorname{encodeNum}$ applied to $n$.

Let $x$ be a numerator. Then $\operatorname{encodeNum}$ applied to $x$ is a list of elements of $\mathrm{Bool}$.

Let $x$ be a positive part numerator. Then $\operatorname{encodePosNum}$ applied to $x$ is a list of elements of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Computability\_\_encodePosNum\_\_\_f}$.

the encoding bool bool (from the name)

The encoding bool bool is an encoding of $\mathrm{Bool}$ and $\mathrm{Bool}$.

the encoding list of x (from the name)

Let $x$ be a set. Then the encoding list of $x$ is an encoding of the set of lists of elements of $x$ and $x$.

the encoding natural bool (from the name)

The encoding natural bool is an encoding of $\Natural$ and $\mathrm{Bool}$.

the encoding natural number (from the name)

The encoding natural number is an encoding of $\Natural$ and $\mathrm{Computability\_\_\_u393\_'}$.

the encoding product of ea and eb (from the name)

Let $\mathrm{ea}$ be an encoding of $x$ and $x_{2}$. Let $\mathrm{eb}$ be an encoding of $x_{1}$ and $x_{3}$. Then the encoding product of $\mathrm{ea}$ and $\mathrm{eb}$ is an encoding of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$.

the natural inclusion of x (from the docstring)

Let $x$ be an element of $\mathrm{Bool}$. Then the natural inclusion of $x$ is an element of $\mathrm{Computability\_\_\_u393\_'}$ defined as the bit of $x$.

the section bool of x (from the name)

Let $x$ be an element of $\mathrm{Computability\_\_\_u393\_'}$. Then the section bool of $x$ is an element of $\mathrm{Bool}$.

the unary decode natural number of x (from the name)

Let $x$ be a list of elements of $\mathrm{Bool}$. Then the unary decode natural number of $x$ is a natural number defined as $\operatorname{length}$ applied to $x$.

Let $x$ be a natural number. Then $\operatorname{unaryEncodeNat}$ applied to $x$ is a list of elements of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Computability\_\_unaryEncodeNat\_\_\_f}$.

the unary encoding natural number (from the name)

The unary encoding natural number is an encoding of $\Natural$ and $\mathrm{Bool}$.

The elements of $\mathrm{Computability\_\_\_u393\_'}$ are a basic type.

the bit of b (from the name)

Let $b$ be an element of $\mathrm{Bool}$. Then the bit of $b$ is an element of $\mathrm{Computability\_\_\_u393\_'}$.

the blank (from the name)

The blank is an element of $\mathrm{Computability\_\_\_u393\_'}$.

$\mathrm{Computability\_\_\_u393\_'\_\_bra}$ is an element of $\mathrm{Computability\_\_\_u393\_'}$.

the comma (from the name)

The comma is an element of $\mathrm{Computability\_\_\_u393\_'}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Computability\_\_\_u393\_'\_\_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 the blank and $\mathrm{PULift}$ applied to the set of functions from elements $b$ of $\mathrm{Bool}$ to elements of $\mathrm{motive}$ applied to the bit of $b$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\mathrm{Computability\_\_\_u393\_'\_\_bra}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\mathrm{Computability\_\_\_u393\_'\_\_ket}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the comma.

$\mathrm{Computability\_\_\_u393\_'\_\_ket}$ is an element of $\mathrm{Computability\_\_\_u393\_'}$.

An element of $\mathrm{Computability\_\_\_u393\_'\_\_proxyType}$ is an element of $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Sum}$ applied to $\mathrm{Bool}$ and $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Unit}$.

$\mathrm{Computability\_\_\_u393\_'\_\_proxyTypeEquiv}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Unit} , \mathrm{Sum} (\mathrm{Bool} , \mathrm{Sum} (\mathrm{Unit} , \mathrm{Sum} (\mathrm{Unit} , \mathrm{Unit}))))}{\mathrm{Computability\_\_\_u393\_'}}$.

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then $\mathrm{NFA\_\_to\_u3b5\_NFA}$ applied to $M$ is an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$.

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$ are a basic type.

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ and $x_{3}$ be elements of $x_{1}$. Let $x_{4}$ be a list of elements of $\mathrm{Option}$ applied to $x$. Then we can say that $\mathrm{\_u3b5\_NFA\_\_IsPath}$ holds for $M$, $x_{2}$, $x_{3}$ and $x_{4}$.

Assume that $\mathrm{\_u3b5\_NFA\_\_IsPath}$ holds for $M$, $x_{2}$, $x_{3}$ and $x_{4}$. Then we can say that $\mathrm{\_u3b5\_NFA\_\_IsPath\_\_below}$ holds for $t$.

Let $\mathrm{self}$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Then $\mathrm{\_u3b5\_NFA\_\_accept}$ applied to $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\mathrm{\_u3b5\_NFA\_\_proj2}$ applied to $\mathrm{self}$.

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Then $\mathrm{\_u3b5\_NFA\_\_accepts}$ applied to $M$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exists an element $S$ of $x_{1}$, such that $\MembershipmemMACRoT {\mathrm{\_u3b5\_NFA\_\_accept} (M)}{S}$ and $S$ is an element of the evaluation of $M$ and $x_{2}$.

the evaluation of M and x2 (from the name)

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then the evaluation of $M$ and $x_{2}$ is an element of $\wp x_{1}$ defined as $\mathrm{\_u3b5\_NFA\_\_evalFrom}$ applied to $M$, the start of $M$ and $x_{2}$.

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $\mathrm{start}$ be an element of $\wp x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then $\mathrm{\_u3b5\_NFA\_\_evalFrom}$ applied to $M$, $\mathrm{start}$ and $x_{2}$ is an element of $\wp x_{1}$ defined as $\operatorname{foldl}$ applied to $\mathrm{\_u3b5\_NFA\_\_stepSet}$, the closure of $M$ and $\mathrm{start}$ and $x_{2}$.

the start of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Then the start of $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\mathrm{\_u3b5\_NFA\_\_proj1}$ applied to $\mathrm{self}$.

the step of x2 and x3 (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{Option}$ applied to $x$. Then the step of $x_{2}$ and $x_{3}$ is an element of $\wp x_{1}$ defined as $\mathrm{\_u3b5\_NFA\_\_proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the step set of S and a (from the name)

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Let $a$ be an element of $x$. Then the step set of $S$ and $a$ is an element of $\wp x_{1}$ defined as the union of the function that maps $s$ to the union of the function that maps $h$ to the closure of $M$ and the step of $s$ and $\operatorname{some}$ applied to $a$.

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Then $\mathrm{\_u3b5\_NFA\_\_toNFA}$ applied to $M$ is an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $S$ and $a$ to the closure of $M$ and the step of $S$ and $\operatorname{some}$ applied to $a$, the closure of $M$ and the start of $M$ and $\mathrm{\_u3b5\_NFA\_\_accept}$ applied to $M$.

the closure of M and S (from the name)

Let $M$ be an element of $\mathrm{\_u3b5\_NFA}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Then the closure of $M$ and $S$ is an element of $\wp x_{1}$.

language of x (from the name)

Let $x$ be a set. Then a language of $x$ is an element of the function that maps $x$ to the power set of the set of lists of elements of $x$.

the map of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a ring homomorphism of the set of languages of $x$ and the set of languages of $x_{1}$.

the reverse of l (from the name)

Let $l$ be a language of $x$. Then the reverse of $l$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $w$ to $\MembershipmemMACRoT {l}{\operatorname{reverse} (w)}$.

the reverse isomorphism of x (from the name)

Let $x$ be a set. Then the reverse isomorphism of $x$ is a ring isomorphism of the set of languages of $x$ and the set of multiplicative opposites of the set of languages of $x$.

symbol of T and N (from the name)

Let $T$ and $N$ be sets. Then the symbols of $T$ and $N$ are a basic type.

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 $t$ of $T$ to elements of $\mathrm{motive}$ applied to $\operatorname{terminal}$ applied to $t$ and $\mathrm{PULift}$ applied to the set of functions from elements $n$ of $N$ to elements of $\mathrm{motive}$ applied to $\operatorname{nonterminal}$ applied to $n$.

Let $n$ be an element of $N$. Then $\operatorname{nonterminal}$ applied to $n$ is a symbol of $T$ and $N$.

Let $T$ and $N$ be sets. Then an element of $\operatorname{proxyType}$ applied to $T$ and $N$ is an element of the function that maps $T$ and $N$ to $\mathrm{Sum}$ applied to $T$ and $N$.

Let $T$ and $N$ be sets. Then $\operatorname{proxyTypeEquiv}$ applied to $T$ and $N$ is an equivalence from $\mathrm{Sum}$ applied to $T$ and $N$ to the set of symbols of $T$ and $N$.

the representation of x4 and x5 (from the name)

Let $x_{4}$ be a symbol of $x$ and $x_{1}$. Let $x_{5}$ be a natural number. Then the representation of $x_{4}$ and $x_{5}$ is an element of $\operatorname{Format}$.

the left quotient of L and x1 (from the name)

Let $L$ be a language of $x$. Let $x_{1}$ be a list of elements of $x$. Then the left quotient of $L$ and $x_{1}$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\MembershipmemMACRoT {L}{\operatorname{hAppend} (x_{1} , y)}$.

Let $L$ be a language of $x$. Then $\operatorname{toDFA}$ applied to $L$ is an element of $\mathrm{DFA}$ applied to $x$ and the set of elements of the range of $\operatorname{leftQuotient}$ applied to $L$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to the left quotient of $s$ and $\operatorname{cons}$ applied to $a$ and $\operatorname{nil}$, $L$ and $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to $\MembershipmemMACRoT {s_{1}}{\operatorname{nil}}$.

Let $M$ be an element of $\mathrm{DFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{toNFA}$ applied to $M$ is an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to $\operatorname{singleton}$ applied to the step of $s$ and $a$, $\operatorname{singleton}$ applied to the start of $M$ and $\operatorname{accept}$ applied to $M$.

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{NFA}$ applied to $x$ and $x_{1}$ are a basic type.

path of x3 and x4 (from the name)

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ and $x_{3}$ be elements of $x_{1}$. Let $x_{4}$ be a list of elements of $x$. Then the paths of $x_{3}$ and $x_{4}$ are a basic type.

Let $t$, $s$ and $u$ be elements of $x_{1}$. Let $a$ be an element of $x$. Let $x_{2}$ be a list of elements of $x$. Assume that $t$ is an element of the step of $s$ and $a$. Let $x_{3}$ be a path of $u$ and $x_{2}$. Then $\operatorname{cons}$ applied to $t$, $s$, $u$, $a$, $x_{2}$, $h$ and $x_{3}$ is a path of $u$ and $\operatorname{cons}$ applied to $a$ and $x_{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 the set of functions from elements $s$ of $x_{1}$ to elements of $\mathrm{motive}$ applied to $s$, $s$, $\operatorname{nil}$ and $\operatorname{nil}$ applied to $s$ and $\mathrm{PULift}$ applied to the set of functions from elements $t$ of $x_{1}$ and elements $s_{1}$ of $x_{1}$ and elements $u$ of $x_{1}$ and elements $a$ of $x$ and lists $x_{2}$ of elements of $x$ and elements $h$ of $\mathrm{Proof}$ applied to the proposition that $t$ is an element of the step of $s_{1}$ and $a$ and paths $x_{3}$ of $u$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $s_{1}$, $u$, $\operatorname{cons}$ applied to $a$ and $x_{2}$ and $\operatorname{cons}$ applied to $t$, $s_{1}$, $u$, $a$, $x_{2}$, $h$ and $x_{3}$.

Let $s$ be an element of $x_{1}$. Then $\operatorname{nil}$ applied to $s$ is a path of $s$ and $\operatorname{nil}$.

the support of x4 (from the name)

Let $x_{4}$ be a path of $t$ and $x_{3}$. Then the support of $x_{4}$ is a finite set of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{NFA\_\_Path\_\_supp\_\_\_f}$.

Let $\mathrm{self}$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{accept}$ applied to $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{accepts}$ applied to $M$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exists an element $S$ of $x_{1}$, such that $\MembershipmemMACRoT {\operatorname{accept} (M)}{S}$ and $S$ is an element of the evaluation of $M$ and $x_{2}$.

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Then $\operatorname{acceptsFrom}$ applied to $M$ and $S$ is a language of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exists an element $s$ of $x_{1}$, such that $\MembershipmemMACRoT {\operatorname{accept} (M)}{s}$ and $\MembershipmemMACRoT {\operatorname{evalFrom} (M , S , x_{2})}{s}$.

the evaluation of M and x2 (from the name)

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then the evaluation of $M$ and $x_{2}$ is an element of $\wp x_{1}$ defined as $\operatorname{evalFrom}$ applied to $M$, the start of $M$ and $x_{2}$.

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{evalFrom}$ applied to $M$, $S$ and $x_{2}$ is an element of $\wp x_{1}$ defined as $\operatorname{foldl}$ applied to $\operatorname{stepSet}$, $S$ and $x_{2}$.

the reverse of M (from the name)

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then the reverse of $M$ is an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $s$ and $a$ to $\operatorname{ofPred}$ applied to the function that maps $\mathrm{s'}$ to the proposition that $s$ is an element of the step of $\mathrm{s'}$ and $a$, $\operatorname{accept}$ applied to $M$ and the start of $M$.

the start of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then the start of $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the step of x2 and x3 (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Let $x_{3}$ be an element of $x$. Then the step of $x_{2}$ and $x_{3}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the step set of S and a (from the name)

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Let $a$ be an element of $x$. Then the step set of $S$ and $a$ is an element of $\wp x_{1}$ defined as the union of the function that maps $s$ to the union of the function that maps $h$ to the step of $s$ and $a$.

Let $M$ be an element of $\mathrm{NFA}$ applied to $x$ and $x_{1}$. Then $\operatorname{toDFA}$ applied to $M$ is an element of $\mathrm{DFA}$ applied to $x$ and $\wp x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{stepSet}$, the start of $M$ and $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that there exists an element $s$ of $x_{1}$, such that $s$ is an element of $S$ and $\MembershipmemMACRoT {\operatorname{accept} (M)}{s}$.

f is computable (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is computable, if $\mathrm{Partrec}$ holds for the lift of $f$.

f is computable (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Then $f$ is computable, if the function that maps $p$ to $f$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is computable.

Let $x$ be a function of $\Natural$ and $\Natural$. Then we can say that $\operatorname{Partrec}$ holds for $x$.

Assume that $\operatorname{Partrec}$ holds for $x$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $p$ be a function of $\Natural$ and $\mathrm{Bool}$. Then $\operatorname{rfind}$ applied to $p$ is a part of $\Natural$ defined as $\operatorname{mk}$ applied to the proposition that there exists a natural number $n$, such that $\MembershipmemMACRoT {p (n)}{\operatorname{true}}$ and for all natural numbers $k$, if $k < n$, then $p$ applied to $k$ is a domain and the function that maps $h_{1}$ to $\operatorname{rfindX}$ applied to $p$ and $h_{1}$.

Let $f$ be a function from natural numbers to elements of $\mathrm{Option}$ applied to $x$. Then $\operatorname{rfindOpt}$ applied to $f$ is a part of $x$ defined as $\operatorname{bind}$ applied to $\operatorname{rfind}$ applied to the function that maps $n$ to the part of $\operatorname{some}$ applied to $\operatorname{isSome}$ applied to $f$ applied to $n$ and the function that maps $n_{1}$ to the part of $f$ applied to $n_{1}$.

Let $p$ be a function of $\Natural$ and $\mathrm{Bool}$ such that there exists a natural number $n_{1}$, such that $\MembershipmemMACRoT {p (n_{1})}{\operatorname{true}}$ and for all natural numbers $k$, if $k < n_{1}$, then $p$ applied to $k$ is a domain. Then $\operatorname{rfindX}$ applied to $p$ and $H$ is an element of $\SubtypeSet {n}{\mathrm{and} (\MembershipmemMACRoT {p (n)}{\operatorname{true}}, \mathrm{forall} (\Natural , \lambda m . \mathrm{if} (\mathrm{Lt} (m , n), \MembershipmemMACRoT {p (m)}{\operatorname{false}})))}$.

Let $f$ be a function of $x$ and $x_{1}$. Then $\mathrm{Partrec}$ holds for $f$, if $\operatorname{Partrec}$ holds for the function that maps $n$ to $\operatorname{bind}$ applied to the part of the decode of $n$ and the function that maps $a$ to the map of $\operatorname{encode}$ and $f$ applied to $a$.

Let $f$ be a function from elements of $x$ to functions of $x_{1}$ and $x_{2}$. Then $\mathrm{Partrec\_u2082\_}$ holds for $f$, if $\mathrm{Partrec}$ holds for the function that maps $p$ to $f$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

Let $x$ be a function of the set of vectors of $\Natural$ and $n$ and $\Natural$. Then we can say that $\operatorname{Partrec'}$ holds for $x$.

f is a vector (from the name)

Let $f$ be a function from vectors of $\Natural$ and $n$ to vectors of $\Natural$ and $m$. Then $f$ is a vector, if for all elements $i$ of $\mathrm{Fin}$ applied to $m$, $\operatorname{Partrec'}$ holds for the function that maps $v$ to the part of $\operatorname{some}$ applied to $\operatorname{get}$ applied to $f$ applied to $v$ and $i$.

Assume that $\operatorname{Partrec'}$ holds for $x$. Then we can say that $\operatorname{below}$ holds for $t$.

code (from the name)

The codes are a basic type.

the composition of x and x1 (from the name)

Let $x$ and $x_{1}$ be codes. Then the composition of $x$ and $x_{1}$ is a code.

the constant of x (from the name)

Let $x$ be a natural number. Then the constant of $x$ is a code defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_Partrec\_\_Code\_\_const\_\_\_f}$.

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 zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the successor and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the left and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the right 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 the set of functions from codes $x$ and codes $x_{1}$ to elements of $\mathrm{motive}$ applied to the pair of $x$ and $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x_{2}$ and codes $x_{3}$ to elements of $\mathrm{motive}$ applied to the composition of $x_{2}$ and $x_{3}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $6$, $\mathrm{PULift}$ applied to the set of functions from codes $x_{4}$ and codes $x_{5}$ to elements of $\mathrm{motive}$ applied to $\operatorname{prec}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x_{6}$ to elements of $\mathrm{motive}$ applied to $\operatorname{rfind'}$ applied to $x_{6}$.

the curry of c and n (from the name)

Let $c$ be a code. Let $n$ be a natural number. Then the curry of $c$ and $n$ is a code defined as the composition of $c$ and the pair of the constant of $n$ and the identity.

Let $x$ be a code. Then $\operatorname{encodeCode}$ applied to $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_Partrec\_\_Code\_\_encodeCode\_\_\_f}$.

the evaluation of x (from the name)

Let $x$ be a code. Then the evaluation of $x$ is a function of $\Natural$ and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_Partrec\_\_Code\_\_eval\_\_\_f}$.

Let $x$ and $x_{2}$ be natural numbers. Let $x_{1}$ be a code. Then $\operatorname{evaln}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $\Natural$ defined as $\mathrm{Nat\_\_Partrec\_\_Code\_\_evaln\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $x$ and $x_{1}$ and $x_{2}$.

the identity (from the name)

The identity is a code defined as the pair of the left and the right.

the left (from the name)

The left is a code.

the code of x (from the name)

Let $x$ be a natural number. Then the code of $x$ is a code.

the pair of x and x1 (from the name)

Let $x$ and $x_{1}$ be codes. Then the pair of $x$ and $x_{1}$ is a code.

Let $x$ and $x_{1}$ be codes. Then $\operatorname{prec}$ applied to $x$ and $x_{1}$ is a code.

Let $x$ be a code. Then $\operatorname{rfind'}$ applied to $x$ is a code.

the right (from the name)

The right is a code.

the successor (from the name)

The successor is a code.

the zero (from the name)

The zero is a code.

Let $x$ be a function from natural numbers to natural numbers. Then we can say that $\operatorname{Primrec}$ holds for $x$.

Assume that $\operatorname{Primrec}$ holds for $x$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $f$ be a function from natural numbers and natural numbers to elements of $x$. Let $n$ be a natural number. Then $\operatorname{unpaired}$ applied to $f$ and $n$ is an element of $x$ defined as $f$ applied to $\ProdfstMACRoZ {\operatorname{unpair} (n)}$ and $\ProdsndMACRoAA {\operatorname{unpair} (n)}$.

Let $x$ be a set. Then we can say that $\mathrm{Primcodable}$ holds for $x$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{Primrec}$ holds for $f$, if $\operatorname{Primrec}$ holds for the function that maps $n$ to $\operatorname{encode}$ applied to $\operatorname{map}$ applied to $f$ and the decode of $n$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{PrimrecBounded}$ holds for $f$, if there exists a function $g$ from elements of $x$ to natural numbers, such that $\mathrm{Primrec}$ holds for $g$ and for all elements $x_{4}$ of $x$, $\operatorname{encode} (f (x_{4}))\leq g (x_{4})$.

Let $p$ be a function from elements of $x$ to propositions. Then $\mathrm{PrimrecPred}$ holds for $p$, if there exists an element $x_{2}$ of $\mathrm{DecidablePred}$ applied to $p$, such that $\mathrm{Primrec}$ holds for the function that maps $a$ to $\operatorname{decide}$ applied to $p$ applied to $a$.

Let $s$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\mathrm{PrimrecRel}$ holds for $s$, if $\mathrm{PrimrecPred}$ holds for the function that maps $p$ to $s$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Then $\mathrm{Primrec\_u2082\_}$ holds for $f$, if $\mathrm{Primrec}$ holds for the function that maps $p$ to $f$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

Let $x$ be a function from vectors of $\Natural$ and $n$ to natural numbers. Then we can say that $\operatorname{Primrec'}$ holds for $x$.

f is a vector (from the name)

Let $f$ be a function from vectors of $\Natural$ and $n$ to vectors of $\Natural$ and $m$. Then $f$ is a vector, if for all elements $i$ of $\mathrm{Fin}$ applied to $m$, $\operatorname{Primrec'}$ holds for the function that maps $v$ to $\operatorname{get}$ applied to $f$ applied to $v$ and $i$.

Assume that $\operatorname{Primrec'}$ holds for $x$. Then we can say that $\operatorname{below}$ holds for $t$.

p is a computable predecessor (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then $p$ is a computable predecessor, if there exists an element $x_{2}$ of $\mathrm{DecidablePred}$ applied to $p$, such that the function that maps $a$ to $\operatorname{decide}$ applied to $p$ applied to $a$ is computable.

p is a real part predecessor (from the name)

Let $p$ be a function from elements of $x$ to propositions. Then $p$ is a real part predecessor, if $\mathrm{Partrec}$ holds for the function that maps $a$ to $\operatorname{assert}$ applied to $p$ applied to $a$ and the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{unit}$.

Let $O$ be an element of the power set of the set of functions of $\Natural$ and $\Natural$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{ComputableIn}$ holds for $O$ and $f$, if $\mathrm{RecursiveIn}$ holds for $O$ and the function that maps $a$ to $\operatorname{some}$ applied to $f$ applied to $a$.

Let $O$ be an element of the power set of the set of functions of $\Natural$ and $\Natural$. Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Then $\mathrm{ComputableIn\_u2082\_}$ holds for $O$ and $f$, if $\mathrm{ComputableIn}$ holds for $O$ and the function that maps $p$ to $f$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

Let $O$ be an element of the power set of the set of functions of $\Natural$ and $\Natural$. Let $x$ be a function of $\Natural$ and $\Natural$. Then we can say that $\operatorname{RecursiveIn}$ holds for $O$ and $x$.

Assume that $\operatorname{RecursiveIn}$ holds for $O$ and $x$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $O$ be an element of the power set of the set of functions of $\Natural$ and $\Natural$. Let $f$ be a function of $x$ and $x_{1}$. Then $\mathrm{RecursiveIn}$ holds for $O$ and $f$, if $\operatorname{RecursiveIn}$ holds for $O$ and the function that maps $n$ to $\operatorname{bind}$ applied to the part of the decode of $n$ and the function that maps $a$ to the map of $\operatorname{encode}$ and $f$ applied to $a$.

Let $O$ be an element of the power set of the set of functions of $\Natural$ and $\Natural$. Let $f$ be a function from elements of $x$ to functions of $x_{1}$ and $x_{2}$. Then $\mathrm{RecursiveIn\_u2082\_}$ holds for $O$ and $f$, if $\mathrm{RecursiveIn}$ holds for $O$ and the function that maps $p$ to $f$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

e is computable (from the name)

Let $e$ be an equivalence from $x$ to $x_{1}$. Then $e$ is computable, if $\operatorname{coe}$ applied to $e$ and $\operatorname{coe}$ applied to the inverse of $e$ are computable.

many one degree (from the name)

The many one degrees are a basic type.

Let $d$ be a many one degree. Let $f$ be a function from elements of $\wp \Natural$ to elements of $x$ such that for all elements $p$ and $q$ of $\wp \Natural$, if $\mathrm{ManyOneEquiv}$ holds for the function that maps $x_{1}$ to $\MembershipmemMACRoT {p}{x_{1}}$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {q}{x_{2}}$, then $\EqtMACRoH {f (p)}{f (q)}$. Then $\operatorname{liftOn}$ applied to $d$, $f$ and $h$ is an element of $x$ defined as $\operatorname{liftOn'}$ applied to $d$, $f$ and $h$.

Let $x_{1}$ and $x_{2}$ be many one degrees. Let $f$ be a function from elements of $\wp \Natural$ and elements of $\wp \Natural$ to elements of $x$ such that for all elements $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ of $\wp \Natural$, if $\mathrm{ManyOneEquiv}$ holds for the function that maps $x_{9}$ to $\MembershipmemMACRoT {x_{3}}{x_{9}}$ and the function that maps $x_{10}$ to $\MembershipmemMACRoT {x_{4}}{x_{10}}$, then if $\mathrm{ManyOneEquiv}$ holds for the function that maps $x_{7}$ to $\MembershipmemMACRoT {x_{5}}{x_{7}}$ and the function that maps $x_{8}$ to $\MembershipmemMACRoT {x_{6}}{x_{8}}$, then $\EqtMACRoH {f (x_{3} , x_{5})}{f (x_{4} , x_{6})}$. Then $\mathrm{ManyOneDegree\_\_liftOn\_u2082\_}$ applied to $x_{1}$, $x_{2}$, $f$ and $h$ is an element of $x$.

Let $p$ be an element of $\wp x$. Then $\operatorname{of}$ applied to $p$ is a many one degree defined as $\operatorname{mk''}$ applied to the natural number of $p$.

Let $p$ be a function from elements of $x$ to propositions. Let $q$ be a function from elements of $x_{1}$ to propositions. Then $\mathrm{ManyOneEquiv}$ holds for $p$ and $q$, if $\mathrm{ManyOneReducible}$ holds for $p$ and $q$ and $\mathrm{ManyOneReducible}$ holds for $q$ and $p$.

Let $p$ be a function from elements of $x$ to propositions. Let $q$ be a function from elements of $x_{1}$ to propositions. Then $\mathrm{ManyOneReducible}$ holds for $p$ and $q$, if there exists a function $f$ from elements of $x$ to elements of $x_{1}$, such that $f$ is computable and for all elements $a$ of $x$, $p$ holds for $a$, if and only if $q$ holds for $f$ applied to $a$.

Let $p$ be a function from elements of $x$ to propositions. Let $q$ be a function from elements of $x_{1}$ to propositions. Then $\mathrm{OneOneEquiv}$ holds for $p$ and $q$, if $\mathrm{OneOneReducible}$ holds for $p$ and $q$ and $\mathrm{OneOneReducible}$ holds for $q$ and $p$.

Let $p$ be a function from elements of $x$ to propositions. Let $q$ be a function from elements of $x_{1}$ to propositions. Then $\mathrm{OneOneReducible}$ holds for $p$ and $q$, if there exists a function $f$ from elements of $x$ to elements of $x_{1}$, such that $f$ is computable and injective and for all elements $a$ of $x$, $p$ holds for $a$, if and only if $q$ holds for $f$ applied to $a$.

the natural number of p (from the name)

Let $p$ be an element of $\wp x$. Then the natural number of $p$ is an element of $\wp \Natural$ defined as $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that $\operatorname{getD}$ applied to the decode of $n$ and $\operatorname{default}$ is an element of $p$.

regular expression of x (from the name)

Let $x$ be a set. Then the regular expressions of $x$ are a basic type.

the characteristic of x1 (from the name)

Let $x_{1}$ be an element of $x$. Then the characteristic of $x_{1}$ is a regular expression of $x$.

the composition of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be regular expressions of $x$. Then the composition of $x_{1}$ and $x_{2}$ is a regular expression of $x$.

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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the epsilon and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to the characteristic of $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from regular expressions $x_{2}$ of $x$ and regular expressions $x_{3}$ of $x$ to elements of $\mathrm{motive}$ applied to the plus of $x_{2}$ and $x_{3}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to the set of functions from regular expressions $x_{4}$ of $x$ and regular expressions $x_{5}$ of $x$ to elements of $\mathrm{motive}$ applied to the composition of $x_{4}$ and $x_{5}$ and $\mathrm{PULift}$ applied to the set of functions from regular expressions $x_{6}$ of $x$ to elements of $\mathrm{motive}$ applied to the star of $x_{6}$.

the derivative of x2 and x3 (from the name)

Let $x_{2}$ be a regular expression of $x$. Let $x_{3}$ be an element of $x$. Then the derivative of $x_{2}$ and $x_{3}$ is a regular expression of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{RegularExpression\_\_deriv\_\_\_f}$ and $x_{3}$.

the epsilon (from the name)

The epsilon is a regular expression of $x$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a regular expression of $x$. Then the map of $f$ and $x_{2}$ is a regular expression of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{RegularExpression\_\_map\_\_\_f}$ applied to $f$.

the match epsilon of x1 (from the name)

Let $x_{1}$ be a regular expression of $x$. Then the match epsilon of $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{RegularExpression\_\_matchEpsilon\_\_\_f}$.

Let $x_{1}$ be a regular expression of $x$. Then $\operatorname{matches'}$ applied to $x_{1}$ is a language of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{RegularExpression\_\_matches'\_\_\_f}$.

the plus of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be regular expressions of $x$. Then the plus of $x_{1}$ and $x_{2}$ is a regular expression of $x$.

Let $x_{2}$ be a regular expression of $x$. Let $x_{3}$ be a list of elements of $x$. Then $\operatorname{rmatch}$ applied to $x_{2}$ and $x_{3}$ is an element of $\mathrm{Bool}$.

the star of x1 (from the name)

Let $x_{1}$ be a regular expression of $x$. Then the star of $x_{1}$ is a regular expression of $x$.

the zero (from the name)

The zero is a regular expression of $x$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ be an element of $x$. Let $b$ be an element of $\mathrm{Option}$ applied to $x$. Then the elements of $\operatorname{EvalsTo}$ applied to $f$, $a$ and $b$ are a basic type.

the identity of f and a (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ be an element of $x$. Then the identity of $f$ and $a$ is an element of $\operatorname{EvalsTo}$ applied to $f$, $a$ and $\operatorname{some}$ applied to $a$.

the step of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{EvalsTo}$ applied to $f$, $a$ and $b$. Then the step of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition of x1 and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ and $b$ be elements of $x$. Let $c$ be an element of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ be an element of $\operatorname{EvalsTo}$ applied to $f$, $a$ and $\operatorname{some}$ applied to $b$. Let $x_{2}$ be an element of $\operatorname{EvalsTo}$ applied to $f$, $b$ and $c$. Then the composition of $x_{1}$ and $x_{2}$ is an element of $\operatorname{EvalsTo}$ applied to $f$, $a$ and $c$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ be an element of $x$. Let $b$ be an element of $\mathrm{Option}$ applied to $x$. Let $m$ be a natural number. Then the elements of $\operatorname{EvalsToInTime}$ applied to $f$, $a$, $b$ and $m$ are a basic type.

the identity of f and a (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ be an element of $x$. Then the identity of $f$ and $a$ is an element of $\operatorname{EvalsToInTime}$ applied to $f$, $a$, $\operatorname{some}$ applied to $a$ and $0$.

the composition of x3 and x4 (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ and $x_{2}$ be natural numbers. Let $a$ and $b$ be elements of $x$. Let $c$ be an element of $\mathrm{Option}$ applied to $x$. Let $x_{3}$ be an element of $\operatorname{EvalsToInTime}$ applied to $f$, $a$, $\operatorname{some}$ applied to $b$ and $x_{1}$. Let $x_{4}$ be an element of $\operatorname{EvalsToInTime}$ applied to $f$, $b$, $c$ and $x_{2}$. Then the composition of $x_{3}$ and $x_{4}$ is an element of $\operatorname{EvalsToInTime}$ applied to $f$, $a$, $c$ and $x_{2} + x_{1}$.

Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $x_{1}$. Let $\mathrm{tr}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $x_{1}$. Let $x_{4}$ be an element of $\mathrm{Option}$ applied to $x$. Then we can say that $\operatorname{FRespects}$ holds for $x_{2}$, $\mathrm{tr}$, $x_{3}$ and $x_{4}$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{Reaches}$ holds for $f$, $x_{1}$ and $x_{2}$, if $\operatorname{ReflTransGen}$ holds for the function that maps $a$ and $b$ to $\MembershipmemMACRoT {f (a)}{b}$, $x_{1}$ and $x_{2}$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{StateTransition\_\_Reaches\_u2080\_}$ holds for $f$, $a$ and $b$, if for all elements $c$ of $x$, if $\mathrm{StateTransition\_\_Reaches\_u2081\_}$ holds for $f$, $b$ and $c$, then $\mathrm{StateTransition\_\_Reaches\_u2081\_}$ holds for $f$, $a$ and $c$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\mathrm{StateTransition\_\_Reaches\_u2081\_}$ holds for $f$, $x_{1}$ and $x_{2}$, if $\operatorname{TransGen}$ holds for the function that maps $a$ and $b$ to $\MembershipmemMACRoT {f (a)}{b}$, $x_{1}$ and $x_{2}$.

Let $x_{2}$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $x_{1}$. Let $\mathrm{tr}$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then we can say that $\operatorname{Respects}$ holds for $x_{2}$, $x_{3}$ and $\mathrm{tr}$.

the evaluation of f and x1 (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the evaluation of $f$ and $x_{1}$ is a part of $x$ defined as $\operatorname{fix}$ applied to the function that maps $s$ to $\operatorname{some}$ applied to $\operatorname{elim}$ applied to $f$ applied to $s$, $\operatorname{inl}$ applied to $s$ and $\operatorname{inr}$ and $x_{1}$.

the evaluation induction of h and H (from the name)

Assume that $b$ is an element of the evaluation of $f$ and $a$. Let $H$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $b$ is an element of the evaluation of $f$ and $a_{1}$ and functions from elements $\mathrm{a'}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {f (a_{1})}{\operatorname{some} (\mathrm{a'})}$ to elements of $C$ applied to $\mathrm{a'}$ to elements of $C$ applied to $a_{1}$. Then the evaluation induction of $h$ and $a_{1}$ is an element of $C$ applied to $a$.

An element of $\mathrm{TuringDegree}$ is an antisymmetrization of the set of functions of $\Natural$ and $\Natural$ and $\mathrm{TuringReducible}$.

Let $f$ and $g$ be functions of $\Natural$ and $\Natural$. Then $\mathrm{TuringEquivalent}$ holds for $f$ and $g$, if $\mathrm{AntisymmRel}$ holds for $\mathrm{TuringReducible}$, $f$ and $g$.

Let $f$ and $g$ be functions of $\Natural$ and $\Natural$. Then $\mathrm{TuringReducible}$ holds for $f$ and $g$, if $\mathrm{RecursiveIn}$ holds for $\operatorname{singleton}$ applied to $g$ and $f$.

The elements of $\operatorname{FinTM2}$ are a basic type.

configuration of tm (from the name)

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Then a configuration of $\mathrm{tm}$ is an element of the function that maps $\mathrm{tm}$ to the set of configurations of $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_\_u3c3\_}$ applied to $\mathrm{tm}$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then an element of $\operatorname{K}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Then an element of $\operatorname{Stmt}$ applied to $\mathrm{tm}$ is an element of the function that maps $\mathrm{tm}$ to $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$, $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_\_u3c3\_}$ applied to $\mathrm{tm}$.

the initial state of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then the initial state of $\mathrm{self}$ is an element of $\mathrm{Turing\_\_FinTM2\_\_\_u3c3\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj10}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then $\mathrm{Turing\_\_FinTM2\_\_k\_u2080\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{K}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then $\mathrm{Turing\_\_FinTM2\_\_k\_u2081\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{K}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Let $x$ be an element of $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{self}$. Then $\operatorname{m}$ applied to $\mathrm{self}$ and $x$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{self}$, $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{self}$ and $\mathrm{Turing\_\_FinTM2\_\_\_u3c3\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj13}$ applied to $\mathrm{self}$ and $x$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then $\operatorname{main}$ applied to $\mathrm{self}$ is an element of $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.

the step of tm and x (from the name)

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Let $x$ be a configuration of $\mathrm{tm}$. Then the step of $\mathrm{tm}$ and $x$ is an element of $\mathrm{Option}$ applied to the set of configurations of $\mathrm{tm}$ defined as the step of $\operatorname{m}$ applied to $\mathrm{tm}$ and $x$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Let $x$ be an element of $\operatorname{K}$ applied to $\mathrm{self}$. Then an element of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{self}$ and $x$ is an element of the function that maps $\mathrm{self}$ and $x$ to $\operatorname{proj5}$ applied to $\mathrm{self}$ and $x$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then an element of $\mathrm{Turing\_\_FinTM2\_\_\_u39b\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj6}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{FinTM2}$. Then an element of $\mathrm{Turing\_\_FinTM2\_\_\_u3c3\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj9}$ applied to $\mathrm{self}$.

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{2}$. Let $\mathrm{eb}$ be a function from elements of $x_{1}$ to lists of elements of $x_{3}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the elements of $\operatorname{TM2Computable}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$ are a basic type.

the output function of self and a (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{TM2Computable}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Let $a$ be an element of $x$. Then the output function of $\mathrm{self}$ and $a$ is an element of $\operatorname{TM2Outputs}$ applied to $\operatorname{tm}$ applied to $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$, $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the input alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{ea}$ applied to $a$ and $\operatorname{some}$ applied to $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the output alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{eb}$ applied to $f$ applied to $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $a$.

the input alphabet of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableAux}$ applied to $x$ and $x_{1}$. Then the input alphabet of $\mathrm{self}$ is an element of $\EquivMACRoAE {\mathrm{Turing\_\_FinTM2\_\_\_u393\_} (\operatorname{tm} (\mathrm{self}), \mathrm{Turing\_\_FinTM2\_\_k\_u2080\_} (\operatorname{tm} (\mathrm{self})))}{x}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the output alphabet of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableAux}$ applied to $x$ and $x_{1}$. Then the output alphabet of $\mathrm{self}$ is an element of $\EquivMACRoAE {\mathrm{Turing\_\_FinTM2\_\_\_u393\_} (\operatorname{tm} (\mathrm{self}), \mathrm{Turing\_\_FinTM2\_\_k\_u2081\_} (\operatorname{tm} (\mathrm{self})))}{x_{1}}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableAux}$ applied to $x$ and $x_{1}$. Then $\operatorname{tm}$ applied to $\mathrm{self}$ is an element of $\operatorname{FinTM2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{2}$. Let $\mathrm{eb}$ be a function from elements of $x_{1}$ to lists of elements of $x_{3}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the elements of $\operatorname{TM2ComputableInPolyTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$ are a basic type.

the output function of self and a (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableInPolyTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Let $a$ be an element of $x$. Then the output function of $\mathrm{self}$ and $a$ is an element of $\operatorname{TM2OutputsInTime}$ applied to $\operatorname{tm}$ applied to $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$, $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the input alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{ea}$ applied to $a$, $\operatorname{some}$ applied to $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the output alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{eb}$ applied to $f$ applied to $a$ and the evaluation of $\operatorname{length}$ applied to $\mathrm{ea}$ applied to $a$ and the time of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $a$.

the time of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableInPolyTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Then the time of $\mathrm{self}$ is a polynomial of $\Natural$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $h$ be an element of $\operatorname{TM2ComputableInPolyTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Then $\operatorname{toTM2ComputableInTime}$ applied to $h$ is an element of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$ defined as $\operatorname{mk}$ applied to $\operatorname{toTM2ComputableAux}$ applied to $h$, the function that maps $n$ to the evaluation of $n$ and the time of $h$ and $\operatorname{outputsFun}$ applied to $h$.

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{2}$. Let $\mathrm{eb}$ be a function from elements of $x_{1}$ to lists of elements of $x_{3}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the elements of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$ are a basic type.

the output function of self and a (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Let $a$ be an element of $x$. Then the output function of $\mathrm{self}$ and $a$ is an element of $\operatorname{TM2OutputsInTime}$ applied to $\operatorname{tm}$ applied to $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$, $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the input alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{ea}$ applied to $a$, $\operatorname{some}$ applied to $\operatorname{map}$ applied to $\operatorname{invFun}$ applied to the output alphabet of $\operatorname{toTM2ComputableAux}$ applied to $\mathrm{self}$ and $\mathrm{eb}$ applied to $f$ applied to $a$ and the time of $\mathrm{self}$ and $\operatorname{length}$ applied to $\mathrm{ea}$ applied to $a$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $a$.

the time of self and x4 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Let $x_{4}$ be a natural number. Then the time of $\mathrm{self}$ and $x_{4}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

Let $h$ be an element of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$. Then $\operatorname{toTM2Computable}$ applied to $h$ is an element of $\operatorname{TM2Computable}$ applied to $\mathrm{ea}$, $\mathrm{eb}$ and $f$ defined as $\operatorname{mk}$ applied to $\operatorname{toTM2ComputableAux}$ applied to $h$ and the function that maps $a$ to $\operatorname{toTM2Outputs}$ applied to the output function of $h$ and $a$.

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Let $l$ be a list of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2080\_}$ applied to $\mathrm{tm}$. Let $\mathrm{l'}$ be an element of $\mathrm{Option}$ applied to the set of lists of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2081\_}$ applied to $\mathrm{tm}$. Then an element of $\operatorname{TM2Outputs}$ applied to $\mathrm{tm}$, $l$ and $\mathrm{l'}$ is an element of the function that maps $\mathrm{tm}$, $l$ and $\mathrm{l'}$ to $\operatorname{EvalsTo}$ applied to $\operatorname{step}$ applied to $\mathrm{tm}$, $\operatorname{initList}$ applied to $\mathrm{tm}$ and $l$ and $\operatorname{map}$ applied to $\operatorname{haltList}$ applied to $\mathrm{tm}$ and $\mathrm{l'}$.

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Let $l$ be a list of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2080\_}$ applied to $\mathrm{tm}$. Let $\mathrm{l'}$ be an element of $\mathrm{Option}$ applied to the set of lists of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2081\_}$ applied to $\mathrm{tm}$. Let $m$ be a natural number. Then an element of $\operatorname{TM2OutputsInTime}$ applied to $\mathrm{tm}$, $l$, $\mathrm{l'}$ and $m$ is an element of the function that maps $\mathrm{tm}$, $l$, $\mathrm{l'}$ and $m$ to $\operatorname{EvalsToInTime}$ applied to $\operatorname{step}$ applied to $\mathrm{tm}$, $\operatorname{initList}$ applied to $\mathrm{tm}$ and $l$, $\operatorname{map}$ applied to $\operatorname{haltList}$ applied to $\mathrm{tm}$ and $\mathrm{l'}$ and $m$.

Let $h$ be an element of $\operatorname{TM2OutputsInTime}$ applied to $\mathrm{tm}$, $l$, $\mathrm{l'}$ and $m$. Then $\operatorname{toTM2Outputs}$ applied to $h$ is an element of $\operatorname{TM2Outputs}$ applied to $\mathrm{tm}$, $l$ and $\mathrm{l'}$ defined as $\operatorname{toEvalsTo}$ applied to $h$.

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Let $s$ be a list of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2081\_}$ applied to $\mathrm{tm}$. Then $\operatorname{haltList}$ applied to $\mathrm{tm}$ and $s$ is a configuration of $\mathrm{tm}$.

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{1}$. Then $\operatorname{idComputable}$ applied to $\mathrm{ea}$ is an element of $\operatorname{TM2Computable}$ applied to $\mathrm{ea}$, $\mathrm{ea}$ and $\mathrm{id}$ defined as $\operatorname{toTM2Computable}$ applied to the identity computable in time of $\mathrm{ea}$.

the identity computable in polynomial time of ea (from the name)

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{1}$. Then the identity computable in polynomial time of $\mathrm{ea}$ is an element of $\operatorname{TM2ComputableInPolyTime}$ applied to $\mathrm{ea}$, $\mathrm{ea}$ and $\mathrm{id}$.

the identity computable in time of ea (from the name)

Let $\mathrm{ea}$ be a function from elements of $x$ to lists of elements of $x_{1}$. Then the identity computable in time of $\mathrm{ea}$ is an element of $\operatorname{TM2ComputableInTime}$ applied to $\mathrm{ea}$, $\mathrm{ea}$ and $\mathrm{id}$ defined as $\operatorname{toTM2ComputableInTime}$ applied to the identity computable in polynomial time of $\mathrm{ea}$.

the identity computer of x (from the name)

Let $x$ be a set. Then the identity computer of $x$ is an element of $\operatorname{FinTM2}$ defined as $\operatorname{mk}$ applied to $\operatorname{unit}$, $\operatorname{unit}$, the function that maps $x_{2}$ to $x$, $\mathrm{Unit}$, $\operatorname{unit}$, $\mathrm{Unit}$, $\operatorname{unit}$ and the function that maps $x_{3}$ to $\operatorname{halt}$.

Let $\mathrm{tm}$ be an element of $\operatorname{FinTM2}$. Let $s$ be a list of elements of $\mathrm{Turing\_\_FinTM2\_\_\_u393\_}$ applied to $\mathrm{tm}$ and $\mathrm{Turing\_\_FinTM2\_\_k\_u2080\_}$ applied to $\mathrm{tm}$. Then $\operatorname{initList}$ applied to $\mathrm{tm}$ and $s$ is a configuration of $\mathrm{tm}$.

configuration (from the name)

The configurations are a basic type.

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 lists $x$ of natural numbers to elements of $\mathrm{motive}$ applied to $\operatorname{halt}$ applied to $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\operatorname{Cont}$ and lists $x_{2}$ of natural numbers to elements of $\mathrm{motive}$ applied to $\operatorname{ret}$ applied to $x_{1}$ and $x_{2}$.

Let $x$ be a list of natural numbers. Then $\operatorname{halt}$ applied to $x$ is a configuration.

Let $x$ be an element of $\operatorname{Cont}$. Let $x_{1}$ be a list of natural numbers. Then $\operatorname{ret}$ applied to $x$ and $x_{1}$ is a configuration.

Let $x$ be a configuration. Let $x_{1}$ be an element of $\operatorname{Cont}$. Then $\operatorname{then}$ applied to $x$ and $x_{1}$ is a configuration.

code (from the name)

The codes are a basic type.

Let $c$ be a code. Then $\operatorname{Ok}$ holds for $c$, if for all elements $k$ of $\operatorname{Cont}$, for all lists $v$ of natural numbers, the evaluation of $\operatorname{step}$ and the step normal of $k$ and $v$ is equal to $\operatorname{bind}$ applied to the evaluation of $c$ and the function that maps $v_{1}$ to the evaluation of $\operatorname{step}$ and $\operatorname{ret}$ applied to $k$ and $v_{1}$.

the case of x and x1 (from the name)

Let $x$ and $x_{1}$ be codes. Then the case of $x$ and $x_{1}$ is a code.

the composition of x and x1 (from the name)

Let $x$ and $x_{1}$ be codes. Then the composition of $x$ and $x_{1}$ is a code.

Let $x$ and $x_{1}$ be codes. Then $\operatorname{cons}$ applied to $x$ and $x_{1}$ is a code.

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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the successor and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the tail and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from codes $x$ and codes $x_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x$ and $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x_{2}$ and codes $x_{3}$ to elements of $\mathrm{motive}$ applied to the composition of $x_{2}$ and $x_{3}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $5$, $\mathrm{PULift}$ applied to the set of functions from codes $x_{4}$ and codes $x_{5}$ to elements of $\mathrm{motive}$ applied to the case of $x_{4}$ and $x_{5}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x_{6}$ to elements of $\mathrm{motive}$ applied to $\operatorname{fix}$ applied to $x_{6}$.

the evaluation of x (from the name)

Let $x$ be a code. Then the evaluation of $x$ is a function of the set of lists of natural numbers and the set of lists of natural numbers defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_ToPartrec\_\_Code\_\_eval\_\_\_f}$.

Let $x$ be a code. Then $\operatorname{fix}$ applied to $x$ is a code.

the head (from the name)

The head is a code defined as $\operatorname{cons}$ applied to the identity and $\operatorname{nil}$.

the identity (from the name)

The identity is a code defined as the composition of the tail and the zero.

$\operatorname{nil}$ is a code defined as the composition of the tail and the successor.

Let $f$ and $g$ be codes. Then $\operatorname{prec}$ applied to $f$ and $g$ is a code defined as $\operatorname{cons}$ applied to the composition of the case of the identity and the composition of the composition of the composition of the tail and the tail and $\operatorname{fix}$ applied to $\operatorname{cons}$ applied to the tail and $\operatorname{cons}$ applied to the successor and $\operatorname{cons}$ applied to the composition of the predecessor and the tail and $\operatorname{cons}$ applied to the composition of $g$ and $\operatorname{cons}$ applied to the identity and the composition of the tail and the tail and the composition of the tail and the composition of the tail and the tail and the zero and $\operatorname{cons}$ applied to the head and $\operatorname{cons}$ applied to the composition of $f$ and the tail and the tail and $\operatorname{nil}$.

the predecessor (from the name)

The predecessor is a code defined as the case of the zero and the head.

Let $f$ be a code. Then $\operatorname{rfind}$ applied to $f$ is a code defined as the composition of the predecessor and the composition of $\operatorname{fix}$ applied to $\operatorname{cons}$ applied to $f$ and $\operatorname{cons}$ applied to the successor and the tail and the zero.

the successor (from the name)

The successor is a code.

the tail (from the name)

The tail is a code.

the zero (from the name)

The zero is a code defined as $\operatorname{cons}$ applied to the zero and $\operatorname{nil}$.

the zero (from the name)

The zero is a code.

The elements of $\operatorname{Cont}$ are a basic type.

the composition of x and x1 (from the name)

Let $x$ be a code. Let $x_{1}$ be an element of $\operatorname{Cont}$. Then the composition of $x$ and $x_{1}$ is an element of $\operatorname{Cont}$.

Let $x$ be a code. Let $x_{1}$ be a list of natural numbers. Let $x_{2}$ be an element of $\operatorname{Cont}$. Then $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_cons\_u2081\_}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $\operatorname{Cont}$.

Let $x$ be a list of natural numbers. Let $x_{1}$ be an element of $\operatorname{Cont}$. Then $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_cons\_u2082\_}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Cont}$.

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 $\operatorname{halt}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x$ and lists $x_{1}$ of natural numbers and elements $x_{2}$ of $\operatorname{Cont}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_cons\_u2081\_}$ applied to $x$, $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 lists $x_{3}$ of natural numbers and elements $x_{4}$ of $\operatorname{Cont}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_cons\_u2082\_}$ applied to $x_{3}$ and $x_{4}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from codes $x_{5}$ and elements $x_{6}$ of $\operatorname{Cont}$ to elements of $\mathrm{motive}$ applied to the composition of $x_{5}$ and $x_{6}$ and $\mathrm{PULift}$ applied to the set of functions from codes $x_{7}$ and elements $x_{8}$ of $\operatorname{Cont}$ to elements of $\mathrm{motive}$ applied to $\operatorname{fix}$ applied to $x_{7}$ and $x_{8}$.

the evaluation of x (from the name)

Let $x$ be an element of $\operatorname{Cont}$. Then the evaluation of $x$ is a function of the set of lists of natural numbers and the set of lists of natural numbers defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_eval\_\_\_f}$.

Let $x$ be a code. Let $x_{1}$ be an element of $\operatorname{Cont}$. Then $\operatorname{fix}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Cont}$.

$\operatorname{halt}$ is an element of $\operatorname{Cont}$.

Let $x$ and $x_{1}$ be elements of $\operatorname{Cont}$. Then $\operatorname{then}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Cont}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Turing\_\_ToPartrec\_\_Cont\_\_then\_\_\_f}$ and $x_{1}$.

the default (from the name)

The default is a configuration defined as $\operatorname{halt}$ applied to $\operatorname{default}$.

the default (from the name)

The default is a code defined as the zero.

the default (from the name)

The default is an element of $\operatorname{Cont}$ defined as $\operatorname{halt}$.

the step of x (from the name)

Let $x$ be a configuration. Then the step of $x$ is an element of $\mathrm{Option}$ applied to the set of configurations.

the step normal of x1 and x2 (from the name)

Let $x$ be a code. Let $x_{1}$ be an element of $\operatorname{Cont}$. Let $x_{2}$ be a list of natural numbers. Then the step normal of $x_{1}$ and $x_{2}$ is a configuration defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Turing\_\_ToPartrec\_\_stepNormal\_\_\_f}$, $x_{1}$ and $x_{2}$.

Let $x$ be an element of $\operatorname{Cont}$. Let $x_{1}$ be a list of natural numbers. Then $\operatorname{stepRet}$ applied to $x$ and $x_{1}$ is a configuration defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Turing\_\_ToPartrec\_\_stepRet\_\_\_f}$ and $x_{1}$.

configuration of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then the configurations of $x$ and $x_{1}$ are a basic type.

Let $\mathrm{self}$ be a configuration of $x$ and $x_{1}$. Then $\operatorname{Tape}$ applied to $\mathrm{self}$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the map of g and x6 (from the name)

Let $f$ be a pointed map of $x$ and $x_{2}$. Let $g$ be a function from elements of $x_{4}$ to elements of $x_{5}$. Let $x_{6}$ be a configuration of $x$ and $x_{4}$. Then the map of $g$ and $x_{6}$ is a configuration of $x_{2}$ and $x_{5}$.

Let $\mathrm{self}$ be a configuration of $x$ and $x_{1}$. Then $\operatorname{q}$ applied to $\mathrm{self}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $x$ and $x_{1}$ be sets. Then an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of functions from elements of $x_{1}$ and elements of $x$ to elements of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $\operatorname{Stmt}$ applied to $x$.

the map of x10 and x11 (from the name)

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{4}$. Let $x_{8}$ be a pointed map of $x$ and $x_{2}$. Let $x_{9}$ be a pointed map of $x_{2}$ and $x$. Let $x_{10}$ be a function from elements of $x_{4}$ to elements of $x_{6}$. Let $x_{11}$ be a function from elements of $x_{6}$ to elements of $x_{4}$. Then the map of $x_{10}$ and $x_{11}$ is an element of $\operatorname{Machine}$ applied to $x_{2}$ and $x_{6}$.

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$. Let $x_{4}$ and $x_{5}$ be configurations of $x$ and $x_{1}$. Then $\operatorname{Reaches}$ holds for $M$, $x_{4}$ and $x_{5}$, if $\operatorname{ReflTransGen}$ holds for the function that maps $a$ and $b$ to the proposition that $b$ is an element of the step of $M$ and $a$, $x_{4}$ and $x_{5}$.

Let $x$ be a set. Then the elements of $\operatorname{Stmt}$ applied to $x$ are a basic type.

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 $\operatorname{Dir}$ to elements of $\mathrm{motive}$ applied to $\operatorname{move}$ applied to $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{write}$ applied to $x_{2}$.

the map of f and x4 (from the name)

Let $f$ be a pointed map of $x$ and $x_{2}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$. Then the map of $f$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x_{2}$.

Let $x_{1}$ be an element of $\operatorname{Dir}$. Then $\operatorname{move}$ applied to $x_{1}$ is an element of $\operatorname{Stmt}$ applied to $x$.

Let $x_{1}$ be an element of $x$. Then $\operatorname{write}$ applied to $x_{1}$ is an element of $\operatorname{Stmt}$ applied to $x$.

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$. Let $S$ be an element of $\wp x_{1}$. Then $\operatorname{Supports}$ holds for $M$ and $S$, if $\operatorname{default}$ is an element of $S$ and for all elements $q$ of $x_{1}$, for all elements $a$ of $x$, for all elements $\mathrm{q'}$ of $x_{1}$, for all elements $s$ of $\operatorname{Stmt}$ applied to $x$, if $\MembershipmemMACRoT {M (q , a)}{\ProdmkMACRoU {\mathrm{q'}}{s}}$, then if $q$ is an element of $S$, then $\mathrm{q'}$ is an element of $S$.

the evaluation of M and l (from the name)

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$. Let $l$ be a list of elements of $x$. Then the evaluation of $M$ and $l$ is a part of the set of list blanks of $x$ defined as the map of the function that maps $c$ to the right of $\operatorname{Tape}$ applied to $c$ and the evaluation of $\operatorname{step}$ applied to $M$ and the initial configuration of $l$.

the initial configuration of l (from the docstring)

Let $l$ be a list of elements of $x$. Then the initial configuration of $l$ is a configuration of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{default}$ and $\mathrm{Turing\_\_Tape\_\_mk\_u2081\_}$ applied to $l$.

the step of M and x4 (from the name)

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$. Let $x_{4}$ be a configuration of $x$ and $x_{1}$. Then the step of $M$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to the set of configurations of $x$ and $x_{1}$.

the trace of M and x3 (from the name)

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{1}$. Let $x_{3}$ be an element of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{1}$. Then the trace of $M$ and $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $x$, $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{1}$ and $\mathrm{Unit}$.

the configuration translation of M and x4 (from the docstring)

Let $M$ be an element of $\operatorname{Machine}$ applied to $x$ and $x_{2}$. Let $x_{4}$ be a configuration of $x$ and $x_{2}$. Then the configuration translation of $M$ and $x_{4}$ is a configuration of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{2}$ and $\mathrm{Unit}$.

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{1}$ are a basic type.

Let $x_{2}$ be an element of $\operatorname{Stmt}$ applied to $x$. Let $x_{3}$ be an element of $x_{1}$. Then $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'\_\_act}$ applied to $x_{2}$ and $x_{3}$ is an element of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{1}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'\_\_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_{2}$ of $x_{1}$ to elements of $\mathrm{motive}$ applied to the normal of $x_{2}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{3}$ of $\operatorname{Stmt}$ applied to $x$ and elements $x_{4}$ of $x_{1}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'\_\_act}$ applied to $x_{3}$ and $x_{4}$.

the normal of x2 (from the name)

Let $x_{2}$ be an element of $x_{1}$. Then the normal of $x_{2}$ is an element of $\mathrm{Turing\_\_TM0to1\_\_\_u39b\_'}$ applied to $x$ and $x_{1}$.

configuration of x1 and x2 (from the name)

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the configurations of $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Then $\operatorname{Tape}$ applied to $\mathrm{self}$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Then $\operatorname{l}$ applied to $\mathrm{self}$ is an element of $\mathrm{Option}$ applied to $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the variable of self (from the name)

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Then the variable of $\mathrm{self}$ is an element of $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ are a basic type.

the branch of x4 and x5 (from the name)

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{Bool}$. Let $x_{4}$ and $x_{5}$ be elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the branch of $x_{4}$ and $x_{5}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{3}$ of $\operatorname{Dir}$ and elements $x_{4}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{move}$ applied to $x_{3}$ and $x_{4}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{5}$ from elements of $x$ and elements of $x_{2}$ to elements of $x$ and elements $x_{6}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{write}$ applied to $x_{5}$ and $x_{6}$ and $\mathrm{PULift}$ applied to the set of functions from functions $x_{9}$ from elements of $x$ and elements of $x_{2}$ to elements of $x_{2}$ and elements $x_{10}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{load}$ applied to $x_{9}$ and $x_{10}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{13}$ from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{Bool}$ and elements $x_{14}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements $x_{15}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to the branch of $x_{14}$ and $x_{15}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{18}$ from elements of $x$ and elements of $x_{2}$ to elements of $x_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{goto}$ applied to $x_{18}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{halt}$.

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{1}$. Then $\operatorname{goto}$ applied to $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

$\operatorname{halt}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{load}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be an element of $\operatorname{Dir}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{move}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{write}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then $\operatorname{Supports}$ holds for $M$ and $S$, if $\operatorname{default}$ is an element of $S$ and for all elements $q$ of $x_{1}$, if $q$ is an element of $S$, then $\operatorname{SupportsStmt}$ holds for $S$ and $M$ applied to $q$.

Let $S$ be a finite set of $x_{1}$. Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{SupportsStmt}$ holds for $S$ and $x_{3}$, if $\operatorname{brecOn}$ holds for $x_{3}$ and $\mathrm{Turing\_\_TM1\_\_SupportsStmt\_\_\_f}$ applied to $S$.

the evaluation of M and l (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $l$ be a list of elements of $x$. Then the evaluation of $M$ and $l$ is a part of the set of list blanks of $x$ defined as the map of the function that maps $c$ to the right of $\operatorname{Tape}$ applied to $c$ and the evaluation of $\operatorname{step}$ applied to $M$ and $\operatorname{init}$ applied to $l$.

Let $l$ be a list of elements of $x$. Then $\operatorname{init}$ applied to $l$ is a configuration of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{some}$ applied to $\operatorname{default}$, $\operatorname{default}$ and $\mathrm{Turing\_\_Tape\_\_mk\_u2081\_}$ applied to $l$.

the step of M and x4 (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{4}$ be a configuration of $x_{1}$ and $x_{2}$. Then the step of $M$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to the set of configurations of $x_{1}$ and $x_{2}$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then $\operatorname{stmts}$ applied to $M$ and $S$ is a finite set of $\mathrm{Option}$ applied to $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{insertNone}$ applied to $\operatorname{biUnion}$ applied to $S$ and the function that maps $q$ to $\mathrm{Turing\_\_TM1\_\_stmts\_u2081\_}$ applied to $M$ applied to $q$.

Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\mathrm{Turing\_\_TM1\_\_stmts\_u2081\_}$ applied to $x_{3}$ is a finite set of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Turing\_\_TM1\_\_stmts\_u2081\_\_\_\_f}$.

the trace of M (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{3}$. Then the trace of $M$ is an element of $\operatorname{Machine}$ applied to $x$ and $\mathrm{Turing\_\_TM1to0\_\_\_u39b\_'}$ applied to $M$.

the trace configuration of M and x4 (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{4}$ be a configuration of $x_{1}$ and $x_{2}$. Then the trace configuration of $M$ and $x_{4}$ is a configuration of $x$ and $\mathrm{Turing\_\_TM1to0\_\_\_u39b\_'}$ applied to $M$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then $\operatorname{trStmts}$ applied to $M$ and $S$ is a finite set of $\mathrm{Turing\_\_TM1to0\_\_\_u39b\_'}$ applied to $M$ defined as $\operatorname{sprod}$ applied to $\operatorname{stmts}$ applied to $M$ and $S$ and the universal set.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then an element of $\mathrm{Turing\_\_TM1to0\_\_\_u39b\_'}$ applied to $M$ is an element of the function that maps $M$ to $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$.

Let $n$ be a natural number. Let $d$ be an element of $\operatorname{Dir}$. Let $q$ be an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$. Then $\operatorname{move}$ applied to $n$, $d$ and $q$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$ defined as $\operatorname{iterate}$ applied to $\operatorname{move}$ applied to $d$, $n$ and $q$.

Let $\mathrm{dec}$ be a function from vectors of $\mathrm{Bool}$ and $n$ to elements of $x$. Let $f$ be a function from elements of $x$ to elements of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$. Then $\operatorname{read}$ applied to $\mathrm{dec}$ and $f$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$ defined as $\operatorname{readAux}$ applied to $n$ and the function that maps $v$ to $\operatorname{move}$ applied to $n$, the left and $f$ applied to $\mathrm{dec}$ applied to $v$.

the trace of M and x3 (from the name)

Let $\mathrm{enc}$ be a function from elements of $x$ to vectors of $\mathrm{Bool}$ and $n$. Let $\mathrm{dec}$ be a function from vectors of $\mathrm{Bool}$ and $n$ to elements of $x$. Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the trace of $M$ and $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$.

the trace configuration of enc and x4 (from the name)

Let $\mathrm{enc}$ be a function from elements of $x$ to vectors of $\mathrm{Bool}$ and $n$ such that $\EqtMACRoH {\mathrm{enc} (\operatorname{default})}{\operatorname{replicate} (n , \operatorname{false})}$. Let $x_{4}$ be a configuration of $x_{1}$ and $x_{2}$. Then the trace configuration of $\mathrm{enc}$ and $x_{4}$ is a configuration of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$.

the trace normal of dec and x3 (from the name)

Let $\mathrm{dec}$ be a function from vectors of $\mathrm{Bool}$ and $n$ to elements of $x$. Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the trace normal of $\mathrm{dec}$ and $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Turing\_\_TM1to1\_\_trNormal\_\_\_f}$ applied to $\mathrm{dec}$.

the trace support of M and S (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then the trace support of $M$ and $S$ is a finite set of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{biUnion}$ applied to $S$ and the function that maps $l$ to $\operatorname{insert}$ applied to the normal of $l$ and $\operatorname{writes}$ applied to $M$ applied to $l$.

Assume that $\EqtMACRoH {\mathrm{enc} (\operatorname{default})}{\operatorname{replicate} (n , \operatorname{false})}$. Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Then $\operatorname{trTape}$ applied to $\mathrm{enc0}$ and $T$ is an element of $\operatorname{Tape}$ applied to $\mathrm{Bool}$ defined as $\operatorname{trTape'}$ applied to $\mathrm{enc0}$, the left of $T$ and the right of $T$.

Assume that $\EqtMACRoH {\mathrm{enc} (\operatorname{default})}{\operatorname{replicate} (n , \operatorname{false})}$. Let $L$ and $R$ be list blanks of $x$. Then $\operatorname{trTape'}$ applied to $\mathrm{enc0}$, $L$ and $R$ is an element of $\operatorname{Tape}$ applied to $\mathrm{Bool}$.

Let $x_{3}$ be a list of elements of $\mathrm{Bool}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$. Then $\operatorname{write}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Bool}$, $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Turing\_\_TM1to1\_\_write\_\_\_f}$ and $x_{4}$.

Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{writes}$ applied to $x_{4}$ is a finite set of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Turing\_\_TM1to1\_\_writes\_\_\_f}$.

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the elements of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'\_\_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_{3}$ of $x_{1}$ to elements of $\mathrm{motive}$ applied to the normal of $x_{3}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{4}$ of $x$ and elements $x_{5}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'\_\_write}$ applied to $x_{4}$ and $x_{5}$.

the normal of x3 (from the name)

Let $x_{3}$ be an element of $x_{1}$. Then the normal of $x_{3}$ is an element of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'\_\_write}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Turing\_\_TM1to1\_\_\_u39b\_'}$ applied to $x$, $x_{1}$ and $x_{2}$.

configuration of x1 and x2 (from the name)

Let $x$ be a function from elements of $K$ to sets. Let $x_{1}$ and $x_{2}$ be sets. Then the configurations of $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Then $\operatorname{l}$ applied to $\mathrm{self}$ is an element of $\mathrm{Option}$ applied to $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Let $k$ be an element of $K$. Then $\operatorname{stk}$ applied to $\mathrm{self}$ and $k$ is a list of elements of $x$ applied to $k$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $k$.

the variable of self (from the name)

Let $\mathrm{self}$ be a configuration of $x_{1}$ and $x_{2}$. Then the variable of $\mathrm{self}$ is an element of $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{4}$ and $x_{5}$ be configurations of $x_{1}$ and $x_{2}$. Then $\operatorname{Reaches}$ holds for $M$, $x_{4}$ and $x_{5}$, if $\operatorname{ReflTransGen}$ holds for the function that maps $a$ and $b$ to the proposition that $b$ is an element of the step of $M$ and $a$, $x_{4}$ and $x_{5}$.

Let $x$ be a function from elements of $K$ to sets. Let $x_{1}$ and $x_{2}$ be sets. Then the elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ are a basic type.

the branch of x4 and x5 (from the name)

Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $\mathrm{Bool}$. Let $x_{4}$ and $x_{5}$ be elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the branch of $x_{4}$ and $x_{5}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{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 $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $k$ of $K$ and functions $x_{3}$ from elements of $x_{2}$ to elements of $x$ applied to $k$ and elements $x_{4}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{push}$ applied to $k$, $x_{3}$ and $x_{4}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $k_{1}$ of $K$ and functions $x_{6}$ from elements of $x_{2}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k_{1}$ to elements of $x_{2}$ and elements $x_{7}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{peek}$ applied to $k_{1}$, $x_{6}$ and $x_{7}$ and $\mathrm{PULift}$ applied to the set of functions from elements $k_{2}$ of $K$ and functions $x_{10}$ from elements of $x_{2}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k_{2}$ to elements of $x_{2}$ and elements $x_{11}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to the pop of $x_{10}$ and $x_{11}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{14}$ from elements of $x_{2}$ to elements of $x_{2}$ and elements $x_{15}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{load}$ applied to $x_{14}$ and $x_{15}$ and $\mathrm{PULift}$ applied to the set of functions from functions $x_{17}$ from elements of $x_{2}$ to elements of $\mathrm{Bool}$ and elements $x_{18}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements $x_{19}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to the branch of $x_{18}$ and $x_{19}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $5$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{21}$ from elements of $x_{2}$ to elements of $x_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{goto}$ applied to $x_{21}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{halt}$.

Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $x_{1}$. Then $\operatorname{goto}$ applied to $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

$\operatorname{halt}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{load}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $k$ be an element of $K$. Let $x_{3}$ be a function from elements of $x_{2}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{peek}$ applied to $k$, $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

the pop of x3 and x4 (from the name)

Let $k$ be an element of $K$. Let $x_{3}$ be a function from elements of $x_{2}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the pop of $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $k$ be an element of $K$. Let $x_{3}$ be a function from elements of $x_{2}$ to elements of $x$ applied to $k$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{push}$ applied to $k$, $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then $\operatorname{Supports}$ holds for $M$ and $S$, if $\operatorname{default}$ is an element of $S$ and for all elements $q$ of $x_{1}$, if $q$ is an element of $S$, then $\operatorname{SupportsStmt}$ holds for $S$ and $M$ applied to $q$.

Let $S$ be a finite set of $x_{1}$. Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{SupportsStmt}$ holds for $S$ and $x_{3}$, if $\operatorname{brecOn}$ holds for $x_{3}$ and $\mathrm{Turing\_\_TM2\_\_SupportsStmt\_\_\_f}$ applied to $S$.

the evaluation of k and L (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $k$ be an element of $K$. Let $L$ be a list of elements of $x$ applied to $k$. Then the evaluation of $k$ and $L$ is a part of the set of lists of elements of $x$ applied to $k$ defined as the map of the function that maps $c$ to $\operatorname{stk}$ applied to $c$ and $k$ and the evaluation of $\operatorname{step}$ applied to $M$ and $\operatorname{init}$ applied to $k$ and $L$.

Let $k$ be an element of $K$. Let $L$ be a list of elements of $x$ applied to $k$. Then $\operatorname{init}$ applied to $k$ and $L$ is a configuration of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{some}$ applied to $\operatorname{default}$, $\operatorname{default}$ and $\operatorname{update}$ applied to the function that maps $x_{6}$ to $\operatorname{nil}$, $k$ and $L$.

the step of M and x4 (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{4}$ be a configuration of $x_{1}$ and $x_{2}$. Then the step of $M$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to the set of configurations of $x_{1}$ and $x_{2}$.

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then $\operatorname{stmts}$ applied to $M$ and $S$ is a finite set of $\mathrm{Option}$ applied to $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{insertNone}$ applied to $\operatorname{biUnion}$ applied to $S$ and the function that maps $q$ to $\mathrm{Turing\_\_TM2\_\_stmts\_u2081\_}$ applied to $M$ applied to $q$.

Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\mathrm{Turing\_\_TM2\_\_stmts\_u2081\_}$ applied to $x_{3}$ is a finite set of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Turing\_\_TM2\_\_stmts\_u2081\_\_\_\_f}$.

Let $K$ and $x_{1}$ be sets. Let $x$ be a function from elements of $K$ to sets. Let $k$ be an element of $K$. Then the elements of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$ are a basic type.

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 functions $x_{2}$ from elements of $x_{1}$ to elements of $x$ applied to $k$ to elements of $\mathrm{motive}$ applied to $\operatorname{push}$ applied to $x_{2}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from functions $x_{4}$ from elements of $x_{1}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{peek}$ applied to $x_{4}$ and $\mathrm{PULift}$ applied to the set of functions from functions $x_{7}$ from elements of $x_{1}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{1}$ to elements of $\mathrm{motive}$ applied to the pop of $x_{7}$.

Let $x_{2}$ be a function from elements of $x_{1}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{1}$. Then $\operatorname{peek}$ applied to $x_{2}$ is an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$.

the pop of x2 (from the name)

Let $x_{2}$ be a function from elements of $x_{1}$ and elements of $\mathrm{Option}$ applied to $x$ applied to $k$ to elements of $x_{1}$. Then the pop of $x_{2}$ is an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$.

Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $x$ applied to $k$. Then $\operatorname{push}$ applied to $x_{2}$ is an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$.

Let $x_{3}$ be a configuration of $x_{1}$ and $x_{2}$. Let $x_{4}$ be a configuration of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ and $x_{2}$. Then we can say that $\operatorname{TrCfg}$ holds for $x_{3}$ and $x_{4}$.

the additive bottom of L (from the name)

Let $L$ be a list blank of the set of functions from elements $k$ of $K$ to elements of $\mathrm{Option}$ applied to $x$ applied to $k$. Then the additive bottom of $L$ is a list blank of $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$.

Let $x_{3}$ be an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{2}$ and $k$. Let $x_{4}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{stRun}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$.

Let $v$ be an element of $x_{1}$. Let $l$ be a list of elements of $x$ applied to $k$. Let $x_{2}$ be an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$. Then $\operatorname{stVar}$ applied to $v$, $l$ and $x_{2}$ is an element of $x_{1}$.

Let $v$ be an element of $x_{1}$. Let $l$ be a list of elements of $x$ applied to $k$. Let $x_{2}$ be an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{1}$ and $k$. Then $\operatorname{stWrite}$ applied to $v$, $l$ and $x_{2}$ is a list of elements of $x$ applied to $k$.

Let $\mathrm{run}$ be a function from elements $k$ of $K$ and elements $s$ of $\operatorname{StAct}$ applied to $K$, $x$, $x_{2}$ and $k$ and elements $q_{1}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements of $\mathrm{motive}$ applied to $q_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{stRun}$ applied to $s$ and $q_{1}$. Let $\mathrm{load}$ be a function from functions $a$ from elements of $x_{2}$ to elements of $x_{2}$ and elements $q$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements of $\mathrm{motive}$ applied to $q$ to elements of $\mathrm{motive}$ applied to $\operatorname{load}$ applied to $a$ and $q$. Let $\mathrm{branch}$ be a function from functions $p$ from elements of $x_{2}$ to elements of $\mathrm{Bool}$ and elements $x_{4}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements $x_{5}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ and elements of $\mathrm{motive}$ applied to $x_{4}$ and elements of $\mathrm{motive}$ applied to $x_{5}$ to elements of $\mathrm{motive}$ applied to the branch of $x_{4}$ and $x_{5}$. Let $\mathrm{goto}$ be a function from functions $l$ from elements of $x_{2}$ to elements of $x_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{goto}$ applied to $l$. Let $\mathrm{halt}$ be an element of $\mathrm{motive}$ applied to $\operatorname{halt}$. Let $n$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\operatorname{stmtStRec}$ applied to $k$, $s$, $q_{1}$, $\mathrm{run}$, $a$, $q$, $\mathrm{load}$, $p$, $x_{4}$, $x_{5}$, $\mathrm{branch}$, $l$, $\mathrm{goto}$, $\mathrm{halt}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$ defined as the function that maps $\mathrm{load}$, $p$, $x_{4}$, $x_{5}$, $\mathrm{branch}$, $l$, $\mathrm{goto}$, $\mathrm{halt}$ and $n$ to $\operatorname{brecOn}$ applied to $q$, $\mathrm{Turing\_\_TM2to1\_\_stmtStRec\_\_\_f}$ applied to $k$, $s$, $q_{1}$, $\mathrm{run}$ and $a$, $\mathrm{load}$, $p$, $x_{4}$, $x_{5}$, $\mathrm{branch}$, $l$, $\mathrm{goto}$, $\mathrm{halt}$ and $n$.

the trace of M and x4 (from the name)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $x_{4}$ be an element of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$. Then the trace of $M$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$, $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ and $x_{2}$.

Let $k$ be an element of $K$. Let $L$ be a list of elements of $x$ applied to $k$. Then $\operatorname{trInit}$ applied to $k$ and $L$ is a list of elements of $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$ defined as $\operatorname{cons}$ applied to $\ProdmkMACRoU {\operatorname{true}}{\ProdsndMACRoAA {\operatorname{headI} (\operatorname{map} (\lambda a . \ProdmkMACRoU {\operatorname{false}}{\operatorname{update} (\lambda x_{2} . \operatorname{none} , k , \operatorname{some} (a))}, \operatorname{reverse} (L)))}}$ and $\operatorname{tail}$ applied to $\operatorname{map}$ applied to the function that maps $a_{1}$ to $\ProdmkMACRoU {\operatorname{false}}{\operatorname{update} (\lambda x_{3} . \operatorname{none} , k , \operatorname{some} (a_{1}))}$ and $\operatorname{reverse}$ applied to $L$.

the trace normal of x3 (from the name)

Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then the trace normal of $x_{3}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$, $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Turing\_\_TM2to1\_\_trNormal\_\_\_f}$.

Let $q$ be an element of $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$, $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ and $x_{2}$. Let $x_{4}$ be an element of $\operatorname{StAct}$ applied to $K$, $x$, $x_{2}$ and $k$. Then $\operatorname{trStAct}$ applied to $q$ and $x_{4}$ is an element of $\operatorname{Stmt}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$, $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ and $x_{2}$.

Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\mathrm{Turing\_\_TM2to1\_\_trStmts\_u2081\_}$ applied to $x_{3}$ is a finite set of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Turing\_\_TM2to1\_\_trStmts\_u2081\_\_\_\_f}$.

the support of M and S (from the docstring)

Let $M$ be a function from elements of $x_{1}$ to elements of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Let $S$ be a finite set of $x_{1}$. Then the support of $M$ and $S$ is a finite set of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ defined as $\operatorname{biUnion}$ applied to $S$ and the function that maps $l$ to $\operatorname{insert}$ applied to the normal of $l$ and $\mathrm{Turing\_\_TM2to1\_\_trStmts\_u2081\_}$ applied to $M$ applied to $l$.

Let $K$ be a set. Let $x$ be a function from elements of $K$ to sets. Then an element of $\mathrm{Turing\_\_TM2to1\_\_\_u393\_'}$ applied to $K$ and $x$ is an element of the function that maps $K$ and $x$ to $\mathrm{Prod}$ applied to $\mathrm{Bool}$ and the set of functions from elements $k$ of $K$ to elements of $\mathrm{Option}$ applied to $x$ applied to $k$.

Let $K$, $x_{1}$ and $x_{2}$ be sets. Let $x$ be a function from elements of $K$ to sets. Then the elements of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'\_\_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_{3}$ of $x_{1}$ to elements of $\mathrm{motive}$ applied to the normal of $x_{3}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $k$ of $K$ and elements $x_{4}$ of $\operatorname{StAct}$ applied to $K$, $x$, $x_{2}$ and $k$ and elements $x_{5}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'\_\_go}$ applied to $k$, $x_{4}$ and $x_{5}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{6}$ of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'\_\_ret}$ applied to $x_{6}$.

the normal of x3 (from the name)

Let $x_{3}$ be an element of $x_{1}$. Then the normal of $x_{3}$ is an element of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$.

Let $x_{3}$ be an element of $\operatorname{Stmt}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'\_\_ret}$ applied to $x_{3}$ is an element of $\mathrm{Turing\_\_TM2to1\_\_\_u39b\_'}$ applied to $K$, $x$, $x_{1}$ and $x_{2}$.