diff --git a/Project.toml b/Project.toml
index ac376dec..aff9a837 100644
--- a/Project.toml
+++ b/Project.toml
@@ -7,16 +7,18 @@ version = "0.4.0"
 MacroTools = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09"
 PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d"
 ProgressMeter = "92933f4c-e287-5a05-a399-4b506db050ca"
+SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
 Tables = "bd369af6-aec1-5ad0-b16a-f7cc5008161c"
 
 [compat]
 MacroTools = "0.5"
 ProgressMeter = "1"
+SparseArrays = "1.6"
 julia = "1.6"
 
 [extras]
-Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
 
 [targets]
 test = ["Test", "Documenter"]
diff --git a/src/Automata/Automata.jl b/src/Automata/Automata.jl
index c1833333..0b179a28 100644
--- a/src/Automata/Automata.jl
+++ b/src/Automata/Automata.jl
@@ -1,16 +1,19 @@
 module Automata
 
 import ..KnuthBendix
-import ..KnuthBendix: AbstractWord, RewritingOrdering, RewritingSystem, Rule
-import ..KnuthBendix: alphabet, rules, word_type
+import ..KnuthBendix:
+    AbstractWord, RewritingOrdering, AbstractRewritingSystem, Rule
+import ..KnuthBendix: alphabet, ordering, rules, word_type
 
-export IndexAutomaton
+export IndexAutomaton, PrefixAutomaton
 
 include("states.jl")
 include("interface.jl")
 include("index_automaton.jl")
 include("rebuilding_idxA.jl")
 
+include("prefix_automaton.jl")
+
 include("backtrack.jl")
 
 end # of module Automata
diff --git a/src/Automata/index_automaton.jl b/src/Automata/index_automaton.jl
index fd84c174..d79cda21 100644
--- a/src/Automata/index_automaton.jl
+++ b/src/Automata/index_automaton.jl
@@ -26,24 +26,17 @@ mutable struct IndexAutomaton{S,O<:RewritingOrdering} <: Automaton{S}
 end
 
 initial(idxA::IndexAutomaton) = idxA.initial
-KnuthBendix.ordering(idxA::IndexAutomaton) = idxA.ordering
-
-hasedge(::IndexAutomaton, ::State, ::Integer) = true
-
-addedge!(idxA::IndexAutomaton, src::State, dst::State, label) = src[label] = dst
-
 isfail(idxA::IndexAutomaton, σ::State) = σ === idxA.fail
-isaccepting(idxA::IndexAutomaton, σ::State) = !isdefined(σ, :value)
-
-signature(idxA::IndexAutomaton, σ::State) = id(σ)
+isaccepting(::IndexAutomaton, σ::State) = !isdefined(σ, :value)
 
-Base.isempty(idxA::IndexAutomaton) = degree(initial(idxA)) == 0
+hasedge(::IndexAutomaton, ::State, ::Integer) = true
 
-function KnuthBendix.word_type(::Type{<:IndexAutomaton{S}}) where {S}
-    return eltype(valtype(S))
+function addedge!(idxA::IndexAutomaton, src::State, dst::State, label)
+    src[label] = dst
+    return idxA
 end
 
