diff --git a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs
index 5e105bc2f9b..b9bf04762a9 100644
--- a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs
+++ b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs
@@ -34,7 +34,8 @@ instance STS SIGCNT where
 
   -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure SIGCNT
-    = TooManyIssuedBlocks VKeyGenesis -- The given genesis key issued too many blocks.
+    = TooManyIssuedBlocks VKeyGenesis
+    -- ^ The given genesis key issued too many blocks.
     | NotADelegate
     -- ^ The key signing the block is not a delegate of a genesis key.
 
diff --git a/byron/ledger/executable-spec/src/Ledger/Update.hs b/byron/ledger/executable-spec/src/Ledger/Update.hs
index a213df1d364..6a48a22d3cc 100644
--- a/byron/ledger/executable-spec/src/Ledger/Update.hs
+++ b/byron/ledger/executable-spec/src/Ledger/Update.hs
@@ -530,14 +530,14 @@ instance STS UPVOTE where
     )
   type Signal UPVOTE = Vote
 
-  -- | `S_CfmThdNotReached` is a structural `PredicateFailure`, used to fail
-  -- from one transition rule to the other. The other `PredicateFailure`s are
-  -- all throwable.
+  -- | The 3 non-embedded `PredicateFailure`s here are all structural. The
+  -- disjuntion of the preconditions is `True` - one rule either fires or the
+  -- other does.
   data PredicateFailure UPVOTE
     = ADDVOTEFailure (PredicateFailure ADDVOTE)
-    | HigherThanThdAndNotAlreadyConfirmed
+    | S_HigherThanThdAndNotAlreadyConfirmed
     | S_CfmThdNotReached
-    | AlreadyConfirmed
+    | S_AlreadyConfirmed
     deriving (Eq, Show)
 
   initialRules = []
@@ -549,7 +549,7 @@ instance STS UPVOTE where
             ) <- judgmentContext
         vts' <- trans @ADDVOTE $ TRC ((rups, dms), vts, vote)
         let pid = vote ^. vPropId
-        size ([pid] ◁ vts') < t || pid ∈ dom cps ?! HigherThanThdAndNotAlreadyConfirmed
+        size ([pid] ◁ vts') < t || pid ∈ dom cps ?! S_HigherThanThdAndNotAlreadyConfirmed
         pure $! ( cps
                 , vts'
                 )
@@ -561,7 +561,7 @@ instance STS UPVOTE where
         vts' <- trans @ADDVOTE $ TRC ((rups, dms), vts, vote)
         let pid = vote ^. vPropId
         t <= size ([pid] ◁ vts') ?! S_CfmThdNotReached
-        pid ∉ dom cps ?! AlreadyConfirmed
+        pid ∉ dom cps ?! S_AlreadyConfirmed
         pure $! ( cps ⨃ [(pid, sn)]
                 , vts'
                 )
diff --git a/byron/semantics/executable-spec/src/Control/State/Transition.hs b/byron/semantics/executable-spec/src/Control/State/Transition.hs
index eedeaed7e45..816400658a2 100644
--- a/byron/semantics/executable-spec/src/Control/State/Transition.hs
+++ b/byron/semantics/executable-spec/src/Control/State/Transition.hs
@@ -82,6 +82,11 @@ class ( Eq (PredicateFailure a)
   -- As a convention, `PredicateFailure`s which are "structural" (meaning that
   -- they are not "throwable" in practice, and are used to pass control from
   -- one transition rule to another) are prefixed with `S_`.
+  --
+  -- Structural `PredicateFailure`s represent conditions between rules where
+  -- the disjunction of all rules' preconditions is equal to `True`. That is,
+  -- either one rule will throw a structural `PredicateFailure` and the other
+  -- will succeed, or vice-versa.
   data PredicateFailure a :: *
 
   -- | Rules governing transition under this system.