Definitions: Mathlib.Computability, part 2 of 2

Let $x_{2}$ and $x_{3}$ be lists of elements of $x$. Then $\operatorname{BlankExtends}$ holds for $x_{2}$ and $x_{3}$, if there exists a natural number $n$, such that $\EqtMACRoH {x_{3}}{\operatorname{hAppend} (x_{2} , \operatorname{replicate} (n , \operatorname{default}))}$.

Assume that $\operatorname{BlankExtends}$ holds for $l$ and $x_{2}$. Assume that $\operatorname{BlankExtends}$ holds for $l$ and $x_{3}$. Then $\operatorname{above}$ applied to $h$ and $h_{1}$ is an element of $\SubtypeSet {\mathrm{l'}}{\mathrm{and} (\operatorname{BlankExtends} (x_{2} , \mathrm{l'}), \operatorname{BlankExtends} (x_{3} , \mathrm{l'}))}$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (\operatorname{length} (x_{2}), \operatorname{length} (x_{3}))$, the function that maps $h_{2}$ to $x_{3}$ and the function that maps $h_{3}$ to $x_{2}$.

Let $x_{2}$ and $x_{3}$ be lists of elements of $x$. Then $\operatorname{BlankRel}$ holds for $x_{2}$ and $x_{3}$, if $\operatorname{BlankExtends}$ holds for $x_{2}$ and $x_{3}$ or $\operatorname{BlankExtends}$ holds for $x_{3}$ and $x_{2}$.

Assume that $\operatorname{BlankRel}$ holds for $x_{2}$ and $x_{3}$. Then $\operatorname{above}$ applied to $h$ is an element of $\SubtypeSet {l}{\mathrm{and} (\operatorname{BlankExtends} (x_{2} , l), \operatorname{BlankExtends} (x_{3} , l))}$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (\operatorname{length} (x_{2}), \operatorname{length} (x_{3}))$, the function that maps $\mathrm{hl}$ to $x_{3}$ and the function that maps $\mathrm{hl1}$ to $x_{2}$.

Assume that $\operatorname{BlankRel}$ holds for $x_{2}$ and $x_{3}$. Then $\operatorname{below}$ applied to $h$ is an element of $\SubtypeSet {l}{\mathrm{and} (\operatorname{BlankExtends} (l , x_{2}), \operatorname{BlankExtends} (l , x_{3}))}$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (\operatorname{length} (x_{2}), \operatorname{length} (x_{3}))$, the function that maps $\mathrm{hl}$ to $x_{2}$ and the function that maps $\mathrm{hl1}$ to $x_{3}$.

The elements of $\operatorname{Dir}$ 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 $\mathrm{motive}$ applied to the left and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the right.

the left (from the name)

The left is an element of $\operatorname{Dir}$.

Let $x$ be a natural number. Then $\operatorname{ofNat}$ applied to $x$ is an element of $\operatorname{Dir}$ defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, the left and the right.

the right (from the name)

The right is an element of $\operatorname{Dir}$.

list blank of x (from the name)

Let $x$ be a set. Then a list blank of $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $x$.

Let $x_{2}$ be a list of elements of $x$. Let $x_{3}$ be a list blank of $x$. Then $\operatorname{append}$ applied to $x_{2}$ and $x_{3}$ is a list blank of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Turing\_\_ListBlank\_\_append\_\_\_f}$ and $x_{3}$.

Let $a$ be an element of $x$. Let $l$ be a list blank of $x$. Then $\operatorname{cons}$ applied to $a$ and $l$ is a list blank of $x$.

the flat map of l and f (from the name)

Let $l$ be a list blank of $x$. Let $f$ be a function from elements of $x$ to lists of elements of $x_{1}$ such that there exists a natural number $n$, such that $\EqtMACRoH {f (\operatorname{default})}{\operatorname{replicate} (n , \operatorname{default})}$. Then the flat map of $l$ and $f$ is a list blank of $x_{1}$.

the head of l (from the docstring)

Let $l$ be a list blank of $x$. Then the head of $l$ is an element of $x$.

Let $l$ be a list blank of $x$. Let $f$ be a function from lists of elements of $x$ to elements of $x_{2}$ such that for all lists $a$ and $b$ of elements of $x$, if $\operatorname{BlankExtends}$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $l$, $f$ and $H$ is an element of $x_{2}$.

the map of f and l (from the name)

Let $f$ be a pointed map of $x$ and $x_{1}$. Let $l$ be a list blank of $x$. Then the map of $f$ and $l$ is a list blank of $x_{1}$.

Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{mk}$ applied to $x_{2}$ is a list blank of $x$ defined as $\operatorname{mk''}$ applied to $x_{2}$.

Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{2}$ be a natural number. Let $x_{3}$ be a list blank of $x$. Then $\operatorname{modifyNth}$ applied to $f$, $x_{2}$ and $x_{3}$ is a list blank of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Turing\_\_ListBlank\_\_modifyNth\_\_\_f}$ applied to $f$ and $x_{3}$.

