diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs
index 51ff7581e1..cd5e15fee8 100644
--- a/kore/src/Kore/Internal/Conditional.hs
+++ b/kore/src/Kore/Internal/Conditional.hs
@@ -32,6 +32,9 @@ import Prelude.Kore
 import Control.DeepSeq
     ( NFData
     )
+import Data.Map.Strict
+    ( Map
+    )
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
@@ -245,6 +248,16 @@ instance
   where
     from = pure
 
+instance
+    InternalVariable variable
+    => From (Map (SomeVariable variable) (TermLike variable)) (Conditional variable ())
+  where
+    from =
+        from @(Substitution variable) @(Conditional variable ())
+        . from
+            @(Map (SomeVariable variable) (TermLike variable))
+            @(Substitution variable)
+
 unparseConditional
     :: Sort
     -> Doc ann    -- ^ term
diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs
index 2381490ffc..684fbedd0d 100644
--- a/kore/src/Kore/Internal/OrPattern.hs
+++ b/kore/src/Kore/Internal/OrPattern.hs
@@ -20,6 +20,8 @@ module Kore.Internal.OrPattern
     , toPattern
     , toTermLike
     , targetBinder
+    , substitute
+    , parseFromTermLike
     , MultiOr.flatten
     , MultiOr.filterOr
     , MultiOr.gather
@@ -29,6 +31,9 @@ module Kore.Internal.OrPattern
 import Prelude.Kore
 
 import qualified Data.Foldable as Foldable
+import Data.Map.Strict
+    ( Map
+    )
 
 import Kore.Internal.Condition
     ( Condition
@@ -52,6 +57,7 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
     )
 import Kore.Internal.TermLike
     ( InternalVariable
+    , pattern Or_
     , Sort
     , TermLike
     , mkBottom_
@@ -219,3 +225,19 @@ targetBinder Binder { binderVariable, binderChild } =
          { binderVariable = newVar
          , binderChild = newChild
          }
+
+substitute
+    :: InternalVariable variable
+    => Map (SomeVariableName variable) (TermLike variable)
+    -> OrPattern variable
+    -> OrPattern variable
+substitute subst =
+    fromPatterns . fmap (Pattern.substitute subst) . toPatterns
+
+parseFromTermLike
+    :: InternalVariable variable
+    => TermLike variable
+    -> OrPattern variable
+parseFromTermLike (Or_ _ term1 term2) =
+    parseFromTermLike term1 <> parseFromTermLike term2
+parseFromTermLike term = fromTermLike term
diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs
index 8012b76d24..5d819ce064 100644
--- a/kore/src/Kore/Internal/Pattern.hs
+++ b/kore/src/Kore/Internal/Pattern.hs
@@ -10,6 +10,7 @@ module Kore.Internal.Pattern
     , patternSort
     , fromCondition
     , fromCondition_
+    , fromTermAndPredicate
     , fromPredicateSorted
     , bottom
     , bottomOf
@@ -96,6 +97,18 @@ program configuration for Kore execution.
  -}
 type Pattern variable = Conditional variable (TermLike variable)
 
+fromTermAndPredicate
+    :: InternalVariable variable
+    => TermLike variable
+    -> Predicate variable
+    -> Pattern variable
+fromTermAndPredicate term predicate =
+    Conditional
+        { term
+        , predicate
+        , substitution = mempty
+        }
+
 fromCondition_
     :: InternalVariable variable
     => Condition variable
diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs
index 963e8ff5da..dfb50c2d32 100644
--- a/kore/src/Kore/Internal/TermLike.hs
+++ b/kore/src/Kore/Internal/TermLike.hs
@@ -45,6 +45,11 @@ module Kore.Internal.TermLike
     -- * Utility functions for dealing with sorts
     , forceSort
     , fullyOverrideSort
+    -- * Reachability modalities and application
+    , Modality (..)
+    , weakExistsFinally
+    , weakAlwaysFinally
+    , applyModality
     -- * Pure Kore pattern constructors
     , mkAnd
     , mkApplyAlias
@@ -2025,3 +2030,60 @@ refreshSetBinder
     -> Binder (SetVariable variable) (TermLike variable)
     -> Binder (SetVariable variable) (TermLike variable)
 refreshSetBinder = refreshBinder refreshSetVariable
+
+data Modality = WEF | WAF
+
+-- | Weak exists finally modality symbol.
+weakExistsFinally :: Text
+weakExistsFinally = "weakExistsFinally"
+
+-- | Weak always finally modality symbol.
+weakAlwaysFinally :: Text
+weakAlwaysFinally = "weakAlwaysFinally"
+
+-- | 'Alias' construct for weak exist finally.
+wEF :: Sort -> Alias (TermLike VariableName)
+wEF sort = Alias
+    { aliasConstructor = Id
+        { getId = weakExistsFinally
+        , idLocation = AstLocationNone
+        }
+    , aliasParams = [sort]
+    , aliasSorts = ApplicationSorts
+        { applicationSortsOperands = [sort]
+        , applicationSortsResult = sort
+        }
+    , aliasLeft = []
+    , aliasRight = mkTop sort
+    }
+
+-- | 'Alias' construct for weak always finally.
+wAF :: Sort -> Alias (TermLike VariableName)
+wAF sort = Alias
+    { aliasConstructor = Id
+        { getId = weakAlwaysFinally
+        , idLocation = AstLocationNone
+        }
+    , aliasParams = [sort]
+    , aliasSorts = ApplicationSorts
+        { applicationSortsOperands = [sort]
+        , applicationSortsResult = sort
+        }
+    , aliasLeft = []
+    , aliasRight = mkTop sort
+    }
+
+-- | Apply one of the reachability modality aliases
+-- to a term.
+applyModality
+    :: Modality
+    -> TermLike VariableName
+    -> TermLike VariableName
+applyModality modality term =
+    case modality of
+        WEF ->
+            mkApplyAlias (wEF sort) [term]
+        WAF ->
+            mkApplyAlias (wAF sort) [term]
+  where
+    sort = termLikeSort term
diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs
index 21c230fc1f..b24865f47d 100644
--- a/kore/src/Kore/Rewriting/RewritingVariable.hs
+++ b/kore/src/Kore/Rewriting/RewritingVariable.hs
@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
+    , RewritingVariable
     , isConfigVariable
     , isRuleVariable
     , isSomeConfigVariable
@@ -26,6 +27,8 @@ module Kore.Rewriting.RewritingVariable
     , getResultPattern
     , getRemainderPredicate
     , getRemainderPattern
+    -- * Exported for reachability rule unparsing
+    , getRewritingVariable
     ) where
 
 import Prelude.Kore
@@ -118,6 +121,8 @@ instance From VariableName RewritingVariableName where
 
 instance FreshName RewritingVariableName
 
+type RewritingVariable = Variable RewritingVariableName
+
 mkElementConfigVariable
     :: ElementVariable VariableName
     -> ElementVariable RewritingVariableName
