diff --git a/formalism/symbols/untyped.tex b/formalism/symbols/untyped.tex index f1e5c8f..91dae5e 100644 --- a/formalism/symbols/untyped.tex +++ b/formalism/symbols/untyped.tex @@ -4,8 +4,8 @@ % zippered types % \newcommand{\ZTMName}{{\normalfont\textsf{ZType}}} -\newcommand{\ZTMSet}{\ensuremath{\hat{T}}} -\newcommand{\ZTMV}{\ensuremath{\hat{\tau}}} +\newcommand{\ZTMSet}{\ensuremath{\underline{T}}} +\newcommand{\ZTMV}{\ensuremath{\underline{\tau}}} % cursor \newcommand{\ZTCursor}[1]{\ensuremath{\ZCursor{#1}}} @@ -20,8 +20,8 @@ % zippered expressions % \newcommand{\ZMName}{{\normalfont\textsf{ZExp}}} -\newcommand{\ZMSet}{\ensuremath{\hat{E}}} -\newcommand{\ZMV}{\ensuremath{\hat{e}}} +\newcommand{\ZMSet}{\ensuremath{\underline{E}}} +\newcommand{\ZMV}{\ensuremath{\underline{e}}} % cursor \definecolor{cursorhighlight}{RGB}{230,255,230} @@ -42,9 +42,6 @@ \newcommand{\ZIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} \newcommand{\ZIfL}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} \newcommand{\ZIfR}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}} -\newcommand{\ZInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} -\newcommand{\ZInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} -\newcommand{\ZInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} % let \newcommand{\ZLetL}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}} @@ -59,7 +56,25 @@ % errors \newcommand{\ZFree}[1]{\ensuremath{\ECFree{#1}}} \newcommand{\ZInconType}[1]{\ensuremath{\ECInconType{#1}}} -\newcommand{\ZInconBr}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}} +\newcommand{\ZInconAsc}[1]{\ensuremath{\ECInconAsc{#1}}} +\newcommand{\ZSynNonMatchedArrow}[1]{\ensuremath{\ECSynNonMatchedArrow{#1}}} +\newcommand{\ZSynNonMatchedProd}[1]{\ensuremath{\ECSynNonMatchedProd{#1}}} +\newcommand{\ZAnaNonMatchedArrow}[1]{\ensuremath{\ECAnaNonMatchedArrow{#1}}} +\newcommand{\ZAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}} + +\newcommand{\ZLamInconAscT}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZLamInconAscE}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZApSynNonMatchedArrowL}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZApSynNonMatchedArrowR}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}} +\newcommand{\ZProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}} +\newcommand{\ZLamAnaNonMatchedArrowT}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZLamAnaNonMatchedArrowE}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}} +\newcommand{\ZPairAnaNonMatchedProdL}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} +\newcommand{\ZPairAnaNonMatchedProdR}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}} % % zipper judgments diff --git a/formalism/typed.tex b/formalism/typed.tex index ec5f84b..92854d3 100644 --- a/formalism/typed.tex +++ b/formalism/typed.tex @@ -21,7 +21,14 @@ \subsection{Syntax} & & \mid & \ZLetL{x}{\ZMV}{\ECMV} \mid \ZLetR{x}{\ECMV}{\ZMV} \\ & & \mid & \ZPlusL{\ZMV}{\ECMV} \mid \ZPlusR{\ECMV}{\ZMV} \\ & & \mid & \ZIfC{\ZMV}{\ECMV}{\ECMV} \mid \ZIfL{\ECMV}{\ZMV}{\ECMV} \mid \ZIfR{\ECMV}{\ECMV}{\ZMV} \\ - & & \mid & \ZInconType{\ZMV} \mid \ZInconBrC{\ZMV}{\ECMV}{\ECMV} \mid \ZInconBrL{\ECMV}{\ZMV}{\ECMV} \mid \ZInconBrR{\ECMV}{\ECMV}{\ZMV} \\ + & & \mid & \ZPairL{\ZMV}{\EMV} \mid \ZPairR{\EMV}{\ZMV} \mid \ZProjL{\ZMV} \mid \ZProjR{\ZMV} \\ + & & \mid & \ZFree{x} \mid \ZInconType{\ZMV} \\ + & & \mid & \ZLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZLamInconAscE{x}{\TMV}{\ZMV} + \mid \ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV} + \mid \ZApSynNonMatchedArrowL{\ZMV}{\ECMV} \mid \ZApSynNonMatchedArrowR{\ECMV}{\ZMV} \\ + & & \mid & \ZInconBrC{\ZMV}{\ECMV}{\ECMV} \mid \ZInconBrL{\ECMV}{\ZMV}{\ECMV} \mid \ZInconBrR{\ECMV}{\ECMV}{\ZMV} \\ + & & \mid & \ZPairAnaNonMatchedProdL{\ZMV}{\ECMV} \mid \ZPairAnaNonMatchedProdR{\ECMV}{\ZMV} + \mid \ZProjLSynNonMatchedProd{\ZMV} \mid \ZProjRSynNonMatchedProd{\ZMV} \end{array}\] \subsubsection{Well-formedness} @@ -33,86 +40,96 @@ \subsubsection{Well-formedness} \zWellFormed{\ZCursor{\ECMV}} } - \inferrule[WFLamT]{ }{ + \inferrule[WFLam1]{ }{ \zWellFormed{\ZLamT{x}{\ZTMV}{\ECMV}} } - \inferrule[WFLamE]{ + \inferrule[WFLam2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLamE{x}{\TMV}{\ZMV}} } - \inferrule[WFApL]{ + \inferrule[WFAp1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZApL{\ZMV}{\ECMV}} } - \inferrule[WFApR]{ + \inferrule[WFAp2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZApR{\ECMV}{\ZMV}} } - \inferrule[WFLetL]{ + \inferrule[WFLet1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLetL{x}{\ZMV}{\ECMV}} } - \inferrule[WFLetR]{ + \inferrule[WFLet2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZLetR{x}{\ECMV}{\ZMV}} } - \inferrule[WFPlusL]{ + \inferrule[WFPlus1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZPlusL{\ZMV}{\ECMV}} } - \inferrule[WFPlusR]{ + \inferrule[WFPlus2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZPlusR{\ECMV}{\ZMV}} } - \inferrule[WFIfC]{ + \inferrule[WFIf1]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}} } - \inferrule[WFIfL]{ + \inferrule[WFIf2]{ \zWellFormed{\ZMV} }{ \zWellFormed{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}} } - \inferrule[WFIfC]{ + \inferrule[WFIf3]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZIfL{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}} } - \inferrule[WFInconsistentBranchesC]{ + \inferrule[WFPair1]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZPairL{\ZMV}{\ECMV}} } - \inferrule[WFInconsistentBranchesL]{ + \inferrule[WFPair2]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}} + \zWellFormed{\ZPairR{\ECMV}{\ZMV}} + } + + \inferrule[WFProjL1]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjL{\ZMV}} } - \inferrule[WFInconsistentBranchesR]{ + \inferrule[WFProjR1]{ \zWellFormed{\ZMV} }{ - \zWellFormed{\ZInconBrL{\ZMV}{\ECMV_1}{\ECMV_2}} + \zWellFormed{\ZProjR{\ZMV}} + } + + \inferrule[WFFree]{ }{ + \zWellFormed{\ZFree{x}} } \inferrule[WFInconsistentTypes]{ @@ -121,6 +138,81 @@ \subsubsection{Well-formedness} }{ \zWellFormed{\ZInconType{\ZMV}} } + + \inferrule[WFLam3]{ }{ + \zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}} + } + + \inferrule[WFLam4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}} + } + + \inferrule[WFLam5]{ + }{ + \zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}} + } + + \inferrule[WFLam6]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}} + } + + \inferrule[WFAp3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}} + } + + \inferrule[WFAp4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}} + } + + \inferrule[WFInconsistentBranches1]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}} + } + + \inferrule[WFInconsistentBranches2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}} + } + + \inferrule[WFInconsistentBranches3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}} + } + + \inferrule[WFPair3]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}} + } + + \inferrule[WFPair4]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}} + } + + \inferrule[WFProjL2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}} + } + + \inferrule[WFProjR2]{ + \zWellFormed{\ZMV} + }{ + \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}} + } \end{mathpar} \subsection{Cursor erasure} diff --git a/formalism/untyped.tex b/formalism/untyped.tex index fe9b6d6..541203d 100644 --- a/formalism/untyped.tex +++ b/formalism/untyped.tex @@ -7,6 +7,14 @@ \section{Untyped hazelnut} \label{sec:untyped} +In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be +layered with the marked lambda calculus to yield a structure editing calculus that supports +non-local hole fixes. + +In comparison with the original calculus, this untyped version is not concerned at all with typing +but only the manipulation of syntax. As such, the action judgments are simplified considerably; in +particular, they are no longer bidirectional. The same core metatheorems, except sensibility which +is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}). \begin{mechanization} \item hazelnut.agda @@ -28,38 +36,38 @@ \subsection{Cursor erasure} \subsubsection{Type cursor erasure} \label{sec:untyped-type-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction $\ZTMName \to \TMName$ defined as follows: % \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}} \[\begin{array}{rcl} \cursorErasesToRow{\ZTCursor{\TMV}}{\TMV} \\ - \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{\cursorErase{\ZTMV}}{\TMV}} \\ - \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{\cursorErase{\ZTMV}}} \\ - \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{\cursorErase{\ZTMV}}{\TMV}} \\ - \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{\cursorErase{\ZTMV}}} \\ + \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{(\cursorErase{\ZTMV})}{\TMV}} \\ + \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{(\cursorErase{\ZTMV})}} \\ + \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{(\cursorErase{\ZTMV})}{\TMV}} \\ + \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{(\cursorErase{\ZTMV})}} \\ \end{array}\] \subsubsection{Expression cursor erasure} \label{sec:untyped-expression-cursor-erasure} -\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows: +\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction $\ZMName \to \EMName$ defined as follows: % \[\begin{array}{rcl} \cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\ - \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{\cursorErase{\ZTMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{\cursorErase{\ZMV}}{\EMV_1}{\EMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{\cursorErase{\ZMV}}{\EMV_2}} \\ - \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZPairL{\ZMV}{\EMV})}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\ - \cursorErasesToRow{(\ZPairR{\EMV}{\ZMV})}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{\cursorErase{\ZMV}}} \\ - \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{(\cursorErase{\ZTMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{(\cursorErase{\ZMV})}{\EMV}} \\ + \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{(\cursorErase{\ZMV})}{\EMV_1}{\EMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{(\cursorErase{\ZMV})}{\EMV_2}} \\ + \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{\ZPairL{\ZMV}{\EMV}}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\ + \cursorErasesToRow{\ZPairR{\EMV}{\ZMV}}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\ + \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{(\cursorErase{\ZMV})}} \\ + \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{(\cursorErase{\ZMV})}} \\ \end{array}\] \subsection{Action model} @@ -586,13 +594,13 @@ \subsubsection{Expression actions} \inferrule[AEZipProjL]{ \AUEAction{\ZMV}{\ZMV'}{\AMV} }{ - \AUEAction{\ZProjL{\ZMV}{\EMV}}{\ZProjL{\ZMV'}{\EMV}}{\AMV} + \AUEAction{\ZProjL{\ZMV}}{\ZProjL{\ZMV'}}{\AMV} } \inferrule[AEZipProjR]{ \AUEAction{\ZMV}{\ZMV'}{\AMV} }{ - \AUEAction{\ZProjR{\EMV}{\ZMV}}{\ZProjR{\EMV}{\ZMV'}}{\AMV} + \AUEAction{\ZProjR{\ZMV}}{\ZProjR{\ZMV'}}{\AMV} } \end{mathparpagebreakable} @@ -644,66 +652,80 @@ \subsubsection{Iterated actions} \subsection{Metatheorems} \label{sec:untyped-metatheorems} -\begin{theorem}[name=Sensibility] -\end{theorem} \begin{theorem}[name=Movement Erasure Invariance] \ \begin{enumerate} - \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} = - \cursorErase{\ZTMV'}$. + \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, + then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$. - \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZMV} = - \cursorErase{\ZMV'}$. + \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, + then $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Reachability] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that - $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. - - \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, then there exists $\AIMV$ such that - $\movements{\AIMV}$ and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$. \end{enumerate} \end{theorem} \begin{lemma}[name=Reach Up] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. - - \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \EMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$. \end{enumerate} \end{lemma} \begin{lemma}[name=Reach Down] \ \begin{enumerate} - \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. - - \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ - and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$. + \item If $\cursorErase{\ZTMV} = \TMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$. + + \item If $\cursorErase{\ZMV} = \EMV$, + then there exists $\AIMV$ + such that $\movements{\AIMV}$ + and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$. \end{enumerate} \end{lemma} \begin{theorem}[name=Constructability] \ \begin{enumerate} - \item For every $\TMV$, there exists $\AIMV$ such that - $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$. + \item For every $\TMV$, + there exists $\AIMV$ + such that $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$. - \item For every $\EMV$, there exists $\AIMV$ such that - $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$. + \item For every $\EMV$, + there exists $\AIMV$ + such that $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$. \end{enumerate} \end{theorem} \begin{theorem}[name=Determinism] \ \begin{enumerate} - \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then - $\ZTMV' = \ZTMV''$. + \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ + and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, + then $\ZTMV' = \ZTMV''$. - \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, then - $\ZMV' = \ZMV''$. + \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ + and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, + then $\ZMV' = \ZMV''$. \end{enumerate} \end{theorem}