S ong No maliza ion o he Sa e F agmen o a Minimal Rew i e
Sys em:
A T iple-Lexicog aphic P oo and he Te mina ion Conjec u e o
he Full Sys em
Moses Rahnama
No embe 24, 2025
Abs ac
We p esen a minimal ope a o -only e m ew i ing sys em wi h se en cons uc o s and
eigh educ ion ules. Ou main con ibu ion is a mechanically- e i ied p oo o s ong
no maliza ion o a gua ded agmen using a no el iple-lexicog aphic measu e combining
a phase bi , mul ise o de ing (De showi z-Manna), and o dinal anking. F om s ong
no maliza ion, we de i e a ce i ied no malize wi h p o en o ali y and soundness. Assuming
local con luence ( e i ied h ough c i ical pai analysis), Newman’s Lemma yields con luence
and he e o e unique no mal o ms o he sa e agmen . We es ablish impossibili y esul s
showing ha simple measu es, such as addi i e coun e s, polynomial in e p e a ions, and
single-bi lags, p o ably ail o ules wi h e m duplica ion. The wo k demons a es
undamen al limi a ions in e mina ion p o ing o sel - e e en ial sys ems. I connec s o
classical undecidabili y esul s while p o iding cons uc i e, mechanically- e i ied p oo s, and
i s a es a conjec u e on undecidable e mina ion: some e mina ing ope a o -only sys ems
ha e e mina ion ha is ue bu unp o able wi hin a gi en base heo y using in e nally
de inable me hods. All heo ems ha e been o mally e i ied in a p oo assis an . The
o mal de elopmen is a ailable o p og am commi ee membe s and e e ees upon eques
o pu poses o pee e iew.
1 In oduc ion
We de elop a minimal ope a o -only ew i e calculus (KO7): he objec language con ains only
cons uc o s and ope a o s wi h ew i e ules; he e a e no binde s, ypes, ex e nal axioms, o
seman ic p edica es. The ules a e he seman ics. Ou goals a e: (i) a clean, duplica ion- obus
p oo o s ong no maliza ion (SN); (ii) a ce i ied no malize ha always e u ns a no mal o m;
(iii) (op ionally) unique no mal o ms ia Newman’s Lemma unde a local-con luence assump ion;
and (i ) an explici conjec u e ha some e mina ing ope a o -only sys ems ha e e mina ion
ha is ue bu unp o able in a gi en base heo y using in e nally de inable me hods.
Scope. All o mal esul s a e es ablished o a gua ded sa e sub ela ion. We do no claim a
single global measu e o he ull ungua ded ela ion. Mo eo e , we exhibi a p ecise nega i e:
a he oo peak
eqW a a
wi h
κM
(
a
) = 0, local join ails in he ull ela ion. The e o e he ull
ela ion is no locally con luen a ha peak, hence no con luen . The designed emedy is o
wo k in he sa e agmen wi h gua ded/con ex joine s (
§
6).
A second concep ual goal is o si ua e KO7 agains esul s abou ixed- a ge eachabili y
in e mina ing TRSs. I we de ine an in e nal p o abili y p edica e by “
educes o
⊤
”, hen
unde SN he se
{ | ⇒∗⊤}
is decidable by no maliza ion/back acking. Wi h con luence,
decision educes o no mal- o m equali y. This explains why single-le el G¨odel encodings canno
coexis wi h globally e mina ing p oo sea ch; he igh mo e is s a i ica ion.
1
Con ibu ions. (1) A duplica ion- obus SN p oo o KO7 using a iple-lex measu e wi h
a mul ise (DM) componen and an MPO-s yle head p ecedence; (2) a o al, p o ed-co ec
no malize ; (3) a gua ded Newman module o he sa e ela ion ha yields con luence (hence
unique no mal o ms) om SN + local con luence; (4) a decidabili y esul o eachabili y
unde SN; (5) a ca alog o impossibili y esul s o addi i e and polynomial measu es unde
duplica ion; (6) a o mal e i ica ion o all esul s; (7) a conjec u e on undecidable e mina ion
o ope a o -only sys ems wi hin a ixed base heo y.
Highligh s ( o maliza ion summa y).
SN (Sa eS ep) ia iple lex: Fo mally p o en using a lexicog aphic measu e combining a
δ-phase bi , a De showi z–Manna mul ise ank, and an o dinal.
Ce i ied no malize : A o al and sound no maliza ion unc ion is de ined by well- ounded
ecu sion.
Newman (Sa eS ep): Con luence is es ablished ia Newman’s Lemma using a e i ied local
con luence p ope y o he sa e agmen .
Full S ep ca ea : We exhibi a speci ic peak (
eqW a a
wi h
κM
(
a
) = 0) whe e local join
ails, jus i ying he es ic ion o he sa e sub ela ion.
Impossibili y esul s: The ailu e o simple addi i e and polynomial measu es is o mally
wi nessed by coun e examples.
2 Backg ound: TRSs, SN, eachabili y, and Newman
We assume s anda d abs ac educ ion and e m ew i ing no ions [
2
,
11
]. A e m is in no mal
o m i no ule applies. A TRS is s ongly no malizing (SN) i he e a e no in ini e educ ions.
A ela ion is con luen i o any
⇒∗u
and
⇒∗
he e exis s
w
wi h
u⇒∗w
and
⇒∗w
.
Local con luence equi es his only o single-s ep o ks. Newman’s Lemma asse s SN + local
con luence ⇒con luence [10], yielding unique no mal o ms.
Fixed- a ge (“small- e m”) eachabili y in e mina ing TRSs has well-cha ed complexi y:
NP-comple e o leng h- educing sys ems (d opping o P unde con luence), NExpTime/N2ExpTime
o (linea ) polynomial in e p e a ions, and PSPACE o KBO- e mina ing TRSs [
1
]. Modula i y
holds in ce ain linea , non-collapsing combina ions [
4
], while e en la non-linea sys ems exhibi
undecidable eachabili y and con luence [
9
]. Te mina ion unde duplica ion ypically equi es
o de s beyond plain sizes; a nai e size can inc ease unde duplica ing ules. The cu e is a mul ise
ex ension o a base o de [6] o ( ecu si e) pa h o de s [5].
3 The KO7 calculus
KO7 is a ini e TRS o e a small signa u e (7 cons uc o s) wi h 8 ules (including a condi ional
spli on eqW). Fo conc e eness we lis he ule shapes below.
Tiny example ( ace consequences). Using he e i ied no malize , we obse e:
In eg a e/del a: in eg a e(δ )⇒∗ oid ( e i ied).
Equali y (me a-le el consequence unde con luence):
–I n (a) = n (b) hen eqW a b ⇒∗ oid.
–O he wise eqW a b ⇒∗in eg a e(me ge a b).
No e: In he sa e agmen , con luence ensu es hese ou comes a e unique.
No e. We p o e SN and Newman-based con luence o he sa e agmen .
2
Rule Head A i y Shape Dup?
R1 me ge 2 me ge oid → No
R2 me ge 2 me ge oid → No
R3 me ge 2 me ge → No
R4 ec∆ 3 ec ∆ bs oid →bNo
R5 ec∆ 3 ec ∆ bs(del a n)→app s( ec ∆ b s n) No
R6 in eg a e 1 in eg a e (del a )→ oid No
R7 eqW 2 eqW aa→ oid No
R8 eqW 2 eqW ab→in eg a e (me ge a b) (i a=b) No
Table 1: KO7’s 8 ules. No e ha R7/R8 p o ide a comple e case spli on equali y. R3 is
collapsing (e ases one copy); R5 is non-duplica ing.
4 S ong no maliza ion
We de ine a iple-lexicog aphic measu e
µ3( ) := (δ- lag( ), κM( ), µo d( ))
o de ed by he lex p oduc o : (i) a phase bi d opping on he successo ecu sion; (ii) a mul ise
o anks
κM
(De showi z–Manna) wi h an explici p ecedence/s a us o ien ing edex
>
pieces;
and (iii) an o dinal payload
µo d
o non-duplica ing ies. O dinal haza ds a e s a ed explici ly
( igh -addi ion is no s ic ly mono one; abso p ion
α
+
β
=
β
equi es
ω≤β
). In duplica ing
b anches (i ex ended o b oade sys ems) we would use a compac MPO-s yle head p ecedence.
S ep s Sa eS ep (measu e uni ica ion). Fo he Sa eS ep ela ion we use a single uni ied
iple lex o de (
δ, κM, µo d
). Fo he ull ela ion we only p o ide a disjunc i e dec ease
ce i ica e: each s ep is co e ed by ei he a KO7 lex d op o an MPO iple d op. We do no
claim a single global well- ounded measu e o all ull s eps.
Theo em 1 (Pe -s ep dec ease (Sa eS ep)).Fo e e y ule ins ance
⇒ ′
in he gua ded
Sa eS ep ela ion, we ha e µ3( ′)<Lex µ3( ).
P oo idea. By ule head. Fo collapsing ules (e.g., me ge-cancel) we use he mul ise componen
wi h he chosen p ecedence so ha e e y RHS piece is s ic ly smalle han he emo ed LHS
edex in he base o de . Fo ec-succ he
δ
bi d ops (1
→
0). In he o maliza ion, each b anch is
a one-line dispa ched by a w appe lemma.
DM s MPO on ules (explici ). Fo me ge-cancel, we use a DM mul ise li o e a base
o de whe e
me ge
s ic ly domina es
. Fo eqW, we use a compac MPO-leaning measu e
whe e he head p ecedence o ien s eqW a b s ic ly abo e in eg a e(me ge a b).
Base-o de p emise (me ge-cancel): in
me ge →
, he RHS is s ic ly smalle han he
LHS.
Base-o de p emise (eqW): in
eqW a b →in eg a e
(
me ge a b
), he RHS is s ic ly smalle
unde head p ecedence.
No-Go o cons an bumps on κ(gene ic duplica o ).
Lemma 1 (No ixed +
k
o boolean lag o ien s a gene ic duplica o ).Le
κ
be a max-dep h-s yle
coun e and ix any
k∈N
. Fo a duplica ing ule o he shape
(
S
)
→C
[
S, S
](one edex eplaced
by wo occu ences o a sub e m
S
), he e exis s an ins ance whe e
κ
(
LHS
)
+k
=
κ
(
RHS
)
+k
, so
no s ic lex d op occu s. The same holds o a boolean phase lag alone.
3
P oo ske ch. Choose
S
wi h
κ
(
S
)
≥
1 and le
base
bound he con ex . Then
κ
(
LHS
) =
base+
1 while
κ
(
RHS
) =
max
(
κ
(
C
[
S
])
, κ
(
C
[
S
])) =
base+
1. Adding a ixed
k
p ese es equali y;
a single lag does no al e he ie. □
Rema k 1.In KO7, he successo ecu sion ule
ec
∆
b s
(
δ n
)
→app s
(
ec
∆
b s n
) is non-
duplica ing in he s ic a iable sense (i edis ibu es
s
and
b
), bu i s o ien a ion elies on he
δphase bi (1→0).
Duplica ion s ess iden i y. Fo any addi i e coun e
ρ
ha coun s a single emo ed edex
and sums subpieces, gene ic duplica o s sa is y
ρ(a e ) = ρ(be o e) −1+ρ(S),
so he e is no s ic d op when
ρ
(
S
)
≥
1. The obus ix uses DM/MPO: eplace one elemen by
a mul ise o s ic ly smalle elemen s (DM), o use RPO/MPO wi h a p ecedence/s a us such
ha he LHS edex s ic ly domina es each RHS piece.
Co olla y 1 (S ong no maliza ion).The gua ded ela ion
Sa eS ep
o KO7 is s ongly
no malizing.
Genealogy o ailu es (why DM/MPO). We eco d minimal coun e pa e ns ha mo i a e
he mul ise /pa h componen s:
Pu e o dinal (µ) only: shape-blind bounds ail o sepa a e nes ed δ om i s con ex .
Addi i e bumps on κ: ies pe sis on duplica o s (Lemma 1).
Addi i e coun e s
ρ
: by he iden i y
ρ
(
a e
) =
ρ
(
be o e
)
−
1 +
ρ
(
S
) he e is no s ic d op
when ρ(S)≥1.
The ix is DM/MPO: ensu e each RHS piece is s ic ly smalle han he emo ed edex in a base
o de and li ia a mul ise /pa h ex ension.
5 A ce i ied no malize
By well- ounded ecu sion on
µ3
we de ine a no maliza ion unc ion. We p o e he ollowing
p ope ies (sepa a ed o a oid o e ull lines):
(To ali y) ∀ ∃n. No malize( )=n
(Soundness) ∀ . no mal(No malize( )) ∧ ⇒∗No malize( ).
These a e exposed in he o maliza ion. We make no e iciency claim: wo s -case no maliza ion
cos ollows he e mina ion wi ness in play (c . he small- e m eachabili y bounds in [
1
]). In
con luen sys ems, decision educes o one no maliza ion and an equali y check.
6 Local con luence and Newman (gua ded sa e ela ion)
We discha ge local con luence by joining he ini e se o c i ical pai s (when p esen ). Combining
Co . 1 wi h Newman’s Lemma [10] yields:
Theo em 2 (Con luence and unique no mal o ms).I a ela ion is s ongly no malizing and
locally con luen , hen i is con luen . Hence e e y e m educes o a unique no mal o m.
4
Ins an ia ion (Sa eS ep). Combining Co . 1 (SN o
Sa eS ep
) wi h local-join lemmas yields
con luence and unique no mal o ms o he sa e agmen by Newman’s Lemma. In con as ,
he ull ela ion is no locally con luen a he oo peak
eqW a a
unde
κM
(
a
) = 0; hus ull
con luence does no hold. The
Sa eS ep
ela ion es ic s
eqW
o cases whe e a gumen s a e
gua ded, p e en ing his di e gence.
The s a -s a join p oo ollows he s anda d accessibili y (Acc) ecu sion a he sou ce, wi h
a case spli o e s a shapes (“head s ep + ail”) and composi ion ia ansi i i y. The module
also p o ides co olla ies o uniqueness o no mal o ms and equali y o no malize s unde s a .
Scope and Gua an ees ( o maliza ion-accu a e). We wo k wi h a gua ded sa e sub ela ion
Sa eS ep o which we p o e:
SN (Sa eS ep). The KO7 iple measu e
µ3
s ic ly d ops on e e y
Sa eS ep
. This yields
ace i ied no malize ha is o al and sound o he sa e agmen .
Local Con luence (Sa eS ep). We p o ide local-join lemmas pe oo shape and con ex
w appe s. Newman hen yields con luence and unique NFs o he sa e agmen .
Full S ep pe - ule dec eases (Hyb id). Fo each ke nel ule, he e is a pe -s ep dec ease
wi nessed ei he by KO7’s
δ/κM/µ
lex o by an MPO-leaning
µ
- i s iple. A uni o m global
agg ega o o all o S ep is le as u u e wo k.
C i ical-pai co e age. The ollowing able co e s he sa e oo con igu a ions wi h explici
local-join lemmas. This is exhaus i e o
Sa eS ep
excep he e lexi e
eqW a a
peak unde
κM
(
a
) = 0, which we show is no locally joinable a he oo . We discha ge many
eqW
cases ia
gua ded/con ex w appe s.
Sou ce Lemma
in eg a e(δ )localJoin in del a (unique a ge oid)
me ge oid localJoin me ge oid le (unique a ge )
me ge oid localJoin me ge oid igh (unique a ge )
me ge localJoin me ge (unique a ge )
ec ∆ bs oid localJoin ec ze o (unique a ge b)
ec ∆ bs(δ n)localJoin ec succ (unique a ge app s( ec ∆ bsn))
eqW a b, a =blocalJoin eqW ne (unique a ge in eg a e(me ge a b))
eqW a a, κM(a) = 0 no locally joinable a oo
Gua ded a ian s exclude spu ious b anches. Con ex ual w appe s li oo joins o con ex .
δ
-gua d: de ini ion and decidabili y. De ine he sa e-phase p edica e by
δ-gua d
(
)
⇐⇒
δFlag
(
) = 0. He e
δFlag
:
Te m →N
is a s uc u ally ecu si e unc ion de ined on e ms in
he a i ac ( acking spli pa i y), so he p edica e is decidable. Fac s:
δFlag
(
eqW a b
) = 0;
me ge- oid ules equi e δFlag( ) = 0.
Tiny δ- lag walk- h ough (1→0).
ec ∆ b s (δ n) app s( ec ∆ b s n)
δ- lag d op
5
7 Impossibili y esul s
We o mally es ablish he ailu e o se e al simple measu e s a egies, which necessi a e he use
o DM mul ise o de s o MPO. These nega i e esul s a e e i ied in he o mal de elopmen .
Addi i e bumps ail: No measu e o he o m
κ
(
) +
k
s ic ly dec eases on gene ic
duplica ing ules.
Ba e lags ail: A single boolean lag is insu icien o o ien ules ha li dep h.
Polynomial in e p e a ions ail: Any polynomial in e p e a ion in ol ing ixed cons an s
equi es ex e nal a i hme ic axioms o “o ien ” he ule, iola ing he ope a o -only cons ain .
Polynomial Impossibili y (The “F ui Sys em” Coun e example). We speci ically
in es iga e polynomial in e p e a ions o he o m
M
(
)
∈N
. Conside a sys em wi h a
cons an
c
and a ule
(
x
)
→g
(
x, x
). A polynomial measu e migh assign
M
(
c
) =
k
and
M
(
(
x
)) =
M
(
x
) +
p
. Fo he ule o dec ease, we need
M
(
x
) +
p >
2
M
(
x
), which implies
p>M(x). This canno hold o all xi M(x) is unbounded.
In ou o maliza ion, we demons a e ha a polynomial p oo o a simila sys em (isomo phic
o KO7) elies on ha dcoding speci ic cons an s (e.g.,
M
(
oid
) = 2) o sa is y inequali ies
like 2
M
(
s
)
> M
(
s
) + 1. This succeeds only by impo ing ex e nal a i hme ic p ope ies
(mul iplica ion) and imposing a bi a y alues on he ope a o s, iola ing he p inciple ha he
ope a o s’ seman ics should be de ined solely by hei ew i e ules. I he cons an is changed
(e.g.,
M
(
oid
) = 1), he p oo collapses. This ailu e is s uc u ally iden ical o he di icul y in
o ien ing gene ic duplica ing ules wi hou such ex e nal hacks.
In e nally de inable measu es. We use a simple con ac o in e nally de ined e mina ion
measu es o s uc u e hese nega i e esul s:
De ini ion 1 (In e nally de inable measu e).An in e nally de inable measu e o a ype
α
consis s o (
β, < β, w ,m,c xMono,piecesL
)whe e:
β
is a base o de ca ie ;
< β
is a
well- ounded ela ion wi h wi ness
w
;
m
:
α→β
is he measu e;
c xMono
exp esses con ex
compa ibili y; and
piecesL
asse s ha in each ule ins ance, e e y RHS piece is s ic ly smalle
han he emo ed LHS edex w. . . < β.
8 Decidabili y o Reachabili y
Theo em 3 (Fixed- a ge eachabili y).In a s ongly no malizing TRS, he se
{ | ⇒∗c}
o
any cons an cis decidable ia no maliza ion.
This connec s ou wo k o classical esul s: i we could encode undecidable p ope ies
h ough educ ion o cons an s, we would iola e known heo e ical limi s. This mo i a es
s a i ied app oaches in p oo assis an s, whe e objec -le el and me a-le el easoning a e ca e ully
sepa a ed.
Assump ions (model). We wo k wi h a ini e i s -o de TRS o e ini e e ms. The decision
me hod is: compu e a no mal o m (by SN) and check whe he i is
⊤
; wi h local con luence,
his educes o one no maliza ion and an equali y es .
6
Complexi y con ex . Small- e m eachabili y in e mina ing TRSs anges om NP (leng h-
educing) o NExpTime/N2ExpTime (polynomial in e p e a ions) and PSPACE (KBO), wi h
con luence lowe ing he leng h- educing class o P [
1
]. This si ua es ou “no malize and compa e”
decision p ocedu e o KO7 wi hin he es ablished landscape.
Mo eo e , decidabili y can be modula o disjoin unions unde le -linea i y/non-collapsing
assump ions [
4
], while e mina ion alone does no gua an ee decidabili y: e en la non-linea
TRSs ha e undecidable eachabili y/joinabili y/con luence [9].
9 Conjec u e: TRS Te mina ion Conjec u e
Conjec u e 1 (TRS Te mina ion Conjec u e).Fo e e y ecu si ely axioma izable base heo y
T
o a i hme ic (e.g., PA), he e exis s an ope a o -only TRS
R
ha encodes a i hme ic such
ha
R
e mina es, bu he e mina ion o a leas one sel - e e en ial ule o
R
is no p o able in
T.
E idence s ems om ue bu unp o able e mina ion phenomena (Goods ein sequences,
hyd a ba les), which admi TRS encodings whose e mina ion equi es p oo - heo e ic s eng h
beyond PA. This sugges s a gap be ween in e nally de inable anking unc ions and he o dinal
s eng h ac ually needed.
In e nal me hod class and base heo y. Fix a signa u e Σ. Le
C
(Σ) deno e in e nal
e mina ion me hods assembled om KO7-de inable ing edien s: simpli ica ion o de s wi h
ixed p ecedence/s a us on Σ (LPO/RPO/MPO), DM-mul ise li s o
N
- alued anks, algeb aic
in e p e a ions, and dependency pai s discha ged by hese. Choose a base heo y
T
(KO7-
in e nal, PRA, o PA) ha soundly o malizes
C
(Σ). The sha pened claim eads: he e exis s a
KO7 ule whose s ic dec ease is ue bu no p o able in Tusing only me hods om C(Σ).
10 Fo maliza ion s uc u e
The o mal e i ica ion is implemen ed in a p oo assis an . The p ojec s uc u e sepa a es he
ke nel de ini ions, me a- heo y p oo s, and impossibili y esul s:
Te mina ion p oo s: Es ablishes he pe - ule dec eases and s ong no maliza ion o he
sa e agmen using he iple-lexicog aphic measu e.
No maliza ion: De ines he no maliza ion unc ion and p o es i s o ali y and soundness.
Con luence: Implemen s he Newman engine and he s a -s a join, elying on local join
lemmas.
Impossibili y esul s: Con ains he e i ied coun e examples o addi i e measu es and he
p oo s ha simple measu es ail unde duplica ion.
All claimed esul s a e o mally p o en wi hou eliance on unp o en pos ula es in he cu en
build. The o mal de elopmen is a ailable o e iewe s unde app op ia e con iden iali y
ag eemen s.
Re e ences
[1]
F anz Baade and J”u gen Giesl. On he complexi y o he small e m eachabili y p oblem o
e mina ing ss. In FSCD 2024, olume 299 o LIPIcs, pages 16:1–16:18, 2024.
7
[2]
F anz Baade and Tobias Nipkow. Te m Rew i ing and All Tha . Camb idge Uni e si y P ess, 1998.
[3]
Wil ied Buchholz. A new sys em o p oo - heo e ic o dinal unc ions. Annals o Pu e and Applied
Logic, 32(3):195–207, 1986.
[4]
Anne-Ca he ine Ca on and Jean-Louis Coquid´e. Decidabili y o eachabili y o disjoin union o
e m ew i ing sys ems. Theo e ical Compu e Science, 126(1):31–52, 1994.
[5]
Nachum De showi z. Te mina ion o ew i ing. Jou nal o Symbolic Compu a ion, 3(1–2):69–116,
1987.
[6]
Nachum De showi z and Zoha Manna. P o ing e mina ion wi h mul ise o de ings. Communica ions
o he ACM, 22(8):465–476, 1979.
[7] R. L. Goods ein. On he es ic ed o dinal heo em. Jou nal o Symbolic Logic, 9(2):33–41, 1944.
[8]
Lau ence Ki by and Je Pa is. Accessible independence esul s o peano a i hme ic. Bulle in o he
London Ma hema ical Socie y, 14(4):285–293, 1982.
[9]
Isao Mi suhashi, Masahi o Oyamaguchi, and Flo en Jacquema d. The con luence p oblem o la
ss. In AISC 2006, olume 4120 o LNCS, pages 73–84, 2006.
[10]
M. H. A. Newman. On heo ies wi h a combina o ial de ini ion o “equi alence”. Annals o
Ma hema ics, 43(2):223–243, 1942.
[11] Te ese. Te m Rew i ing Sys ems. Camb idge Uni e si y P ess, 2003.
Appendix: Addendum
KO7 Rules Table (7 cons uc o s, 8 ules)
Rule Head A i y Shape Dup?
R1 me ge 2 me ge oid → No
R2 me ge 2 me ge oid → No
R3 me ge 2 me ge → No
R4 ec∆ 3 ec ∆ bs oid →bNo
R5 ec∆ 3 ec ∆ bs(del a n)→app s( ec ∆ b s n) No
R6 in eg a e 1 in eg a e (del a )→ oid No
R7 eqW 2 eqW aa→ oid No
R8 eqW 2 eqW ab→in eg a e (me ge a b) (i a=b) No
Table 2: KO7’s 8 ules. No e ha R7/R8 p o ide a comple e case spli on equali y. R3 is
collapsing (e ases one copy); R5 is non-duplica ing.
T iple-lexicog aphic measu e and duplica ion handling (DM/MPO)
We o de µ3( ) = (δ- lag( ), κM( ), µo d( )) by lex:
δ- lag: phase bi d opping on he successo ecu sion b anch.
Mul ise
κM
: a De showi z–Manna mul ise ex ension o e a base p ecedence/s a us (o
MPO head p ecedence) o ien ing edexes s ic ly abo e pieces; co e s duplica o s.
O dinal
µo d
: esol es non-duplica ing ies; igh -addi ion is no s ic ly mono one; abso p ion
α+β=βneeds ω≤β.
Pe - ule lemmas show e e y RHS componen is s ic ly smalle han he emo ed edex in he
base o de .
8
Agg ega ion o
κM
(union, no sum). We emphasize ha
κM
agg ega es ia mul ise
union (
∪
), no nume ic addi ion. Fo duplica ing ules, he mul ise o piece-weigh s on he RHS
is DM-smalle han he single on mul ise con aining he LHS edex weigh , yielding a s ic d op
in he
κM
componen . Fo non-duplica ing ules,
κM
ies by de ini ional equali y and he o dinal
µo d
esol es he b anch. In pa icula , o ungua ded ins ances o
eqW
- e l and me ge-cancel we
use a
κ
-b anch: when
κM
(
a
)
= 0 we ob ain a le -lex d op ia DM; when
κM
(
a
) = 0 he
κM
componen ies by
l
and he s ic dec ease is wi nessed in he
µo d
coo dina e ( igh b anch
o P od.Lex).
Sho wi ness snippe s ( oy duplica ion). Toy ule: pai (s x, y)→pai (x, pai (y, y)).
DM mul ise on sizes. Le
S
(
x, y
) =
size
(
pai
(s
x, y
)) =
size
(
x
) +
size
(
y
) + 2. Then
size
(
x
)
< S
(
x, y
) and
size
(
y
)
< S
(
x, y
). Use
X
=
∅
,
Y
=
{size
(
x
)
,size
(
y
)
}
,
Z
=
{S
(
x, y
)
}
o
conclude Y <DM Z.
MPO iple weigh .
weigh
(
pai a b
) = (
headRank
(
a
)
,size
(
a
)
,size
(
b
)) wi h
headRank
(s ) =
2, else 1. I
x
is uni /pai hen i s componen s dec ease (1¡2). I
x
= s
hen ie on 2; he
second componen s sa is y size( ) + 1 <size( ) + 2.
δ- lag
phase d op
κM(DM/MPO)
edex >pieces
µo d
ie-b eak
lex lex
Figu e 1: T iple-lex measu e componen s. Duplica o s dec ease ia
κM
; non-duplica ing ies ia
µo d.
Newman scope (gua ded sa e ela ion)
SN + local con luence implies con luence; in he a i ac his is ins an ia ed o he sa e ela ion
ia an Acc-based s a –s a join. Scope no e: all con luence s a emen s and hei Newman
ins an ia ions a e o Sa eS ep only. Full S ep is no locally joinable a oo o
eqW
a a wi h
κM(a) = 0; acco dingly we do no claim ull-s ep con luence.
Module map
The e i ica ion logic is dis ibu ed ac oss key modules o SN, no malize , and con luence engine.
Local con luence lemmas a e p o ed sepa a ely. No e: con ex closu e and local-join lemmas a e
explici ly ins an ia ed o he Sa eS ep agmen (Sa eS epC x) a he han he ull ela ion.
Pe - ule o ien a ion (DM/MPO/δ/µ)
Rule Base componen P ecedence/S a us Wi ness Sou ce
me ge oid le µ(o dinal) — Theo em 4.1 Te mina ion
me ge oid igh µ(o dinal) — Theo em 4.2 Te mina ion
me ge cancel DM on κM( edex >pieces) head p ecedence Theo em 4.3 Te mina ion
ec ze o DM on κM ec >pieces Theo em 4.4 Te mina ion
ec succ δphase bi (1 →0) — Theo em 4.5 Te mina ion
eqW e l MPO (µ- i s iple) head p ecedence Theo em 4.6 Te mina ion
eqW di MPO (µ- i s iple) head p ecedence Theo em 4.7 Te mina ion
in eg a e (del a ) µ(unique a ge ) — Theo em 4.8 Te mina ion
oy duplica ion DM on size s >pai Lemma 7.1 Impossibili y
oy duplica ion MPO iple headRank(s) >
headRank(pai )
Lemma 7.2 Impossibili y
Table 3: Pe - ule o ien a ion summa y.
Pa en he ical aliases: o subs i u ion con enience we expose simp o ms alongside he main
ec lemmas.
9
