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
--------
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-
er adaptations of earlier Chalcidic signs. These adapted figures and their
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.
)
See also: http://www.jimloy.com/arith/division.htm
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
See also: →#.roman←
dfns.dws/notes.roman
Back to: →Overview←