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←