!(function (e) { var t = {}; function r(o) { if (t[o]) return t[o].exports; var n = (t[o] = { i: o, l: !1, exports: {} }); return e[o].call(n.exports, n, n.exports, r), (n.l = !0), n.exports; } (r.m = e), (r.c = t), (r.d = function (e, t, o) { r.o(e, t) || Object.defineProperty(e, t, { enumerable: !0, get: o }); }), (r.r = function (e) { "undefined" != typeof Symbol && Symbol.toStringTag && Object.defineProperty(e, Symbol.toStringTag, { value: "Module" }), Object.defineProperty(e, "__esModule", { value: !0 }); }), (r.t = function (e, t) { if ((1 & t && (e = r(e)), 8 & t)) return e; if (4 & t && "object" == typeof e && e && e.__esModule) return e; var o = Object.create(null); if ( (r.r(o), Object.defineProperty(o, "default", { enumerable: !0, value: e }), 2 & t && "string" != typeof e) ) for (var n in e) r.d( o, n, function (t) { return e[t]; }.bind(null, n), ); return o; }), (r.n = function (e) { var t = e && e.__esModule ? function () { return e.default; } : function () { return e; }; return r.d(t, "a", t), t; }), (r.o = function (e, t) { return Object.prototype.hasOwnProperty.call(e, t); }), (r.p = ""), r((r.s = 15)); })([ function (e, t, r) { "use strict"; var o, n = (this && this.__read) || function (e, t) { var r = "function" == typeof Symbol && e[Symbol.iterator]; if (!r) return e; var o, n, a = r.call(e), i = []; try { for (; (void 0 === t || t-- > 0) && !(o = a.next()).done; ) i.push(o.value); } catch (e) { n = { error: e }; } finally { try { o && !o.done && (r = a.return) && r.call(a); } finally { if (n) throw n.error; } } return i; }, a = (this && this.__values) || function (e) { var t = "function" == typeof Symbol && Symbol.iterator, r = t && e[t], o = 0; if (r) return r.call(e); if (e && "number" == typeof e.length) return { next: function () { return ( e && o >= e.length && (e = void 0), { value: e && e[o++], done: !e } ); }, }; throw new TypeError( t ? "Object is not iterable." : "Symbol.iterator is not defined.", ); }; Object.defineProperty(t, "__esModule", { value: !0 }), (t.clearDocument = t.saveDocument = t.makeBsprAttributes = t.removeProperty = t.getProperty = t.setProperty = t.balanceRules = void 0); var i = r(10), l = r(4), u = null, f = null, s = function (e) { return (f.root = e), u.outputJax.getBBox(f, u).w; }, c = function (e) { for (var t = 0; e && !i.default.isType(e, "mtable"); ) { if (i.default.isType(e, "text")) return null; i.default.isType(e, "mrow") ? ((e = e.childNodes[0]), (t = 0)) : ((e = e.parent.childNodes[t]), t++); } return e; }, d = function (e, t) { return e.childNodes["up" === t ? 1 : 0].childNodes[0].childNodes[0] .childNodes[0].childNodes[0]; }, p = function (e, t) { return e.childNodes[t].childNodes[0].childNodes[0]; }, m = function (e) { return p(e, 0); }, h = function (e) { return p(e, e.childNodes.length - 1); }, y = function (e, t) { return e.childNodes["up" === t ? 0 : 1].childNodes[0].childNodes[0] .childNodes[0]; }, v = function (e) { for (; e && !i.default.isType(e, "mtd"); ) e = e.parent; return e; }, P = function (e) { return e.parent.childNodes[e.parent.childNodes.indexOf(e) + 1]; }, g = function (e) { for (; e && null == t.getProperty(e, "inference"); ) e = e.parent; return e; }, b = function (e, t, r) { void 0 === r && (r = !1); var o = 0; if (e === t) return o; if (e !== t.parent) { var n = e.childNodes, a = r ? n.length - 1 : 0; i.default.isType(n[a], "mspace") && (o += s(n[a])), (e = t.parent); } if (e === t) return o; var l = e.childNodes, u = r ? l.length - 1 : 0; return l[u] !== t && (o += s(l[u])), o; }, x = function (e, r) { void 0 === r && (r = !1); var o = c(e), n = y(o, t.getProperty(o, "inferenceRule")); return b(e, o, r) + (s(o) - s(n)) / 2; }, M = function (e, r, o, n) { if ( (void 0 === n && (n = !1), t.getProperty(r, "inferenceRule") || t.getProperty(r, "labelledRule")) ) { var a = e.nodeFactory.create("node", "mrow"); r.parent.replaceChild(a, r), a.setChildren([r]), _(r, a), (r = a); } var u = n ? r.childNodes.length - 1 : 0, f = r.childNodes[u]; i.default.isType(f, "mspace") ? i.default.setAttribute( f, "width", l.default.Em( l.default.dimen2em(i.default.getAttribute(f, "width")) + o, ), ) : ((f = e.nodeFactory.create("node", "mspace", [], { width: l.default.Em(o), })), n ? r.appendChild(f) : ((f.parent = r), r.childNodes.unshift(f))); }, _ = function (e, r) { ["inference", "proof", "maxAdjust", "labelledRule"].forEach( function (o) { var n = t.getProperty(e, o); null != n && (t.setProperty(r, o, n), t.removeProperty(e, o)); }, ); }, w = function (e, r, o, n, a) { var i = e.nodeFactory.create("node", "mspace", [], { width: l.default.Em(a), }); if ("left" === n) { var u = r.childNodes[o].childNodes[0]; (i.parent = u), u.childNodes.unshift(i); } else r.childNodes[o].appendChild(i); t.setProperty(r.parent, "sequentAdjust_" + n, a); }, T = function (e, r) { for (var o = r.pop(); r.length; ) { var a = r.pop(), i = n(C(o, a), 2), l = i[0], u = i[1]; t.getProperty(o.parent, "axiom") && (w(e, l < 0 ? o : a, 0, "left", Math.abs(l)), w(e, u < 0 ? o : a, 2, "right", Math.abs(u))), (o = a); } }, C = function (e, t) { var r = s(e.childNodes[2]), o = s(t.childNodes[2]); return [s(e.childNodes[0]) - s(t.childNodes[0]), r - o]; }; t.balanceRules = function (e) { var r, o; f = new e.document.options.MathItem("", null, e.math.display); var n = e.data; !(function (e) { var r = e.nodeLists.sequent; if (r) for (var o = r.length - 1, n = void 0; (n = r[o]); o--) if (t.getProperty(n, "sequentProcessed")) t.removeProperty(n, "sequentProcessed"); else { var a = [], i = g(n); if (1 === t.getProperty(i, "inference")) { for (a.push(n); 1 === t.getProperty(i, "inference"); ) { i = c(i); var l = m(d(i, t.getProperty(i, "inferenceRule"))), u = t.getProperty(l, "inferenceRule") ? y(l, t.getProperty(l, "inferenceRule")) : l; t.getProperty(u, "sequent") && ((n = u.childNodes[0]), a.push(n), t.setProperty(n, "sequentProcessed", !0)), (i = l); } T(e, a); } } })(n); var i = n.nodeLists.inference || []; try { for (var l = a(i), u = l.next(); !u.done; u = l.next()) { var s = u.value, p = t.getProperty(s, "proof"), _ = c(s), w = d(_, t.getProperty(_, "inferenceRule")), C = m(w); if (t.getProperty(C, "inference")) { var I = x(C); if (I) { M(n, C, -I); var S = b(s, _, !1); M(n, s, I - S); } } var N = h(w); if (null != t.getProperty(N, "inference")) { var A = x(N, !0); M(n, N, -A, !0); var j = b(s, _, !0), L = t.getProperty(s, "maxAdjust"); null != L && (A = Math.max(A, L)); var k = void 0; if (!p && (k = v(s))) { var O = P(k); if (O) { var J = n.nodeFactory.create("node", "mspace", [], { width: A - j + "em", }); O.appendChild(J), s.removeProperty("maxAdjust"); } else { var B = g(k); B && ((A = t.getProperty(B, "maxAdjust") ? Math.max(t.getProperty(B, "maxAdjust"), A) : A), t.setProperty(B, "maxAdjust", A)); } } else M(n, t.getProperty(s, "proof") ? s : s.parent, A - j, !0); } } } catch (e) { r = { error: e }; } finally { try { u && !u.done && (o = l.return) && o.call(l); } finally { if (r) throw r.error; } } }; var I = (((o = {}).bspr_maxAdjust = !0), o); (t.setProperty = function (e, t, r) { i.default.setProperty(e, "bspr_" + t, r); }), (t.getProperty = function (e, t) { return i.default.getProperty(e, "bspr_" + t); }), (t.removeProperty = function (e, t) { e.removeProperty("bspr_" + t); }), (t.makeBsprAttributes = function (e) { e.data.root.walkTree(function (e, t) { var r = []; e.getPropertyNames().forEach(function (t) { !I[t] && t.match(RegExp("^bspr_")) && r.push(t + ":" + e.getProperty(t)); }), r.length && i.default.setAttribute(e, "semantics", r.join(";")); }); }), (t.saveDocument = function (e) { if (!("getBBox" in (u = e.document).outputJax)) throw Error( "The bussproofs extension requires an output jax with a getBBox() method", ); }), (t.clearDocument = function (e) { u = null; }); }, function (e, t, r) { "use strict"; var o, n = (this && this.__extends) || ((o = function (e, t) { return (o = Object.setPrototypeOf || ({ __proto__: [] } instanceof Array && function (e, t) { e.__proto__ = t; }) || function (e, t) { for (var r in t) t.hasOwnProperty(r) && (e[r] = t[r]); })(e, t); }), function (e, t) { function r() { this.constructor = e; } o(e, t), (e.prototype = null === t ? Object.create(t) : ((r.prototype = t.prototype), new r())); }); Object.defineProperty(t, "__esModule", { value: !0 }), (t.ProofTreeItem = void 0); var a = r(3), i = r(8), l = r(9), u = r(0), f = (function (e) { function t() { var t = (null !== e && e.apply(this, arguments)) || this; return ( (t.leftLabel = null), (t.rigthLabel = null), (t.innerStack = new l.default(t.factory, {}, !0)), t ); } return ( n(t, e), Object.defineProperty(t.prototype, "kind", { get: function () { return "proofTree"; }, enumerable: !1, configurable: !0, }), (t.prototype.checkItem = function (e) { if (e.isKind("end") && "prooftree" === e.getName()) { var t = this.toMml(); return ( u.setProperty(t, "proof", !0), [[this.factory.create("mml", t), e], !0] ); } if (e.isKind("stop")) throw new a.default( "EnvMissingEnd", "Missing \\end{%1}", this.getName(), ); return this.innerStack.Push(e), i.BaseItem.fail; }), (t.prototype.toMml = function () { var t = e.prototype.toMml.call(this), r = this.innerStack.Top(); if (r.isKind("start") && !r.Size()) return t; this.innerStack.Push(this.factory.create("stop")); var o = this.innerStack.Top().toMml(); return this.create("node", "mrow", [o, t], {}); }), t ); })(i.BaseItem); t.ProofTreeItem = f; }, function (e, t, r) { "use strict"; var o = (this && this.__read) || function (e, t) { var r = "function" == typeof Symbol && e[Symbol.iterator]; if (!r) return e; var o, n, a = r.call(e), i = []; try { for (; (void 0 === t || t-- > 0) && !(o = a.next()).done; ) i.push(o.value); } catch (e) { n = { error: e }; } finally { try { o && !o.done && (r = a.return) && r.call(a); } finally { if (n) throw n.error; } } return i; }, n = (this && this.__spread) || function () { for (var e = [], t = 0; t < arguments.length; t++) e = e.concat(o(arguments[t])); return e; }; Object.defineProperty(t, "__esModule", { value: !0 }); var a = r(3), i = r(12), l = r(4), u = r(0), f = { Prooftree: function (e, t) { return ( e.Push(t), e.itemFactory.create("proofTree").setProperties({ name: t.getName(), line: "solid", currentLine: "solid", rootAtTop: !1, }) ); }, Axiom: function (e, t) { var r = e.stack.Top(); if ("proofTree" !== r.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); var o = s(e, e.GetArgument(t)); u.setProperty(o, "axiom", !0), r.Push(o); }, }, s = function (e, t) { var r = l.default.internalMath(e, l.default.trimSpaces(t), 0); if (!r[0].childNodes[0].childNodes.length) return e.create("node", "mrow", []); var o = e.create("node", "mspace", [], { width: ".5ex" }), a = e.create("node", "mspace", [], { width: ".5ex" }); return e.create("node", "mrow", n([o], r, [a])); }; function c(e, t, r, o, n, a, i) { var l, f, s, c, d = e.create("node", "mtr", [e.create("node", "mtd", [t], {})], {}), p = e.create("node", "mtr", [e.create("node", "mtd", r, {})], {}), m = e.create("node", "mtable", i ? [p, d] : [d, p], { align: "top 2", rowlines: a, framespacing: "0 0", }); if ( (u.setProperty(m, "inferenceRule", i ? "up" : "down"), o && ((l = e.create("node", "mpadded", [o], { height: "+.5em", width: "+.5em", voffset: "-.15em", })), u.setProperty(l, "prooflabel", "left")), n && ((f = e.create("node", "mpadded", [n], { height: "+.5em", width: "+.5em", voffset: "-.15em", })), u.setProperty(f, "prooflabel", "right")), o && n) ) (s = [l, m, f]), (c = "both"); else if (o) (s = [l, m]), (c = "left"); else { if (!n) return m; (s = [m, f]), (c = "right"); } return ( (m = e.create("node", "mrow", s)), u.setProperty(m, "labelledRule", c), m ); } function d(e, t) { if ("$" !== e.GetNext()) throw new a.default( "IllegalUseOfCommand", "Use of %1 does not match it's definition.", t, ); e.i++; var r = e.GetUpTo(t, "$"); if (-1 === r.indexOf("\\fCenter")) throw new a.default( "IllegalUseOfCommand", "Missing \\fCenter in %1.", t, ); var n = o(r.split("\\fCenter"), 2), l = n[0], f = n[1], s = new i.default(l, e.stack.env, e.configuration).mml(), c = new i.default(f, e.stack.env, e.configuration).mml(), d = new i.default("\\fCenter", e.stack.env, e.configuration).mml(), p = e.create("node", "mtd", [s], {}), m = e.create("node", "mtd", [d], {}), h = e.create("node", "mtd", [c], {}), y = e.create("node", "mtr", [p, m, h], {}), v = e.create("node", "mtable", [y], { columnspacing: ".5ex", columnalign: "center 2", }); return ( u.setProperty(v, "sequent", !0), e.configuration.addNode("sequent", y), v ); } (f.Inference = function (e, t, r) { var o = e.stack.Top(); if ("proofTree" !== o.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); if (o.Size() < r) throw new a.default("BadProofTree", "Proof tree badly specified."); var n = o.getProperty("rootAtTop"), i = 1 !== r || o.Peek()[0].childNodes.length ? r : 0, l = []; do { l.length && l.unshift(e.create("node", "mtd", [], {})), l.unshift( e.create("node", "mtd", [o.Pop()], { rowalign: n ? "top" : "bottom", }), ), r--; } while (r > 0); var f = e.create("node", "mtr", l, {}), d = e.create("node", "mtable", [f], { framespacing: "0 0" }), p = s(e, e.GetArgument(t)), m = o.getProperty("currentLine"); m !== o.getProperty("line") && o.setProperty("currentLine", o.getProperty("line")); var h = c(e, d, [p], o.getProperty("left"), o.getProperty("right"), m, n); o.setProperty("left", null), o.setProperty("right", null), u.setProperty(h, "inference", i), e.configuration.addNode("inference", h), o.Push(h); }), (f.Label = function (e, t, r) { var o = e.stack.Top(); if ("proofTree" !== o.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); var n = l.default.internalMath(e, e.GetArgument(t), 0), i = n.length > 1 ? e.create("node", "mrow", n, {}) : n[0]; o.setProperty(r, i); }), (f.SetLine = function (e, t, r, o) { var n = e.stack.Top(); if ("proofTree" !== n.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); n.setProperty("currentLine", r), o && n.setProperty("line", r); }), (f.RootAtTop = function (e, t, r) { var o = e.stack.Top(); if ("proofTree" !== o.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); o.setProperty("rootAtTop", r); }), (f.AxiomF = function (e, t) { var r = e.stack.Top(); if ("proofTree" !== r.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); var o = d(e, t); u.setProperty(o, "axiom", !0), r.Push(o); }), (f.FCenter = function (e, t) {}), (f.InferenceF = function (e, t, r) { var o = e.stack.Top(); if ("proofTree" !== o.kind) throw new a.default( "IllegalProofCommand", "Proof commands only allowed in prooftree environment.", ); if (o.Size() < r) throw new a.default("BadProofTree", "Proof tree badly specified."); var n = o.getProperty("rootAtTop"), i = 1 !== r || o.Peek()[0].childNodes.length ? r : 0, l = []; do { l.length && l.unshift(e.create("node", "mtd", [], {})), l.unshift( e.create("node", "mtd", [o.Pop()], { rowalign: n ? "top" : "bottom", }), ), r--; } while (r > 0); var f = e.create("node", "mtr", l, {}), s = e.create("node", "mtable", [f], { framespacing: "0 0" }), p = d(e, t), m = o.getProperty("currentLine"); m !== o.getProperty("line") && o.setProperty("currentLine", o.getProperty("line")); var h = c( e, s, [p], o.getProperty("left"), o.getProperty("right"), m, n, ); o.setProperty("left", null), o.setProperty("right", null), u.setProperty(h, "inference", i), e.configuration.addNode("inference", h), o.Push(h); }), (t.default = f); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.TexError.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.ParseUtil.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.isObject = MathJax._.components.global.isObject), (t.combineConfig = MathJax._.components.global.combineConfig), (t.combineDefaults = MathJax._.components.global.combineDefaults), (t.combineWithMathJax = MathJax._.components.global.combineWithMathJax), (t.MathJax = MathJax._.components.global.MathJax); }, function (e, t, r) { "use strict"; var o; Object.defineProperty(t, "__esModule", { value: !0 }), (t.BussproofsConfiguration = void 0); var n = r(7), a = r(1), i = r(0); r(11), (t.BussproofsConfiguration = n.Configuration.create("bussproofs", { handler: { macro: ["Bussproofs-macros"], environment: ["Bussproofs-environments"], }, items: ((o = {}), (o[a.ProofTreeItem.prototype.kind] = a.ProofTreeItem), o), preprocessors: [[i.saveDocument, 1]], postprocessors: [ [i.clearDocument, 3], [i.makeBsprAttributes, 2], [i.balanceRules, 1], ], })); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.Configuration = MathJax._.input.tex.Configuration.Configuration), (t.ConfigurationHandler = MathJax._.input.tex.Configuration.ConfigurationHandler), (t.ParserConfiguration = MathJax._.input.tex.Configuration.ParserConfiguration); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.MmlStack = MathJax._.input.tex.StackItem.MmlStack), (t.BaseItem = MathJax._.input.tex.StackItem.BaseItem); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.Stack.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.NodeUtil.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }); var o = r(2), n = r(13), a = r(14); new a.CommandMap( "Bussproofs-macros", { AxiomC: "Axiom", UnaryInfC: ["Inference", 1], BinaryInfC: ["Inference", 2], TrinaryInfC: ["Inference", 3], QuaternaryInfC: ["Inference", 4], QuinaryInfC: ["Inference", 5], RightLabel: ["Label", "right"], LeftLabel: ["Label", "left"], AXC: "Axiom", UIC: ["Inference", 1], BIC: ["Inference", 2], TIC: ["Inference", 3], RL: ["Label", "right"], LL: ["Label", "left"], noLine: ["SetLine", "none", !1], singleLine: ["SetLine", "solid", !1], solidLine: ["SetLine", "solid", !1], dashedLine: ["SetLine", "dashed", !1], alwaysNoLine: ["SetLine", "none", !0], alwaysSingleLine: ["SetLine", "solid", !0], alwaysSolidLine: ["SetLine", "solid", !0], alwaysDashedLine: ["SetLine", "dashed", !0], rootAtTop: ["RootAtTop", !0], alwaysRootAtTop: ["RootAtTop", !0], rootAtBottom: ["RootAtTop", !1], alwaysRootAtBottom: ["RootAtTop", !1], fCenter: "FCenter", Axiom: "AxiomF", UnaryInf: ["InferenceF", 1], BinaryInf: ["InferenceF", 2], TrinaryInf: ["InferenceF", 3], QuaternaryInf: ["InferenceF", 4], QuinaryInf: ["InferenceF", 5], }, o.default, ), new a.EnvironmentMap( "Bussproofs-environments", n.default.environment, { prooftree: ["Prooftree", null, !1] }, o.default, ); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.TexParser.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.default = MathJax._.input.tex.ParseMethods.default); }, function (e, t, r) { "use strict"; Object.defineProperty(t, "__esModule", { value: !0 }), (t.AbstractSymbolMap = MathJax._.input.tex.SymbolMap.AbstractSymbolMap), (t.RegExpMap = MathJax._.input.tex.SymbolMap.RegExpMap), (t.AbstractParseMap = MathJax._.input.tex.SymbolMap.AbstractParseMap), (t.CharacterMap = MathJax._.input.tex.SymbolMap.CharacterMap), (t.DelimiterMap = MathJax._.input.tex.SymbolMap.DelimiterMap), (t.MacroMap = MathJax._.input.tex.SymbolMap.MacroMap), (t.CommandMap = MathJax._.input.tex.SymbolMap.CommandMap), (t.EnvironmentMap = MathJax._.input.tex.SymbolMap.EnvironmentMap); }, function (e, t, r) { "use strict"; r.r(t); var o = r(5), n = r(6), a = r(1), i = r(2), l = r(0); Object(o.combineWithMathJax)({ _: { input: { tex: { bussproofs: { BussproofsConfiguration: n, BussproofsItems: a, BussproofsMethods: i, BussproofsUtil: l, }, }, }, }, }); }, ]);