Necessary of the Rule 4

Due to a further problem from this, the Rule 4 (shown below) is necessary.

  • Rule 4: {# A 1 B #′} = {# B #′} if lv(A) < lv(B)

The problem first comes with pDAN. In mEAN, the double grave accent reduces to {1` `2`}, then expands to {1{1…{1{1,2` `1`}2` `1`}…2` `1`}2` `1`}. Notice that the tailing rule apply in this case, so it becomes {1{1…{1{1,2`}2`}…2`}2`}. However, in pDAN without the Rule 4, {1,,3} reduces to {1{1,,3}2,,2}, then expands to {1…{1 {1,2{1,,3}1,,2} 2{1,,3}1,,2}…2{1,,3}1,,2}. For a lower {1{1,,3}1,,2}, we meet the blue double comma, then it reduces to {1{1,,3}1{1{1,,3}1,,2}2}, then {1{1,,3}1…{1{1,,3}1 {1{1,,3}1,2} 2}…2}. And a lower {1{1,,3}2} can reduce to {1{1{1,,3}2,,2}2}, and now we loop back to the first step. So {1,,3} never solves in pDAN.

In {# {1,,3} 1 ,, 2}, the {1,,3} is “blocked” by the double comma, and it’s not the last separator in {# {1,,3} 1 ,, 2}, so the tailing rule doesn’t apply on it. That’s the reason of the problem. To fix this, we enable the Rule 4, then {# {1,,3} 1 ,, 2} reduces to {# ,, 2}, and the problem will clear.

Enabling the Rule 4 from pDAN to DAN (where we must enable the Rule 4) making them inconsistent with lower parts from exAN to mEAN. To make the whole “first generation” consistent, we need to enable the Rule 4 from exAN on, so exAN, EAN and mEAN also need the “level comparison” part.

.