```Roman Numerals
--------------
A  Roman  number is represented by an expression with operands I V X L C D M and
operator  '.',  which  binds  the digits. For example, the Roman number for 999,
CMXCIX is represented by C.M.X.C.I.X, or in tree form:

roman script('t'∘eval)'⍴9.9.9'        ⍝ Roman numeral form of 999.
.
┌─┴┐
.  X
┌─┴┐
.  I
┌─┴┐
.  C
┌─┴┐
.  X
┌┴┐
C M

The  script  handles numerals in the range I-M.M.M.C.M.X.C.I.X (1-3999) together
with three special non-numbers:

nulla       "nothing",
absurdus    attempt to subtract a larger number from a smaller one,
nimius      too big to represent.

This means that the script deals with a finite set of 4,002 distinct values.

See below for details.

The Roman numerals used here are:

┌─────── Powers of ten
│   ┌─── Half-way numbers
↓   ↓
1    I
5    ·   V
10    X
50    ·   L
100    C
500    ·   D
1000    M

A  feature of the Roman counting system is the "subtractive" or negative numeral
placed to the left of a larger-valued one. Six such combinations occur:

I.V: one before five (4)
I.X: one before ten  (9)

X.L: ten before fifty       (40)
X.C: ten before one hundred (90)

C.D: one hundred before five hundred (400)
C.M: one hundred before one thousand (900)

For example, 1,999 is represented by M.C.M.X.C.I.X, which is interpreted as: one
thousand  (M),  plus  one hundred before one thousand (C.M), plus ten before one
hundred (X.C), plus one before ten (I.X).

(
To a certain extent, this concept is reflected in the language:

X.I.X   (or I.X.X)   un-de-vi-ginti  (one from two tens)
X.X.I.X (or I.X.X.X) un-de-tri-ginta (one from three tens)
...
etc

but the correlation is not perfect:

duodeviginti (two from two tens) is not I.I.X.X, but X.V.I.I.I and
undecentum (one from a hundred) is not I.C, but X.C.I.X.

This may be because a consensus on the strict rules for subtractive numerals
emerged only comparatively recently. In Roman times, less rigorous combinat-
ions  such  as the following, frequently occurred. Search the web for "roman
numerals IIXX" etc., for examples.

VIIII for nine,
IIXX  for eighteen,
IC    for ninety nine.
(
A  related  phenomenon occurs in old English from Gothic, where the word
"elev" meant approximately "left over", giving us:

elev-en  "left over: one"
tw-elve  "two left over"
)

Incidentally:  for  such an ungainly number system, Roman numerals were sur-
prisingly successful, being used in business and commerce well into medieval
times.  A possible reason for their success was that they are hard to alter;
it  is  relatively  easy  to  cheat someone who uses Hindu-Arabic numbers by
changing a 9 to an 8 or a 1 to a 7, but much harder to change IX into XVIII.

Presumably,  one would prevent the fraudulent appending of extra numerals to
(either  side  of) a sequence, by surrounding it with dashes: "Claudius owes
Julius  -V-  amphorae of wine", but I have been unable to find an historical
example of this -JMS-.
)

To simplify the arithmetic, we expand subtractive sequences, using function '\',
so that all digits represent positive values:

I.V →   I.I.I.I
I.X → V.I.I.I.I

X.L →   X.X.X.X
X.C → L.X.X.X.X

C.D →   C.C.C.C
C.M → D.C.C.C.C

To  prevent the normalisation templates from immediately re-compressing such ex-
pressions,  the expansion replaces the '.' with an inert equivalent '∘', so that
the new expression does not match any of the normalisation patterns.

\ I.V →   I∘I∘I∘I
\ I.X → V∘I∘I∘I∘I

\ X.L →   X∘X∘X∘X
\ X.C → L∘X∘X∘X∘X

\ C.D →   C∘C∘C∘C
\ C.M → D∘C∘C∘C∘C

After  the  arithmetic operation is complete, function '/' is used to recompress
the result by replacing each '∘' with a '.', allowing the normalisation templat-
es to reinstall appropriate subtractive numerals:

/   I∘I∘I∘I →   I.I.I.I → I.V
/ V∘I∘I∘I∘I → V.I.I.I.I → I.X
...
etc.

Thus, arithmetic is implemented using the following simple steps:

- Expand (simplify) each argument, using \.
- Process the simplified arguments using auxiliary function ++, --, ××, etc.
- Compress  (normalise) the result using /.

--------
Addition  of  expanded numeral strings amounts to nothing more than merging them
while preserving the relative order of the numerals. For example:

X∘V∘I∘I ++ V∘I∘I∘I -> X∘V∘V∘I∘I∘I∘I∘I

This is achieved using 7×4 reduction templates:

For each of 7 numerals: n ∊ I V X L C D M
(
For each of 4 cases
(
p   ++   n = p∘n
n ++ q   = q∘n
p   ++ q∘n = (p++q)∘n
p∘n ++ q   = (p++q)∘n
)
)

Following merge and re-compression, normalisation yields:

/ X∘V∘V∘I∘I∘I∘I∘I -> X.V.V.I.I.I.I.I -> X.X.V

(
The  word   "normalise"  comes from the Latin word "norma" for a carpenter's
square, so normalise means literally "to square up".
)

Subtraction
-----------
Subtraction  consists  of cancelling corresponding numerals in the expanded left
and right argument strings. For example:

X∘X∘V∘I∘I - V∘I -> X∘X∘I
¯   ¯   ¯ ¯
If  the least significant numerals do not correspond, the larger one is replaced
by a string of the next lowest:

V - I -> I∘I∘I∘I∘I - I -> I∘I∘I∘I

Subtracting  equal  values  results in the special value "nulla", the Latin word
for nothing.

(
Nulla  has  a  connotation, slightly different from zero: the Roman counting
system had no _concept_ of zero as a number; "nulla" is more akin to "not-a-
number":

Ask a mathematician how many hippopotami are present in the room and the
chances are, s/he will respond with the number: zero. *

Ask  a  four-year-old  child the same question and the chances are, s/he
will  object  to  the  question on the grounds that there are no (nulla)
hippopotami in the room to count.

* unless of course, we happen to be in a zoo or doing acid.
(
A similar discussion sometimes arises between programmers of C, in which
a "scalar" is very different from an "array", and a programmer of APL in
which there is nothing other than the array.

Ask  an  APL programmer what is the shape of the number 3.14 and the
chances are s/he will respond with the vector: ⍬.

Ask  a  C programmer the same question and the chances are s/he will
object  to the question  on the grounds that the number is a scalar,
not an array, and therefore has no (nulla) shape.

One  source  of confusion is that, as APL has no scalars, in the C sense
of the word, it recycles the word "scalar" to denote an rank-0 array.

Try this little demonstration to convince your doubting C colleague:

(⊂2/2) ⊃ (2/4)⍴⎕A   ⍝ 2-vector picks from a rank-2 array.
F
(⊂1/2) ⊃ (1/4)⍴⎕A   ⍝ 1-vector picks from a rank-1 array.
B
(⊂0/2) ⊃ (0/4)⍴⎕A   ⍝ 0-vector picks from a rank-0 array.
A
(⊂0/2) ⊃ 3.14       ⍝ ditto.
3.14
)

Another contender for a Latin "zero" might be "noenum" (not one).  Wikipedia
says: "Bede and Dionysius Exiguus did use a Latin word, nulla meaning "noth-
ing",  alongside Roman numerals or Latin number words wherever a modern zero
would have been used."
)

Similarly, as Roman numerals have no concept of a negative number, the subtract-
ion of a larger number from a smaller one results in "absurdus".

For example:

roman script until'exit'

V-I         ⍝ some left.
I.V

V-V         ⍝ none left.
nulla

V-X         ⍝ absurd subtraction.
absurdus

exit

Multiplication
--------------
Single digit products use the following multiplication table:

I   V   X   L   C   D   M
┌───┬───┬───┬───┬───┬───┬───┐
I │ I │ V │ X │ L │ C │ D │ M │
├───┼───┼───┼───┼───┼───┼───┘
V │ V │XXV│ L │CCL│ D │MMD│
├───┼───┼───┼───┼───┼───┘
X │ X │ L │ C │ D │ M │
├───┼───┼───┼───┼───┘
L │ L │CCL│ D │MMD│
├───┼───┼───┼───┘
C │ C │ D │ M │
├───┼───┼───┘
D │ D │MMD│
├───┼───┘
M │ M │
└───┘

The  missing half of the table corresponds to products whose result is too large
to represent. Although the Romans did have ways of coping with much larger numb-
ers, they are rarely encountered these days.

(
According to http://www.roman-britain.org/numerals.htm :

"Numbers in the thousands were at first represented by the Romans with furth-
numeric  values ..."  appear  as  a  vertical line with circular handle-like
strokes  attached  to  either side. An ASCII character transliteration might
use "(", "|" and ")".

5,000    |)
10,000   (|)
50,000    |))
100,000  ((|))
500,000    |)))
1,000,000 (((|)))

During  the  later  Republic, thousands were represented by a line inscribed
above the appropriate numeral; e.g.
_               _
I =  1,000      V = 5,000

Hundreds  of  thousands were denoted by additional lines on each side of the
numeral; e.g.
_               _
|V| = 500,000   |X| = 1,000,000

A million is literally "ten hundred-thousands". The M symbol was not used to
denote thousands until the second century AD.

We will ignore these extended systems for the purposes of this workspace.
)

The  digits used here are good for numbers up to M.M.M.C.M.X.C.I.X (3999). Calc-
ulations  that  would  result in a number larger than this, return "nimius" (too
big).

For  multiple  digits, the permutations of single digit products is summed. This
amounts to an outer product in the APL sense:

p∘q ×× r∘s = (p××r)++(p××s)++(q××r)++(q××s)
p   ×× r∘s = (p××r)++(p××s)
p∘q ×× s   = (p××s)++(q××s)

Multiplication is optimised by including some intermediate simplification equat-
ions that reduce the increasingly longer strings produced by the above:

I∘I∘I∘I∘I =   V
p∘I∘I∘I∘I∘I = p∘V
V∘V =   X
... etc

An Alternative
--------------
An  alternative  to expanding I.V → I∘I∘I∘I ···, is to create six new artificial
numerals to represent subtractive sequences directly.

\ I.V → v
\ I.X → x

\ X.L → l
\ X.C → c

\ C.D → d
\ C.M → m

Doing  this  would speed up multiplication at the expense of increasing the size
of the table:

I     v     V     x     X     l     L     c     C     d     D     m     M
┌─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┐
I │  I  │  v  │  V  │  x  │  X  │  l  │  L  │  c  │  C  │  d  │  D  │  m  │  M  │
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
v │  v  │ XVI │ XX  │XXXVI│  l  │ CLX │ CC  │CCCLX│ CD  │ MDC │ MM  │MMMDC│
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┘
V │  V  │ XX  │ XXV │ lV  │  L  │ CC  │ CCL │ dL  │  D  │ MM  │ MMD │
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┘
x │  x  │XXXVI│ lV  │LXXXI│  c  │CCCLX│ dL  │DCCCX│  m  │MMMDC│
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┘
X │  X  │  l  │  L  │  c  │  C  │  d  │  D  │  m  │  M  │
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┘
l │  l  │ CLX │ CC  │CCCLX│  d  │ MDC │ MM  │MMMDC│
├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┘
L │  L  │ CC  │ CCL │ dL  │  D  │ MM  │ MMD │
├─────┼─────┼─────┼─────┼─────┼─────┼─────┘
c │  c  │CCCLX│ dL  │DCCCX│  m  │MMMDC│
├─────┼─────┼─────┼─────┼─────┼─────┘
C │  C  │ CD  │  D  │  m  │  M  │
├─────┼─────┼─────┼─────┼─────┘
d │  d  │ MDC │ MM  │MMMDC│
├─────┼─────┼─────┼─────┘
D │  D  │ MM  │ MMD │
├─────┼─────┼─────┘
m │  m  │MMMDC│
├─────┼─────┘
M │  M  │
└─────┘

Division
--------
The standard long division algorithm for Hindu-Arabic numbers shifts the divisor
to  the  left at the start of the process and shifts the result to compensate as
the division proceeds. This shift is equivalent to multiplication by 10. In fact
any  multiplier  would do; 10 is chosen solely because multiplication by 10 is a
trivial operation. Such shifting is not applicable to Roman numerals, but multi-
plication by 10 also turns out to be our best bet: the "tenfold" reduction sequ-
ence  for  ∘-expanded  numbers  is simply as follows. Note that in this context,
"10" is a function:

10 I = X                    ⍝ single-digit tenfold
10 V = L                    ⍝       ..      ..
10 X = C
10 L = D
10 C = M

10 p∘n = (10 p)∘(10 n)      ⍝ multiple-digit tenfold.

For example: 10(X∘X∘V∘I) → C∘C∘L∘X.

An  alternative  multiplier of 2 is also tempting because it has an even simpler
reduction sequence. If "2" stands for "twofold", then:

2   n =       n∘n           ⍝ single-digit twofold.
2 p∘n = (2 p)∘n∘n           ⍝ multiple-digit twofold.

For example: 2(X∘X∘V∘I) → X∘X∘X∘X∘V∘V∘I∘I

However,  as  "2"  produces  longer results, it slows down subsequent operations
considerably. Using the example (C.X.L.V ÷ V.I), 2 is slower than 10 by a factor
of around 3.

The shifted divisor is repeatedly subtracted from the dividend until it is larg-
er than what remains.

Roman  numerals  present  a small problem, not found in other number systems, in
that negative numbers are not distinguished; anything less than nulla is absurd-
us. This means that Charles Babbage's trick (see →Long_division←) of subtracting
until  negative  and then adding back, won't work. There are various ways around
this  problem.  The one adopted here is to compare numbers _before_ subtraction,
using auxiliary function ?() and so stopping short of going negative. Comparison
is most easily achieved starting from the left, that is, by comparing most sign-
ificant  numerals  first. In order to do this, the number binding is temporarily
reversed using auxiliary function ⌽().

A Coding Tip
------------
For  complex  functions leading to a number of reduction equations, it may prove
easier  to  develop the function in APL and then translate it. Here is the Roman
long division function used to code the div and rem equations in →#.roman←:

div←{                   ⍝ div function emulator.

ten←×∘10            ⍝ multiplier (any +ive number would do).

dv←{                ⍝ divide
p(q s)r←⍵
q≡'⊥':r p         ⍝ dividend too small.
t u←sb p q 0
rr←t+ten r
s≡'⊥':rr u        ⍝ finished.
∇ u s rr
}

sb←{                ⍝ repeated sub of divisor from dividend.
p q r←⍵
p<q:r p
∇(p-q)q(r+1)
}

sh←{                ⍝ "shift" divisor to just less than dividend.
p q r←⍵
p<q:r
∇ p(ten q)(q r)
}

dv ⍺(sh ⍺ ⍵'⊥')0    ⍝ quotient and remainder.
}

In general, translating the above yields a set of equations for each subfunction
and  subequations at each guard and local variable assignment. For example, sub-
function sb, above:

sb←{                ⍝ repeated sub of divisor from dividend.
p q r←⍵
p<q:r p
∇(p-q)q(r+1)
}

is translated into equations:

sb  p; q; r      = sb' p; q; r; p??q            ⍝ dividend ?? subtrahend:
sb' p; q; r; lt  = r; p                         ⍝ p<q:
sb' p; q; r; s   = sb p--q; q; r∘I              ⍝ p≥q:

Note the introduction of auxiliary function "sb prime".

(
Some effort was made in the coding to restrict the number of variables to 4:
p, q, r and s.  The principal reason for doing so was that their declaration
should make a highly obscure and vanishingly feeble Roman joke:

s p q r ::                    ⍝ match anything.
)

The "⍺" and "⍴" functions
-------------------------
Instead  of  relying  on 60-or-so  reduction templates to convert from Arabic to
Roman  numerals,  we  could "cheat" by using APL code directly. This single-line
implementation  of  ⍴ is considerably more efficient (but arguably less satisfy-
ing):

⍴(n:parse 1↓,'.',,[⍬]((4⍴10)⊤n)     ⍝ Roman from Arabic.

As  it  stands, the conversion is completely "blind". That is, the system has no
knowledge of the values of symbols such as '1', '2', ···; they are just parts of
patterns to be matched in selecting a reduction template.

Note  that Microsoft Excel provides a macro: roman(), which does the same job as
⍴. For example, =roman(42) yields the value XLII.

"⍺"  is  the  inverse of "⍴" in that it returns the Arabic equivalent of a given
Roman number.

Examples:

load roman                ⍝ install Roman rules.

until'et cetera'

⍴ 1.2.3                     ⍝ Roman from Arabic numerals
C.X.X.I.I.I

⍺ C.X.X.I.I.I               ⍝ Arabic from Roman.
1.2.3

⍺ ⍴ 1.2.3                   ⍝ full circle.
1.2.3

I.I.I.I                     ⍝ normalise
I.V

I.V + V.I                   ⍝ sum
X

V.I - I.V                   ⍝ subtraction
I.I

V.I × I.V                   ⍝ product
X.X.I.V

X.X ÷ I.I.I                 ⍝ division
V.I

X.X % I.I.I                 ⍝ remainder
I.I

X-V-V                       ⍝ nothing left
nulla

I-V                         ⍝ absurd subtraction
absurdus

M×M                         ⍝ number too big
nimius

et cetera
⍝            ┌──199──┐
eval 397⍴'I.'             ⍝ normalise: I.I.···.I
C.X.C.I.X

⍝ The following traces show why some operations take a while:

roman trace eval'X.I × X.I'       ⍝ 11×11 → 121
·X.I×X.I [p×q → /(\p××\q)] /(\X.I××\X.I)
···\X.I [\p.n → \p∘n] \X∘I
····\X [\j → j] X
···\X.I [\p.n → \p∘n] \X∘I
····\X [\j → j] X
··X∘I××X∘I [p∘m××q∘n → (p××q)++(p××n)++(m××q)++(m××n)] (X××X)++(X××I)++(I××X)++(I××I)
·····X××X [X××X → C] C
·····X××I [p××I → p] X
····C++X [p++X → p∘X] C∘X
····I××X [I××q → q] X
···C∘X++X [p++X → p∘X] C∘X∘X
···I××I [p××I → p] I
··C∘X∘X++I [p++I → p∘I] C∘X∘X∘I
·/(C∘X∘X∘I) [/(p∘n) → (/p).n] (/(C∘X∘X)).I
··/(C∘X∘X) [/(p∘n) → (/p).n] (/(C∘X)).X
···/(C∘X) [/(p∘n) → (/p).n] (/C).X
····/C [/j → j] C
C.X.X.I

⍝ The next example would generate many more reductions, but for the
⍝ intermediate simplification of expanded strings: V∘V = X, etc.

roman trace eval'I.X × I.X'       ⍝ 9 × 9 → 81
·I.X×I.X [p×q → /(\p××\q)] /(\I.X××\I.X)
···\I.X [\I.X → V∘I∘I∘I∘I] V∘I∘I∘I∘I
···\I.X [\I.X → V∘I∘I∘I∘I] V∘I∘I∘I∘I
··V∘I∘I∘I∘I××V∘I∘I∘I∘I [p∘m××q∘n → (p××q)++(p××n)++(m××q)++(m××n)] (V∘I∘I∘I××V∘I∘I∘I)++(V∘I∘I∘I××I)++(I××V∘I∘I∘I)++(I××I)
·····V∘I∘I∘I××V∘I∘I∘I [p∘m××q∘n → (p××q)++(p××n)++(m××q)++(m××n)] (V∘I∘I××V∘I∘I)++(V∘I∘I××I)++(I××V∘I∘I)++(I××I)
········V∘I∘I××V∘I∘I [p∘m××q∘n → (p××q)++(p××n)++(m××q)++(m××n)] (V∘I××V∘I)++(V∘I××I)++(I××V∘I)++(I××I)
···········V∘I××V∘I [p∘m××q∘n → (p××q)++(p××n)++(m××q)++(m××n)] (V××V)++(V××I)++(I××V)++(I××I)
··············V××V [V××V → X∘X∘V] X∘X∘V
··············V××I [p××I → p] V
·············X∘X∘V++V [p++V → p∘V] X∘X∘V∘V
·············X∘X∘V∘V [p∘V∘V → p∘X] X∘X∘X
·············I××V [I××q → q] V
············X∘X∘X++V [p++V → p∘V] X∘X∘X∘V
············I××I [p××I → p] I
···········X∘X∘X∘V++I [p++I → p∘I] X∘X∘X∘V∘I
···········V∘I××I [p××I → p] V∘I
··········X∘X∘X∘V∘I++V∘I [p++q∘I → (p++q)∘I] (X∘X∘X∘V∘I++V)∘I
···········X∘X∘X∘V∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘V++V)∘I
············X∘X∘X∘V++V [p++V → p∘V] X∘X∘X∘V∘V
············X∘X∘X∘V∘V [p∘V∘V → p∘X] X∘X∘X∘X
··········I××V∘I [I××q → q] V∘I
·········X∘X∘X∘X∘I∘I++V∘I [p++q∘I → (p++q)∘I] (X∘X∘X∘X∘I∘I++V)∘I
··········X∘X∘X∘X∘I∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X∘I++V)∘I
···········X∘X∘X∘X∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X++V)∘I
············X∘X∘X∘X++V [p++V → p∘V] X∘X∘X∘X∘V
·········I××I [p××I → p] I
········X∘X∘X∘X∘V∘I∘I∘I++I [p++I → p∘I] X∘X∘X∘X∘V∘I∘I∘I∘I
········V∘I∘I××I [p××I → p] V∘I∘I
·······X∘X∘X∘X∘V∘I∘I∘I∘I++V∘I∘I [p++q∘I → (p++q)∘I] (X∘X∘X∘X∘V∘I∘I∘I∘I++V∘I)∘I
········X∘X∘X∘X∘V∘I∘I∘I∘I++V∘I [p++q∘I → (p++q)∘I] (X∘X∘X∘X∘V∘I∘I∘I∘I++V)∘I
·········X∘X∘X∘X∘V∘I∘I∘I∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X∘V∘I∘I∘I++V)∘I
··········X∘X∘X∘X∘V∘I∘I∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X∘V∘I∘I++V)∘I
···········X∘X∘X∘X∘V∘I∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X∘V∘I++V)∘I
············X∘X∘X∘X∘V∘I++V [p∘I++q → (p++q)∘I] (X∘X∘X∘X∘V++V)∘I
·············X∘X∘X∘X∘V++V [p++V → p∘V] X∘X∘X∘X∘V∘V
·············X∘X∘X∘X∘V∘V [p∘V∘V → p∘X] X∘X∘X∘X∘X
·············X∘X∘X∘X∘X [X∘X∘X∘X∘X → L] L
········L∘I∘I∘I∘I∘I [p∘I∘I∘I∘I∘I → p∘V] L∘V
·······I××V∘I∘I [I××q → q] V∘I∘I
······L∘V∘I++V∘I∘I [p++q∘I → (p++q)∘I] (L∘V∘I++V∘I)∘I
·······L∘V∘I++V∘I [p++q∘I → (p++q)∘I] (L∘V∘I++V)∘I
········L∘V∘I++V [p∘I++q → (p++q)∘I] (L∘V++V)∘I
·········L∘V++V [p++V → p∘V] L∘V∘V
·········L∘V∘V [p∘V∘V → p∘X] L∘X
······I××I [p××I → p] I
·····L∘X∘I∘I∘I++I [p++I → p∘I] L∘X∘I∘I∘I∘I
·····V∘I∘I∘I××I [p××I → p] V∘I∘I∘I
····L∘X∘I∘I∘I∘I++V∘I∘I∘I [p++q∘I → (p++q)∘I] (L∘X∘I∘I∘I∘I++V∘I∘I)∘I
·····L∘X∘I∘I∘I∘I++V∘I∘I [p++q∘I → (p++q)∘I] (L∘X∘I∘I∘I∘I++V∘I)∘I
······L∘X∘I∘I∘I∘I++V∘I [p++q∘I → (p++q)∘I] (L∘X∘I∘I∘I∘I++V)∘I
·······L∘X∘I∘I∘I∘I++V [p∘I++q → (p++q)∘I] (L∘X∘I∘I∘I++V)∘I
········L∘X∘I∘I∘I++V [p∘I++q → (p++q)∘I] (L∘X∘I∘I++V)∘I
·········L∘X∘I∘I++V [p∘I++q → (p++q)∘I] (L∘X∘I++V)∘I
··········L∘X∘I++V [p∘I++q → (p++q)∘I] (L∘X++V)∘I
···········L∘X++V [p++V → p∘V] L∘X∘V
······L∘X∘V∘I∘I∘I∘I∘I [p∘I∘I∘I∘I∘I → p∘V] L∘X∘V∘V
······L∘X∘V∘V [p∘V∘V → p∘X] L∘X∘X
····I××V∘I∘I∘I [I××q → q] V∘I∘I∘I
···L∘X∘X∘I∘I++V∘I∘I∘I [p++q∘I → (p++q)∘I] (L∘X∘X∘I∘I++V∘I∘I)∘I
····L∘X∘X∘I∘I++V∘I∘I [p++q∘I → (p++q)∘I] (L∘X∘X∘I∘I++V∘I)∘I
·····L∘X∘X∘I∘I++V∘I [p++q∘I → (p++q)∘I] (L∘X∘X∘I∘I++V)∘I
······L∘X∘X∘I∘I++V [p∘I++q → (p++q)∘I] (L∘X∘X∘I++V)∘I
·······L∘X∘X∘I++V [p∘I++q → (p++q)∘I] (L∘X∘X++V)∘I
········L∘X∘X++V [p++V → p∘V] L∘X∘X∘V
···L∘X∘X∘V∘I∘I∘I∘I∘I [p∘I∘I∘I∘I∘I → p∘V] L∘X∘X∘V∘V
···L∘X∘X∘V∘V [p∘V∘V → p∘X] L∘X∘X∘X
···I××I [p××I → p] I
··L∘X∘X∘X++I [p++I → p∘I] L∘X∘X∘X∘I
·/(L∘X∘X∘X∘I) [/(p∘n) → (/p).n] (/(L∘X∘X∘X)).I
··/(L∘X∘X∘X) [/(p∘n) → (/p).n] (/(L∘X∘X)).X
···/(L∘X∘X) [/(p∘n) → (/p).n] (/(L∘X)).X
····/(L∘X) [/(p∘n) → (/p).n] (/L).X
·····/L [/j → j] L
L.X.X.X.I

⍝ Roman long division example:

roman trace eval'C.X.L.V ÷ V.I'           ⍝ 145 ÷ 6 → 24
·C.X.L.V÷V.I [p÷q → /divqr(\p;\q)] /divqr(\C.X.L.V;\V.I)
·····\C.X.L.V [\p.n → \p∘n] \C.X.L∘V
······\C.X.L [\p.X.L → \p∘X∘X∘X∘X] \C∘X∘X∘X∘X
··········\C [\j → j] C
·····\V.I [\p.n → \p∘n] \V∘I
······\V [\j → j] V
···qr(C∘X∘X∘X∘X∘V;V∘I) [qr(p;q) → dv(p;sh(p;q;⊥);nulla)] dv(C∘X∘X∘X∘X∘V;sh(C∘X∘X∘X∘X∘V;V∘I;⊥);nulla)
······sh(C∘X∘X∘X∘X∘V;V∘I;⊥) [sh(p;q;r) → sh'(p;q;r;(p?q))] sh'(C∘X∘X∘X∘X∘V;V∘I;⊥;(C∘X∘X∘X∘X∘V?V∘I))
········C∘X∘X∘X∘X∘V?V∘I [p?q → (⌽p)??⌽q] (⌽C∘X∘X∘X∘X∘V)??⌽V∘I
·········⌽C∘X∘X∘X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(C∘X∘X∘X∘X;V)
·········⌽⌽(C∘X∘X∘X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X∘X;X∘V)
·········⌽⌽(C∘X∘X∘X;X∘V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X;X∘(X∘V))
·········⌽⌽(C∘X∘X;X∘(X∘V)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X;X∘(X∘(X∘V)))
·········⌽⌽(C∘X;X∘(X∘(X∘V))) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C;X∘(X∘(X∘(X∘V))))
·········⌽⌽(C;X∘(X∘(X∘(X∘V)))) [⌽⌽(j;r) → j∘r] C∘(X∘(X∘(X∘(X∘V))))
·········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
·········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
········C∘(X∘(X∘(X∘(X∘V))))??V∘I [m∘p??n∘q → (m??n)∘(p??q)] (C??V)∘(X∘(X∘(X∘(X∘V)))??I)
·········C??V [m??V → gt] gt
·········X∘(X∘(X∘(X∘V)))??I [m∘p??n → (m??n)∘gt] (X??I)∘gt
··········X??I [m??I → gt] gt
········· gt   ∘  ¯1  gt  [gt∘q → gt] gt
········ gt   ∘  ¯1  gt  [gt∘q → gt] gt
······sh'(C∘X∘X∘X∘X∘V;V∘I;⊥;gt) [sh'(p;q;r;s) → sh(p;10(q);(q;r))] sh(C∘X∘X∘X∘X∘V;10(V∘I);(V∘I;⊥))
·········10(V∘I) [10(p∘n) → (10(p))∘10(n)] (10(V))∘10(I)
··········10(V) [10(V) → L] L
··········10(I) [10(I) → X] X
······sh(C∘X∘X∘X∘X∘V;L∘X;(V∘I;⊥)) [sh(p;q;r) → sh'(p;q;r;(p?q))] sh'(C∘X∘X∘X∘X∘V;L∘X;(V∘I;⊥);(C∘X∘X∘X∘X∘V?L∘X))
········C∘X∘X∘X∘X∘V?L∘X [p?q → (⌽p)??⌽q] (⌽C∘X∘X∘X∘X∘V)??⌽L∘X
·········⌽C∘X∘X∘X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(C∘X∘X∘X∘X;V)
·········⌽⌽(C∘X∘X∘X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X∘X;X∘V)
·········⌽⌽(C∘X∘X∘X;X∘V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X;X∘(X∘V))
·········⌽⌽(C∘X∘X;X∘(X∘V)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X;X∘(X∘(X∘V)))
·········⌽⌽(C∘X;X∘(X∘(X∘V))) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C;X∘(X∘(X∘(X∘V))))
·········⌽⌽(C;X∘(X∘(X∘(X∘V)))) [⌽⌽(j;r) → j∘r] C∘(X∘(X∘(X∘(X∘V))))
·········⌽L∘X [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(L;X)
·········⌽⌽(L;X) [⌽⌽(j;r) → j∘r] L∘X
········C∘(X∘(X∘(X∘(X∘V))))??L∘X [m∘p??n∘q → (m??n)∘(p??q)] (C??L)∘(X∘(X∘(X∘(X∘V)))??X)
·········C??L [m??L → gt] gt
·········X∘(X∘(X∘(X∘V)))??X [m∘p??n → (m??n)∘gt] (X??X)∘gt
··········X??X [m??m → eq] eq
········· eq   ∘  ¯1  gt  [eq∘q → q] gt
········ gt   ∘  ¯1  gt  [gt∘q → gt] gt
······sh'(C∘X∘X∘X∘X∘V;L∘X;(V∘I;⊥);gt) [sh'(p;q;r;s) → sh(p;10(q);(q;r))] sh(C∘X∘X∘X∘X∘V;10(L∘X);(L∘X;(V∘I;⊥)))
·········10(L∘X) [10(p∘n) → (10(p))∘10(n)] (10(L))∘10(X)
··········10(L) [10(L) → D] D
··········10(X) [10(X) → C] C
······sh(C∘X∘X∘X∘X∘V;D∘C;(L∘X;(V∘I;⊥))) [sh(p;q;r) → sh'(p;q;r;(p?q))] sh'(C∘X∘X∘X∘X∘V;D∘C;(L∘X;(V∘I;⊥));(C∘X∘X∘X∘X∘V?D∘C))
········C∘X∘X∘X∘X∘V?D∘C [p?q → (⌽p)??⌽q] (⌽C∘X∘X∘X∘X∘V)??⌽D∘C
·········⌽C∘X∘X∘X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(C∘X∘X∘X∘X;V)
·········⌽⌽(C∘X∘X∘X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X∘X;X∘V)
·········⌽⌽(C∘X∘X∘X;X∘V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X;X∘(X∘V))
·········⌽⌽(C∘X∘X;X∘(X∘V)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X;X∘(X∘(X∘V)))
·········⌽⌽(C∘X;X∘(X∘(X∘V))) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C;X∘(X∘(X∘(X∘V))))
·········⌽⌽(C;X∘(X∘(X∘(X∘V)))) [⌽⌽(j;r) → j∘r] C∘(X∘(X∘(X∘(X∘V))))
·········⌽D∘C [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(D;C)
·········⌽⌽(D;C) [⌽⌽(j;r) → j∘r] D∘C
········C∘(X∘(X∘(X∘(X∘V))))??D∘C [m∘p??n∘q → (m??n)∘(p??q)] (C??D)∘(X∘(X∘(X∘(X∘V)))??C)
·········C??D [C??n → lt] lt
·········X∘(X∘(X∘(X∘V)))??C [m∘p??n → (m??n)∘gt] (X??C)∘gt
··········X??C [X??n → lt] lt
········· lt   ∘  ¯1  gt  [lt∘q → lt] lt
········ lt   ∘  ¯1  lt  [lt∘q → lt] lt
······sh'(C∘X∘X∘X∘X∘V;D∘C;(L∘X;(V∘I;⊥));lt) [sh'(p;q;r;lt) → r] L∘X;(V∘I;⊥)
···dv(C∘X∘X∘X∘X∘V;(L∘X;(V∘I;⊥));nulla) [dv(p;(q;s);r) → dv'(r;s;sb(p;q;nulla))] dv'(nulla;(V∘I;⊥);sb(C∘X∘X∘X∘X∘V;L∘X;nulla))
·····sb(C∘X∘X∘X∘X∘V;L∘X;nulla) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(C∘X∘X∘X∘X∘V;L∘X;nulla;(C∘X∘X∘X∘X∘V?L∘X))
·······C∘X∘X∘X∘X∘V?L∘X [p?q → (⌽p)??⌽q] (⌽C∘X∘X∘X∘X∘V)??⌽L∘X
········⌽C∘X∘X∘X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(C∘X∘X∘X∘X;V)
········⌽⌽(C∘X∘X∘X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X∘X;X∘V)
········⌽⌽(C∘X∘X∘X;X∘V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X∘X;X∘(X∘V))
········⌽⌽(C∘X∘X;X∘(X∘V)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C∘X;X∘(X∘(X∘V)))
········⌽⌽(C∘X;X∘(X∘(X∘V))) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(C;X∘(X∘(X∘(X∘V))))
········⌽⌽(C;X∘(X∘(X∘(X∘V)))) [⌽⌽(j;r) → j∘r] C∘(X∘(X∘(X∘(X∘V))))
········⌽L∘X [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(L;X)
········⌽⌽(L;X) [⌽⌽(j;r) → j∘r] L∘X
·······C∘(X∘(X∘(X∘(X∘V))))??L∘X [m∘p??n∘q → (m??n)∘(p??q)] (C??L)∘(X∘(X∘(X∘(X∘V)))??X)
········C??L [m??L → gt] gt
········X∘(X∘(X∘(X∘V)))??X [m∘p??n → (m??n)∘gt] (X??X)∘gt
·········X??X [m??m → eq] eq
········ eq   ∘  ¯1  gt  [eq∘q → q] gt
······· gt   ∘  ¯1  gt  [gt∘q → gt] gt
·····sb'(C∘X∘X∘X∘X∘V;L∘X;nulla;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(C∘X∘X∘X∘X∘V--L∘X;L∘X;nulla∘I)
········C∘X∘X∘X∘X∘V--L∘X [p--q∘m → p--q--m] C∘X∘X∘X∘X∘V--L--X
·········C∘X∘X∘X∘X∘V--L [p∘m--r → (p--r)++m] (C∘X∘X∘X∘X--L)++V
··········C∘X∘X∘X∘X--L [p∘m--r → (p--r)++m] (C∘X∘X∘X--L)++X
···········C∘X∘X∘X--L [p∘m--r → (p--r)++m] (C∘X∘X--L)++X
············C∘X∘X--L [p∘m--r → (p--r)++m] (C∘X--L)++X
·············C∘X--L [p∘m--r → (p--r)++m] (C--L)++X
··············C--L [C--L → L] L
·············L++X [p++X → p∘X] L∘X
············L∘X++X [p++X → p∘X] L∘X∘X
···········L∘X∘X++X [p++X → p∘X] L∘X∘X∘X
··········L∘X∘X∘X++X [p++X → p∘X] L∘X∘X∘X∘X
·········L∘X∘X∘X∘X++V [p++V → p∘V] L∘X∘X∘X∘X∘V
········L∘X∘X∘X∘X∘V--X [p∘m--r → (p--r)++m] (L∘X∘X∘X∘X--X)++V
·········L∘X∘X∘X∘X--X [p∘m--m → p] L∘X∘X∘X
········L∘X∘X∘X++V [p++V → p∘V] L∘X∘X∘X∘V
·····sb(L∘X∘X∘X∘V;L∘X;nulla∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(L∘X∘X∘X∘V;L∘X;nulla∘I;(L∘X∘X∘X∘V?L∘X))
·······L∘X∘X∘X∘V?L∘X [p?q → (⌽p)??⌽q] (⌽L∘X∘X∘X∘V)??⌽L∘X
········⌽L∘X∘X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(L∘X∘X∘X;V)
········⌽⌽(L∘X∘X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(L∘X∘X;X∘V)
········⌽⌽(L∘X∘X;X∘V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(L∘X;X∘(X∘V))
········⌽⌽(L∘X;X∘(X∘V)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(L;X∘(X∘(X∘V)))
········⌽⌽(L;X∘(X∘(X∘V))) [⌽⌽(j;r) → j∘r] L∘(X∘(X∘(X∘V)))
········⌽L∘X [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(L;X)
········⌽⌽(L;X) [⌽⌽(j;r) → j∘r] L∘X
·······L∘(X∘(X∘(X∘V)))??L∘X [m∘p??n∘q → (m??n)∘(p??q)] (L??L)∘(X∘(X∘(X∘V))??X)
········L??L [m??m → eq] eq
········X∘(X∘(X∘V))??X [m∘p??n → (m??n)∘gt] (X??X)∘gt
·········X??X [m??m → eq] eq
········ eq   ∘  ¯1  gt  [eq∘q → q] gt
······· eq   ∘  ¯1  gt  [eq∘q → q] gt
·····sb'(L∘X∘X∘X∘V;L∘X;nulla∘I;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(L∘X∘X∘X∘V--L∘X;L∘X;nulla∘I∘I)
········L∘X∘X∘X∘V--L∘X [p--q∘m → p--q--m] L∘X∘X∘X∘V--L--X
·········L∘X∘X∘X∘V--L [p∘m--r → (p--r)++m] (L∘X∘X∘X--L)++V
··········L∘X∘X∘X--L [p∘m--r → (p--r)++m] (L∘X∘X--L)++X
···········L∘X∘X--L [p∘m--r → (p--r)++m] (L∘X--L)++X
············L∘X--L [p∘m--r → (p--r)++m] (L--L)++X
·············L--L [m--m → nulla] nulla
············nulla++X [i++q → q] X
···········X++X [p++X → p∘X] X∘X
··········X∘X++X [p++X → p∘X] X∘X∘X
·········X∘X∘X++V [p++V → p∘V] X∘X∘X∘V
········X∘X∘X∘V--X [p∘m--r → (p--r)++m] (X∘X∘X--X)++V
·········X∘X∘X--X [p∘m--m → p] X∘X
········X∘X++V [p++V → p∘V] X∘X∘V
·····sb(X∘X∘V;L∘X;nulla∘I∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(X∘X∘V;L∘X;nulla∘I∘I;(X∘X∘V?L∘X))
·······X∘X∘V?L∘X [p?q → (⌽p)??⌽q] (⌽X∘X∘V)??⌽L∘X
········⌽X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(X∘X;V)
········⌽⌽(X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X;X∘V)
········⌽⌽(X;X∘V) [⌽⌽(j;r) → j∘r] X∘(X∘V)
········⌽L∘X [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(L;X)
········⌽⌽(L;X) [⌽⌽(j;r) → j∘r] L∘X
·······X∘(X∘V)??L∘X [m∘p??n∘q → (m??n)∘(p??q)] (X??L)∘(X∘V??X)
········X??L [X??n → lt] lt
········X∘V??X [m∘p??n → (m??n)∘gt] (X??X)∘gt
·········X??X [m??m → eq] eq
········ eq   ∘  ¯1  gt  [eq∘q → q] gt
······· lt   ∘  ¯1  gt  [lt∘q → lt] lt
·····sb'(X∘X∘V;L∘X;nulla∘I∘I;lt) [sb'(p;q;r;lt) → r;p] nulla∘I∘I;X∘X∘V
···dv'(nulla;(V∘I;⊥);(nulla∘I∘I;X∘X∘V)) [dv'(r;s;(p;q)) → dv"(q;s;p++10(r))] dv"(X∘X∘V;(V∘I;⊥);nulla∘I∘I++10(nulla))
······10(nulla) [10(j) → j] nulla
·····nulla∘I∘I++nulla [p++i → p] nulla∘I∘I
···dv"(X∘X∘V;(V∘I;⊥);nulla∘I∘I) [dv"(p;q;r) → dv(p;q;r)] dv(X∘X∘V;(V∘I;⊥);nulla∘I∘I)
···dv(X∘X∘V;(V∘I;⊥);nulla∘I∘I) [dv(p;(q;s);r) → dv'(r;s;sb(p;q;nulla))] dv'(nulla∘I∘I;⊥;sb(X∘X∘V;V∘I;nulla))
·····sb(X∘X∘V;V∘I;nulla) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(X∘X∘V;V∘I;nulla;(X∘X∘V?V∘I))
·······X∘X∘V?V∘I [p?q → (⌽p)??⌽q] (⌽X∘X∘V)??⌽V∘I
········⌽X∘X∘V [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(X∘X;V)
········⌽⌽(X∘X;V) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X;X∘V)
········⌽⌽(X;X∘V) [⌽⌽(j;r) → j∘r] X∘(X∘V)
········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
·······X∘(X∘V)??V∘I [m∘p??n∘q → (m??n)∘(p??q)] (X??V)∘(X∘V??I)
········X??V [m??V → gt] gt
········X∘V??I [m∘p??n → (m??n)∘gt] (X??I)∘gt
·········X??I [m??I → gt] gt
········ gt   ∘  ¯1  gt  [gt∘q → gt] gt
······· gt   ∘  ¯1  gt  [gt∘q → gt] gt
·····sb'(X∘X∘V;V∘I;nulla;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(X∘X∘V--V∘I;V∘I;nulla∘I)
········X∘X∘V--V∘I [p--q∘m → p--q--m] X∘X∘V--V--I
·········X∘X∘V--V [p∘m--m → p] X∘X
········X∘X--I [p∘m--r → (p--r)++m] (X--I)++X
·········X--I [X--I → V∘I∘I∘I∘I] V∘I∘I∘I∘I
········V∘I∘I∘I∘I++X [p∘I++q → (p++q)∘I] (V∘I∘I∘I++X)∘I
·········V∘I∘I∘I++X [p∘I++q → (p++q)∘I] (V∘I∘I++X)∘I
··········V∘I∘I++X [p∘I++q → (p++q)∘I] (V∘I++X)∘I
···········V∘I++X [p∘I++q → (p++q)∘I] (V++X)∘I
············V++X [V++q → q∘V] X∘V
·····sb(X∘V∘I∘I∘I∘I;V∘I;nulla∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(X∘V∘I∘I∘I∘I;V∘I;nulla∘I;(X∘V∘I∘I∘I∘I?V∘I))
·······X∘V∘I∘I∘I∘I?V∘I [p?q → (⌽p)??⌽q] (⌽X∘V∘I∘I∘I∘I)??⌽V∘I
········⌽X∘V∘I∘I∘I∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(X∘V∘I∘I∘I;I)
········⌽⌽(X∘V∘I∘I∘I;I) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X∘V∘I∘I;I∘I)
········⌽⌽(X∘V∘I∘I;I∘I) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X∘V∘I;I∘(I∘I))
········⌽⌽(X∘V∘I;I∘(I∘I)) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X∘V;I∘(I∘(I∘I)))
········⌽⌽(X∘V;I∘(I∘(I∘I))) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X;V∘(I∘(I∘(I∘I))))
········⌽⌽(X;V∘(I∘(I∘(I∘I)))) [⌽⌽(j;r) → j∘r] X∘(V∘(I∘(I∘(I∘I))))
········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
·······X∘(V∘(I∘(I∘(I∘I))))??V∘I [m∘p??n∘q → (m??n)∘(p??q)] (X??V)∘(V∘(I∘(I∘(I∘I)))??I)
········X??V [m??V → gt] gt
········V∘(I∘(I∘(I∘I)))??I [m∘p??n → (m??n)∘gt] (V??I)∘gt
·········V??I [m??I → gt] gt
········ gt   ∘  ¯1  gt  [gt∘q → gt] gt
······· gt   ∘  ¯1  gt  [gt∘q → gt] gt
·····sb'(X∘V∘I∘I∘I∘I;V∘I;nulla∘I;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(X∘V∘I∘I∘I∘I--V∘I;V∘I;nulla∘I∘I)
········X∘V∘I∘I∘I∘I--V∘I [p--q∘m → p--q--m] X∘V∘I∘I∘I∘I--V--I
·········X∘V∘I∘I∘I∘I--V [p∘m--r → (p--r)++m] (X∘V∘I∘I∘I--V)++I
··········X∘V∘I∘I∘I--V [p∘m--r → (p--r)++m] (X∘V∘I∘I--V)++I
···········X∘V∘I∘I--V [p∘m--r → (p--r)++m] (X∘V∘I--V)++I
············X∘V∘I--V [p∘m--r → (p--r)++m] (X∘V--V)++I
·············X∘V--V [p∘m--m → p] X
············X++I [p++I → p∘I] X∘I
···········X∘I++I [p++I → p∘I] X∘I∘I
··········X∘I∘I++I [p++I → p∘I] X∘I∘I∘I
·········X∘I∘I∘I++I [p++I → p∘I] X∘I∘I∘I∘I
········X∘I∘I∘I∘I--I [p∘m--m → p] X∘I∘I∘I
·····sb(X∘I∘I∘I;V∘I;nulla∘I∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(X∘I∘I∘I;V∘I;nulla∘I∘I;(X∘I∘I∘I?V∘I))
·······X∘I∘I∘I?V∘I [p?q → (⌽p)??⌽q] (⌽X∘I∘I∘I)??⌽V∘I
········⌽X∘I∘I∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(X∘I∘I;I)
········⌽⌽(X∘I∘I;I) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X∘I;I∘I)
········⌽⌽(X∘I;I∘I) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(X;I∘(I∘I))
········⌽⌽(X;I∘(I∘I)) [⌽⌽(j;r) → j∘r] X∘(I∘(I∘I))
········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
·······X∘(I∘(I∘I))??V∘I [m∘p??n∘q → (m??n)∘(p??q)] (X??V)∘(I∘(I∘I)??I)
········X??V [m??V → gt] gt
········I∘(I∘I)??I [m∘p??n → (m??n)∘gt] (I??I)∘gt
·········I??I [m??m → eq] eq
········ eq   ∘  ¯1  gt  [eq∘q → q] gt
······· gt   ∘  ¯1  gt  [gt∘q → gt] gt
·····sb'(X∘I∘I∘I;V∘I;nulla∘I∘I;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(X∘I∘I∘I--V∘I;V∘I;nulla∘I∘I∘I)
········X∘I∘I∘I--V∘I [p--q∘m → p--q--m] X∘I∘I∘I--V--I
·········X∘I∘I∘I--V [p∘m--r → (p--r)++m] (X∘I∘I--V)++I
··········X∘I∘I--V [p∘m--r → (p--r)++m] (X∘I--V)++I
···········X∘I--V [p∘m--r → (p--r)++m] (X--V)++I
············X--V [X--V → V] V
···········V++I [p++I → p∘I] V∘I
··········V∘I++I [p++I → p∘I] V∘I∘I
·········V∘I∘I++I [p++I → p∘I] V∘I∘I∘I
········V∘I∘I∘I--I [p∘m--m → p] V∘I∘I
·····sb(V∘I∘I;V∘I;nulla∘I∘I∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(V∘I∘I;V∘I;nulla∘I∘I∘I;(V∘I∘I?V∘I))
·······V∘I∘I?V∘I [p?q → (⌽p)??⌽q] (⌽V∘I∘I)??⌽V∘I
········⌽V∘I∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V∘I;I)
········⌽⌽(V∘I;I) [⌽⌽(p∘q;r) → ⌽⌽(p;q∘r)] ⌽⌽(V;I∘I)
········⌽⌽(V;I∘I) [⌽⌽(j;r) → j∘r] V∘(I∘I)
········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
·······V∘(I∘I)??V∘I [m∘p??n∘q → (m??n)∘(p??q)] (V??V)∘(I∘I??I)
········V??V [m??m → eq] eq
········I∘I??I [m∘p??n → (m??n)∘gt] (I??I)∘gt
·········I??I [m??m → eq] eq
········ eq   ∘  ¯1  gt  [eq∘q → q] gt
······· eq   ∘  ¯1  gt  [eq∘q → q] gt
·····sb'(V∘I∘I;V∘I;nulla∘I∘I∘I;gt) [sb'(p;q;r;s) → sb(p--q;q;r∘I)] sb(V∘I∘I--V∘I;V∘I;nulla∘I∘I∘I∘I)
········V∘I∘I--V∘I [p--q∘m → p--q--m] V∘I∘I--V--I
·········V∘I∘I--V [p∘m--r → (p--r)++m] (V∘I--V)++I
··········V∘I--V [p∘m--r → (p--r)++m] (V--V)++I
···········V--V [m--m → nulla] nulla
··········nulla++I [i++q → q] I
·········I++I [p++I → p∘I] I∘I
········I∘I--I [p∘m--m → p] I
·····sb(I;V∘I;nulla∘I∘I∘I∘I) [sb(p;q;r) → sb'(p;q;r;(p?q))] sb'(I;V∘I;nulla∘I∘I∘I∘I;(I?V∘I))
·······I?V∘I [p?q → (⌽p)??⌽q] (⌽I)??⌽V∘I
········⌽I [⌽j → j] I
········⌽V∘I [⌽p∘q → ⌽⌽(p;q)] ⌽⌽(V;I)
········⌽⌽(V;I) [⌽⌽(j;r) → j∘r] V∘I
·······I??V∘I [m??n∘q → (m??n)∘lt] (I??V)∘lt
········I??V [I??n → lt] lt
······· lt   ∘  ¯1  lt  [lt∘q → lt] lt
·····sb'(I;V∘I;nulla∘I∘I∘I∘I;lt) [sb'(p;q;r;lt) → r;p] nulla∘I∘I∘I∘I;I
···dv'(nulla∘I∘I;⊥;(nulla∘I∘I∘I∘I;I)) [dv'(r;s;(p;q)) → dv"(q;s;p++10(r))] dv"(I;⊥;nulla∘I∘I∘I∘I++10(nulla∘I∘I))
······10(nulla∘I∘I) [10(p∘n) → (10(p))∘10(n)] (10(nulla∘I))∘10(I)
·······10(nulla∘I) [10(p∘n) → (10(p))∘10(n)] (10(nulla))∘10(I)
········10(nulla) [10(j) → j] nulla
········10(I) [10(I) → X] X
·······10(I) [10(I) → X] X
·····nulla∘I∘I∘I∘I++nulla∘X∘X [p∘I++q → (p++q)∘I] (nulla∘I∘I∘I++nulla∘X∘X)∘I
······nulla∘I∘I∘I++nulla∘X∘X [p∘I++q → (p++q)∘I] (nulla∘I∘I++nulla∘X∘X)∘I
·······nulla∘I∘I++nulla∘X∘X [p∘I++q → (p++q)∘I] (nulla∘I++nulla∘X∘X)∘I
········nulla∘I++nulla∘X∘X [p∘I++q → (p++q)∘I] (nulla++nulla∘X∘X)∘I
·········nulla++nulla∘X∘X [i++q → q] nulla∘X∘X
···dv"(I;⊥;nulla∘X∘X∘I∘I∘I∘I) [dv"(r;⊥;q) → q;r] nulla∘X∘X∘I∘I∘I∘I;I
··div(nulla∘X∘X∘I∘I∘I∘I;I) [div(q;r) → q] nulla∘X∘X∘I∘I∘I∘I
·/(nulla∘X∘X∘I∘I∘I∘I) [/(p∘n) → (/p).n] (/(nulla∘X∘X∘I∘I∘I)).I
··/(nulla∘X∘X∘I∘I∘I) [/(p∘n) → (/p).n] (/(nulla∘X∘X∘I∘I)).I
···/(nulla∘X∘X∘I∘I) [/(p∘n) → (/p).n] (/(nulla∘X∘X∘I)).I
····/(nulla∘X∘X∘I) [/(p∘n) → (/p).n] (/(nulla∘X∘X)).I
·····/(nulla∘X∘X) [/(p∘n) → (/p).n] (/(nulla∘X)).X
······/(nulla∘X) [/(p∘n) → (/p).n] (/nulla).X
·······/nulla [/j → j] nulla
······nulla.X [i.q → q] X
·X.X.I.I.I.I [p.I.I.I.I → p.I.V] X.X.I.V
X.X.I.V