Let $l$ be a list blank of $x$. Let $n$ be a natural number. Then $\operatorname{nth}$ applied to $l$ and $n$ is an element of $x$.

the tail of l (from the docstring)

Let $l$ be a list blank of $x$. Then the tail of $l$ is a list blank of $x$.

pointed map of x and x1 (from the name)

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

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

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

the current position of the head of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{Tape}$ applied to $x$. Then the current position of the head of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the left of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{Tape}$ applied to $x$. Then the left of $\mathrm{self}$ is a list blank of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the left of T (from the name)

Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Then the left of $T$ is a list blank of $x$ defined as $\operatorname{cons}$ applied to the current position of the head of $T$ and the left of $T$.

the map of f and T (from the name)

Let $f$ be a pointed map of $x$ and $x_{1}$. Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Then the map of $f$ and $T$ is an element of $\operatorname{Tape}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $f$ and the current position of the head of $T$, the map of $f$ and the left of $T$ and the map of $f$ and the right of $T$.

Let $L$ and $R$ be list blanks of $x$. Then $\operatorname{mk'}$ applied to $L$ and $R$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\operatorname{mk}$ applied to the head of $R$, $L$ and the tail of $R$.

Let $l$ be a list of elements of $x$. Then $\mathrm{Turing\_\_Tape\_\_mk\_u2081\_}$ applied to $l$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\mathrm{Turing\_\_Tape\_\_mk\_u2082\_}$ applied to $\operatorname{nil}$ and $l$.

Let $L$ and $R$ be lists of elements of $x$. Then $\mathrm{Turing\_\_Tape\_\_mk\_u2082\_}$ applied to $L$ and $R$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\operatorname{mk'}$ applied to $\operatorname{mk}$ applied to $L$ and $\operatorname{mk}$ applied to $R$.

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

Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Let $x_{2}$ be an integer. Then $\operatorname{nth}$ applied to $T$ and $x_{2}$ is an element of $x$.

the right of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{Tape}$ applied to $x$. Then the right of $\mathrm{self}$ is a list blank of $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the right of T (from the name)

Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Then the right of $T$ is a list blank of $x$ defined as $\operatorname{cons}$ applied to the current position of the head of $T$ and the right of $T$.

Let $b$ be an element of $x$. Let $T$ be an element of $\operatorname{Tape}$ applied to $x$. Then $\operatorname{write}$ applied to $b$ and $T$ is an element of $\operatorname{Tape}$ applied to $x$ defined as $\operatorname{mk}$ applied to $b$, the left of $T$ and the right of $T$.

the default (from the name)

The default is an element of $\operatorname{Dir}$ defined as the left.

the projection of i (from the name)

Let $i$ be an element of $x$. Then the projection of $i$ is a pointed map of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ and $x_{1}$ applied to $i$.

configuration (from the name)

A configuration is a configuration of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ and $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

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 an element of $\operatorname{Cont'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_Cont'\_\_cons\_u2081\_}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Cont'}$.

Let $x$ be an element of $\operatorname{Cont'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_Cont'\_\_cons\_u2082\_}$ applied to $x$ 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 elements $x_{1}$ of $\operatorname{Cont'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_Cont'\_\_cons\_u2081\_}$ applied to $x$ and $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{Cont'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_Cont'\_\_cons\_u2082\_}$ applied to $x_{2}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from codes $x_{3}$ and elements $x_{4}$ of $\operatorname{Cont'}$ to elements of $\mathrm{motive}$ applied to the composition of $x_{3}$ and $x_{4}$ and $\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 $\operatorname{fix}$ applied to $x_{5}$ and $x_{6}$.

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'}$.

The elements of $\operatorname{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 $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{main}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{rev}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{aux}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the stack.

the eliminator of d and x (from the name)

Let $a$, $b$, $c$ and $d$ be lists of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$. Let $x$ be an element of $\operatorname{K'}$. Then the eliminator of $d$ and $x$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

$\operatorname{main}$ is an element of $\operatorname{K'}$.

Let $x$ be a natural number. Then $\operatorname{ofNat}$ applied to $x$ is an element of $\operatorname{K'}$ defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, $\operatorname{main}$ and $\operatorname{rev}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $2$, $\operatorname{aux}$ and the stack.

$\operatorname{rev}$ is an element of $\operatorname{K'}$.

the stack (from the name)

The stack is an element of $\operatorname{K'}$.

An element of $\operatorname{Stmt'}$ is an element of $\operatorname{Stmt}$ applied to the function that maps $x$ to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$, $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ and $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

Let $K$ and $S$ be finite sets of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\operatorname{Supports}$ holds for $K$ and $S$, if for all elements $q$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$, if $q$ is an element of $K$, then $\operatorname{SupportsStmt}$ holds for $S$ and the trace of $q$.

Let $x$ and $x_{1}$ be configurations. Then we can say that $\operatorname{TrCfg}$ holds for $x$ and $x_{1}$.

the code support of c and k (from the name)

Let $c$ be a code. Let $k$ be an element of $\operatorname{Cont'}$. Then the code support of $c$ and $k$ is a finite set of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as the union of the code support of $c$ and $k$ and the continuous support of $k$.

the code support of x and x1 (from the name)

Let $x$ be a code. Let $x_{1}$ be an element of $\operatorname{Cont'}$. Then the code support of $x$ and $x_{1}$ is a finite set of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Turing\_\_PartrecToTM2\_\_codeSupp'\_\_\_f}$ and $x_{1}$.

the continuous stack of x (from the name)

Let $x$ be an element of $\operatorname{Cont}$. Then the continuous stack of $x$ is a list of lists of natural numbers defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_contStack\_\_\_f}$.

the continuous support of x (from the name)

Let $x$ be an element of $\operatorname{Cont'}$. Then the continuous support of $x$ is a finite set of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_contSupp\_\_\_f}$.

Let $v$ be a list of natural numbers. Then $\operatorname{halt}$ applied to $v$ is a configuration defined as $\operatorname{mk}$ applied to $\operatorname{none}$, $\operatorname{none}$ and $\operatorname{elim}$ applied to $\operatorname{nil}$.

the head of k and q (from the name)

Let $k$ be an element of $\operatorname{K'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then the head of $k$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to $\operatorname{natEnd}$, $k$, $\operatorname{rev}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_push}$ applied to $\operatorname{rev}$, the function that maps $x$ to $\operatorname{some}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_read}$ applied to the function that maps $s$ to $\iteMACRoG {(\EqtMACRoH {s}{\operatorname{some} (\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_})})}{\mathrm{id}}{\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_clear} (\lambda x_{1} . \operatorname{decide} (\EqtMACRoH {x_{1}}{\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}}), k)}$.

Let $c$ be a code. Let $v$ be a list of natural numbers. Then $\operatorname{init}$ applied to $c$ and $v$ is a configuration defined as $\operatorname{mk}$ applied to $\operatorname{some}$ applied to the trace normal of $c$ and $\operatorname{halt}$, $\operatorname{none}$ and $\operatorname{elim}$ applied to $\operatorname{nil}$.

the default (from the name)

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

the default (from the name)

The default is an element of $\operatorname{K'}$ defined as $\operatorname{main}$.

the default (from the name)

The default is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}$.

Let $p$ be a function from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$. Let $x$ and $x_{1}$ be elements of $\operatorname{K'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\operatorname{moveExcl}$ applied to $p$, $x$, $x_{1}$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to $p$, $x$, $x_{1}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_push}$ applied to $x$, $\mathrm{id}$ and $q$.

Let $p$ be a function from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$. Let $x$ and $x_{1}$ be elements of $\operatorname{K'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_move\_u2082\_}$ applied to $p$, $x$, $x_{1}$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\operatorname{moveExcl}$ applied to $p$, $x$, $\operatorname{rev}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to the function that maps $x_{2}$ to $\operatorname{false}$, $\operatorname{rev}$, $x_{1}$ and $q$.

the natural end of x (from the name)

Let $x$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$. Then the natural end of $x$ is an element of $\mathrm{Bool}$.

Let $k$ be an element of $\operatorname{K'}$. Let $x$ be an element of $\operatorname{Stmt'}$. Then $\operatorname{peek'}$ applied to $k$ and $x$ is an element of $\operatorname{Stmt'}$ defined as $\operatorname{peek}$ applied to $k$, the function that maps $x$ and $v$ to $v$ and $x$.

the pop of k and x (from the name)

Let $k$ be an element of $\operatorname{K'}$. Let $x$ be an element of $\operatorname{Stmt'}$. Then the pop of $k$ and $x$ is an element of $\operatorname{Stmt'}$ defined as the pop of the function that maps $x$ and $v$ to $v$ and $x$.

Let $k$ be an element of $\operatorname{K'}$. Let $x$ be an element of $\operatorname{Stmt'}$. Then $\operatorname{push'}$ applied to $k$ and $x$ is an element of $\operatorname{Stmt'}$ defined as $\operatorname{push}$ applied to $k$, the function that maps $x$ to $\operatorname{getD}$ applied to $x$ and $\operatorname{default}$ and $x$.

the split at predecessor of p and x1 (from the name)

Let $p$ be a function from elements of $x$ to elements of $\mathrm{Bool}$. Let $x_{1}$ be a list of elements of $x$. Then the split at predecessor of $p$ and $x_{1}$ is an element of $\mathrm{Prod}$ applied to the set of lists of elements of $x$ and $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x$ and the set of lists of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_splitAtPred\_\_\_f}$ applied to $p$.

the trace of x (from the name)

Let $x$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then the trace of $x$ is an element of $\operatorname{Stmt'}$.

Let $x$ be an element of $\operatorname{Cont}$. Then $\operatorname{trCont}$ applied to $x$ is an element of $\operatorname{Cont'}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_trCont\_\_\_f}$.

the trace continuous stack of k (from the name)

Let $k$ be an element of $\operatorname{Cont}$. Then the trace continuous stack of $k$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as the trace list of the continuous stack of $k$.

the trace list of x (from the name)

Let $x$ be a list of lists of natural numbers. Then the trace list of $x$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_trLList\_\_\_f}$.

the trace list of x (from the name)

Let $x$ be a list of natural numbers. Then the trace list of $x$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_trList\_\_\_f}$.

the trace natural number of n (from the name)

Let $n$ be a natural number. Then the trace natural number of $n$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as the trace numerator of $n$.

the trace normal of x and x1 (from the name)

Let $x$ be a code. Let $x_{1}$ be an element of $\operatorname{Cont'}$. Then the trace normal of $x$ and $x_{1}$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Turing\_\_PartrecToTM2\_\_trNormal\_\_\_f}$ and $x_{1}$.

the trace numerator of x (from the name)

Let $x$ be a numerator. Then the trace numerator of $x$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

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

Let $x$ be a positive part numerator. Then the trace positive part numerator of $x$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_trPosNum\_\_\_f}$.

Let $x$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_trStmts\_u2081\_}$ applied to $x$ is a finite set of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_brecOn}$ applied to $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_trStmts\_u2081\_\_\_\_f}$.

Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\operatorname{unrev}$ applied to $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ defined as $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to the function that maps $x$ to $\operatorname{false}$, $\operatorname{rev}$, $\operatorname{main}$ and $q$.

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

the bit (from the name)

The bit is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

the bit (from the name)

The bit is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

$\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons}$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

$\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_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 $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the bit and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the bit.

$\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_enumList}$ is a list of elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\operatorname{cons}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}$ and $\operatorname{cons}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons}$ and $\operatorname{cons}$ applied to the bit and $\operatorname{cons}$ applied to the bit and $\operatorname{nil}$.

Let $x$ be a natural number. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_ofNat}$ applied to $x$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons\_u2097\_}$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'\_\_cons}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $2$, the bit and the bit.

The elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ are a basic type.

Let $S$ be a finite set of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Let $x$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_Supports}$ holds for $S$ and $x$, if $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_brecOn}$ holds for $x$ and $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_Supports\_\_\_f}$ applied to $S$.

Let $p$ be a function from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$. Let $k$ be an element of $\operatorname{K'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_clear}$ applied to $p$, $k$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

the copy of q (from the name)

Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then the copy of $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_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 $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 the set of functions from functions $p$ from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$ and elements $x$ of $\operatorname{K'}$ and elements $x_{1}$ of $\operatorname{K'}$ and elements $q$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to $p$, $x$, $x_{1}$ and $q$ and $\mathrm{PULift}$ applied to the set of functions from functions $p_{1}$ from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$ and elements $k$ of $\operatorname{K'}$ and elements $q_{1}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_clear}$ applied to $p_{1}$, $k$ and $q_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $q_{2}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to the copy of $q_{2}$ and $\mathrm{PULift}$ applied to the set of functions from elements $k_{1}$ of $\operatorname{K'}$ and functions $s$ from elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ and elements $q_{3}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_push}$ applied to $k_{1}$, $s$ and $q_{3}$ 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 functions $f$ from elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_read}$ applied to $f$ and $\mathrm{PULift}$ applied to the set of functions from elements $q_{4}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to the successor of $q_{4}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $6$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{6}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ and elements $x_{7}$ of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$ to elements of $\mathrm{motive}$ applied to the predecessor of $x_{6}$ and $x_{7}$ and $\mathrm{PULift}$ applied to the set of functions from elements $k_{2}$ of $\operatorname{Cont'}$ to elements of $\mathrm{motive}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_ret}$ applied to $k_{2}$.

Let $p$ be a function from elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Bool}$. Let $x$ and $x_{1}$ be elements of $\operatorname{K'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_move}$ applied to $p$, $x$, $x_{1}$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

the predecessor of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then the predecessor of $x$ and $x_{1}$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

Let $k$ be an element of $\operatorname{K'}$. Let $s$ be a function from elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$. Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_push}$ applied to $k$, $s$ and $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

Let $f$ be a function from elements of $\mathrm{Option}$ applied to $\mathrm{Turing\_\_PartrecToTM2\_\_\_u393\_'}$ to elements of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_read}$ applied to $f$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

Let $k$ be an element of $\operatorname{Cont'}$. Then $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'\_\_ret}$ applied to $k$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.

the successor of q (from the name)

Let $q$ be an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$. Then the successor of $q$ is an element of $\mathrm{Turing\_\_PartrecToTM2\_\_\_u39b\_'}$.