diff --git a/kore/src/Kore/Step/ClaimPattern.hs b/kore/src/Kore/Step/ClaimPattern.hs
new file mode 100644
index 0000000000..3cf69dd2bd
--- /dev/null
+++ b/kore/src/Kore/Step/ClaimPattern.hs
@@ -0,0 +1,423 @@
+{-|
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Step.ClaimPattern
+    ( ClaimPattern (..)
+    , freeVariablesLeft
+    , freeVariablesRight
+    , claimPattern
+    , OnePathRule (..)
+    , AllPathRule (..)
+    , ReachabilityRule (..)
+    , toSentence
+    , applySubstitution
+    , termToExistentials
+    -- * For unparsing
+    , onePathRuleToTerm
+    , allPathRuleToTerm
+    ) where
+
+import Prelude.Kore
+
+import Control.DeepSeq
+    ( NFData
+    )
+import qualified Data.Default as Default
+import Data.Map.Strict
+    ( Map
+    )
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+import qualified Generics.SOP as SOP
+import qualified GHC.Generics as GHC
+
+import qualified Kore.Attribute.Axiom as Attribute
+import Kore.Attribute.Pattern.FreeVariables
+    ( FreeVariables
+    , HasFreeVariables (..)
+    )
+import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
+import Kore.Debug
+import Kore.Internal.OrPattern
+    ( OrPattern
+    )
+import qualified Kore.Internal.OrPattern as OrPattern
+import Kore.Internal.Pattern
+    ( Pattern
+    )
+import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.Substitution
+    ( Substitution
+    )
+import qualified Kore.Internal.Substitution as Substitution
+import Kore.Internal.Symbol
+    ( Symbol
+    )
+import Kore.Internal.TermLike
+    ( ElementVariable
+    , Modality
+    , SomeVariable
+    , SomeVariableName (..)
+    , TermLike
+    , VariableName
+    )
+import qualified Kore.Internal.TermLike as TermLike
+import Kore.Rewriting.RewritingVariable
+    ( RewritingVariableName
+    , getRewritingVariable
+    )
+import qualified Kore.Syntax.Definition as Syntax
+import Kore.TopBottom
+    ( TopBottom (..)
+    )
+import Kore.Unparser
+    ( Unparse (..)
+    )
+import qualified Kore.Verified as Verified
+
+import Pretty
+    ( Pretty (..)
+    )
+import qualified Pretty
+
+-- | Representation of reachability claim types.
+data ClaimPattern =
+    ClaimPattern
+    { left :: !(Pattern RewritingVariableName)
+    , existentials :: ![ElementVariable RewritingVariableName]
+    , right :: !(OrPattern RewritingVariableName)
+    , attributes :: !(Attribute.Axiom Symbol RewritingVariableName)
+    }
+    deriving (Eq, Ord, Show, GHC.Generic)
+
+instance NFData ClaimPattern
+
+instance SOP.Generic ClaimPattern
+
+instance SOP.HasDatatypeInfo ClaimPattern
+
+instance Debug ClaimPattern
+
+instance Diff ClaimPattern
+
+instance From ClaimPattern Attribute.SourceLocation where
+    from = Attribute.sourceLocation . attributes
+
+instance From ClaimPattern Attribute.Label where
+    from = Attribute.label . attributes
+
+instance From ClaimPattern Attribute.RuleIndex where
+    from = Attribute.identifier . attributes
+
+instance Pretty ClaimPattern where
+    pretty claimPattern'@(ClaimPattern _ _ _ _) =
+        Pretty.vsep
+            [ "left:"
+            , Pretty.indent 4 (unparse left)
+            , "existentials:"
+            , Pretty.indent 4 (Pretty.list $ unparse <$> existentials)
+            , "right:"
+            , Pretty.indent 4 (unparse $ OrPattern.toTermLike right)
+            ]
+      where
+        ClaimPattern
+            { left
+            , right
+            , existentials
+            } = claimPattern'
+
+instance TopBottom ClaimPattern where
+    isTop _ = False
+    isBottom _ = False
+
+instance From ClaimPattern Attribute.PriorityAttributes where
+    from = from @(Attribute.Axiom _ _) . attributes
+
+instance From ClaimPattern Attribute.HeatCool where
+    from = from @(Attribute.Axiom _ _) . attributes
+
+freeVariablesRight
+    :: ClaimPattern
+    -> FreeVariables RewritingVariableName
+freeVariablesRight claimPattern'@(ClaimPattern _ _ _ _) =
+    freeVariables
+        ( TermLike.mkExistsN existentials
+            (OrPattern.toTermLike right)
+        )
+  where
+    ClaimPattern { right, existentials } = claimPattern'
+
+freeVariablesLeft
+    :: ClaimPattern
+    -> FreeVariables RewritingVariableName
+freeVariablesLeft claimPattern'@(ClaimPattern _ _ _ _) =
+    freeVariables left
+  where
+    ClaimPattern { left } = claimPattern'
+
+instance HasFreeVariables ClaimPattern RewritingVariableName where
+    freeVariables claimPattern'@(ClaimPattern _ _ _ _) =
+        freeVariablesLeft claimPattern'
+        <> freeVariablesRight claimPattern'
+
+-- | Creates a 'ClaimPattern' from a left hand side 'Pattern'
+-- and an 'OrPattern', representing the right hand side pattern.
+-- The list of element variables are existentially quantified
+-- in the right hand side.
+
+claimPattern
+    :: Pattern RewritingVariableName
+    -> OrPattern RewritingVariableName
+    -> [ElementVariable RewritingVariableName]
+    -> ClaimPattern
+claimPattern left right existentials =
+    ClaimPattern
+        { left
+        , right
+        , existentials
+        , attributes = Default.def
+        }
+
+claimPatternToTerm
+    :: Modality
+    -> ClaimPattern
+    -> TermLike VariableName
+claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) =
+    TermLike.mkImplies
+        leftPattern
+        (TermLike.applyModality modality rightPattern)
+  where
+    ClaimPattern { left, right, existentials } = representation
+    leftPattern =
+        Pattern.toTermLike left
+        & TermLike.mapVariables getRewritingVariable
+    rightPattern =
+        TermLike.mkExistsN existentials (OrPattern.toTermLike right)
+        & TermLike.mapVariables getRewritingVariable
+
+substituteRight
+    :: Map
+        (SomeVariableName RewritingVariableName)
+        (TermLike RewritingVariableName)
+    -> ClaimPattern
+    -> ClaimPattern
+substituteRight subst claimPattern'@ClaimPattern { right, existentials } =
+    claimPattern'
+        { right = OrPattern.substitute subst' right
+        }
+  where
+    subst' =
+        foldr
+            ( Map.delete
+            . inject
+            . TermLike.variableName
+            )
+            subst
+            existentials
+
+-- | Apply the substitution to the claim.
+substitute
+    :: Map
+        (SomeVariableName RewritingVariableName)
+        (TermLike RewritingVariableName)
+    -> ClaimPattern
+    -> ClaimPattern
+substitute subst claimPattern'@(ClaimPattern _ _ _ _) =
+    substituteRight subst
+    $ claimPattern'
+        { left = Pattern.substitute subst left
+        }
+  where
+    ClaimPattern { left } = claimPattern'
+
+-- | Applies a substitution to a claim and checks that
+-- it was fully applied, i.e. there is no substitution
+-- variable left in the claim.
+applySubstitution
+    :: HasCallStack
+    => Substitution RewritingVariableName
+    -> ClaimPattern
+    -> ClaimPattern
+applySubstitution substitution claim =
+    if finalClaim `isFreeOf` substitutedVariables
+        then finalClaim
+        else error
+            (  "Substituted variables not removed from the rule, cannot throw "
+            ++ "substitution away."
+            )
+  where
+    subst = Substitution.toMap substitution
+    finalClaim = substitute subst claim
+    substitutedVariables = Substitution.variables substitution
+
+-- | Is the rule free of the given variables?
+isFreeOf
+    :: ClaimPattern
+    -> Set.Set (SomeVariable RewritingVariableName)
+    -> Bool
+isFreeOf rule =
+    Set.disjoint
+    $ FreeVariables.toSet
+    $ freeVariables rule
+
+-- TODO(Ana): move this to Internal.TermLike?
+-- | Extracts all top level existential quantifications.
+termToExistentials
+    :: TermLike RewritingVariableName
+    -> [ElementVariable RewritingVariableName]
+termToExistentials (TermLike.Exists_ _ v term) =
+    v : termToExistentials term
+termToExistentials _ = []
+
+-- | One-Path-Claim claim pattern.
+newtype OnePathRule =
+    OnePathRule { getOnePathRule :: ClaimPattern }
+    deriving (Eq, GHC.Generic, Ord, Show)
+
+instance NFData OnePathRule
+
+instance SOP.Generic OnePathRule
+
+instance SOP.HasDatatypeInfo OnePathRule
+
+instance Debug OnePathRule
+
+instance Diff OnePathRule
+
+-- | Converts a 'OnePathRule' into its term representation.
+-- This is intended to be used only in unparsing situations,
+-- as some of the variable information related to the
+-- rewriting algorithm is lost.
+onePathRuleToTerm :: OnePathRule -> TermLike VariableName
+onePathRuleToTerm (OnePathRule claimPattern') =
+    claimPatternToTerm TermLike.WEF claimPattern'
+
+instance Unparse OnePathRule where
+    unparse claimPattern' =
+        unparse $ onePathRuleToTerm claimPattern'
+    unparse2 claimPattern' =
+        unparse2 $ onePathRuleToTerm claimPattern'
+
+instance TopBottom OnePathRule where
+    isTop _ = False
+    isBottom _ = False
+
+instance From OnePathRule Attribute.SourceLocation where
+    from = Attribute.sourceLocation . attributes . getOnePathRule
+
+instance From OnePathRule Attribute.Label where
+    from = Attribute.label . attributes . getOnePathRule
+
+instance From OnePathRule Attribute.RuleIndex where
+    from = Attribute.identifier . attributes . getOnePathRule
+
+instance From OnePathRule Attribute.Trusted where
+    from = Attribute.trusted . attributes . getOnePathRule
+
+-- | All-Path-Claim claim pattern.
+newtype AllPathRule =
+    AllPathRule { getAllPathRule :: ClaimPattern }
+    deriving (Eq, GHC.Generic, Ord, Show)
+
+instance NFData AllPathRule
+
+instance SOP.Generic AllPathRule
+
+instance SOP.HasDatatypeInfo AllPathRule
+
+instance Debug AllPathRule
+
+instance Diff AllPathRule
+
+instance Unparse AllPathRule where
+    unparse claimPattern' =
+        unparse $ allPathRuleToTerm claimPattern'
+    unparse2 claimPattern' =
+        unparse2 $ allPathRuleToTerm claimPattern'
+
+instance TopBottom AllPathRule where
+    isTop _ = False
+    isBottom _ = False
+
+instance From AllPathRule Attribute.SourceLocation where
+    from = Attribute.sourceLocation . attributes . getAllPathRule
+
+instance From AllPathRule Attribute.Label where
+    from = Attribute.label . attributes . getAllPathRule
+
+instance From AllPathRule Attribute.RuleIndex where
+    from = Attribute.identifier . attributes . getAllPathRule
+
+instance From AllPathRule Attribute.Trusted where
+    from = Attribute.trusted . attributes . getAllPathRule
+
+-- | Converts an 'AllPathRule' into its term representation.
+-- This is intended to be used only in unparsing situations,
+-- as some of the variable information related to the
+-- rewriting algorithm is lost.
+allPathRuleToTerm :: AllPathRule -> TermLike VariableName
+allPathRuleToTerm (AllPathRule claimPattern') =
+    claimPatternToTerm TermLike.WAF claimPattern'
+
+-- | Unified One-Path and All-Path claim pattern.
+data ReachabilityRule
+    = OnePath !OnePathRule
+    | AllPath !AllPathRule
+    deriving (Eq, GHC.Generic, Ord, Show)
+
+instance NFData ReachabilityRule
+
+instance SOP.Generic ReachabilityRule
+
+instance SOP.HasDatatypeInfo ReachabilityRule
+
+instance Debug ReachabilityRule
+
+instance Diff ReachabilityRule
+
+instance Unparse ReachabilityRule where
+    unparse (OnePath rule) = unparse rule
+    unparse (AllPath rule) = unparse rule
+    unparse2 (AllPath rule) = unparse2 rule
+    unparse2 (OnePath rule) = unparse2 rule
+
+instance TopBottom ReachabilityRule where
+    isTop _ = False
+    isBottom _ = False
+
+instance Pretty ReachabilityRule where
+    pretty (OnePath (OnePathRule rule)) =
+        Pretty.vsep ["One-Path reachability rule:", Pretty.pretty rule]
+    pretty (AllPath (AllPathRule rule)) =
+        Pretty.vsep ["All-Path reachability rule:", Pretty.pretty rule]
+
+instance From ReachabilityRule Attribute.SourceLocation where
+    from (OnePath onePathRule) = from onePathRule
+    from (AllPath allPathRule) = from allPathRule
+
+instance From ReachabilityRule Attribute.Label where
+    from (OnePath onePathRule) = from onePathRule
+    from (AllPath allPathRule) = from allPathRule
+
+instance From ReachabilityRule Attribute.RuleIndex where
+    from (OnePath onePathRule) = from onePathRule
+    from (AllPath allPathRule) = from allPathRule
+
+instance From ReachabilityRule Attribute.Trusted where
+    from (OnePath onePathRule) = from onePathRule
+    from (AllPath allPathRule) = from allPathRule
+
+toSentence :: ReachabilityRule -> Verified.Sentence
+toSentence rule =
+    Syntax.SentenceClaimSentence $ Syntax.SentenceClaim Syntax.SentenceAxiom
+        { sentenceAxiomParameters = []
+        , sentenceAxiomPattern    = patt
+        , sentenceAxiomAttributes = Default.def
+        }
+  where
+    patt = case rule of
+        OnePath rule' -> onePathRuleToTerm rule'
+        AllPath rule' -> allPathRuleToTerm rule'
diff --git a/kore/src/Kore/Step/Rule.hs b/kore/src/Kore/Step/Rule.hs
index 0b32273373..11e43d0b73 100644
--- a/kore/src/Kore/Step/Rule.hs
+++ b/kore/src/Kore/Step/Rule.hs
@@ -52,13 +52,22 @@ import Kore.IndexedModule.IndexedModule
 import Kore.Internal.Alias
     ( Alias (..)
     )
+import qualified Kore.Internal.OrPattern as OrPattern
+import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.Symbol as Internal.Symbol
+import Kore.Internal.TermLike
+    ( weakAlwaysFinally
+    , weakExistsFinally
+    )
 import qualified Kore.Internal.TermLike as TermLike
 import Kore.Internal.Variable
     ( InternalVariable
     , VariableName
     )
+import Kore.Rewriting.RewritingVariable
+    ( mkRuleVariable
+    )
 import Kore.Sort
     ( Sort (..)
     , SortVariable (SortVariable)
@@ -66,22 +75,25 @@ import Kore.Sort
 import qualified Kore.Step.AntiLeft as AntiLeft
     ( parse
     )
-import Kore.Step.RulePattern
+import Kore.Step.ClaimPattern
     ( AllPathRule (..)
-    , ImplicationRule (..)
+    , ClaimPattern (ClaimPattern)
     , OnePathRule (..)
+    , allPathRuleToTerm
+    , onePathRuleToTerm
+    )
+import qualified Kore.Step.ClaimPattern as ClaimPattern
+import Kore.Step.RulePattern
+    ( ImplicationRule (..)
     , RewriteRule (..)
     , RulePattern (..)
     , allPathGlobally
-    , allPathRuleToTerm
     , implicationRuleToTerm
     , injectTermIntoRHS
-    , onePathRuleToTerm
     , rewriteRuleToTerm
     , termToRHS
-    , weakAlwaysFinally
-    , weakExistsFinally
     )
+import qualified Kore.Step.RulePattern as OLD
 import Kore.Step.Simplification.ExpandAlias
     ( substituteInAlias
     )
@@ -102,12 +114,22 @@ newtype AxiomPatternError = AxiomPatternError ()
 
 instance NFData AxiomPatternError
 
+reachabilityModalityToConstructor
+    :: Alias (TermLike.TermLike VariableName)
+    -> Maybe (ClaimPattern -> QualifiedAxiomPattern VariableName)
+reachabilityModalityToConstructor patternHead
+    | headName == weakExistsFinally = Just $ OnePathClaimPatternNEW . OnePathRule
+    | headName == weakAlwaysFinally = Just $ AllPathClaimPatternNEW . AllPathRule
+    | otherwise = Nothing
+  where
+    headName = getId (aliasConstructor patternHead)
+
 qualifiedAxiomOpToConstructor
     :: Alias (TermLike.TermLike VariableName)
     -> Maybe (RulePattern VariableName -> QualifiedAxiomPattern VariableName)
 qualifiedAxiomOpToConstructor patternHead
-    | headName == weakExistsFinally = Just $ OnePathClaimPattern . OnePathRule
-    | headName == weakAlwaysFinally = Just $ AllPathClaimPattern . AllPathRule
+    | headName == weakExistsFinally = Just $ OnePathClaimPattern . OLD.OnePathRule
+    | headName == weakAlwaysFinally = Just $ AllPathClaimPattern . OLD.AllPathRule
     | otherwise = Nothing
   where
     headName = getId (aliasConstructor patternHead)
@@ -117,8 +139,10 @@ from function axioms (used for functional simplification).
 --}
 data QualifiedAxiomPattern variable
     = RewriteAxiomPattern (RewriteRule variable)
-    | OnePathClaimPattern OnePathRule
-    | AllPathClaimPattern AllPathRule
+    | OnePathClaimPattern OLD.OnePathRule
+    | AllPathClaimPattern OLD.AllPathRule
+    | OnePathClaimPatternNEW OnePathRule
+    | AllPathClaimPatternNEW AllPathRule
     | ImplicationAxiomPattern (ImplicationRule variable)
     deriving (Eq, GHC.Generic, Ord, Show)
     -- TODO(virgil): Rename the above since it applies to all sorts of axioms,
@@ -312,7 +336,7 @@ termToAxiomPattern
     -> Either (Error AxiomPatternError) (QualifiedAxiomPattern VariableName)
 termToAxiomPattern attributes pat =
     case pat of
-        -- Reachability claims
+        -- OLD: Reachability claims
         TermLike.Implies_ _
             (TermLike.And_ _ requires lhs)
             (TermLike.ApplyAlias_ op [rhs])
@@ -324,6 +348,23 @@ termToAxiomPattern attributes pat =
                 , rhs = termToRHS rhs
                 , attributes
                 }
+        -- NEW: Reachability claims
+        TermLike.Implies_ _
+            (TermLike.And_ _ requires lhs)
+            (TermLike.ApplyAlias_ op [rhs])
+          | Just constructor <- reachabilityModalityToConstructor op ->
+            let rhs' = TermLike.mapVariables (pure mkRuleVariable) rhs
+                attributes' = Attribute.mapAxiomVariables (pure mkRuleVariable) attributes
+             in pure $ constructor ClaimPattern
+                { ClaimPattern.left =
+                    Pattern.fromTermAndPredicate
+                        lhs
+                        (Predicate.wrapPredicate requires)
+                    & Pattern.mapVariables (pure mkRuleVariable)
+                , ClaimPattern.right = OrPattern.parseFromTermLike rhs'
+                , ClaimPattern.existentials = ClaimPattern.termToExistentials rhs'
+                , ClaimPattern.attributes = attributes'
+                }
         TermLike.Forall_ _ _ child -> termToAxiomPattern attributes child
         -- implication axioms:
         -- init -> modal_op ( prop )
@@ -363,10 +404,13 @@ axiomPatternToTerm
     -> TermLike.TermLike VariableName
 axiomPatternToTerm = \case
     RewriteAxiomPattern rule -> rewriteRuleToTerm rule
-    OnePathClaimPattern rule -> onePathRuleToTerm rule
-    AllPathClaimPattern rule -> allPathRuleToTerm rule
+    OnePathClaimPattern rule -> OLD.onePathRuleToTerm rule
+    AllPathClaimPattern rule -> OLD.allPathRuleToTerm rule
+    OnePathClaimPatternNEW rule -> onePathRuleToTerm rule
+    AllPathClaimPatternNEW rule -> allPathRuleToTerm rule
     ImplicationAxiomPattern rule -> implicationRuleToTerm rule
 
+-- TODO(Ana): are these three functions used anywhere anymore?
 {- | Construct a 'VerifiedKoreSentence' corresponding to 'RewriteRule'.
 
 The requires clause must be a predicate, i.e. it can occur in any sort.
diff --git a/kore/src/Kore/Step/Rule/Expand.hs b/kore/src/Kore/Step/Rule/Expand.hs
index 9612b109aa..a0725ad991 100644
--- a/kore/src/Kore/Step/Rule/Expand.hs
+++ b/kore/src/Kore/Step/Rule/Expand.hs
@@ -12,12 +12,12 @@ import Prelude.Kore
 import Control.Lens
     ( (%=)
     )
-import qualified Control.Monad as Monad
 import Control.Monad.State.Strict
     ( State
-    , execState
+    , evalState
     )
 import qualified Control.Monad.State.Strict as State
+import qualified Data.Bifunctor as Bifunctor
 import Data.Generics.Product
     ( field
     )
@@ -46,19 +46,29 @@ import Kore.IndexedModule.MetadataTools
     ( SmtMetadataTools
     , findSortConstructors
     )
+import qualified Kore.Internal.Condition as Condition
+import qualified Kore.Internal.OrPattern as OrPattern
+import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makeAndPredicate
     )
 import qualified Kore.Internal.Predicate as Predicate
+import Kore.Internal.Substitution
+    ( Substitution
+    )
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
-    ( TermLike
+    ( InternalVariable
+    , TermLike
     , mkApplySymbol
     , mkElemVar
     )
 import qualified Kore.Internal.TermLike as TermLike
     ( substitute
     )
+import Kore.Rewriting.RewritingVariable
+    ( RewritingVariableName
+    )
 import Kore.Sort
     ( Sort (..)
     , SortActual (SortActual)
@@ -67,13 +77,17 @@ import qualified Kore.Sort as Sort.DoNotUse
 import qualified Kore.Step.AntiLeft as AntiLeft
     ( substitute
     )
-import Kore.Step.RulePattern
+import Kore.Step.ClaimPattern
     ( AllPathRule (..)
+    , ClaimPattern (..)
     , OnePathRule (..)
     , ReachabilityRule (..)
-    , RulePattern (RulePattern)
+    , freeVariablesLeft
     )
-import qualified Kore.Step.RulePattern as RulePattern
+import Kore.Step.RulePattern
+    ( RulePattern (RulePattern)
+    )
+import qualified Kore.Step.RulePattern as OLD
 import Kore.Syntax.Variable
 import Kore.Variables.Fresh
     ( refreshVariable
@@ -97,8 +111,8 @@ instance ExpandSingleConstructors (RulePattern VariableName) where
         rule@(RulePattern _ _ _ _ _)
       = case rule of
         RulePattern
-            {left, antiLeft, requires
-            , rhs = RulePattern.RHS {existentials, right, ensures}
+            { left, antiLeft, requires
+            , rhs = OLD.RHS {existentials, right, ensures}
             } ->
             let leftVariables :: [ElementVariable VariableName]
                 leftVariables =
@@ -131,20 +145,96 @@ instance ExpandSingleConstructors (RulePattern VariableName) where
                         (Map.toList expansion)
                 subst = Map.mapKeys variableName expansion
             in rule
-                { RulePattern.left = TermLike.substitute subst left
-                , RulePattern.antiLeft =
+                { OLD.left = TermLike.substitute subst left
+                , OLD.antiLeft =
                     AntiLeft.substitute subst <$> antiLeft
-                , RulePattern.requires =
+                , OLD.requires =
                     makeAndPredicate
                         (Predicate.substitute subst requires)
                         substitutionPredicate
-                , RulePattern.rhs = RulePattern.RHS
+                , OLD.rhs = OLD.RHS
                     { existentials
                     , right = TermLike.substitute subst right
                     , ensures = Predicate.substitute subst ensures
                     }
                 }
 
+instance ExpandSingleConstructors OLD.OnePathRule where
+    expandSingleConstructors tools =
+        OLD.OnePathRule . expandSingleConstructors tools . OLD.getOnePathRule
+
+instance ExpandSingleConstructors OLD.AllPathRule where
+    expandSingleConstructors tools =
+        OLD.AllPathRule . expandSingleConstructors tools . OLD.getAllPathRule
+
+instance ExpandSingleConstructors OLD.ReachabilityRule where
+    expandSingleConstructors tools (OLD.OnePath rule) =
+        OLD.OnePath
+        . OLD.OnePathRule
+        . expandSingleConstructors tools
+        . OLD.getOnePathRule
+        $ rule
+    expandSingleConstructors tools (OLD.AllPath rule) =
+        OLD.AllPath
+        . OLD.AllPathRule
+        . expandSingleConstructors tools
+        . OLD.getAllPathRule
+        $ rule
+
+instance ExpandSingleConstructors ClaimPattern where
+    expandSingleConstructors
+        metadataTools
+        rule@(ClaimPattern _ _ _ _)
+      = case rule of
+        ClaimPattern
+            { left
+            , existentials
+            , right
+            } ->
+            let leftElementVariables
+                    :: [ElementVariable RewritingVariableName]
+                leftElementVariables =
+                    extractFreeElementVariables
+                    . freeVariablesLeft
+                    $ rule
+                freeElementVariables
+                    :: [ElementVariable RewritingVariableName]
+                freeElementVariables =
+                    extractFreeElementVariables
+                    . freeVariables
+                    $ rule
+                allElementVariableNames
+                    :: Set (ElementVariableName RewritingVariableName)
+                allElementVariableNames =
+                    variableName <$> freeElementVariables <> existentials
+                    & Set.fromList
+                expansion
+                    ::  Map.Map
+                            (SomeVariable RewritingVariableName)
+                            (TermLike RewritingVariableName)
+                expansion =
+                    expandVariables
+                        metadataTools
+                        leftElementVariables
+                        allElementVariableNames
+                substitutionPredicate =
+                    Substitution.toPredicate
+                    . from @(Map _ _) @(Substitution _)
+                    $ expansion
+                subst = Map.mapKeys variableName expansion
+            in rule
+                { left =
+                    Pattern.andCondition
+                        (Pattern.substitute subst left)
+                        (Condition.fromPredicate substitutionPredicate)
+                , existentials
+                , right = OrPattern.substitute subst right
+                }
+      where
+        extractFreeElementVariables =
+            mapMaybe retractElementVariable
+            . FreeVariables.toList
+
 instance ExpandSingleConstructors OnePathRule where
     expandSingleConstructors tools =
         OnePathRule . expandSingleConstructors tools . getOnePathRule
@@ -167,45 +257,52 @@ instance ExpandSingleConstructors ReachabilityRule where
         . getAllPathRule
         $ rule
 
-data Expansion =
-    Expansion
-    { substitution :: !(Map (SomeVariable VariableName) (TermLike VariableName))
-    , stale :: !(Set (ElementVariableName VariableName))
-    }
+newtype Expansion variable =
+    Expansion { stale :: Set (ElementVariableName variable) }
     deriving (GHC.Generic)
 
-type Expander = State Expansion
+type Expander variable = State (Expansion variable)
 
 expandVariables
-    :: SmtMetadataTools attributes
-    -> [ElementVariable VariableName]
-    -> Set (ElementVariableName VariableName)
-    -> Map (SomeVariable VariableName) (TermLike VariableName)
+    :: forall variable attributes
+    .  InternalVariable variable
+    => SmtMetadataTools attributes
+    -> [ElementVariable variable]
+    -> Set (ElementVariableName variable)
+    -> Map (SomeVariable variable) (TermLike variable)
 expandVariables metadataTools variables stale =
-    traverse expandAddVariable variables
-    & flip execState Expansion { substitution = Map.empty, stale }
-    & substitution
+    wither expandAddVariable variables
+    & flip evalState Expansion { stale }
+    & (map . Bifunctor.first) inject
+    & Map.fromList
   where
-    expandAddVariable :: ElementVariable VariableName -> Expander ()
+    expandAddVariable
+        ::  ElementVariable variable
+        ->  Expander variable
+                (Maybe (ElementVariable variable, TermLike variable))
     expandAddVariable variable = do
         term <- expandVariable metadataTools variable
-        Monad.unless
-            (mkElemVar variable == term)
-            (field @"substitution" %= Map.insert (inject variable) term)
+        if mkElemVar variable == term
+            then return Nothing
+            else return $ Just (variable, term)
 
 expandVariable
-    :: SmtMetadataTools attributes
-    -> ElementVariable VariableName
-    -> Expander (TermLike VariableName)
+    :: forall variable attributes
+    .  InternalVariable variable
+    => SmtMetadataTools attributes
+    -> ElementVariable variable
+    -> Expander variable (TermLike variable)
 expandVariable metadataTools variable@Variable { variableSort } =
     expandSort metadataTools variable UseDirectly variableSort
 
 expandSort
-    :: SmtMetadataTools attributes
-    -> ElementVariable VariableName
+    :: forall variable attributes
+    .  InternalVariable variable
+    => SmtMetadataTools attributes
+    -> ElementVariable variable
     -> VariableUsage
     -> Sort
-    -> Expander (TermLike VariableName)
+    -> Expander variable (TermLike variable)
 expandSort metadataTools defaultVariable variableUsage sort =
     case findSingleConstructor sort of
         Just constructor ->
@@ -224,10 +321,12 @@ expandSort metadataTools defaultVariable variableUsage sort =
             _ -> Nothing
 
 expandConstructor
-    :: SmtMetadataTools attributes
-    -> ElementVariable VariableName
+    :: forall variable attributes
+    .  InternalVariable variable
+    => SmtMetadataTools attributes
+    -> ElementVariable variable
     -> Attribute.Constructors.Constructor
-    -> Expander (TermLike VariableName)
+    -> Expander variable (TermLike variable)
 expandConstructor
     metadataTools
     defaultVariable
@@ -235,7 +334,7 @@ expandConstructor
   =
     mkApplySymbol symbol <$> traverse expandChildSort sorts
   where
-    expandChildSort :: Sort -> Expander (TermLike VariableName)
+    expandChildSort :: Sort -> Expander variable (TermLike variable)
     expandChildSort = expandSort metadataTools defaultVariable UseAsPrototype
 
 {-| Context: we have a TermLike that contains a variables, and we
@@ -261,11 +360,13 @@ data VariableUsage =
     -- variable, so we need to generate a new one based on it.
 
 maybeNewVariable
-    :: HasCallStack
-    => ElementVariable VariableName
+    :: forall variable
+    .  InternalVariable variable
+    => HasCallStack
+    => ElementVariable variable
     -> Sort
     -> VariableUsage
-    -> Expander (TermLike VariableName)
+    -> Expander variable (TermLike variable)
 maybeNewVariable
     variable@Variable { variableSort }
     sort
diff --git a/kore/src/Kore/Step/Rule/Simplify.hs b/kore/src/Kore/Step/Rule/Simplify.hs
index 870c2fad31..39b9b345c7 100644
--- a/kore/src/Kore/Step/Rule/Simplify.hs
+++ b/kore/src/Kore/Step/Rule/Simplify.hs
@@ -14,6 +14,7 @@ import Control.Monad
     ( (>=>)
     )
 
+import qualified Kore.Internal.Condition as Condition
 import Kore.Internal.Conditional
     ( Conditional (Conditional)
     )
@@ -24,6 +25,7 @@ import qualified Kore.Internal.MultiAnd as MultiAnd
     ( make
     )
 import qualified Kore.Internal.MultiOr as MultiOr
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -37,13 +39,21 @@ import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.TermLike
     ( termLikeSort
     )
-import Kore.Step.RulePattern
+import Kore.Rewriting.RewritingVariable
+    ( RewritingVariableName
+    )
+import Kore.Step.ClaimPattern
     ( AllPathRule (..)
+    , ClaimPattern (ClaimPattern)
     , OnePathRule (..)
     , ReachabilityRule (..)
-    , RewriteRule (..)
+    )
+import qualified Kore.Step.ClaimPattern as ClaimPattern
+import Kore.Step.RulePattern
+    ( RewriteRule (..)
     , RulePattern (RulePattern)
     )
+import qualified Kore.Step.RulePattern as OLD
 import qualified Kore.Step.RulePattern as RulePattern
     ( RulePattern (..)
     , applySubstitution
@@ -63,7 +73,7 @@ import Logic
     )
 import qualified Logic
 
--- | Simplifies the left-hand-side of a rule/claim
+-- | Simplifies the left-hand-side of a rewrite rule (claim or axiom)
 class SimplifyRuleLHS rule where
     simplifyRuleLhs
         :: forall simplifier
@@ -101,10 +111,55 @@ instance InternalVariable variable => SimplifyRuleLHS (RulePattern variable)
                         $ makeAndPredicate predicate requires'
                     }
 
+instance SimplifyRuleLHS ClaimPattern
+  where
+    simplifyRuleLhs rule@(ClaimPattern _ _ _ _) = do
+        simplifiedTerms <-
+            Pattern.simplifyTopConfiguration left
+        fullySimplified <-
+            SMT.Evaluator.filterMultiOr simplifiedTerms
+        let rules =
+                setRuleLeft rule
+                <$> OrPattern.toPatterns fullySimplified
+        return (MultiAnd.make rules)
+      where
+        ClaimPattern { left } = rule
+
+        setRuleLeft
+            :: ClaimPattern
+            -> Pattern RewritingVariableName
+            -> ClaimPattern
+        setRuleLeft
+            claimPattern@ClaimPattern { left = left' }
+            patt@Conditional { substitution }
+          =
+            ClaimPattern.applySubstitution
+                substitution
+                claimPattern
+                    { ClaimPattern.left =
+                        Condition.andCondition
+                            patt
+                            (Condition.eraseConditionalTerm left')
+                    }
+
 instance SimplifyRuleLHS (RewriteRule VariableName) where
     simplifyRuleLhs =
         fmap (fmap RewriteRule) . simplifyRuleLhs . getRewriteRule
 
+instance SimplifyRuleLHS OLD.OnePathRule where
+    simplifyRuleLhs =
+        fmap (fmap OLD.OnePathRule) . simplifyClaimRuleOLD . OLD.getOnePathRule
+
+instance SimplifyRuleLHS OLD.AllPathRule where
+    simplifyRuleLhs =
+        fmap (fmap OLD.AllPathRule) . simplifyClaimRuleOLD . OLD.getAllPathRule
+
+instance SimplifyRuleLHS OLD.ReachabilityRule where
+    simplifyRuleLhs (OLD.OnePath rule) =
+        (fmap . fmap) OLD.OnePath $ simplifyRuleLhs rule
+    simplifyRuleLhs (OLD.AllPath rule) =
+        (fmap . fmap) OLD.AllPath $ simplifyRuleLhs rule
+
 instance SimplifyRuleLHS OnePathRule where
     simplifyRuleLhs =
         fmap (fmap OnePathRule) . simplifyClaimRule . getOnePathRule
@@ -119,13 +174,13 @@ instance SimplifyRuleLHS ReachabilityRule where
     simplifyRuleLhs (AllPath rule) =
         (fmap . fmap) AllPath $ simplifyRuleLhs rule
 
-simplifyClaimRule
+simplifyClaimRuleOLD
     :: forall simplifier variable
     .  MonadSimplify simplifier
     => InternalVariable variable
     => RulePattern variable
     -> simplifier (MultiAnd (RulePattern variable))
-simplifyClaimRule =
+simplifyClaimRuleOLD =
     fmap MultiAnd.make . Logic.observeAllT . worker
   where
     simplify, filterWithSolver
@@ -148,3 +203,33 @@ simplifyClaimRule =
             & Lens.set RulePattern.leftPattern lhs'
             & RulePattern.applySubstitution substitution
             & return
+
+simplifyClaimRule
+    :: forall simplifier
+    .  MonadSimplify simplifier
+    => ClaimPattern
+    -> simplifier (MultiAnd ClaimPattern)
+simplifyClaimRule =
+    fmap MultiAnd.make . Logic.observeAllT . worker
+  where
+    simplify, filterWithSolver
+        :: Pattern RewritingVariableName
+        -> LogicT simplifier (Pattern RewritingVariableName)
+    simplify =
+        (return . Pattern.requireDefined)
+        >=> Pattern.simplifyTopConfiguration
+        >=> Logic.scatter
+        >=> filterWithSolver
+    filterWithSolver = SMT.Evaluator.filterBranch
+
+    worker :: ClaimPattern -> LogicT simplifier ClaimPattern
+    worker claimPattern = do
+        let lhs = ClaimPattern.left claimPattern
+        simplified <- simplify lhs
+        let substitution = Pattern.substitution simplified
+            lhs' = simplified { Pattern.substitution = mempty }
+        claimPattern
+            { ClaimPattern.left = lhs'
+            }
+            & ClaimPattern.applySubstitution substitution
+            & return
diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs
index 49adf7ef3c..27af9a973c 100644
--- a/kore/src/Kore/Step/RulePattern.hs
+++ b/kore/src/Kore/Step/RulePattern.hs
@@ -8,10 +8,10 @@ License     : NCSA
 module Kore.Step.RulePattern
     ( RulePattern (..)
     , RewriteRule (..)
+    , ImplicationRule (..)
     , OnePathRule (..)
     , AllPathRule (..)
     , ReachabilityRule (..)
-    , ImplicationRule (..)
     , RHS (..)
     , HasAttributes (..)
     , ToRulePattern (..)
@@ -197,7 +197,7 @@ topExistsToImplicitForall avoid' RHS { existentials, right, ensures } =
             (Set.fromList $ mkSomeVariable <$> existentials)
     subst = TermLike.mkVar <$> rename
 
-{- | Normal rewriting axioms and claims
+{- | Normal rewriting axioms
 
  -}
 data RulePattern variable = RulePattern
@@ -596,7 +596,6 @@ instance
     unparse = unparse . implicationRuleToTerm
     unparse2 = unparse2 . implicationRuleToTerm
 
-
 {-  | One-Path-Claim rule pattern.
 -}
 newtype OnePathRule =
diff --git a/kore/test/Test/Kore/Step/Rule.hs b/kore/test/Test/Kore/Step/Rule.hs
index 5713f620c0..3dd29c2ef3 100644
--- a/kore/test/Test/Kore/Step/Rule.hs
+++ b/kore/test/Test/Kore/Step/Rule.hs
@@ -36,7 +36,10 @@ import Kore.Internal.ApplicationSorts
 import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.TermLike
 import Kore.Step.Rule
-import Kore.Step.RulePattern
+import Kore.Step.RulePattern hiding
+    ( wAF
+    , wEF
+    )
 import Kore.Syntax.Definition hiding
     ( Alias (..)
     )
@@ -246,12 +249,11 @@ test_patternToAxiomPatternAndBack =
     testGroup
         "pattern to axiomPattern to pattern"
         [
-             let op = wEF $ termLikeSort leftP
-                 initialPattern = mkImplies
+             let initialPattern = mkImplies
                     (mkAnd (Predicate.unwrapPredicate requiresP) leftP)
-                    (mkApplyAlias
-                        op
-                        [mkAnd (Predicate.unwrapPredicate ensuresP) rightP]
+                    (applyModality
+                       WEF
+                        (mkAnd (Predicate.unwrapPredicate ensuresP) rightP)
                     )
             in
                 testCase "Reachability claim wEF" $
@@ -259,12 +261,11 @@ test_patternToAxiomPatternAndBack =
                         (Right initialPattern)
                         (perhapsFinalPattern def initialPattern)
         ,
-            let op = wAF $ termLikeSort leftP
-                initialPattern = mkImplies
+            let initialPattern = mkImplies
                     (mkAnd (Predicate.unwrapPredicate requiresP) leftP)
-                    (mkApplyAlias
-                        op
-                        [mkAnd (Predicate.unwrapPredicate ensuresP) rightP]
+                    (applyModality
+                        WAF
+                        (mkAnd (Predicate.unwrapPredicate ensuresP) rightP)
                     )
             in
                 testCase "Reachability claim wAF" $
diff --git a/kore/test/Test/Kore/Step/Rule/Common.hs b/kore/test/Test/Kore/Step/Rule/Common.hs
new file mode 100644
index 0000000000..0a1e2e659c
--- /dev/null
+++ b/kore/test/Test/Kore/Step/Rule/Common.hs
@@ -0,0 +1,113 @@
+module Test.Kore.Step.Rule.Common
+    ( Pair (..)
+    , RuleBase (..)
+    ) where
+
+import Prelude.Kore
+
+import qualified Data.Default as Default
+
+import qualified Kore.Internal.OrPattern as OrPattern
+import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.Predicate
+    ( Predicate
+    , makeTruePredicate
+    , makeTruePredicate_
+    )
+import qualified Kore.Internal.Predicate as Predicate
+import Kore.Internal.TermLike
+    ( TermLike
+    , VariableName
+    )
+import qualified Kore.Internal.TermLike as TermLike
+import Kore.Rewriting.RewritingVariable
+    ( mkRuleVariable
+    )
+import Kore.Step.ClaimPattern
+    ( OnePathRule (..)
+    , claimPattern
+    )
+import Kore.Step.RulePattern
+    ( RHS (RHS)
+    , RewriteRule (RewriteRule)
+    , RulePattern (RulePattern)
+    )
+import qualified Kore.Step.RulePattern as OLD
+
+newtype Pair variable = Pair (TermLike variable, Predicate variable)
+
+class RuleBase base rule where
+    rewritesTo :: base VariableName -> base VariableName -> rule
+    rewritesToWithSort :: base VariableName -> base VariableName -> rule
+
+instance RuleBase Pair OnePathRule where
+    Pair (t1, p1) `rewritesTo` Pair (t2, p2) =
+        OnePathRule
+        $ claimPattern
+            (Pattern.fromTermAndPredicate t1' p1')
+            (Pattern.fromTermAndPredicate t2' p2' & OrPattern.fromPattern)
+            []
+      where
+        t1' = TermLike.mapVariables (pure mkRuleVariable) t1
+        t2' = TermLike.mapVariables (pure mkRuleVariable) t2
+        p1' = Predicate.mapVariables (pure mkRuleVariable) p1
+        p2' = Predicate.mapVariables (pure mkRuleVariable) p2
+
+    rewritesToWithSort = rewritesTo
+
+instance RuleBase TermLike OnePathRule where
+    t1 `rewritesTo` t2 =
+        Pair (t1, makeTruePredicate_)
+        `rewritesTo` Pair (t2, makeTruePredicate_)
+
+    t1 `rewritesToWithSort` t2 =
+        Pair (t1, makeTruePredicate (TermLike.termLikeSort t1))
+        `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2))
+
+instance RuleBase Pair (RewriteRule VariableName) where
+    Pair (t1, p1) `rewritesTo` Pair (t2, p2) =
+        RewriteRule RulePattern
+            { OLD.left = t1
+            , OLD.requires = p1
+            , OLD.rhs = RHS
+                { OLD.existentials = []
+                , OLD.right = t2
+                , OLD.ensures = p2
+                }
+            , OLD.antiLeft = Nothing
+            , OLD.attributes = Default.def
+            }
+    rewritesToWithSort = rewritesTo
+
+instance RuleBase TermLike (RewriteRule VariableName) where
+    t1 `rewritesTo` t2 =
+        Pair (t1, makeTruePredicate_)
+        `rewritesTo` Pair (t2, makeTruePredicate_)
+
+    t1 `rewritesToWithSort` t2 =
+        Pair (t1, makeTruePredicate (TermLike.termLikeSort t1))
+        `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2))
+
+instance RuleBase Pair OLD.OnePathRule where
+    Pair (t1, p1) `rewritesTo` Pair (t2, p2) =
+        OLD.OnePathRule RulePattern
+            { OLD.left = t1
+            , OLD.requires = p1
+            , OLD.rhs = RHS
+                { OLD.existentials = []
+                , OLD.right = t2
+                , OLD.ensures = p2
+                }
+            , OLD.antiLeft = Nothing
+            , OLD.attributes = Default.def
+            }
+    rewritesToWithSort = rewritesTo
+
+instance RuleBase TermLike OLD.OnePathRule where
+    t1 `rewritesTo` t2 =
+        Pair (t1, makeTruePredicate_)
+        `rewritesTo` Pair (t2, makeTruePredicate_)
+
+    t1 `rewritesToWithSort` t2 =
+        Pair (t1, makeTruePredicate (TermLike.termLikeSort t1))
+        `rewritesToWithSort` Pair (t2, makeTruePredicate (TermLike.termLikeSort t2))
diff --git a/kore/test/Test/Kore/Step/Rule/Expand.hs b/kore/test/Test/Kore/Step/Rule/Expand.hs
index 2c27961ae3..d3195acb24 100644
--- a/kore/test/Test/Kore/Step/Rule/Expand.hs
+++ b/kore/test/Test/Kore/Step/Rule/Expand.hs
@@ -1,14 +1,12 @@
 module Test.Kore.Step.Rule.Expand
     ( test_expandRule
+    , test_expandRule_OLD
     ) where
 
 import Prelude.Kore
 
 import Test.Tasty
 
-import Data.Default
-    ( def
-    )
 import Data.Generics.Product
     ( field
     )
@@ -34,8 +32,7 @@ import qualified Kore.IndexedModule.MetadataTools as MetadataTools
     ( MetadataTools (..)
     )
 import Kore.Internal.Predicate
-    ( Predicate
-    , makeEqualsPredicate_
+    ( makeEqualsPredicate_
     , makeTruePredicate_
     )
 import Kore.Internal.Symbol
@@ -50,13 +47,11 @@ import Kore.Internal.TermLike
     , mkApplySymbol
     , mkElemVar
     )
-import Kore.Step.Rule.Expand
-import Kore.Step.RulePattern
-    ( OnePathRule (OnePathRule)
-    , RHS (..)
-    , RulePattern (RulePattern)
+import Kore.Step.ClaimPattern
+    ( OnePathRule
     )
-import qualified Kore.Step.RulePattern as Rule.DoNotUse
+import Kore.Step.Rule.Expand
+import qualified Kore.Step.RulePattern as OLD
 import Kore.Syntax.Id
     ( Id
     )
@@ -66,38 +61,351 @@ import Test.Kore
     ( testId
     )
 import qualified Test.Kore.Step.MockSymbols as Mock
+import Test.Kore.Step.Rule.Common
+    ( Pair (..)
+    , RuleBase
+    )
+import qualified Test.Kore.Step.Rule.Common as Common
 import Test.Kore.With
     ( with
     )
 import Test.Tasty.HUnit.Ext
 
-class OnePathRuleBase base where
-    rewritesTo :: base VariableName -> base VariableName -> OnePathRule
-
-newtype Pair variable = Pair (TermLike variable, Predicate variable)
-
-instance OnePathRuleBase Pair where
-    Pair (t1, p1) `rewritesTo` Pair (t2, p2) =
-        OnePathRule RulePattern
-            { left = t1
-            , requires = p1
-            , rhs = RHS
-                { existentials = []
-                , right = t2
-                , ensures = p2
-                }
-            , antiLeft = Nothing
-            , attributes = def
-            }
-
-instance OnePathRuleBase TermLike where
-    t1 `rewritesTo` t2 =
-        Pair (t1, makeTruePredicate_) `rewritesTo` Pair (t2, makeTruePredicate_)
-
+test_expandRule_OLD :: [TestTree]
+test_expandRule_OLD =
+    [ testCase "Nothing to expand" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools [])
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Nothing to expand without constructors" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [ (Mock.testSortId, noConstructor) ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Nothing to expand with multiple constructors" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSortId
+                            , noConstructor
+                                `with` constructor Mock.aSymbol
+                                `with` constructor Mock.bSymbol
+                            )
+                        ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Expands variable once to constant" $
+        let expected =
+                Pair (Mock.f Mock.a, makeEqualsPredicate_ x Mock.a)
+                `rewritesToOLD`
+                Pair (Mock.g Mock.a, makeTruePredicate_)
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Expands variable once to argument constructor" $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor1 x00TestSort)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor1 x00TestSort)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor1 x00TestSort)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor1Symbol
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands variable twice." $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor1 Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor1 Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor1 Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor1Symbol
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands multiple arguments." $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor2 Mock.a Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor2 Mock.a Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor2 Mock.a Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor2Symbol
+                                    `with` Mock.testSort
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands one of multiple arguments" $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor2a x00TestSort1 Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor2a x00TestSort1 Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor2a x00TestSort1 Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor2aSymbol
+                                    `with` Mock.testSort1
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    ]
 
 test_expandRule :: [TestTree]
 test_expandRule =
     [ testCase "Nothing to expand" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools [])
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Nothing to expand without constructors" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [ (Mock.testSortId, noConstructor) ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Nothing to expand with multiple constructors" $
+        let expected = Mock.f x `rewritesToOLD` Mock.g x
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSortId
+                            , noConstructor
+                                `with` constructor Mock.aSymbol
+                                `with` constructor Mock.bSymbol
+                            )
+                        ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Expands variable once to constant" $
+        let expected =
+                Pair (Mock.f Mock.a, makeEqualsPredicate_ x Mock.a)
+                `rewritesToOLD`
+                Pair (Mock.g Mock.a, makeTruePredicate_)
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.f x `rewritesToOLD` Mock.g x)
+        in assertEqual "" expected actual
+    , testCase "Expands variable once to argument constructor" $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor1 x00TestSort)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor1 x00TestSort)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor1 x00TestSort)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor1Symbol
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands variable twice." $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor1 Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor1 Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor1 Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor1Symbol
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands multiple arguments." $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor2 Mock.a Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor2 Mock.a Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor2 Mock.a Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor2Symbol
+                                    `with` Mock.testSort
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Expands one of multiple arguments" $
+        let expected =
+                Pair
+                    ( Mock.fSort0 (expandableConstructor2a x00TestSort1 Mock.a)
+                    , makeEqualsPredicate_
+                        x0
+                        (expandableConstructor2a x00TestSort1 Mock.a)
+                    )
+                `rewritesToOLD`
+                Pair
+                    ( Mock.gSort0 (expandableConstructor2a x00TestSort1 Mock.a)
+                    , makeTruePredicate_
+                    )
+            actual =
+                expandSingleConstructors
+                    (metadataTools
+                        [   ( Mock.testSort0Id
+                            , noConstructor
+                                `with`
+                                    ( constructor expandableConstructor2aSymbol
+                                    `with` Mock.testSort1
+                                    `with` Mock.testSort
+                                    )
+                            )
+                        ,   ( Mock.testSortId
+                            , noConstructor `with` constructor Mock.aSymbol
+                            )
+                        ]
+                    )
+                    (Mock.fSort0 x0 `rewritesToOLD` Mock.gSort0 x0)
+        in assertEqual "" expected actual
+    , testCase "Nothing to expand" $
         let expected = Mock.f x `rewritesTo` Mock.g x
             actual =
                 expandSingleConstructors
@@ -262,80 +570,107 @@ test_expandRule =
                     (Mock.fSort0 x0 `rewritesTo` Mock.gSort0 x0)
         in assertEqual "" expected actual
     ]
-  where
-    x = mkElemVar Mock.x
-    x0 = mkElemVar Mock.x0
 
-    x00TestSortVar =
-        mkElementVariable (testId "x0") Mock.testSort
-        & Lens.set
-            (field @"variableName" . Lens.mapped . field @"counter")
-            (Just (Element 0))
-    x00TestSort = mkElemVar x00TestSortVar
+rewritesTo
+    :: RuleBase base OnePathRule
+    => base VariableName
+    -> base VariableName
+    -> OnePathRule
+rewritesTo = Common.rewritesTo
+
+rewritesToOLD
+    :: RuleBase base OLD.OnePathRule
+    => base VariableName
+    -> base VariableName
+    -> OLD.OnePathRule
+rewritesToOLD = Common.rewritesTo
+
+x, x0 :: TermLike VariableName
+x = mkElemVar Mock.x
+x0 = mkElemVar Mock.x0
+
+x00TestSortVar :: ElementVariable VariableName
+x00TestSortVar =
+    mkElementVariable (testId "x0") Mock.testSort
+    & Lens.set
+        (field @"variableName" . Lens.mapped . field @"counter")
+        (Just (Element 0))
+
+x00TestSort :: TermLike VariableName
+x00TestSort = mkElemVar x00TestSortVar
+
+x00TestSort1Var :: ElementVariable VariableName
+x00TestSort1Var =
+    mkElementVariable (testId "x0") Mock.testSort1
+    & Lens.set
+        (field @"variableName" . Lens.mapped . field @"counter")
+        (Just (Element 0))
+
+x00TestSort1 :: TermLike VariableName
+x00TestSort1 = mkElemVar x00TestSort1Var
+
+metadataTools
+    :: [(Id, Attribute.Constructors)]
+    -> SmtMetadataTools Attribute.Symbol
+metadataTools sortAndConstructors =
+    Mock.metadataTools
+        { MetadataTools.sortConstructors = Map.fromList sortAndConstructors
+        }
+
+expandableConstructor1Id :: Id
+expandableConstructor1Id = testId "expandableConstructor1"
+
+expandableConstructor1Symbol :: Symbol
+expandableConstructor1Symbol =
+    Mock.symbol expandableConstructor1Id [Mock.testSort] Mock.testSort0
+    & Symbol.functional
+    & Symbol.constructor
+
+expandableConstructor1
+    :: HasCallStack
+    => TermLike VariableName -> TermLike VariableName
+expandableConstructor1 arg =
+    mkApplySymbol expandableConstructor1Symbol [arg]
+
+expandableConstructor2Id :: Id
+expandableConstructor2Id = testId "expandableConstructor2"
 
-    x00TestSort1Var =
-        mkElementVariable (testId "x0") Mock.testSort1
-        & Lens.set
-            (field @"variableName" . Lens.mapped . field @"counter")
-            (Just (Element 0))
-    x00TestSort1 = mkElemVar x00TestSort1Var
+expandableConstructor2Symbol :: Symbol
+expandableConstructor2Symbol =
+    Mock.symbol
+        expandableConstructor2Id
+        [Mock.testSort, Mock.testSort]
+        Mock.testSort0
+    & Symbol.functional
+    & Symbol.constructor
 
-    metadataTools
-        :: [(Id, Attribute.Constructors)]
-        -> SmtMetadataTools Attribute.Symbol
-    metadataTools sortAndConstructors =
-        Mock.metadataTools
-            { MetadataTools.sortConstructors = Map.fromList sortAndConstructors
-            }
+expandableConstructor2
+    :: HasCallStack
+    => TermLike VariableName
+    -> TermLike VariableName
+    -> TermLike VariableName
+expandableConstructor2 arg1 arg2 =
+    mkApplySymbol expandableConstructor2Symbol [arg1, arg2]
 
-    expandableConstructor1Id :: Id
-    expandableConstructor1Id = testId "expandableConstructor1"
-    expandableConstructor1Symbol :: Symbol
-    expandableConstructor1Symbol =
-        Mock.symbol expandableConstructor1Id [Mock.testSort] Mock.testSort0
-        & Symbol.functional
-        & Symbol.constructor
-    expandableConstructor1
-        :: HasCallStack
-        => TermLike VariableName -> TermLike VariableName
-    expandableConstructor1 arg =
-        mkApplySymbol expandableConstructor1Symbol [arg]
+expandableConstructor2aId :: Id
+expandableConstructor2aId = testId "expandableConstructor2a"
 
-    expandableConstructor2Id :: Id
-    expandableConstructor2Id = testId "expandableConstructor2"
-    expandableConstructor2Symbol :: Symbol
-    expandableConstructor2Symbol =
-        Mock.symbol
-            expandableConstructor2Id
-            [Mock.testSort, Mock.testSort]
-            Mock.testSort0
-        & Symbol.functional
-        & Symbol.constructor
-    expandableConstructor2
-        :: HasCallStack
-        => TermLike VariableName
-        -> TermLike VariableName
-        -> TermLike VariableName
-    expandableConstructor2 arg1 arg2 =
-        mkApplySymbol expandableConstructor2Symbol [arg1, arg2]
+expandableConstructor2aSymbol :: Symbol
+expandableConstructor2aSymbol =
+    Mock.symbol
+        expandableConstructor2aId
+        [Mock.testSort1, Mock.testSort]
+        Mock.testSort0
+    & Symbol.functional
+    & Symbol.constructor
 
-    expandableConstructor2aId :: Id
-    expandableConstructor2aId = testId "expandableConstructor2a"
-    expandableConstructor2aSymbol :: Symbol
-    expandableConstructor2aSymbol =
-        Mock.symbol
-            expandableConstructor2aId
-            [Mock.testSort1, Mock.testSort]
-            Mock.testSort0
-        & Symbol.functional
-        & Symbol.constructor
-    expandableConstructor2a
-        :: HasCallStack
-        => TermLike VariableName
-        -> TermLike VariableName
-        -> TermLike VariableName
-    expandableConstructor2a arg1 arg2 =
-        mkApplySymbol expandableConstructor2aSymbol [arg1, arg2]
+expandableConstructor2a
+    :: HasCallStack
+    => TermLike VariableName
+    -> TermLike VariableName
+    -> TermLike VariableName
+expandableConstructor2a arg1 arg2 =
+    mkApplySymbol expandableConstructor2aSymbol [arg1, arg2]
 
 noConstructor :: Attribute.Constructors
 noConstructor = Attribute.Constructors Nothing
diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs
index 89f75c864b..b3b5184847 100644
--- a/kore/test/Test/Kore/Step/Rule/Simplify.hs
+++ b/kore/test/Test/Kore/Step/Rule/Simplify.hs
@@ -1,5 +1,8 @@
 module Test.Kore.Step.Rule.Simplify
-    ( test_simplifyRule
+    ( test_simplifyRule_RewriteRule
+    , test_simplifyRule_OnePathRule
+    , test_simplifyRule_OnePathRuleOLD
+    , test_simplifyClaimRuleOLD
     , test_simplifyClaimRule
     ) where
 
@@ -18,19 +21,20 @@ import Control.Monad.Reader
     )
 import qualified Control.Monad.Reader as Reader
 import qualified Data.Bifunctor as Bifunctor
-import Data.Default
-    ( def
-    )
 import qualified Data.Foldable as Foldable
 import Data.Generics.Product
     ( field
     )
 
+import Kore.Internal.Condition
+    ( Condition
+    )
 import qualified Kore.Internal.Condition as Condition
 import qualified Kore.Internal.MultiAnd as MultiAnd
     ( extractPatterns
     )
 import qualified Kore.Internal.OrPattern as OrPattern
+import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( Predicate
     , makeAndPredicate
@@ -42,7 +46,8 @@ import Kore.Internal.Predicate
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.TermLike
-    ( InternalVariable
+    ( AdjSomeVariableName
+    , InternalVariable
     , TermLike
     , mkAnd
     , mkElemVar
@@ -51,17 +56,25 @@ import Kore.Internal.TermLike
     , termLikeSort
     )
 import qualified Kore.Internal.TermLike as TermLike
+import Kore.Rewriting.RewritingVariable
+    ( RewritingVariableName
+    , getRewritingVariable
+    )
 import Kore.Sort
     ( predicateSort
     )
+import Kore.Step.ClaimPattern
+    ( ClaimPattern
+    , OnePathRule (..)
+    , claimPattern
+    )
 import Kore.Step.Rule.Simplify
 import Kore.Step.RulePattern
-    ( OnePathRule (..)
-    , RHS (..)
-    , RulePattern (RulePattern)
+    ( RewriteRule
+    , RulePattern
     , rulePattern
     )
-import qualified Kore.Step.RulePattern as Rule.DoNotUse
+import qualified Kore.Step.RulePattern as OLD
 import Kore.Step.Simplification.Data
     ( Env (..)
     , runSimplifier
@@ -79,39 +92,179 @@ import Kore.Syntax.Variable
     )
 
 import qualified Test.Kore.Step.MockSymbols as Mock
+import Test.Kore.Step.Rule.Common
+    ( Pair (..)
+    , RuleBase
+    )
+import qualified Test.Kore.Step.Rule.Common as Common
 import Test.SMT
     ( runNoSMT
     )
 import Test.Tasty.HUnit.Ext
 
-class OnePathRuleBase base where
-    rewritesTo :: base VariableName -> base VariableName -> OnePathRule
+test_simplifyRule_RewriteRule :: [TestTree]
+test_simplifyRule_RewriteRule =
+    [ testCase "No simplification needed" $ do
+        let rule = Mock.a `rewritesToWithSortRewriteRule` Mock.cf
+            expected = [rule]
 
-newtype Pair variable = Pair (TermLike variable, Predicate variable)
+        actual <- runSimplifyRule rule
 
-instance OnePathRuleBase Pair where
-    Pair (t1, p1) `rewritesTo` Pair (t2, p2) =
-        OnePathRule RulePattern
-            { left = t1
-            , requires = p1
-            , rhs = RHS
-                { existentials = []
-                , right = t2
-                , ensures = p2
-                }
-            , antiLeft = Nothing
-            , attributes = def
-            }
+        assertEqual "" expected actual
+
+    , testCase "Simplify lhs term" $ do
+        let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.cf]
+
+        actual <- runSimplifyRule
+            (   mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a)
+                `rewritesToWithSortRewriteRule`
+                Mock.cf
+            )
+
+        assertEqual "" expected actual
+
+    , testCase "Does not simplify rhs term" $ do
+        let rule =
+                Mock.a
+                `rewritesToWithSortRewriteRule`
+                mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a)
+            expected = [rule]
+
+        actual <- runSimplifyRule rule
+
+        assertEqual "" expected actual
+
+    , testCase "Substitution in lhs term" $ do
+        let expected = [Mock.a `rewritesToWithSortRewriteRule` Mock.f Mock.b]
+
+        actual <- runSimplifyRule
+            (   mkAnd Mock.a (mkEquals Mock.testSort Mock.b x)
+                `rewritesToWithSortRewriteRule` Mock.f x
+            )
+
+        assertEqual "" expected actual
+
+    , testCase "Does not simplify ensures predicate" $ do
+        let rule =
+                Pair (Mock.a,  makeTruePredicate Mock.testSort)
+                `rewritesToWithSortRewriteRule`
+                Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b)
+            expected = [rule]
+
+        actual <- runSimplifyRule rule
+
+        assertEqual "" expected actual
+
+    , testCase "Splits rule" $ do
+        let expected =
+                [ Mock.a `rewritesToWithSortRewriteRule` Mock.cf
+                , Mock.b `rewritesToWithSortRewriteRule` Mock.cf
+                ]
+
+        actual <- runSimplifyRule
+            (   mkOr Mock.a Mock.b
+                `rewritesToWithSortRewriteRule`
+                Mock.cf
+            )
+
+        assertEqual "" expected actual
+    , testCase "f(x) is always defined" $ do
+        let expected =
+                [ Mock.functional10 x `rewritesToWithSortRewriteRule` Mock.a
+                ]
+
+        actual <- runSimplifyRule
+            (   Pair (Mock.functional10 x, makeTruePredicate Mock.testSort)
+                `rewritesToWithSortRewriteRule`
+                Pair (Mock.a, makeTruePredicate Mock.testSort)
+            )
+
+        assertEqual "" expected actual
+    ]
+  where
+    rewritesToWithSortRewriteRule
+        :: RuleBase base (RewriteRule VariableName)
+        => base VariableName
+        -> base VariableName
+        -> RewriteRule VariableName
+    rewritesToWithSortRewriteRule = Common.rewritesToWithSort
+
+    x = mkElemVar Mock.x
+
+test_simplifyRule_OnePathRuleOLD :: [TestTree]
+test_simplifyRule_OnePathRuleOLD =
+    [ testCase "Predicate simplification removes trivial claim" $ do
+        let expected = []
+        actual <- runSimplifyRule
+            ( Pair
+                ( Mock.b
+                , makeAndPredicate
+                    (makeNotPredicate
+                        (makeEqualsPredicate Mock.testSort x Mock.b)
+                    )
+                    (makeNotPredicate
+                        (makeNotPredicate
+                            (makeEqualsPredicate Mock.testSort x Mock.b)
+                        )
+                    )
+                )
+              `rewritesToWithSortOLD`
+              Pair (Mock.a, makeTruePredicate Mock.testSort)
+            )
+        assertEqual "" expected actual
 
-instance OnePathRuleBase TermLike where
-    t1 `rewritesTo` t2 =
-        Pair (t1, makeTruePredicate (termLikeSort t1))
-        `rewritesTo` Pair (t2, makeTruePredicate (termLikeSort t2))
+    , testCase "Case where f(x) is defined;\
+               \ Case where it is not is simplified" $ do
+        let expected =
+                [   Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x))
+                    `rewritesToWithSortOLD`
+                    Pair (Mock.a, makeTruePredicate Mock.testSort)
+                ]
 
-test_simplifyRule :: [TestTree]
-test_simplifyRule =
+        actual <- runSimplifyRule
+            (   Pair (Mock.f x, makeTruePredicate Mock.testSort)
+                `rewritesToWithSortOLD`
+                Pair (Mock.a, makeTruePredicate Mock.testSort)
+            )
+
+        assertEqual "" expected actual
+
+    , testCase "Substitution in requires predicate" $ do
+        let expected = [Mock.a `rewritesToWithSortOLD` Mock.f Mock.b]
+
+        actual <- runSimplifyRule
+            (   Pair (Mock.a,  makeEqualsPredicate Mock.testSort Mock.b x)
+                `rewritesToWithSortOLD`
+                Pair (Mock.f x, makeTruePredicate Mock.testSort)
+            )
+
+        assertEqual "" expected actual
+
+    , testCase "Simplifies requires predicate" $ do
+        let expected = [Mock.a `rewritesToWithSortOLD` Mock.cf]
+
+        actual <- runSimplifyRule
+            (   Pair (Mock.a,  makeEqualsPredicate Mock.testSort Mock.b Mock.b)
+                `rewritesToWithSortOLD`
+                Pair (Mock.cf, makeTruePredicate Mock.testSort)
+            )
+
+        assertEqual "" expected actual
+    ]
+  where
+    rewritesToWithSortOLD
+        :: RuleBase base OLD.OnePathRule
+        => base VariableName
+        -> base VariableName
+        -> OLD.OnePathRule
+    rewritesToWithSortOLD = Common.rewritesToWithSort
+
+    x = mkElemVar Mock.x
+
+test_simplifyRule_OnePathRule :: [TestTree]
+test_simplifyRule_OnePathRule =
     [ testCase "No simplification needed" $ do
-        let rule = Mock.a `rewritesTo` Mock.cf
+        let rule = Mock.a `rewritesToWithSort` Mock.cf
             expected = [rule]
 
         actual <- runSimplifyRule rule
@@ -119,11 +272,11 @@ test_simplifyRule =
         assertEqual "" expected actual
 
     , testCase "Simplify lhs term" $ do
-        let expected = [Mock.a `rewritesTo` Mock.cf]
+        let expected = [Mock.a `rewritesToWithSort` Mock.cf]
 
         actual <- runSimplifyRule
             (   mkAnd Mock.a (mkEquals Mock.testSort Mock.a Mock.a)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Mock.cf
             )
 
@@ -132,7 +285,7 @@ test_simplifyRule =
     , testCase "Does not simplify rhs term" $ do
         let rule =
                 Mock.a
-                `rewritesTo`
+                `rewritesToWithSort`
                 mkAnd Mock.cf (mkEquals Mock.testSort Mock.a Mock.a)
             expected = [rule]
 
@@ -141,21 +294,21 @@ test_simplifyRule =
         assertEqual "" expected actual
 
     , testCase "Substitution in lhs term" $ do
-        let expected = [Mock.a `rewritesTo` Mock.f Mock.b]
+        let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b]
 
         actual <- runSimplifyRule
             (   mkAnd Mock.a (mkEquals Mock.testSort Mock.b x)
-                `rewritesTo` Mock.f x
+                `rewritesToWithSort` Mock.f x
             )
 
         assertEqual "" expected actual
 
     , testCase "Simplifies requires predicate" $ do
-        let expected = [Mock.a `rewritesTo` Mock.cf]
+        let expected = [Mock.a `rewritesToWithSort` Mock.cf]
 
         actual <- runSimplifyRule
             (   Pair (Mock.a,  makeEqualsPredicate Mock.testSort Mock.b Mock.b)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Pair (Mock.cf, makeTruePredicate Mock.testSort)
             )
 
@@ -164,7 +317,7 @@ test_simplifyRule =
     , testCase "Does not simplify ensures predicate" $ do
         let rule =
                 Pair (Mock.a,  makeTruePredicate Mock.testSort)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Pair (Mock.cf, makeEqualsPredicate Mock.testSort Mock.b Mock.b)
             expected = [rule]
 
@@ -173,11 +326,11 @@ test_simplifyRule =
         assertEqual "" expected actual
 
     , testCase "Substitution in requires predicate" $ do
-        let expected = [Mock.a `rewritesTo` Mock.f Mock.b]
+        let expected = [Mock.a `rewritesToWithSort` Mock.f Mock.b]
 
         actual <- runSimplifyRule
             (   Pair (Mock.a,  makeEqualsPredicate Mock.testSort Mock.b x)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Pair (Mock.f x, makeTruePredicate Mock.testSort)
             )
 
@@ -185,13 +338,13 @@ test_simplifyRule =
 
     , testCase "Splits rule" $ do
         let expected =
-                [ Mock.a `rewritesTo` Mock.cf
-                , Mock.b `rewritesTo` Mock.cf
+                [ Mock.a `rewritesToWithSort` Mock.cf
+                , Mock.b `rewritesToWithSort` Mock.cf
                 ]
 
         actual <- runSimplifyRule
             (   mkOr Mock.a Mock.b
-                `rewritesTo`
+                `rewritesToWithSort`
                 Mock.cf
             )
 
@@ -200,25 +353,25 @@ test_simplifyRule =
                \ Case where it is not is simplified" $ do
         let expected =
                 [   Pair (Mock.f x, makeCeilPredicate Mock.testSort (Mock.f x))
-                    `rewritesTo`
+                    `rewritesToWithSort`
                     Pair (Mock.a, makeTruePredicate Mock.testSort)
                 ]
 
         actual <- runSimplifyRule
             (   Pair (Mock.f x, makeTruePredicate Mock.testSort)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Pair (Mock.a, makeTruePredicate Mock.testSort)
             )
 
         assertEqual "" expected actual
     , testCase "f(x) is always defined" $ do
         let expected =
-                [ Mock.functional10 x `rewritesTo` Mock.a
+                [ Mock.functional10 x `rewritesToWithSort` Mock.a
                 ]
 
         actual <- runSimplifyRule
             (   Pair (Mock.functional10 x, makeTruePredicate Mock.testSort)
-                `rewritesTo`
+                `rewritesToWithSort`
                 Pair (Mock.a, makeTruePredicate Mock.testSort)
             )
 
@@ -238,17 +391,25 @@ test_simplifyRule =
                         )
                     )
                 )