-Base.Base.@propagate_inbounds function trace(
+function trace(
     label::Integer,
     ::IndexAutomaton,
     σ::State,
@@ -51,32 +44,11 @@ Base.Base.@propagate_inbounds function trace(
     return σ[label]
 end
 
-function IndexAutomaton(rws::RewritingSystem{W}) where {W}
-    if !KnuthBendix.isreduced(rws)
-        throw(
-            ArgumentError(
-                """`IndexAutomaton` can be constructed from reduced rewriting systems only.
-                Call `KnuthBendix.reduce!(rws)` and try again.""",
-            ),
-        )
-    end
-
-    id = @view one(W)[1:0]
-    S = State{typeof(id),UInt32,eltype(rules(rws))}
-    ord = KnuthBendix.ordering(rws)
-    A = alphabet(ord)
-    fail = S(Vector{S}(undef, length(A)), id, 0)
-    α = State(fail, id, 0)
+Base.isempty(idxA::IndexAutomaton) = degree(initial(idxA)) == 0
 
-    idxA = IndexAutomaton(ord, α, fail, Vector{typeof(α)}[])
-    idxA = self_complete!(idxA, fail, override = true)
-    idxA = direct_edges!(idxA, rules(rws))
-    idxA = skew_edges!(idxA)
+signature(::IndexAutomaton, σ::State) = id(σ)
 
-    return idxA
-end
-
-KnuthBendix.isreduced(idxA::Automata.IndexAutomaton) = true
+# construction/modification
 
 function direct_edges!(idxA::IndexAutomaton, rwrules)
     for (idx, rule) in enumerate(rwrules)
@@ -179,11 +151,45 @@ function Base.show(io::IO, idxA::IndexAutomaton)
         count(st -> !Automata.isaccepting(idxA, st), states) for
         states in idxA.states
     ]
-    ord = KnuthBendix.ordering(idxA)
+    ord = ordering(idxA)
     A = alphabet(ord)
     println(io, "index automaton over $(typeof(ord)) with $(length(A)) letters")
-    nstates = sum(length, idxA.states)
+    nstates = sum(length, idxA.states) + 1 # the initial one
     println(io, "  • ", nstates, " state" * (nstates == 1 ? "" : "s"))
     print(io, "  • ", sum(rules_count), " non-accepting states (rw rules)")
     return
 end
+
+# for using IndexAutomaton as rewriting struct in KnuthBendix
+KnuthBendix.ordering(idxA::IndexAutomaton) = idxA.ordering
+
+function KnuthBendix.word_type(::Type{<:IndexAutomaton{S}}) where {S}
+    return eltype(valtype(S))
+end
+
+function IndexAutomaton(rws::AbstractRewritingSystem{W}) where {W}
+    if !KnuthBendix.isreduced(rws)
+        throw(
+            ArgumentError(
+                """`IndexAutomaton` can be constructed from reduced rewriting systems only.
+                Call `KnuthBendix.reduce!(rws)` and try again.""",
+            ),
+        )
+    end
+
+    id = @view one(W)[1:0]
+    S = State{typeof(id),UInt32,eltype(rules(rws))}
+    ord = ordering(rws)
+    A = alphabet(ord)
+    fail = S(Vector{S}(undef, length(A)), id, 0)
+    α = State(fail, id, 0)
+
+    idxA = IndexAutomaton(ord, α, fail, Vector{typeof(α)}[])
+    idxA = self_complete!(idxA, fail, override = true)
+    idxA = direct_edges!(idxA, rules(rws))
+    idxA = skew_edges!(idxA)
+
+    return idxA
+end
+
+KnuthBendix.isreduced(::IndexAutomaton) = true
diff --git a/src/Automata/interface.jl b/src/Automata/interface.jl
index a2acb99f..c1d8c6d0 100644
--- a/src/Automata/interface.jl
+++ b/src/Automata/interface.jl
@@ -55,11 +55,11 @@ returned.
     for (i, l) in enumerate(w)
         if hasedge(A, σ, l)
             τ = trace(l, A, σ)
+            isfail(A, τ) && return i - 1, σ
+            σ = τ
+        else
+            return return i - 1, σ
         end
-        if isfail(A, τ)
-            return i - 1, σ
-        end
-        σ = τ
     end
     return length(w), σ
 end
diff --git a/src/Automata/prefix_automaton.jl b/src/Automata/prefix_automaton.jl
new file mode 100644
index 00000000..c02fbafd
--- /dev/null
+++ b/src/Automata/prefix_automaton.jl
@@ -0,0 +1,177 @@
+using SparseArrays
+
+struct PrefixAutomaton{O<:RewritingOrdering,V} <: Automaton{Int32}
+    ordering::O
+    transitions::Vector{SparseVector{Int32,UInt32}}
+    __storage::BitSet
+    rwrules::V
+    # 1 is the initial state
+    # 0 is the fail state
+    # negative values in transitions indicate indices to values stored in rwrules
+
+    function PrefixAutomaton(
+        ordering::RewritingOrdering,
+        rules::V,
+    ) where {V<:AbstractVector}
+        transitions = Vector{SparseVector{Int32,UInt32}}(undef, 0)
+        __storage = BitSet()
+        pfxA = new{typeof(ordering),V}(ordering, transitions, __storage, rules)
+        _ = addstate!(pfxA)
+        for (i, rule) in pairs(rules)
+            add_direct_path!(pfxA, rule.lhs, -i)
+        end
+        return pfxA
+    end
+end
+
+initial(::PrefixAutomaton) = one(Int32)
+isfail(::PrefixAutomaton, σ::Integer) = iszero(σ)
+isaccepting(pfx::PrefixAutomaton, σ::Integer) = 1 ≤ σ ≤ length(pfx.transitions)
+
+hasedge(pfxA::PrefixAutomaton, σ::Integer, lab) = pfxA.transitions[σ][lab] ≠ 0
+
+function addedge!(
+    pfxA::PrefixAutomaton,
+    src::Integer,
+    dst::Integer,
+    label,
+)
+    pfxA.transitions[src][label] = dst
+    return pfxA
+end
+
+function trace(label::Integer, pfxA::PrefixAutomaton, σ::Integer)
+    return pfxA.transitions[σ][label]
+end
+
+function Base.isempty(pfxA::PrefixAutomaton)
+    return all(iszero, pfxA.transitions[initial(pfxA)])
+end
+
+function Base.empty!(pfxA::PrefixAutomaton)
+    union!(pfxA.__storage, 2:length(pfxA.transitions))
+    pfxA.transitions[1] .= 0
+    return pfxA
+end
+
+# construction/modification
+
+function addstate!(pfxA::PrefixAutomaton)
+    if !isempty(pfxA.__storage)
+        st = popfirst!(pfxA.__storage)
+        pfxA.transitions[st] .= 0
+        # dropzeros!(pfxA.transitions[st])
+        return st
+    else
+        l = length(alphabet(ordering(pfxA)))
+        vec = SparseVector(l, UInt32[], Int32[])
+        push!(pfxA.transitions, vec)
+        return length(pfxA.transitions)
+    end
+end
+
+function add_direct_path!(
+    pfxA::PrefixAutomaton,
+    lhs::AbstractWord,
+    val::Integer,
+)
+    @assert val ≤ 0
+    σ = initial(pfxA)
+    for (i, letter) in pairs(lhs)
+        τ = trace(letter, pfxA, σ)
+        # @info "idx = $i" letter τ
+        if i == lastindex(lhs)
+            addedge!(pfxA, σ, val, letter)
+            return true, pfxA
+        elseif isfail(pfxA, τ)
+            τ = addstate!(pfxA)
+            addedge!(pfxA, σ, τ, letter)
+        end
+        σ = τ
+        if !isaccepting(pfxA, σ)
+            @debug "prefix of length $i of $lhs is aready a lhs of a rule" σ
+
+            # this may happen if the rule.lhs we push into pfxA
+            # has a prefix that is reducible; then we return false,
+            # and we don't enlarge pfxA
+            return false, pfxA
+        end
+    end
+    @error "unintended exit"
+    return false, pfxA
+end
+
+function remove_direct_path!(pfxA::PrefixAutomaton, lhs::AbstractWord)
+    σ = initial(pfxA)
+    on_leaf = false
+    leaf_start = (σ, 0)
+
+    for (i, letter) in enumerate(lhs)
+        # analyze edge with (src=σ, label=letter, dst=τ)
+        τ = trace(letter, pfxA, σ)
+        isfail(pfxA, τ) && return pfxA
+        if !isaccepting(pfxA, τ)
+            if i == length(lhs)
+                break # we reached the leaf corresponding to lhs
+            end
+            # reached a leaf node before lhs is completed
+            # i.e. lhs does not define a leaf, so there's nothing to remove
+            return pfxA
+        end
+        if degree(pfxA, τ) > 1
+            on_leaf = false
+        elseif !on_leaf
+            on_leaf = true
+            leaf_start = (σ, i)
+        end
+        σ = τ
+    end
+
+    σ, i = leaf_start
+    for letter in @view lhs[i+1:end-1]
+        # we're on the "long-leaf" part
+        τ = trace(letter, pfxA, σ)
+        # by the early exit above we know there's something to remove
+        @assert isaccepting(pfxA, τ)
+        pfxA.transitions[σ][letter] = 0
+        push!(pfxA.__storage, τ)
+        σ = τ
+    end
+
+    return pfxA
+end
+
+function Base.show(io::IO, ::MIME"text/plain", pfxA::PrefixAutomaton)
+    ord = ordering(pfxA)
+    A = alphabet(ord)
+    println(
+        io,
+        "prefix automaton over $(typeof(ord)) with $(length(A)) letters",
+    )
+    accept_states = length(pfxA.transitions) - length(pfxA.__storage)
+    nrules = mapreduce(+, pairs(pfxA.transitions)) do (i, t)
+        return i in pfxA.__storage ? 0 : sum(<(0), t)
+    end
+    println(io, "  • $(accept_states+nrules) states")
+    return print(io, "  • $(nrules) non-accepting states (rw rules)")
+end
+
+function Base.push!(pfxA::PrefixAutomaton, rule::KnuthBendix.Rule)
+    n = length(pfxA.rwrules) + 1
+    added, pfxA = add_direct_path!(pfxA, rule.lhs, -n)
+    if added
+        push!(pfxA.rwrules, rule)
+    end
+    return pfxA
+end
+
+# for using IndexAutomaton as rewriting struct in KnuthBendix
+KnuthBendix.ordering(pfxA::PrefixAutomaton) = pfxA.ordering
+
+function KnuthBendix.word_type(::Type{<:PrefixAutomaton{O,V}}) where {O,V}
+    return KnuthBendix.word_type(eltype(V))
+end
+
+function PrefixAutomaton(rws::AbstractRewritingSystem)
+    return PrefixAutomaton(ordering(rws), KnuthBendix.__rawrules(rws))
+end
diff --git a/src/Automata/rebuilding_idxA.jl b/src/Automata/rebuilding_idxA.jl
index 7d9b6e6a..51c19252 100644
--- a/src/Automata/rebuilding_idxA.jl
+++ b/src/Automata/rebuilding_idxA.jl
@@ -1,4 +1,4 @@
-function _rebuild!(idxA::IndexAutomaton, rws::RewritingSystem)
+function _rebuild!(idxA::IndexAutomaton, rws::AbstractRewritingSystem)
     # Most of the information in idxA can be reused;
     # however here we just rebuild it from scratch
     at = IndexAutomaton(rws)
@@ -8,7 +8,7 @@ function _rebuild!(idxA::IndexAutomaton, rws::RewritingSystem)
     return idxA
 end
 
-function rebuild!(idxA::IndexAutomaton, rws::RewritingSystem)
+function rebuild!(idxA::IndexAutomaton, rws::AbstractRewritingSystem)
     # mark all states as not up to date
     for states in idxA.states
         for σ in states
diff --git a/src/KnuthBendix.jl b/src/KnuthBendix.jl
index 0ec2090a..ab2d7e0a 100644
--- a/src/KnuthBendix.jl
+++ b/src/KnuthBendix.jl
@@ -6,6 +6,9 @@ export Alphabet, Word, RewritingSystem
 export LenLex, WreathOrder, Recursive, WeightedLex
 export alphabet, isconfluent, ordering, knuthbendix
 
+const Stack{W} = Vector{Tuple{W,W}}
+
+include("utils/packed_vector.jl")
 include("Words/Words.jl")
 using .Words
 include("buffer_pair.jl")
diff --git a/src/confluence_check.jl b/src/confluence_check.jl
index e144ac6c..3d3230f5 100644
--- a/src/confluence_check.jl
+++ b/src/confluence_check.jl
@@ -52,7 +52,7 @@ function check_confluence(
     is_reduced = isreduced(rws),
 )
     W = word_type(rws)
-    stack = Vector{Tuple{W,W}}()
+    stack = Stack{W}()
     return check_confluence!(stack, rws; is_reduced = is_reduced)
 end
 
diff --git a/src/knuthbendix2.jl b/src/knuthbendix2.jl
index d0f3b220..adf6ff89 100644
--- a/src/knuthbendix2.jl
+++ b/src/knuthbendix2.jl
@@ -112,6 +112,7 @@ function deriverule!(
                 push!(rws, new_rule)
                 deactivate_rules!(rws, stack, new_rule, work)
             else
+                push!(work.dropped_stack, (a, b))
                 work.dropped_rules += 1
             end
         end
@@ -169,7 +170,7 @@ function knuthbendix!(
     rws::RewritingSystem{W},
 ) where {W}
     work = Workspace(rws, settings)
-    stack = Vector{Tuple{W,W}}()
+    stack = Stack{W}()
     if !isreduced(rws)
         rws = reduce!(settings.algorithm, rws, work) # we begin with a reduced system
     end
diff --git a/src/knuthbendix_base.jl b/src/knuthbendix_base.jl
index 22c64938..ed1d3a7d 100644
--- a/src/knuthbendix_base.jl
+++ b/src/knuthbendix_base.jl
@@ -96,4 +96,5 @@ function _kb_progress(prog::Progress, total, current, on_stack)
     return prog
 end
 
-word_type(stack::AbstractVector{<:Tuple{W,W}}) where {W<:AbstractWord} = W
+word_type(st::Stack) = word_type(typeof(st))
+word_type(::Type{<:Stack{W}}) where {W} = W
diff --git a/src/knuthbendix_delete.jl b/src/knuthbendix_delete.jl
index 4048c727..4962e0cd 100644
--- a/src/knuthbendix_delete.jl
+++ b/src/knuthbendix_delete.jl
@@ -21,7 +21,7 @@ function knuthbendix!(
     rws::RewritingSystem{W},
 ) where {W}
     work = Workspace(rws, settings)
-    stack = Vector{Tuple{W,W}}()
+    stack = Stack{W}()
     rws = reduce!(settings.algorithm, rws, work) # we begin with a reduced system
 
     rwrules = __rawrules(rws)
diff --git a/src/knuthbendix_idxA.jl b/src/knuthbendix_idxA.jl
index c96110d9..8c2cb55c 100644
--- a/src/knuthbendix_idxA.jl
+++ b/src/knuthbendix_idxA.jl
@@ -48,16 +48,27 @@ end
 
 function knuthbendix!(
     settings::Settings{KBIndex},
-    rws::AbstractRewritingSystem{W},
-) where {W}
+    rws::AbstractRewritingSystem,
+)
     if !isreduced(rws)
         rws = reduce!(settings.algorithm, rws)
     end
     # rws is reduced now so we can create its index
     idxA = IndexAutomaton(rws)
     work = Workspace(idxA, settings)
-    stack = Vector{Tuple{W,W}}()
+    knuthbendix!(work, rws, idxA)
+
+    __post!(rws, idxA, work)
+    return rws
+end
 
+function knuthbendix!(
+    work::Workspace{KBIndex},
+    rws::AbstractRewritingSystem{W},
+    idxA::IndexAutomaton = IndexAutomaton(rws),
+) where {W}
+    @assert isreduced(rws)
+    stack = Stack{W}()
     rwrules = __rawrules(rws)
     settings = work.settings
 
@@ -133,14 +144,13 @@ function knuthbendix!(
         i += 1
     end
 
-    __post!(rws, idxA, work)
-
     return rws # so the rws is reduced here as well
 end
 
 function __post!(rws::AbstractRewritingSystem, rewriting, work::Workspace)
     settings = work.settings
-    stack = Vector{Tuple{word_type(rws),word_type(rws)}}()
+    W = word_type(rws)
+    stack = Stack{W}()
 
     if work.dropped_rules > 0
         @assert isempty(stack)
@@ -160,7 +170,7 @@ function __post!(rws::AbstractRewritingSystem, rewriting, work::Workspace)
             if settings.verbosity ≥ 1
                 @warn "The rws does NOT represent the original congruence. Re-adding the missing rules."
             end
-            rws = reduce!(settings.algorithm, rws, stack, work)
+            rws, _ = reduce!(settings.algorithm, rws, stack, 0, 0, work)
         else
             if settings.verbosity == 2
                 @info "Some rules have been dropped but the congruence is preserved."
@@ -169,3 +179,4 @@ function __post!(rws::AbstractRewritingSystem, rewriting, work::Workspace)
     end
     return rws
 end
+
diff --git a/src/rewriting.jl b/src/rewriting.jl
index b1c9bb10..bda44208 100644
--- a/src/rewriting.jl
+++ b/src/rewriting.jl
@@ -1,5 +1,8 @@
 RewritingBuffer{T}(::Any) where {T} = RewritingBuffer{T}() # no history
 RewritingBuffer{T}(::IndexAutomaton{S}) where {T,S} = RewritingBuffer{T}(S[])
+function RewritingBuffer{T}(::PrefixAutomaton) where {T,S}
+    return RewritingBuffer{T}(PackedVector{UInt32}())
+end
 
 """
     rewrite(u::AbstractWord, rewriting)
@@ -39,6 +42,42 @@ function rewrite(
     return W(v)
 end
 
+"""
+    function rewrite!(bp::BufferPair, rewriting; kwargs...)
+Rewrites word stored in `BufferPair` using `rewriting` object.
+
+To store a word in `bp`
+[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
+should be used.
+
+!!! warning
+    This implementation returns an instance of `Words.BufferWord` aliased with
+    the intenrals of `BufferPair`. You need to copy the return value if you
+    want to take the ownership.
+"""
+function rewrite!(rwb::RewritingBuffer, rewriting; kwargs...)
+    v = if isempty(rewriting)
+        Words.store!(rwb.output, rwb.input)
+    else
+        rewrite!(rwb.output, rwb.input, rewriting; kwargs...)
+    end
+    empty!(rwb.input) # shifts bp.input pointers to the beginning of its storage
+    return v
+end
+function rewrite!(
+    rwb::RewritingBuffer,
+    rewriting::Automata.Automaton;
+    kwargs...,
+)
+    v = if isempty(rewriting)
+        Words.store!(rwb.output, rwb.input)
+    else
+        rewrite!(rwb.output, rwb.input, rewriting; history = rwb.history, kwargs...)
+    end
+    empty!(rwb.input) # shifts bp.input pointers to the beginning of its storage
+    return v
+end
+
 function rewrite!(v::AbstractWord, w::AbstractWord, A::Any; kwargs...)
     throw(
         """No method for rewriting with $(typeof(A)). You need to implement
@@ -182,7 +221,7 @@ Whenever a terminal (i.e. accepting) state is encountered
 2. the appropriate suffix of `v` (equal to `lhs`) is removed, and
 3. `rhs` is prepended to `w`.
 
-Tracing continues from the newly prepended letter.
+Tracing continues from the first letter of the newly prepended word.
 
 To continue tracing `w` through the automaton we need to backtrack on our path
 in the automaton and for this `rewrite` maintains a vector of visited states of
@@ -233,33 +272,86 @@ function rewrite!(
 end
 
 """
-    function rewrite!(bp::BufferPair, rewriting; kwargs...)
-Rewrites word stored in `BufferPair` using `rewriting` object.
+    rewrite!(v::AbstractWord, w::AbstractWord, pfxA::PrefixAutomaton[; history, skipping])
+Rewrite word `w` storing the result in `v` using prefix automaton `idxA`.
+As rewriting rules are stored **externally**, they must be passed in the
+`rules` keyword argument.
 
-To store a word in `bp`
-[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
-should be used.
+Rewriting with a [`PrefixAutomaton`](@ref Automata.PrefixAutomaton) traces
+(i.e. follows) simultanously all paths in the automaton determined by `w`.
+To be more precise we trace a path in the power-set automaton (states are the
+subsets of states of the original automaton) via lazy accessible set construction.
+Since the non-deterministic part of the automaton consists of `ε`-loop at the
+initial state there are at most `length(w)-1` such paths.
 
-!!! warning
-    This implementation returns an instance of `Words.BufferWord` aliased with
-    the intenrals of `BufferPair`. You need to copy the return value if you
-    want to take the ownership.
+Whenever a non-accepting state is encountered **on any** of those paths
+
+1. its corresponding rule `lhs → rhs` is retrived,
+2. the appropriate suffix of `v` (equal to `lhs`) is removed, and
+3. `rhs` is prepended to `w`.
+
+Tracing continues from the first letter of the newly prepended word.
+
+To continue tracing `w` through the automaton we need to backtrack on our path
+in the automaton and for this `rewrite` maintains a history of visited
+states of `pfxA`. Whenever a suffix is removed from `v`, the path is rewinded
+(i.e. shortened to the appropriate length) and the next letter of `w` is traced
+from the last state on the path. This maintains the property that signature of
+the path is equal to `v` at all times.
+
+Once prefix automaton is build the complexity of this rewriting is `Ω(length(w)²)`.
 """
-function rewrite!(bp::RewritingBuffer, rewriting; kwargs...)
-    v = if isempty(rewriting)
-        Words.store!(bp.output, bp.input)
-    else
-        rewrite!(bp.output, bp.input, rewriting; kwargs...)
-    end
-    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
-    return v
-end
-function rewrite!(bp::RewritingBuffer, rewriting::IndexAutomaton; kwargs...)
-    v = if isempty(rewriting)
-        Words.store!(bp.output, bp.input)
-    else
-        rewrite!(bp.output, bp.input, rewriting; history = bp.history, kwargs...)
+function rewrite!(
+    v::AbstractWord,
+    w::AbstractWord,
+    pfxA::PrefixAutomaton;
+    history::PackedVector = PackedVector{UInt32}(),
+    skipping = nothing,
+)
+    resize!(history, 0)
+    __unsafe_push!(history, Automata.initial(pfxA))
+    __unsafe_finalize!(history)
+    v = resize!(v, 0)
+    # we're doing path tracing on PrefixAutomaton that is non-deterministic
+    # in the sense that we add an ε-loop at the initial state
+    # thus this is path tracing via (lazy) accessible set construction
+    # i.e. simultanously tracing all possible paths with the given signature,
+    # or tracing a path in power-set automaton (states are the subsets of
+    # states of the original automaton).
+    # We rewind the history of ALL paths whenever a terminal is found in ONE of them.
+    while !isone(w)
+        letter = popfirst!(w)
+        # we're tracing a bunch of paths simultanously:
+        found_terminal = false
+        # @info "current multi-state" last(history)
+        for σ in last(history)
+            τ = Automata.trace(letter, pfxA, σ)
+            # @info "with letter=$letter we transition" src = σ dst = τ
+            Automata.isfail(pfxA, τ) && continue # this path doesn't proceed any further
+            if !Automata.isaccepting(pfxA, τ) && -τ ≠ skipping
+                # find the length of the corresponding lhs and rewind
+                # @info "The dst is terminal, using:" pfxA.rwrules[-τ]
+                lhs, rhs = pfxA.rwrules[-τ]
+                resize!(v, length(v) - length(lhs) + 1)
+                prepend!(w, rhs)
+                resize!(history, length(history) - length(lhs) + 1)
+                found_terminal = true
+                break
+            end
+            if !found_terminal
+                __unsafe_push!(history, τ)
+            end
+        end
+        if !found_terminal
+            # @info """none of the dsts were terminal:
+            # extending v (by $letter) & pushing initial (1) to history"""
+            push!(v, letter)
+            # we finish by a suffix of w by adding the initial state:
+            __unsafe_push!(history, Automata.initial(pfxA))
+            # after we're done with all of the path we proclaim the next subset
+            __unsafe_finalize!(history)
+        end
+        # @info "afterwards:" v w
     end
-    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
     return v
 end
diff --git a/src/rewriting_system.jl b/src/rewriting_system.jl
index bc3fead6..8f7176ee 100644
--- a/src/rewriting_system.jl
+++ b/src/rewriting_system.jl
@@ -124,7 +124,7 @@ function RewritingSystem(
 end
 
 function RewritingSystem(
-    rwrules::Vector{Tuple{W,W}},
+    rwrules::Stack{W},
     order::RewritingOrdering;
     confluent::Bool = false,
     reduced::Bool = false,
diff --git a/src/rules.jl b/src/rules.jl
index af93aac8..e5be9c90 100644
--- a/src/rules.jl
+++ b/src/rules.jl
@@ -51,6 +51,8 @@ Base.length(r::Rule) = 2
 Base.last(r::Rule) = first(iterate(r, 1))
 Base.eltype(::Type{Rule{W}}) where {W} = W
 
+word_type(::Type{<:Rule{W}}) where {W} = W
+
 Base.show(io::IO, r::Rule) = ((a, b) = r; print(io, a, " ⇒ ", b))
 
 """
diff --git a/src/settings_workspace.jl b/src/settings_workspace.jl
index 6f56b3d9..69ad9a28 100644
--- a/src/settings_workspace.jl
+++ b/src/settings_workspace.jl
@@ -81,6 +81,7 @@ mutable struct Workspace{CA,T,H,S<:Settings{CA}}
     settings::S
     confluence_timer::Int
     dropped_rules::Int
+    dropped_stack::Stack{Word{T}}
 end
 
 function Workspace(word_t, history, settings::Settings)
@@ -91,6 +92,7 @@ function Workspace(word_t, history, settings::Settings)
         settings,
         0,
         0,
+        Stack{word_t}(),
     )
 end
 
diff --git a/src/utils/packed_vector.jl b/src/utils/packed_vector.jl
new file mode 100644
index 00000000..1786b4ce
--- /dev/null
+++ b/src/utils/packed_vector.jl
@@ -0,0 +1,36 @@
+
+struct PackedVector{T} <:
+       AbstractVector{SubArray{T,1,Vector{T},Tuple{UnitRange{Int64}},true}}
+    linear_tape::Vector{T}
+    subset_pointers::Vector{Int}
+    PackedVector{T}() where {T} = new{T}(T[], [1])
+end
+
+Base.size(pvec::PackedVector) = (length(pvec.subset_pointers) - 1,)
+Base.@propagate_inbounds function Base.getindex(pvec::PackedVector, i::Integer)
+    @boundscheck 1 ≤ i ≤ length(pvec)
+    ptr = pvec.subset_pointers
+    return @inbounds @view pvec.linear_tape[ptr[i]:ptr[i+1]-1]
+end
+
+__unsafe_push!(pvec::PackedVector, v) = (push!(pvec.linear_tape, v); pvec)
+function __unsafe_finalize!(pvec::PackedVector)
+    k = length(pvec.linear_tape) + 1
+    @assert k ≥ last(pvec.subset_pointers)
+    push!(pvec.subset_pointers, k)
+    return pvec
+end
+
+function Base.resize!(pvec::PackedVector, n::Integer)
+    @assert 0 ≤ n ≤ length(pvec) "growing of pvec is not supported"
+    resize!(pvec.subset_pointers, n + 1)
+    resize!(pvec.linear_tape, pvec.subset_pointers[end] - 1)
+    return pvec
+end
+
+function Base.push!(pvec::PackedVector, v::AbstractVector)
+    append!(pvec.linear_tape, v)
+    push!(pvec.subset_pointers, pvec.subset_pointers[end] + length(v))
+    return pvec
+end
+
diff --git a/test/automata.jl b/test/automata.jl
index c71cbeb5..36611202 100644
--- a/test/automata.jl
+++ b/test/automata.jl
@@ -69,8 +69,10 @@ end
     rs =
         KB.RewritingSystem([(A, ε), (B, ε)], lenlexord, reduced = true)
     ia = KB.IndexAutomaton(rs)
+    pa = KB.PrefixAutomaton(rs)
     @test KB.rewrite(testword, rs) ==
           KB.rewrite(testword, ia) ==
+          KB.rewrite(testword, pa) ==
           Word([1])
 
     rs = KB.RewritingSystem(
@@ -88,13 +90,18 @@ end
         reduced = true,
     )
     ia = KB.IndexAutomaton(rs)
+    pa = KB.PrefixAutomaton(rs)
 
     @test !isempty(ia)
+    @test !isempty(pa)
 
-    @test KB.rewrite(testword, rs) == KB.rewrite(testword, ia)
+    @test KB.rewrite(testword, rs) ==
+          KB.rewrite(testword, ia) ==
+          KB.rewrite(testword, pa)
 
     w = Word([1, 3, 4, 1, 4, 4, 1, 1, 4, 2, 3, 2, 4, 2, 2, 3, 1, 2, 1])
-    @test KB.rewrite(w, rs) == KB.rewrite(w, ia)
+    @test KB.rewrite(w, rs) == KB.rewrite(w, ia) == KB.rewrite(w, pa)
 
     @test sprint(show, ia) isa String
+    @test sprint(show, pa) isa String
 end
diff --git a/test/kbs.jl b/test/kbs.jl
index 859c498d..2b9afdbe 100644
--- a/test/kbs.jl
+++ b/test/kbs.jl
@@ -1,4 +1,4 @@
-@testset "KBS" begin
+@testset "KBStack" begin
     lenlex = let A = Alphabet([:a, :b, :A, :B])
         KB.setinverse!(A, :a, :A)
         KB.setinverse!(A, :b, :B)
@@ -19,7 +19,6 @@
     @test Set(KB.rules(knuthbendix(KB.Settings(KB.KBPlain()), R))) == crs
     @test Set(KB.rules(knuthbendix(KB.Settings(KB.KBStack()), R))) == crs
     @test Set(KB.rules(knuthbendix(KB.Settings(KB.KBS2AlgRuleDel()), R))) == crs
-    @test Set(KB.rules(knuthbendix(KB.Settings(KB.KBIndex()), R))) == crs
 
     @testset "io for RewritingSystem" begin
         @test sprint(show, MIME"text/plain"(), RC) isa String
@@ -37,3 +36,53 @@
         @test occursin("• verbosity            : 2", res)
     end
 end
+
+@testset "Automaton rewriting" begin
+    rws = KB.ExampleRWS.Hurwitz4()
+    RC = knuthbendix(KB.Settings(KB.KBStack()), rws)
+
+    idxA = KB.IndexAutomaton(RC)
+    pfxA = KB.PrefixAutomaton(RC)
+
+    w = Word([1, 1, 1, 2, 2, 2, 1, 1, 3, 2, 3, 3, 1, 1, 1, 3, 3, 1, 2, 2, 3, 2])
+    v = Word([1, 2, 1, 2, 1, 3])
+    @test v == KB.rewrite(w, RC)
+    @test v == KB.rewrite(w, idxA)
+    @test v == KB.rewrite(w, pfxA)
+
+    let at = idxA
+        rwb = KB.RewritingBuffer{UInt16}(at)
+        k = @allocated begin
+            KB.Words.store!(rwb, w)
+            KB.rewrite!(rwb, at)
+        end
+        @test length(w) == 22
+        @test rwb.output == v
+
+        @test 0 == @allocated begin
+            KB.Words.store!(rwb, w)
+            KB.rewrite!(rwb, at)
+        end
+    end
+
+    let at = pfxA
+        rwb = KB.RewritingBuffer{UInt16}(at)
+        k = @allocated begin
+            KB.Words.store!(rwb, w)
+            KB.rewrite!(rwb, at)
+        end
+        @test length(w) == 22
+        @test rwb.output == v
+
+        @test 0 == @allocated begin
+            KB.Words.store!(rwb, w)
+            KB.rewrite!(rwb, at)
+        end
+    end
+
+    @test all(1:10) do _
+        w = Word(rand(1:length(alphabet(rws)), 50))
+        v = KB.rewrite(w, RC)
+        return v == KB.rewrite(w, idxA) == KB.rewrite(w, pfxA)
+    end
+end
diff --git a/test/kbs1.jl b/test/kbs1.jl
index 3f1e8224..b1c832a8 100644
--- a/test/kbs1.jl
+++ b/test/kbs1.jl
@@ -1,4 +1,4 @@
-@testset "KBS1" begin
+@testset "KBPlain" begin
     Al = Alphabet([:a, :A, :b, :B])
     KB.setinverse!(Al, :a, :A)
     KB.setinverse!(Al, :b, :B)
diff --git a/test/packed_vector.jl b/test/packed_vector.jl
new file mode 100644
index 00000000..69a2bf33
--- /dev/null
+++ b/test/packed_vector.jl
@@ -0,0 +1,30 @@
+@testset "PackedVector" begin
+    pvec = KB.PackedVector{Char}()
+    @test pvec isa AbstractVector
+    @test length(pvec) == 0
+
+    push!(pvec, 'a':'c')
+    @test length(pvec) == 1
+    @test pvec == [['a', 'b', 'c']]
+
+    push!(pvec, 'd':'g')
+    @test length(pvec) == 2
+    @test pvec == [['a', 'b', 'c'], ['d', 'e', 'f', 'g']]
+
+    KB.__unsafe_finalize!(pvec)
+    @test length(pvec) == 3
+    @test pvec == [['a', 'b', 'c'], ['d', 'e', 'f', 'g'], Char[]]
+
+    KB.__unsafe_push!(pvec, 'a')
+    KB.__unsafe_push!(pvec, 'a')
+    @test length(pvec) == 3
+    @test pvec == [['a', 'b', 'c'], ['d', 'e', 'f', 'g'], Char[]]
+
+    KB.__unsafe_finalize!(pvec)
+    @test length(pvec) == 4
+    @test pvec == [['a', 'b', 'c'], ['d', 'e', 'f', 'g'], Char[], ['a', 'a']]
+
+    @test_throws AssertionError resize!(pvec, 5)
+    @test resize!(pvec, 2) == [['a', 'b', 'c'], ['d', 'e', 'f', 'g']]
+    @test length(pvec) == 2
+end
diff --git a/test/runtests.jl b/test/runtests.jl
index 59bc25b6..b71549c6 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -7,6 +7,7 @@ import KnuthBendix.Automata
 include("abstract_words.jl")
 
 @testset "KnuthBendix.jl" begin
+    include("packed_vector.jl")
     include("words.jl")
     include("bufferwords.jl")
     include("alphabets.jl")