Remove duplicate check for required scripts in UTXOW

IntersectMBO · Jul 28, 2021 · ba20b8e · ba20b8e
1 parent 93c1d76
commit ba20b8e
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/alonzo/formal-spec/utxo.tex b/alonzo/formal-spec/utxo.tex
@@ -874,11 +874,10 @@ \subsection{Witnessing}
       \hldiff{\var{inputHashes}\leteq \{ h \mid (\_ \mapsto (a, \_, h)) \in \txins{txb} \restrictdom \var{utxo}, \fun{isTwoPhaseScriptAddress}~{tx}~{a}\}}   \\~\\
       \hldiff{\forall \var{s} \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhOne,
       \fun{validateScript}~\var{s}~\var{tx}}\\~\\
-      \hldiff{\{ s \mid (\_, s) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
+      \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
       \hldiff{\var{inputHashes} \subseteq \dom (\fun{txdats}~{txw})} \\~\\
       \hldiff{\dom (\fun{txdats}~{txw}) \subseteq \var{inputHashes} \cup \{h~\mid~ (\wcard, \wcard, h)\in\fun{txouts}\}}
       \\~\\
-      \hldiff{\forall (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~h \in \dom (\fun{txscripts}~(\fun{txwits}~tx))} \\
       \hldiff{\ \dom (\fun{txrdmrs}~tx) ~=~\{~\fun{rdptr}~txb~sp~
        \vert~ (sp,h)~\in~\fun{scriptsNeeded}~\var{utxo}~\var{tx}, } \\
       \hldiff{h\mapsto s~\in~\fun{txscripts}~{txw}, s~\in~\ScriptPhTwo \}}