-              `rewritesTo`
+              `rewritesToWithSort`
               Pair (Mock.a, makeTruePredicate Mock.testSort)
             )
         assertEqual "" expected actual
     ]
   where
+    rewritesToWithSort
+        :: RuleBase base OnePathRule
+        => base VariableName
+        -> base VariableName
+        -> OnePathRule
+    rewritesToWithSort = Common.rewritesToWithSort
+
     x = mkElemVar Mock.x
 
 runSimplifyRule
-    :: OnePathRule
-    -> IO [OnePathRule]
+    :: SimplifyRuleLHS rule
+    => rule
+    -> IO [rule]
 runSimplifyRule rule =
     fmap MultiAnd.extractPatterns
     $ runNoSMT
@@ -256,8 +417,8 @@ runSimplifyRule rule =
         SMT.All.declare Mock.smtDeclarations
         simplifyRuleLhs rule
 
-test_simplifyClaimRule :: [TestTree]
-test_simplifyClaimRule =
+test_simplifyClaimRuleOLD :: [TestTree]
+test_simplifyClaimRuleOLD =
     [ test "infers definedness" []
         rule1
         [rule1']
@@ -271,14 +432,14 @@ test_simplifyClaimRule =
     rule1' = rule1 & requireDefined
     rule2 =
         rulePattern @VariableName (Mock.g Mock.a) Mock.b
-        & Lens.set (field @"requires") requires
+        & Lens.set (field @"requires") requiresOLD
     rule2' =
         rule2
         & requireDefined
         & Lens.set (field @"left") (Mock.f Mock.a)
 
-    requires :: Predicate VariableName
-    requires = makeEqualsPredicate Mock.testSort Mock.a Mock.b
+    requiresOLD :: Predicate VariableName
+    requiresOLD = makeEqualsPredicate Mock.testSort Mock.a Mock.b
 
     requireDefined rule =
         Lens.over
@@ -298,6 +459,86 @@ test_simplifyClaimRule =
         -> RulePattern VariableName
         -> [RulePattern VariableName]
         -> TestTree
+    test name replacementsOLD (OLD.OnePathRule -> inputOLD) (map OLD.OnePathRule -> expect) =
+        -- Test simplifyClaimRule through the OnePathRule instance.
+        testCase name $ do
+            actual <- run $ simplifyRuleLhs inputOLD
+            assertEqual "" expect (MultiAnd.extractPatterns actual)
+      where
+        run =
+            runNoSMT
+            . runSimplifier env
+            . flip runReaderT TestEnvOLD { replacementsOLD, inputOLD, requiresOLD }
+            . runTestSimplifierTOLD
+        env =
+            Mock.env
+                { simplifierCondition = emptyConditionSimplifier
+                , simplifierAxioms = mempty
+                }
+
+test_simplifyClaimRule :: [TestTree]
+test_simplifyClaimRule =
+    [ test "infers definedness" []
+        rule1
+        [rule1']
+    , test "includes side condition" [(Mock.g Mock.a, Mock.f Mock.a)]
+        rule2
+        [rule2']
+    ]
+  where
+    rule1, rule2, rule2' :: ClaimPattern
+    rule1 =
+        claimPattern
+            (Pattern.fromTermLike (Mock.f Mock.a))
+            (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b])
+            []
+    rule1' = rule1 & requireDefined
+    rule2 =
+        claimPattern
+            (Pattern.fromTermLike (Mock.g Mock.a))
+            (OrPattern.fromPatterns [Pattern.fromTermLike Mock.b])
+            []
+        & require aEqualsb
+    rule2' =
+        rule2
+        & requireDefined
+        & Lens.over
+            (field @"left")
+            ( Pattern.andCondition
+                (Mock.f Mock.a & Pattern.fromTermLike)
+            . Pattern.withoutTerm
+            )
+
+    require condition =
+        Lens.over
+            (field @"left")
+            (flip Pattern.andCondition condition)
+
+    aEqualsb =
+        makeEqualsPredicate Mock.testSort Mock.a Mock.b
+        & Condition.fromPredicate
+
+    requireDefined =
+        Lens.over
+            (field @"left")
+            (\left' ->
+                let leftTerm = Pattern.term left'
+                    leftSort = TermLike.termLikeSort leftTerm
+                 in Pattern.andCondition
+                        left'
+                        ( makeCeilPredicate leftSort leftTerm
+                        & Condition.fromPredicate
+                        )
+            )
+
+    test
+        :: HasCallStack
+        => TestName
+        -> [(TermLike RewritingVariableName, TermLike RewritingVariableName)]
+        -- ^ replacements
+        -> ClaimPattern
+        -> [ClaimPattern]
+        -> TestTree
     test name replacements (OnePathRule -> input) (map OnePathRule -> expect) =
         -- Test simplifyClaimRule through the OnePathRule instance.
         testCase name $ do
@@ -307,7 +548,8 @@ test_simplifyClaimRule =
         run =
             runNoSMT
             . runSimplifier env
-            . flip runReaderT TestEnv { replacements, input, requires }
+            . flip runReaderT TestEnv
+                { replacements, input, requires = aEqualsb }
             . runTestSimplifierT
         env =
             Mock.env
@@ -315,11 +557,80 @@ test_simplifyClaimRule =
                 , simplifierAxioms = mempty
                 }
 
+data TestEnvOLD =
+    TestEnvOLD
+    { replacementsOLD :: ![(TermLike VariableName, TermLike VariableName)]
+    , inputOLD :: !OLD.OnePathRule
+    , requiresOLD :: !(Predicate VariableName)
+    }
+
+newtype TestSimplifierTOLD m a =
+    TestSimplifierTOLD { runTestSimplifierTOLD :: ReaderT TestEnvOLD m a }
+    deriving (Functor, Applicative, Monad)
+    deriving (MonadReader TestEnvOLD)
+    deriving (MonadLog, MonadSMT)
+
+instance MonadTrans TestSimplifierTOLD where
+    lift = TestSimplifierTOLD . lift
+
+instance MFunctor TestSimplifierTOLD where
+    hoist f = TestSimplifierTOLD . hoist f . runTestSimplifierTOLD
+
+instance MonadSimplify m => MonadSimplify (TestSimplifierTOLD m) where
+    simplifyTermLike sideCondition termLike = do
+        TestEnvOLD { replacementsOLD, inputOLD, requiresOLD } <- Reader.ask
+        let rule = OLD.getOnePathRule inputOLD
+            left = Lens.view (field @"left") rule
+            sort = termLikeSort left
+            expectSideCondition =
+                makeAndPredicate requiresOLD (makeCeilPredicate sort left)
+                & liftPredicate
+                & Predicate.coerceSort predicateSort
+                & Condition.fromPredicate
+                & SideCondition.fromCondition
+            satisfied = sideCondition == expectSideCondition
+        return
+            . OrPattern.fromTermLike
+            . (if satisfied then applyReplacements replacementsOLD else id)
+            $ termLike
+      where
+        applyReplacements
+            :: InternalVariable variable
+            => [(TermLike VariableName, TermLike VariableName)]
+            -> TermLike variable
+            -> TermLike variable
+        applyReplacements replacements zero =
+            Foldable.foldl' applyReplacement zero
+            $ map liftReplacement replacements
+
+        applyReplacement orig (ini, fin)
+          | orig == ini = fin
+          | otherwise   = orig
+
+        liftPredicate
+            :: InternalVariable variable
+            => Predicate VariableName
+            -> Predicate variable
+        liftPredicate = Predicate.mapVariables (pure fromVariableName)
+
+        liftTermLike
+            :: InternalVariable variable
+            => TermLike VariableName
+            -> TermLike variable
+        liftTermLike = TermLike.mapVariables (pure fromVariableName)
+
+        liftReplacement
+            :: InternalVariable variable
+            => (TermLike VariableName, TermLike VariableName)
+            -> (TermLike variable, TermLike variable)
+        liftReplacement = Bifunctor.bimap liftTermLike liftTermLike
+
 data TestEnv =
     TestEnv
-    { replacements :: ![(TermLike VariableName, TermLike VariableName)]
+    { replacements
+        :: ![(TermLike RewritingVariableName, TermLike RewritingVariableName)]
     , input :: !OnePathRule
-    , requires :: !(Predicate VariableName)
+    , requires :: !(Condition RewritingVariableName)
     }
 
 newtype TestSimplifierT m a =
@@ -338,10 +649,14 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where
     simplifyTermLike sideCondition termLike = do
         TestEnv { replacements, input, requires } <- Reader.ask
         let rule = getOnePathRule input
-            left = Lens.view (field @"left") rule
-            sort = termLikeSort left
+            leftTerm =
+                Lens.view (field @"left") rule
+                & Pattern.term
+            sort = termLikeSort leftTerm
             expectSideCondition =
-                makeAndPredicate requires (makeCeilPredicate sort left)
+                makeAndPredicate
+                    (Condition.toPredicate requires)
+                    (makeCeilPredicate sort leftTerm)
                 & liftPredicate
                 & Predicate.coerceSort predicateSort
                 & Condition.fromPredicate
@@ -354,12 +669,12 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where
       where
         applyReplacements
             :: InternalVariable variable
-            => [(TermLike VariableName, TermLike VariableName)]
+            => [(TermLike RewritingVariableName, TermLike RewritingVariableName)]
             -> TermLike variable
             -> TermLike variable
         applyReplacements replacements zero =
             Foldable.foldl' applyReplacement zero
-            $ map liftReplacement replacements
+            $ fmap liftReplacement replacements
 
         applyReplacement orig (ini, fin)
           | orig == ini = fin
@@ -367,18 +682,26 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where
 
         liftPredicate
             :: InternalVariable variable
-            => Predicate VariableName
+            => Predicate RewritingVariableName
             -> Predicate variable
-        liftPredicate = Predicate.mapVariables (pure fromVariableName)
+        liftPredicate =
+            Predicate.mapVariables liftRewritingVariable
 
         liftTermLike
             :: InternalVariable variable
-            => TermLike VariableName
+            => TermLike RewritingVariableName
             -> TermLike variable
-        liftTermLike = TermLike.mapVariables (pure fromVariableName)
+        liftTermLike =
+            TermLike.mapVariables liftRewritingVariable
 
         liftReplacement
             :: InternalVariable variable
-            => (TermLike VariableName, TermLike VariableName)
+            => (TermLike RewritingVariableName, TermLike RewritingVariableName)
             -> (TermLike variable, TermLike variable)
         liftReplacement = Bifunctor.bimap liftTermLike liftTermLike
+
+        liftRewritingVariable
+            :: InternalVariable variable
+            => AdjSomeVariableName (RewritingVariableName -> variable)
+        liftRewritingVariable =
+            pure (.) <*> pure fromVariableName <*> getRewritingVariable