diff --git a/testsuite/tests/input/tex/Bussproofs.test.ts b/testsuite/tests/input/tex/Bussproofs.test.ts index c4ef5a2b3..2b29bd9e5 100644 --- a/testsuite/tests/input/tex/Bussproofs.test.ts +++ b/testsuite/tests/input/tex/Bussproofs.test.ts @@ -12,7 +12,7 @@ describe('BussproofsRegInf', () => { ` - + A @@ -31,9 +31,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -45,9 +43,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -69,9 +65,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -79,9 +73,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -93,9 +85,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -117,9 +107,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -127,9 +115,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -137,9 +123,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -151,9 +135,7 @@ describe('BussproofsRegInf', () => { - - D - + D @@ -175,9 +157,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -185,9 +165,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -195,9 +173,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -205,9 +181,7 @@ describe('BussproofsRegInf', () => { - - D - + D @@ -219,9 +193,7 @@ describe('BussproofsRegInf', () => { - - E - + E @@ -243,9 +215,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -253,9 +223,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -263,9 +231,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -273,9 +239,7 @@ describe('BussproofsRegInf', () => { - - D - + D @@ -283,9 +247,7 @@ describe('BussproofsRegInf', () => { - - E - + E @@ -297,9 +259,7 @@ describe('BussproofsRegInf', () => { - - F - + F @@ -315,7 +275,7 @@ describe('BussproofsRegInf', () => { ` - + L @@ -327,9 +287,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -341,9 +299,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -367,9 +323,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -381,16 +335,14 @@ describe('BussproofsRegInf', () => { - - B - + B - + R @@ -405,7 +357,7 @@ describe('BussproofsRegInf', () => { ` - + L @@ -417,9 +369,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -431,16 +381,14 @@ describe('BussproofsRegInf', () => { - - B - + B - + R @@ -453,7 +401,7 @@ describe('BussproofsRegInf', () => { ` - + A @@ -472,9 +420,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -486,9 +432,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -508,9 +452,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -518,9 +460,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -532,9 +472,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -556,9 +494,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -566,9 +502,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -576,9 +510,7 @@ describe('BussproofsRegInf', () => { - - C - + C @@ -590,9 +522,7 @@ describe('BussproofsRegInf', () => { - - D - + D @@ -608,7 +538,7 @@ describe('BussproofsRegInf', () => { ` - + L @@ -620,9 +550,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -634,9 +562,7 @@ describe('BussproofsRegInf', () => { - - B - + B @@ -660,9 +586,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -674,16 +598,14 @@ describe('BussproofsRegInf', () => { - - B - + B - + R @@ -698,7 +620,7 @@ describe('BussproofsRegInf', () => { ` - + L @@ -710,9 +632,7 @@ describe('BussproofsRegInf', () => { - - A - + A @@ -724,16 +644,14 @@ describe('BussproofsRegInf', () => { - - B - + B - + R @@ -758,9 +676,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -775,9 +691,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -791,9 +705,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -801,9 +713,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -815,15 +725,13 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + @@ -838,9 +746,7 @@ describe('BussproofsRegProofs', () => { - - E - + E @@ -857,9 +763,7 @@ describe('BussproofsRegProofs', () => { - - F - + F @@ -891,9 +795,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -908,9 +810,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -924,9 +824,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -934,9 +832,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -948,15 +844,13 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + @@ -971,9 +865,7 @@ describe('BussproofsRegProofs', () => { - - E - + E @@ -990,9 +882,7 @@ describe('BussproofsRegProofs', () => { - - F - + F @@ -1034,9 +924,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -1044,9 +932,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -1054,9 +940,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -1068,9 +952,7 @@ describe('BussproofsRegProofs', () => { - - Q - + Q @@ -1089,9 +971,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -1105,9 +985,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -1115,9 +993,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -1129,15 +1005,13 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + @@ -1152,9 +1026,7 @@ describe('BussproofsRegProofs', () => { - - E - + E @@ -1171,9 +1043,7 @@ describe('BussproofsRegProofs', () => { - - F - + F @@ -1187,9 +1057,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -1201,13 +1069,11 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + @@ -1252,9 +1118,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -1262,9 +1126,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -1272,9 +1134,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -1286,9 +1146,7 @@ describe('BussproofsRegProofs', () => { - - Q - + Q @@ -1308,9 +1166,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -1326,9 +1182,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -1336,9 +1190,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -1350,24 +1202,20 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + - - AAAA - + AAAA @@ -1381,18 +1229,14 @@ describe('BussproofsRegProofs', () => { - - E - + E - - BBB - + BBB @@ -1406,18 +1250,14 @@ describe('BussproofsRegProofs', () => { - - F - + F - - CCCCC - + CCCCC @@ -1429,9 +1269,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -1443,20 +1281,18 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + - + QERE @@ -1474,7 +1310,7 @@ describe('BussproofsRegProofs', () => { - + QERE @@ -1491,9 +1327,7 @@ describe('BussproofsRegProofs', () => { - - CCCCC - + CCCCC @@ -1511,9 +1345,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -1521,9 +1353,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -1531,9 +1361,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -1545,9 +1373,7 @@ describe('BussproofsRegProofs', () => { - - Q - + Q @@ -1560,9 +1386,7 @@ describe('BussproofsRegProofs', () => { - - BBB - + BBB @@ -1572,9 +1396,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -1582,9 +1404,7 @@ describe('BussproofsRegProofs', () => { - - AAAA - + AAAA @@ -1594,9 +1414,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -1604,9 +1422,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -1618,15 +1434,13 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + @@ -1642,9 +1456,7 @@ describe('BussproofsRegProofs', () => { - - E - + E @@ -1662,9 +1474,7 @@ describe('BussproofsRegProofs', () => { - - F - + F @@ -1680,9 +1490,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -1694,13 +1502,11 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + @@ -1720,7 +1526,7 @@ describe('BussproofsRegProofs', () => { - + DD @@ -1737,9 +1543,7 @@ describe('BussproofsRegProofs', () => { - - CCCCC - + CCCCC @@ -1757,9 +1561,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -1767,9 +1569,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -1777,9 +1577,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -1791,9 +1589,7 @@ describe('BussproofsRegProofs', () => { - - Q - + Q @@ -1806,9 +1602,7 @@ describe('BussproofsRegProofs', () => { - - BBB - + BBB @@ -1818,9 +1612,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -1836,9 +1628,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -1846,9 +1636,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -1860,24 +1648,20 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + - - AAAA - + AAAA @@ -1891,9 +1675,7 @@ describe('BussproofsRegProofs', () => { - - E - + E @@ -1911,9 +1693,7 @@ describe('BussproofsRegProofs', () => { - - F - + F @@ -1929,9 +1709,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -1943,20 +1721,18 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + - + QERE @@ -2000,9 +1776,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -2010,9 +1784,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -2020,9 +1792,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -2034,18 +1804,14 @@ describe('BussproofsRegProofs', () => { - - Q - + Q - - AAAA - + AAAA @@ -2062,9 +1828,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -2080,9 +1844,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -2090,9 +1852,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -2104,24 +1864,20 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + - - Nowhere - + Nowhere @@ -2135,18 +1891,14 @@ describe('BussproofsRegProofs', () => { - - E - + E - - BBB - + BBB @@ -2160,18 +1912,14 @@ describe('BussproofsRegProofs', () => { - - F - + F - - CCCCC - + CCCCC @@ -2203,9 +1951,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -2217,18 +1963,14 @@ describe('BussproofsRegProofs', () => { - - More and more - + More and more - - QERE - + QERE @@ -2242,9 +1984,7 @@ describe('BussproofsRegProofs', () => { - - More and more - + More and more @@ -2259,9 +1999,7 @@ describe('BussproofsRegProofs', () => { - - More and more - + More and more @@ -2276,13 +2014,11 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + @@ -2297,636 +2033,584 @@ describe('BussproofsRegProofs', () => { tex2mml( '\\begin{prooftree}\\AXC{}\\RL{$Hyp^{1}$}\\UIC{$P$}\\AXC{$P\\rightarrow Q$}\\RL{$\\rightarrow_E$}\\solidLine\\BIC{$Q^2$}\\AXC{$Q\\rightarrow R$} \\RL{$\\rightarrow_E$} \\BIC{$R$} \\AXC{$Q$}\\RL{Rit$^2$} \\UIC{$Q$}\\RL{$\\wedge_I$}\\BIC{$Q\\wedge R$}\\RL{${\\rightarrow_I}^1$}\\UIC{$P\\rightarrow Q\\wedge R$}\\end{prooftree}' ), - ` - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - P + ` + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + P + + - - + + + + + + H + y + + p + + 1 + + - - - - - + + + + + + + - H - y - - p - - 1 - - + P + → + Q - - - - - - - - - - - P - → - Q + - - + + + + + + + + + + + + Q + 2 + - - - - - - - - - - - - - Q - 2 - + - - + + + + + + + → + E + - - - - - - - - → - E - - - - - - - - - - - - - - Q - → - R + + - - - - - - - - - - - - - - - R - - - - - - - - - - - - → - E - - - - - - - - - - - - - - - - + + + + + + + Q + → + R + + + + + + + + - - + + - - - Q - - + + R + - - - - - - - - - Q - - - - - - - - - - Rit - - - - 2 - + + + + → + E + + + - - - - + + + + + + + + + + + + + + + + + Q + + + + + + + + + + + + + + Q + + + + + + + + + Rit + + + + 2 + + + + + + + + + + + + + + + + + + Q + ∧ + R - - - - - - - - - - - - Q - ∧ - R + - - + + + + + + + ∧ + I + - - - - - - - - ∧ - I - - - - + + + + - - + + + + + + + + + + + P + → + Q + ∧ + R - - - - - - - - - - - - P - → - Q - ∧ - R + - - - - - - - - - - - - - → - I - + + + + + + + + + + → + I + + + 1 + - 1 - - - - + + + + + - - - -` + ` )); it('Proof Mixing Order', () => toXmlMatch( tex2mml( - '\\begin{prooftree}\\alwaysRootAtTop\\AXC{}\\RL{$Hyp^{1}$}\\UIC{$P$}\\AXC{$P\\rightarrow Q$}\\RL{$\\rightarrow_E$}\\solidLine\\BIC{$Q^2$}\\alwaysRootAtBottom\\AXC{$Q\\rightarrow R$} \\RL{$\\rightarrow_E$} \\BIC{$R$} \\AXC{$Q$}\\RL{Rit$^2$} \\UIC{$Q$}\\RL{$\\wedge_I$}\\BIC{$Q\\wedge R$}\\RL{${\\rightarrow_I}^1$}\\UIC{$P\\rightarrow Q\\wedge R$}\\end{prooftree}' + '\\begin{prooftree}\\alwaysRootAtTop\\AXC{}\\RL{$Hyp^{1}$}\\UIC{$P$}\\AXC{$P\\rightarrow Q$}\\RL{$\\rightarrow_E$}\\solidLine\\BIC{$Q^2$}\\alwaysRootAtBottom\\AXC{$Q\\rightarrow R$} \\RL{$\\rightarrow_E$} \\BIC{$R$} \\AXC{$Q$}\\RL{Rit$^2$} \\UIC{$Q$}\\RL{$\\wedge_I$}\\BIC{$Q\\wedge R$}\\RL{\${\\rightarrow_I}^1$}\\UIC{$P\\rightarrow Q\\wedge R$}\\end{prooftree}' ), - ` - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Q - 2 - + ` + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Q + 2 + + + - - - - - - - - - - - - - - - - - - - P + + + + + + + + + + + + + + + P + + + + + + + + + + + + + + + + + + + + H + y + + p + + 1 - - + - - - - - - - - - - - - - - - - + + + + + + + - H - y - - p - - 1 - - + P + → + Q - - - - - - - - - - - P - → - Q + - - - - - - - - - - - - - - → - E - - - - - - - - - - - - - - Q - → - R + + + + + + + + + + → + E + + + + - - - - - - - - - - - - - - - R - - - - - - - - - - - - → - E - - - - - - - - - - - - - - - - + + + + + + + Q + → + R + + + + + + + + - - + + - - - Q - - + + R + - - - - - - - - - Q - - - - - - - - - - Rit - - - - 2 - + + + + → + E + + + - - - - + + + + + + + + + + + + + + + + + Q + + + + + + + + + + + + + + Q + + + + + + + + + Rit + + + + 2 + + + + + + + + + + + + + + + + + + Q + ∧ + R - - - - - - - - - - - - Q - ∧ - R + - - + + + + + + + ∧ + I + - - - - - - - - ∧ - I - - - - + + + + - - + + + + + + + + + + + P + → + Q + ∧ + R - - - - - - - - - - - - P - → - Q - ∧ - R + - - - - - - - - - - - - - → - I - + + + + + + + + + + → + I + + + 1 + - 1 - - - - + + + + + - - - -` + ` )); it('Extreme', () => toXmlMatch( @@ -2938,7 +2622,7 @@ describe('BussproofsRegProofs', () => { - + BBB @@ -2954,9 +2638,7 @@ describe('BussproofsRegProofs', () => { - - WWW - + WWW @@ -2968,9 +2650,7 @@ describe('BussproofsRegProofs', () => { - - HHHHH - + HHHHH @@ -2980,9 +2660,7 @@ describe('BussproofsRegProofs', () => { - - D - + D @@ -2990,9 +2668,7 @@ describe('BussproofsRegProofs', () => { - - A1 - + A1 @@ -3000,9 +2676,7 @@ describe('BussproofsRegProofs', () => { - - A2 - + A2 @@ -3014,18 +2688,14 @@ describe('BussproofsRegProofs', () => { - - Q - + Q - - 11111111111111111 - + 11111111111111111 @@ -3035,9 +2705,7 @@ describe('BussproofsRegProofs', () => { - - BBBB - + BBBB @@ -3047,9 +2715,7 @@ describe('BussproofsRegProofs', () => { - - A - + A @@ -3058,9 +2724,7 @@ describe('BussproofsRegProofs', () => { - - qqqq - + qqqq @@ -3070,9 +2734,7 @@ describe('BussproofsRegProofs', () => { - - B - + B @@ -3080,9 +2742,7 @@ describe('BussproofsRegProofs', () => { - - R - + R @@ -3094,24 +2754,20 @@ describe('BussproofsRegProofs', () => { - - - C - → - D - → - Q - - + + C + → + D + → + Q + - - AAAA - + AAAA @@ -3125,18 +2781,14 @@ describe('BussproofsRegProofs', () => { - - E - + E - - MMM - + MMM @@ -3150,18 +2802,14 @@ describe('BussproofsRegProofs', () => { - - F - + F - - CCCCC - + CCCCC @@ -3173,9 +2821,7 @@ describe('BussproofsRegProofs', () => { - - M - + M @@ -3187,20 +2833,18 @@ describe('BussproofsRegProofs', () => { - - - N - → - R - - + + N + → + R + - + QERE