commit 05c20e40ad5041a5c1e2276fd2b3242bebe5a27b
parent 1f0e73241547398fe04df40d0bcba6097162cd75
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 19 Jul 2017 23:30:13 +0200
Finished most typing rules, managed to get a \tag{} to render nicely next to grammar cases
Diffstat:
10 files changed, 492 insertions(+), 86 deletions(-)
diff --git a/.travis.yml b/.travis.yml
@@ -45,7 +45,6 @@ jobs:
- if test "$TRAVIS_BUILD_ID" != `cat ~/.racket/travis_build_id`; then travis_terminate 1; fi
- rm -f ~/.racket/travis_build_id
# Do this before modifying anything in the build folder, to avoid the "x" marker indicating changes since last commit.
- - zipfile_folder_name="$(racket -e '(begin (require phc-thesis/scribblings/util) (display (version-text "phc-thesis-" "")))')"
- echo "LaTeX extra packages:"
- latex_home=$(kpsewhich -var-value=TEXMFHOME)
- curl -L -o newunicodechar.ins http://mirrors.ctan.org/macros/latex/contrib/newunicodechar/newunicodechar.ins
@@ -60,6 +59,7 @@ jobs:
- mv mathpartir.sty "$latex_home/tex/latex/mathpartir"
- echo "Finished installing extra latex packages."
- raco pkg install --deps search-auto -j 2
+ - zipfile_folder_name="$(racket -e '(begin (require phc-thesis/scribblings/util) (display (version-text "phc-thesis-" "")))')"
- raco test -x -p "$(basename "$TRAVIS_BUILD_DIR")"
- raco setup --check-pkg-deps --no-zo --no-launcher --no-install --no-post-install --no-docs --pkgs "$(basename "$TRAVIS_BUILD_DIR")";
- rm -fr doc/
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -7,7 +7,34 @@
The following definitions and rules are copied and adjusted
from@~cite["tobin-hochstadt_typed_2010"], with the author's permission. Some
-of the notations were changed to use those of@~cite["kent2016occurrence"]
+of the notations were changed to use those of@~cite["kent2016occurrence"]. We
+include below the grammar, semantics and typing rules related to the minimal
+core of the Typed Racket language@note{The core language is defined
+ in@~cite[#:precision "pp. 61–70" "tobin-hochstadt_typed_2010"].}, dubbed @${
+ λ_{\mathit{TS}}}, including extensions which add pairs@note{The extensions
+ needed to handle pairs are described
+ in@~cite[#:precision "pp. 71–75" "tobin-hochstadt_typed_2010"].}, functions of
+multiple arguments, variadic functions and variadic polymorphic
+functions@note{The extensions needed to handle functions of multiple
+ arguments, variadic functions, and variadic functions where the type of the
+ “rest” arguments are not uniform are described
+ in@~cite[#:precision "pp. 91–77" "tobin-hochstadt_typed_2010"].}, @todo{
+ intersection types}, @todo{recursive types}, @todo{symbols} and @todo{
+ promises}. We purposefully omit extensions which allow advanced logic
+reasoning when propagating information gained by complex combinations of
+conditionals@note{The extensions which allow advanced logic reasoning are
+ described in@~cite[#:precision "pp. 75–78" "tobin-hochstadt_typed_2010"].},
+refinement types@note{The extensions which introduce refinement types are
+ described in@~cite[#:precision "pp. 85–89" "tobin-hochstadt_typed_2010"].},
+dependent refinement types@note{Dependent refinement types are presented in
+ @~cite["kent2016occurrence"].} (which allow using theories from external
+solvers to reason about values and their type, e.g. using bitvector theory to
+ensure that a sequence of operations does not produce a result exceeding a
+certain machine integer size), structs and classes. These extensions are not
+relevant to our work@note{We informally describe a translation of our system
+ of records into structs in section @todo{[??]}, but settle for an alternative
+ implementation in section @todo{[??]} which does not rely on structs.}, and
+their inclusion in the following semantics would needlessly complicate things.
@require["../scribblings/util.rkt"
"../scribblings/adt-utils.rkt"
@@ -27,20 +54,23 @@ of the notations were changed to use those of@~cite["kent2016occurrence"]
Expressions:
@cases["e" #:first-sep "⩴"
- @acase{x}
- @acase{@num-e}
- @acase{@true-e}
+ @acase{x@tag*{variable}}
+ @acase{@num-e @tag*{number}}
+ @acase{@true-e @tag*{booleans}}
@acase{@false-e}
- @acase{@primop}
- @acase{@app[e @repeated{e}]}
- @acase{@ifop[e e e]}
- @acase{@λe[(@repeated{x:τ}) e]}
- @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]}
- @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]}
- @acase{@Λe[(@repeated{α}) e]}
- @acase{@Λe[(@repeated{α} @polydotα[α]) e]}
- @acase{@conse[e e]} @; TODO: shouldn't it be a primop?
- @acase{@at[e @repeated{τ}]}]
+ @acase{@primop @tag*{primitive operations}}
+ @acase{@app[e @repeated{e}] @tag*{function application}}
+ @acase{@ifop[e e e] @tag*{conditional}}
+ @acase{@λe[(@repeated{x:τ}) e] @tag*{lambda function}}
+ @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
+ @tag*{variadic function}}
+ @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]
+ @tag*{variadic polymorpic function}}
+ @acase{@Λe[(@repeated{α}) e]@tag*{polymorphic abstraction}}
+ @acase{@Λe[(@repeated{α} @polydotα[α]) e]
+ @tag*{variadic polymorphic abstraction}}
+ @acase{@at[e @repeated{τ}] @tag*{polymorphic instantiation}}
+ @acase{@conse[e e]@tag*{pair}}] @; TODO: shouldn't it be a primop?
Primitive operations:
@@ -106,10 +136,13 @@ Types:
@acase{@∀r[@${(@repeated{α})} @repeated{τ}]}
@acase{@∀r[@${(@repeated{α} @polydotα[α])} @repeated{τ}]}
@acase{@un[@repeated{τ}]}
- @acase{@consτ[τ τ]}]
+ @acase{@consτ[τ τ]}
+ @acase{@nullτ}]
+
+@htodo{Add the rec types}
@cases[@R #:first-sep "⩴"
- @R[@→Values[@repeated{τ}]
+ @R[τ
@${φ⁺}
@${φ⁻}
@${o}]]
@@ -120,14 +153,18 @@ Filters (conditional typing information):
@cases[@${φ} #:first-sep "⩴" @acase{@repeatset{ψ}}]
@cases["ψ" #:first-sep "⩴"
- @acase{τₓ}
- @acase{\overline{τ}ₓ}
+ @acase{τ_{@loc}}
+ @acase{@!{τ}_{@loc}}
@acase{⊥}]
+@cases[@loc #:first-sep "⩴"
+ @acase{•\qquad\qquad@text{function's first argument}}
+ @acase{x}]
+
Objects (aliasing information):
@cases[@textrm{o} #:first-sep "⩴"
- @acase{π}
+ @acase{π(@loc)}
@acase{∅}]
Paths:
@@ -150,13 +187,13 @@ Path elements (aliasing information):
Subtyping:
@$inferrule[
- @${}
+ -
@${⊢ τ <: τ}
@${@textsc{S-Refl}}
]
@$inferrule[
- @${}
+ -
@${⊢ τ <: ⊤}
@${@textsc{S-Top}}
]
@@ -166,7 +203,7 @@ empty union. The @${⊥} type is a shorthand for @${(∪)}. It is a subtype of
every other type, and is not inhabited by any value.
@$inferrule[
- @${}
+ -
@${⊢ ⊥ <: τ}
@${@textsc{S-Bot}}
]
@@ -182,17 +219,17 @@ every other type, and is not inhabited by any value.
@$inferrule[
@${
- @repeated{@<:[τ_r σ_r]} \\
+ @<:[τ_r σ_r] \\
@${φ⁺' ⊆ φ⁺ } \\
@${φ⁻' ⊆ φ⁻ } \\
o = o' ∨ o' = ∅}
- @${@<:R[@R[@→Values[@repeated{τ_r}]
+ @${@<:R[@R[τ_r
@${φ⁺}
@${φ⁻}
@${o}]
- @R[@→Values[@repeated{σ_r}]
- @${φ'⁺}
- @${φ'⁻}
+ @R[σ_r
+ @${φ⁺'}
+ @${φ⁻'}
@${o'}]]}
@${@textsc{S-R}}
]
@@ -297,36 +334,207 @@ Operational semantics:
Typing rules:
-@$inferrule[@${}
- @${@Γ[⊢ x @${Γ(x)} @${\overline{@false-τ}} @true-τ x]}
+@$inferrule[-
+ @${@Γ[⊢ x @${Γ(x)} @${@!{@false-τ}} @true-τ x]}
@${@textsc{T-Var}}]
-@$inferrule[@${}
+@$inferrule[-
@${@Γ[⊢ p @${δ_τ(p)} ϵ ⊥ ∅]}
@${@textsc{T-Primop}}]
-@$inferrule[@${}
- @${@Γ[⊢ @truev @true-τ ϵ ⊥ ∅]}
+@$inferrule[-
+ @${@Γ[⊢ @true-v @true-τ ϵ ⊥ ∅]}
@${@textsc{T-True}}]
-@$inferrule[@${}
- @${@Γ[⊢ @falsev @false-τ ⊥ ϵ ∅]}
+@$inferrule[-
+ @${@Γ[⊢ @false-v @false-τ ⊥ ϵ ∅]}
@${@textsc{T-False}}]
-@$inferrule[@${}
+@$inferrule[-
@${@Γ[⊢ @num-v @num-τ ϵ ⊥ ∅]}
@${@textsc{T-Num}}]
+@$inferrule[-
+ @${@Γ[⊢ @nullv @nullτ ⊥ ϵ ∅]}
+ @${@textsc{T-Null}}]
+
-TODO: Drop the object and filters which are not in terms of x₀, rename
-otherwise.
+@$inferrule[@${@Γ[@${x₀:σ₀} @repeated{xᵢ:σ} ⊢ e τ φ⁺ φ⁻ o] \\
+ φ⁺' = φ⁺\vphantom{φ}@substφo[x₀ ↦ •] \\
+ φ⁻' = φ⁻\vphantom{φ}@substφo[x₀ ↦ •] \\
+ o' = o\vphantom{o}@substφo[x₀ ↦ •]}
+ @${@Γ[⊢ @λe[(@repeated{x:σ}) e]
+ (f→ (@repeated{σ})
+ @R[τ
+ @${φ⁺'}
+ @${φ⁻'}
+ @${o'}])
+ ϵ ⊥ ∅]}
+ @${@textsc{T-AbsPred}}]
-@$inferrule[@${@Γ[@repeated{x:σ} ⊢ e τ φ⁺ φ⁻ o]}
+@$inferrule[@${@Γ[⊢ e τ φ⁺ φ⁻ o]}
@${@Γ[⊢ @λe[(@repeated{x:σ}) e]
(f→ (@repeated{σ})
- @R[@→Values[τ]
- @${φ⁺[x ↦ ?]}
- @${φ⁻[x ↦ ?]}
- @${o[x ↦ ?]}])
+ @R[τ
+ ϵ
+ ϵ
+ ∅])
ϵ ⊥ ∅]}
- @${@textsc{T-Abs}}]
-\ No newline at end of file
+ @${@textsc{T-Abs}}]
+
+The @${\vphantom{φ}@substφo[x ↦ z]} operation restricts the information
+contained within a @${φ} or @${o} so that the result only contains information
+about the variable @${x}, and renames it to @${z}. When applied to a filter
+@${φ}, it corresponds to the @${\operatorname{abo}} and @${\operatorname{
+ apo}} operators from
+@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"].
+
+The @${⊥} cases of the @${\operatorname{apo}} operator
+from@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"] are covered
+by the corresponding cases in the @${@restrict} and @${@remove} operators, and
+therefore should not need to be included in our @${\vphantom{
+ φ}@substφo[x ↦ z]} operator.
+
+@$${
+ \begin{aligned}
+ φ@substφo[x ↦ z] &= \bigcup @repeated{ψ@substφo[x ↦ z]}&\\
+ ⊥@substφo[x ↦ z] &= \{⊥\}&\\
+ τ_{π(y)}\vphantom{τ}@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\
+ @!{τ}_{π(y)}\vphantom{τ}@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\
+ τ_{π(x)}\vphantom{τ}@substφo[x ↦ z] &= \{τ_{π(z)}\} &\\
+ @!{τ}_{π(x)}\vphantom{τ}@substφo[x ↦ z] &= \{@!{τ}_{π(z)}\} &
+ \end{aligned}
+}
+
+@$${
+ \begin{aligned}
+ π(x)@substφo[x ↦ ∅] &= ∅ &\\
+ π(x)@substφo[x ↦ z] &= π(z) &@textif z ≠ ∅ \\
+ π(y)@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\
+ ∅@substφo[x ↦ z] &= ∅ &
+ \end{aligned}
+}
+
+@(define _op @${_{\mathit{op}}})
+
+@$inferrule[@${@Γ[⊢ @${e@_op} @${τ@_op} @${φ⁺@_op} @${φ⁻@_op} @${o@_op}] \\
+ @repeated[@Γ[⊢ @${aᵢ} @${τ_{aᵢ}}
+ @${φ⁺_{aᵢ}} @${φ⁻_{aᵢ}} @${o_{aᵢ}}]] \\
+ @repeated[@<:[τ_a @${τ_{\mathit{in}}}]]
+ @<:[@${τ@_op} @f→[(@repeated{τ_{\mathit{in}}})
+ @R[τ_r φ⁺_r φ⁻_r o_r]]]
+ φ⁺_r' = φ⁺_r@substφo[• ↦ @${o_{a₀}}] \\
+ φ⁻_r' = φ⁻_r@substφo[• ↦ @${o_{a₀}}] \\
+ o' = o@substφo[• ↦ @${o_{a₀}}]}
+ @${@Γ[⊢ @app[@${e@_op} @repeated{aᵢ}]
+ (f→ (@repeated{σ})
+ @R[τ_r
+ @${φ⁺'}
+ @${φ⁻'}
+ @${o'}])
+ ϵ ⊥ ∅]}
+ @${@textsc{T-App}}]
+
+@$inferrule[@${@Γ[⊢ @${e₁} @${τ₁} @${φ⁺₁} @${φ⁻₁} @${o₁}] \\
+ @Γ[+ φ⁺₁ ⊢ @${e₂} @${τ₂} @${φ⁺₂} @${φ⁻₂} @${o₂}] \\
+ @Γ[+ φ⁻₁ ⊢ @${e₃} @${τ₃} @${φ⁺₃} @${φ⁻₃} @${o₃}] \\
+ @<:[τ₂ τ_r] \\
+ @<:[τ₃ τ_r] \\
+ φ_r = @combinefilter(φ⁺₁ / φ⁻₁, φ⁺₂ / φ⁻₂, φ⁺₃ / φ⁻₃) \\
+ o_r = \begin{cases}
+ o₂ @& @textif o₂ = o₃
+ @nl ∅ @& @otherwise
+ \end{cases}
+ }
+ @${@Γ[⊢ @ifop[e₁ e₂ e₃]
+ τ_r
+ ϵ ⊥ ∅]}
+ @${@textsc{T-If}}]
+
+@htodo{The definition of Γ' does not specify what the other cases ≠ x are
+ (they are the same as the original Γ, but this is only implicit).}
+
+@aligned{
+ Γ + \{τ_{π(x)}\} ∪ @repeatset{ψ}
+ &= (Γ, x : @update(Γ(x), τ_π)) + @repeatset{ψ}\\
+ Γ + \{@!{τ}_{π(x)}\} ∪ @repeatset{ψ}
+ &= (Γ, x : @update(Γ(x), @!{τ}_π)) + @repeatset{ψ}\\
+ Γ + \{⊥\} ∪ @repeatset{ψ} &= Γ' @where ∀x∈ \operatorname{dom}(Γ).Γ'(x) = ⊥\\
+ Γ + ϵ &= Γ \\
+}
+
+@aligned{
+ @update(@consτ[τ τ′], σ_{π∷car} )
+ &= @consτ[@${@update(τ, σ_π)} τ′]\\
+ @update(@consτ[τ τ′], @!{σ}_{π∷car})
+ &= @consτ[@${@update(τ, @!{σ}_π)} τ′]\\
+ @update(@consτ[τ τ′], σ_{π∷cdr} )
+ &= @consτ[τ @${@update(τ′, σ_π)}]\\
+ @update(@consτ[τ τ′], @!{σ}_{π∷cdr} )
+ &= @consτ[τ @${@update(τ′, @!{σ}_π)}]\\
+ @update(τ, σ_ϵ) &= @restrict(τ, σ) \\
+ @update(τ, @!{σ}_ϵ) &= @remove(τ, σ)
+}
+
+@aligned{
+ @restrict(τ, σ) &= ⊥ &@textif @no-overlap(τ,σ)\\
+ @restrict((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@restrict(τ,σ)} &\\
+ @restrict(τ, σ) &= τ &@textif @<:[τ σ]\\
+ @restrict(τ, σ) &= σ &@otherwise
+}
+
+@aligned{
+ @remove(τ, σ) &= ⊥ &@textif @<:[τ σ] \\
+ @remove((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@remove(τ,σ)} &\\
+ @remove(τ, σ) &= τ &@otherwise
+}
+
+@todo{Shouldn't no-overlap be simplified to @${@no-overlap(τ, τ') = (@<:[σ τ]
+ ∧ @<:[σ τ′] ⇒ σ = ⊥)}? Then @${@restrict(τ,σ)} can be simplified to returning
+ the most general type which is a subtype of τ and σ if one exists (or maybe
+ simply returning the intersection of τ and σ).}
+
+@aligned{
+ @no-overlap(@num-τ[n], @num-τ[m]) &= @metatrue @textif n ≠ m \\
+ @no-overlap(@num-τ, @true-τ) &= @metatrue \\
+ @no-overlap(@num-τ, @false-τ) &= @metatrue \\
+ @no-overlap(@num-τ, @nullτ) &= @metatrue \\
+ @no-overlap(@true-τ, @false-τ) &= @metatrue \\
+ @no-overlap(@true-τ, @nullτ) &= @metatrue \\
+ @no-overlap(@false-τ, @nullτ) &= @metatrue \\
+ @no-overlap(@num-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\
+ @no-overlap(@true-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\
+ @no-overlap(@false-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\
+ @no-overlap(@consτ[τ τ′]) &= , @f→[(@repeated{τ}) @R]) &= @metatrue \\
+ @no-overlap(@nullτ, @f→[(@repeated{τ}) @R]) &= @metatrue \\
+ @no-overlap(@num-τ, @consτ[τ τ′]) &= @metatrue \\
+ @no-overlap(@true-τ, @consτ[τ τ′]) &= @metatrue \\
+ @no-overlap(@false-τ, @consτ[τ τ′]) &= @metatrue \\
+ @no-overlap(@nullτ, @consτ[τ τ′]) &= @metatrue \\
+ @no-overlap(@consτ[τ τ′], @consτ[σ σ′])
+ &= @no-overlap(τ,σ) ∨ @no-overlap(τ′,σ′)\\
+ @no-overlap((⋃ @repeatset{τ}), σ) &= ⋀@repeated{@no-overlap(τ,σ)}\\
+ @no-overlap(τ, σ) &= @metatrue @textif @no-overlap(σ, τ)\\
+ @no-overlap(τ, σ) &= @metafalse @otherwise \\
+}
+
+@htodo{Say that there are more rules in the implementation, to handle various
+ boolean operations.}
+
+@aligned{
+ @combinefilter(ϵ / ⊥, φ^±₂, φ^±₃) &= φ₂ &\\
+ @combinefilter(⊥ / ϵ, φ^±₂, φ^±₃) &= φ₃ &\\
+ @combinefilter(⊥ / ⊥, φ^±₂, φ^±₃) &= ⊥ &\\
+ @combinefilter(φ⁺₁ / φ⁻₁, φ⁺₂ / φ⁻₂, ⊥/ϵ) &= φ⁺₁ ∪ φ⁺₂ &\\
+ @combinefilter(
+ \{ τ_@loc \} ∪ φ⁺₁ / \{ @!{τ}_@loc \} φ⁻₁,
+ ϵ / ⊥,
+ ⊥/ϵ)
+ &= (∪ τ σ)_@loc / @!{(∪ τ σ)_@loc} &\\
+ … & … & \\
+ @combinefilter(⊥ / ⊥, φ^±₂, φ^±₃) &= ϵ / ϵ &@otherwise \\
+}
+
+@htodo{The Γ ⊢ x : τ … does not generate a Γ(x) = τ, I suspect. There should
+ be indicated somewhere an equivalence between these two notations (and we
+ should fix the @${Γ,x:update(…)}, as it is a third notation).}
+\ No newline at end of file
diff --git a/qaligned.patch b/qaligned.patch
@@ -6,7 +6,7 @@ diff -r -u ./node_modules.orig/mathjax/extensions/TeX/AMSmath.js ./node_modules/
*/
-MathJax.Extension["TeX/AMSmath"]={version:"2.7.1",number:0,startNumber:0,IDs:{},eqIDs:{},labels:{},eqlabels:{},refs:[]};MathJax.Hub.Register.StartupHook("TeX Jax Ready",function(){var b=MathJax.ElementJax.mml,h=MathJax.InputJax.TeX,g=MathJax.Extension["TeX/AMSmath"];var d=h.Definitions,f=h.Stack.Item,a=h.config.equationNumbers;var c=function(k){var n=[];for(var l=0,j=k.length;l<j;l++){n[l]=h.Parse.prototype.Em(k[l])}return n.join(" ")};var e=(document.getElementsByTagName("base").length===0)?"":String(document.location).replace(/#.*$/,"");d.Add({mathchar0mo:{iiiint:["2A0C",{texClass:b.TEXCLASS.OP}]},macros:{mathring:["Accent","2DA"],nobreakspace:"Tilde",negmedspace:["Spacer",b.LENGTH.NEGATIVEMEDIUMMATHSPACE],negthickspace:["Spacer",b.LENGTH.NEGATIVETHICKMATHSPACE],idotsint:["MultiIntegral","\\int\\cdots\\int"],dddot:["Accent","20DB"],ddddot:["Accent","20DC"],sideset:["Macro","\\mathop{\\mathop{\\rlap{\\phantom{#3}}}\\nolimits#1\\!\\mathop{#3}\\nolimits#2}",3],boxed:["Macro","\\fbox{$\\displaystyle{#1}$}",1],tag:"HandleTag",notag:"HandleNoTag",label:"HandleLabel",ref:"HandleRef",eqref:["HandleRef",true],substack:["Macro","\\begin{subarray}{c}#1\\end{subarray}",1],injlim:["NamedOp","inj lim"],projlim:["NamedOp","proj lim"],varliminf:["Macro","\\mathop{\\underline{\\mmlToken{mi}{lim}}}"],varlimsup:["Macro","\\mathop{\\overline{\\mmlToken{mi}{lim}}}"],varinjlim:["Macro","\\mathop{\\underrightarrow{\\mmlToken{mi}{lim}}}"],varprojlim:["Macro","\\mathop{\\underleftarrow{\\mmlToken{mi}{lim}}}"],DeclareMathOperator:"HandleDeclareOp",operatorname:"HandleOperatorName",SkipLimits:"SkipLimits",genfrac:"Genfrac",frac:["Genfrac","","","",""],tfrac:["Genfrac","","","",1],dfrac:["Genfrac","","","",0],binom:["Genfrac","(",")","0",""],tbinom:["Genfrac","(",")","0",1],dbinom:["Genfrac","(",")","0",0],cfrac:"CFrac",shoveleft:["HandleShove",b.ALIGN.LEFT],shoveright:["HandleShove",b.ALIGN.RIGHT],xrightarrow:["xArrow",8594,5,6],xleftarrow:["xArrow",8592,7,3]},environment:{align:["AMSarray",null,true,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],"align*":["AMSarray",null,false,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],multline:["Multline",null,true],"multline*":["Multline",null,false],split:["AMSarray",null,false,false,"rl",c([0])],gather:["AMSarray",null,true,true,"c"],"gather*":["AMSarray",null,false,true,"c"],alignat:["AlignAt",null,true,true],"alignat*":["AlignAt",null,false,true],alignedat:["AlignAt",null,false,false],aligned:["AlignedAMSArray",null,null,null,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0]),".5em","D"],gathered:["AlignedAMSArray",null,null,null,"c",null,".5em","D"],subarray:["Array",null,null,null,null,c([0]),"0.1em","S",1],smallmatrix:["Array",null,null,null,"c",c([1/3]),".2em","S",1],equation:["EquationBegin","Equation",true],"equation*":["EquationBegin","EquationStar",false],eqnarray:["AMSarray",null,true,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"],"eqnarray*":["AMSarray",null,false,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"]},delimiter:{"\\lvert":["007C",{texClass:b.TEXCLASS.OPEN}],"\\rvert":["007C",{texClass:b.TEXCLASS.CLOSE}],"\\lVert":["2016",{texClass:b.TEXCLASS.OPEN}],"\\rVert":["2016",{texClass:b.TEXCLASS.CLOSE}]}},null,true);h.Parse.Augment({HandleTag:function(k){var m=this.GetStar();var j=this.trimSpaces(this.GetArgument(k)),i=j;if(!m){j=a.formatTag(j)}var l=this.stack.global;l.tagID=i;if(l.notags){h.Error(["CommandNotAllowedInEnv","%1 not allowed in %2 environment",k,l.notags])}if(l.tag){h.Error(["MultipleCommand","Multiple %1",k])}l.tag=b.mtd.apply(b,this.InternalMath(j)).With({id:a.formatID(i)})},HandleNoTag:function(i){if(this.stack.global.tag){delete this.stack.global.tag}this.stack.global.notag=true},HandleLabel:function(j){var k=this.stack.global,i=this.GetArgument(j);if(i===""){return}if(!g.refUpdate){if(k.label){h.Error(["MultipleCommand","Multiple %1",j])}k.label=i;if(g.labels[i]||g.eqlabels[i]){h.Error(["MultipleLabel","Label '%1' multiply defined",i])}g.eqlabels[i]={tag:"???",id:""}}},HandleRef:function(k,m){var j=this.GetArgument(k);var l=g.labels[j]||g.eqlabels[j];if(!l){l={tag:"???",id:""};g.badref=!g.refUpdate}var i=l.tag;if(m){i=a.formatTag(i)}this.Push(b.mrow.apply(b,this.InternalMath(i)).With({href:a.formatURL(l.id,e),"class":"MathJax_ref"}))},HandleDeclareOp:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));if(k.charAt(0)=="\\"){k=k.substr(1)}var l=this.GetArgument(j);l=l.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");h.Definitions.macros[k]=["Macro","\\mathop{\\rm "+l+"}"+i]},HandleOperatorName:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));k=k.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");this.string="\\mathop{\\rm "+k+"}"+i+" "+this.string.slice(this.i);this.i=0},SkipLimits:function(j){var l=this.GetNext(),k=this.i;if(l==="\\"&&++this.i&&this.GetCS()!=="limits"){this.i=k}},HandleShove:function(j,i){var k=this.stack.Top();if(k.type!=="multline"||k.data.length){h.Error(["CommandAtTheBeginingOfLine","%1 must come at the beginning of the line",j])}k.data.shove=i},CFrac:function(l){var i=this.trimSpaces(this.GetBrackets(l,"")),k=this.GetArgument(l),m=this.GetArgument(l);var j=b.mfrac(h.Parse("\\strut\\textstyle{"+k+"}",this.stack.env).mml(),h.Parse("\\strut\\textstyle{"+m+"}",this.stack.env).mml());i=({l:b.ALIGN.LEFT,r:b.ALIGN.RIGHT,"":""})[i];if(i==null){h.Error(["IllegalAlign","Illegal alignment specified in %1",l])}if(i){j.numalign=j.denomalign=i}this.Push(j)},Genfrac:function(j,l,q,n,i){if(l==null){l=this.GetDelimiterArg(j)}if(q==null){q=this.GetDelimiterArg(j)}if(n==null){n=this.GetArgument(j)}if(i==null){i=this.trimSpaces(this.GetArgument(j))}var m=this.ParseArg(j);var p=this.ParseArg(j);var k=b.mfrac(m,p);if(n!==""){k.linethickness=n}if(l||q){k=h.fixedFence(l,k.With({texWithDelims:true}),q)}if(i!==""){var o=(["D","T","S","SS"])[i];if(o==null){h.Error(["BadMathStyleFor","Bad math style for %1",j])}k=b.mstyle(k);if(o==="D"){k.displaystyle=true;k.scriptlevel=0}else{k.displaystyle=false;k.scriptlevel=i-1}}this.Push(k)},Multline:function(j,i){this.Push(j);this.checkEqnEnv();return f.multline(i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",width:h.config.MultLineWidth,columnwidth:"100%",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AMSarray:function(k,j,i,m,l){this.Push(k);if(i){this.checkEqnEnv()}m=m.replace(/[^clr]/g,"").split("").join(" ");m=m.replace(/l/g,"left").replace(/r/g,"right").replace(/c/g,"center");return f.AMSarray(k.name,j,i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",columnalign:m,columnspacing:(l||"1em"),rowspacing:"3pt",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AlignedAMSArray:function(i){var j=this.GetBrackets("\\begin{"+i.name+"}");return this.setArrayAlign(this.AMSarray.apply(this,arguments),j)},AlignAt:function(l,j,i){var q,k,p="",o=[];if(!i){k=this.GetBrackets("\\begin{"+l.name+"}")}q=this.GetArgument("\\begin{"+l.name+"}");if(q.match(/[^0-9]/)){h.Error(["PositiveIntegerArg","Argument to %1 must me a positive integer","\\begin{"+l.name+"}"])}while(q>0){p+="rl";o.push("0em 0em");q--}o=o.join(" ");if(i){return this.AMSarray(l,j,i,p,o)}var m=this.AMSarray(l,j,i,p,o);return this.setArrayAlign(m,k)},EquationBegin:function(i,j){this.checkEqnEnv();this.stack.global.forcetag=(j&&a.autoNumber!=="none");return i},EquationStar:function(i,j){this.stack.global.tagged=true;return j},checkEqnEnv:function(){if(this.stack.global.eqnenv){h.Error(["ErroneousNestingEq","Erroneous nesting of equation structures"])}this.stack.global.eqnenv=true},MultiIntegral:function(j,m){var l=this.GetNext();if(l==="\\"){var k=this.i;l=this.GetArgument(j);this.i=k;if(l==="\\limits"){if(j==="\\idotsint"){m="\\!\\!\\mathop{\\,\\,"+m+"}"}else{m="\\!\\!\\!\\mathop{\\,\\,\\,"+m+"}"}}}this.string=m+" "+this.string.slice(this.i);this.i=0},xArrow:function(k,o,n,i){var m={width:"+"+(n+i)+"mu",lspace:n+"mu"};var p=this.GetBrackets(k),q=this.ParseArg(k);var s=b.mo(b.chars(String.fromCharCode(o))).With({stretchy:true,texClass:b.TEXCLASS.REL});var j=b.munderover(s);j.SetData(j.over,b.mpadded(q).With(m).With({voffset:".15em"}));if(p){p=h.Parse(p,this.stack.env).mml();j.SetData(j.under,b.mpadded(p).With(m).With({voffset:"-.24em"}))}this.Push(j.With({subsupOK:true}))},GetDelimiterArg:function(i){var j=this.trimSpaces(this.GetArgument(i));if(j==""){return null}if(j in d.delimiter){return j}h.Error(["MissingOrUnrecognizedDelim","Missing or unrecognized delimiter for %1",i])},GetStar:function(){var i=(this.GetNext()==="*");if(i){this.i++}return i}});f.Augment({autoTag:function(){var j=this.global;if(!j.notag){g.number++;j.tagID=a.formatNumber(g.number.toString());var i=h.Parse("\\text{"+a.formatTag(j.tagID)+"}",{}).mml();j.tag=b.mtd(i).With({id:a.formatID(j.tagID)})}},getTag:function(){var m=this.global,k=m.tag;m.tagged=true;if(m.label){if(a.useLabelIds){k.id=a.formatID(m.label)}g.eqlabels[m.label]={tag:m.tagID,id:k.id}}if(document.getElementById(k.id)||g.IDs[k.id]||g.eqIDs[k.id]){var l=0,j;do{l++;j=k.id+"_"+l}while(document.getElementById(j)||g.IDs[j]||g.eqIDs[j]);k.id=j;if(m.label){g.eqlabels[m.label].id=j}}g.eqIDs[k.id]=1;this.clearTag();return k},clearTag:function(){var i=this.global;delete i.tag;delete i.tagID;delete i.label},fixInitialMO:function(l){for(var k=0,j=l.length;k<j;k++){if(l[k]&&(l[k].type!=="mspace"&&(l[k].type!=="texatom"||(l[k].data[0]&&l[k].data[0].data.length)))){if(l[k].isEmbellished()){l.unshift(b.mi())}break}}}});f.multline=f.array.Subclass({type:"multline",Init:function(j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(j&&a.autoNumber!=="none");this.save={notag:i.global.notag};i.global.tagged=!j&&!i.global.forcetag},EndEntry:function(){if(this.table.length){this.fixInitialMO(this.data)}var i=b.mtd.apply(b,this.data);if(this.data.shove){i.columnalign=this.data.shove}this.row.push(i);this.data=[]},EndRow:function(){if(this.row.length!=1){h.Error(["MultlineRowsOneCol","The rows within the %1 environment must have exactly one column","multline"])}this.table.push(this.row);this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);if(this.table.length){var k=this.table.length-1,n,l=-1;if(!this.table[0][0].columnalign){this.table[0][0].columnalign=b.ALIGN.LEFT}if(!this.table[k][0].columnalign){this.table[k][0].columnalign=b.ALIGN.RIGHT}if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){l=(this.arraydef.side==="left"?0:this.table.length-1);this.table[l]=[this.getTag()].concat(this.table[l])}for(n=0,k=this.table.length;n<k;n++){var j=(n===l?b.mlabeledtr:b.mtr);this.table[n]=j.apply(b,this.table[n])}}this.global.notag=this.save.notag}});f.AMSarray=f.array.Subclass({type:"AMSarray",Init:function(l,k,j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(k&&a.autoNumber!=="none");this.save={notags:i.global.notags,notag:i.global.notag};i.global.notags=(j?null:l);i.global.tagged=!k&&!i.global.forcetag},EndEntry:function(){if(this.row.length){this.fixInitialMO(this.data)}this.row.push(b.mtd.apply(b,this.data));this.data=[]},EndRow:function(){var i=b.mtr;if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){this.row=[this.getTag()].concat(this.row);i=b.mlabeledtr}else{this.clearTag()}if(this.numbered){delete this.global.notag}this.table.push(i.apply(b,this.row));this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);this.global.notags=this.save.notags;this.global.notag=this.save.notag}});f.start.Augment({oldCheckItem:f.start.prototype.checkItem,checkItem:function(k){if(k.type==="stop"){var i=this.mmlData(),j=this.global;if(g.display&&!j.tag&&!j.tagged&&!j.isInner&&(a.autoNumber==="all"||j.forcetag)){this.autoTag()}if(j.tag){var m=[this.getTag(),b.mtd(i)];var l={side:h.config.TagSide,minlabelspacing:h.config.TagIndent,displaystyle:"inherit"};i=b.mtable(b.mlabeledtr.apply(b,m)).With(l)}return f.mml(i)}return this.oldCheckItem.call(this,k)}});h.prefilterHooks.Add(function(i){g.display=i.display;g.number=g.startNumber;g.eqlabels={};g.eqIDs={};g.badref=false;if(g.refUpdate){g.number=i.script.MathJax.startNumber}});h.postfilterHooks.Add(function(i){i.script.MathJax.startNumber=g.startNumber;g.startNumber=g.number;MathJax.Hub.Insert(g.IDs,g.eqIDs);MathJax.Hub.Insert(g.labels,g.eqlabels);if(g.badref&&!i.math.texError){g.refs.push(i.script)}},100);MathJax.Hub.Register.MessageHook("Begin Math Input",function(){g.refs=[];g.refUpdate=false});MathJax.Hub.Register.MessageHook("End Math Input",function(l){if(g.refs.length){g.refUpdate=true;for(var k=0,j=g.refs.length;k<j;k++){g.refs[k].MathJax.state=MathJax.ElementJax.STATE.UPDATE}return MathJax.Hub.processInput({scripts:g.refs,start:new Date().getTime(),i:0,j:0,jax:{},jaxIDs:[]})}return null});h.resetEquationNumbers=function(j,i){g.startNumber=(j||0);if(!i){g.labels={};g.IDs={}}};MathJax.Hub.Startup.signal.Post("TeX AMSmath Ready")});MathJax.Ajax.loadComplete("[MathJax]/extensions/TeX/AMSmath.js");
-+MathJax.Extension["TeX/AMSmath"]={version:"2.7.1",number:0,startNumber:0,IDs:{},eqIDs:{},labels:{},eqlabels:{},refs:[]};MathJax.Hub.Register.StartupHook("TeX Jax Ready",function(){var b=MathJax.ElementJax.mml,h=MathJax.InputJax.TeX,g=MathJax.Extension["TeX/AMSmath"];var d=h.Definitions,f=h.Stack.Item,a=h.config.equationNumbers;var c=function(k){var n=[];for(var l=0,j=k.length;l<j;l++){n[l]=h.Parse.prototype.Em(k[l])}return n.join(" ")};var e=(document.getElementsByTagName("base").length===0)?"":String(document.location).replace(/#.*$/,"");d.Add({mathchar0mo:{iiiint:["2A0C",{texClass:b.TEXCLASS.OP}]},macros:{mathring:["Accent","2DA"],nobreakspace:"Tilde",negmedspace:["Spacer",b.LENGTH.NEGATIVEMEDIUMMATHSPACE],negthickspace:["Spacer",b.LENGTH.NEGATIVETHICKMATHSPACE],idotsint:["MultiIntegral","\\int\\cdots\\int"],dddot:["Accent","20DB"],ddddot:["Accent","20DC"],sideset:["Macro","\\mathop{\\mathop{\\rlap{\\phantom{#3}}}\\nolimits#1\\!\\mathop{#3}\\nolimits#2}",3],boxed:["Macro","\\fbox{$\\displaystyle{#1}$}",1],tag:"HandleTag",notag:"HandleNoTag",label:"HandleLabel",ref:"HandleRef",eqref:["HandleRef",true],substack:["Macro","\\begin{subarray}{c}#1\\end{subarray}",1],injlim:["NamedOp","inj lim"],projlim:["NamedOp","proj lim"],varliminf:["Macro","\\mathop{\\underline{\\mmlToken{mi}{lim}}}"],varlimsup:["Macro","\\mathop{\\overline{\\mmlToken{mi}{lim}}}"],varinjlim:["Macro","\\mathop{\\underrightarrow{\\mmlToken{mi}{lim}}}"],varprojlim:["Macro","\\mathop{\\underleftarrow{\\mmlToken{mi}{lim}}}"],DeclareMathOperator:"HandleDeclareOp",operatorname:"HandleOperatorName",SkipLimits:"SkipLimits",genfrac:"Genfrac",frac:["Genfrac","","","",""],tfrac:["Genfrac","","","",1],dfrac:["Genfrac","","","",0],binom:["Genfrac","(",")","0",""],tbinom:["Genfrac","(",")","0",1],dbinom:["Genfrac","(",")","0",0],cfrac:"CFrac",shoveleft:["HandleShove",b.ALIGN.LEFT],shoveright:["HandleShove",b.ALIGN.RIGHT],xrightarrow:["xArrow",8594,5,6],xleftarrow:["xArrow",8592,7,3]},environment:{align:["AMSarray",null,true,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],"align*":["AMSarray",null,false,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],multline:["Multline",null,true],"multline*":["Multline",null,false],split:["AMSarray",null,false,false,"rl",c([0])],gather:["AMSarray",null,true,true,"c"],"gather*":["AMSarray",null,false,true,"c"],alignat:["AlignAt",null,true,true],"alignat*":["AlignAt",null,false,true],alignedat:["AlignAt",null,false,false],aligned:["AlignedAMSArray",null,null,null,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0]),".5em","D"],qaligned:["AlignedAMSArray",null,null,null,"rclrclrclrc",c([0,0,0,0,0,0,0,0,0,0,0]),"0em","D"],gathered:["AlignedAMSArray",null,null,null,"c",null,".5em","D"],subarray:["Array",null,null,null,null,c([0]),"0.1em","S",1],smallmatrix:["Array",null,null,null,"c",c([1/3]),".2em","S",1],equation:["EquationBegin","Equation",true],"equation*":["EquationBegin","EquationStar",false],eqnarray:["AMSarray",null,true,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"],"eqnarray*":["AMSarray",null,false,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"]},delimiter:{"\\lvert":["007C",{texClass:b.TEXCLASS.OPEN}],"\\rvert":["007C",{texClass:b.TEXCLASS.CLOSE}],"\\lVert":["2016",{texClass:b.TEXCLASS.OPEN}],"\\rVert":["2016",{texClass:b.TEXCLASS.CLOSE}]}},null,true);h.Parse.Augment({HandleTag:function(k){var m=this.GetStar();var j=this.trimSpaces(this.GetArgument(k)),i=j;if(!m){j=a.formatTag(j)}var l=this.stack.global;l.tagID=i;if(l.notags){h.Error(["CommandNotAllowedInEnv","%1 not allowed in %2 environment",k,l.notags])}if(l.tag){h.Error(["MultipleCommand","Multiple %1",k])}l.tag=b.mtd.apply(b,this.InternalMath(j)).With({id:a.formatID(i)})},HandleNoTag:function(i){if(this.stack.global.tag){delete this.stack.global.tag}this.stack.global.notag=true},HandleLabel:function(j){var k=this.stack.global,i=this.GetArgument(j);if(i===""){return}if(!g.refUpdate){if(k.label){h.Error(["MultipleCommand","Multiple %1",j])}k.label=i;if(g.labels[i]||g.eqlabels[i]){h.Error(["MultipleLabel","Label '%1' multiply defined",i])}g.eqlabels[i]={tag:"???",id:""}}},HandleRef:function(k,m){var j=this.GetArgument(k);var l=g.labels[j]||g.eqlabels[j];if(!l){l={tag:"???",id:""};g.badref=!g.refUpdate}var i=l.tag;if(m){i=a.formatTag(i)}this.Push(b.mrow.apply(b,this.InternalMath(i)).With({href:a.formatURL(l.id,e),"class":"MathJax_ref"}))},HandleDeclareOp:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));if(k.charAt(0)=="\\"){k=k.substr(1)}var l=this.GetArgument(j);l=l.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");h.Definitions.macros[k]=["Macro","\\mathop{\\rm "+l+"}"+i]},HandleOperatorName:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));k=k.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");this.string="\\mathop{\\rm "+k+"}"+i+" "+this.string.slice(this.i);this.i=0},SkipLimits:function(j){var l=this.GetNext(),k=this.i;if(l==="\\"&&++this.i&&this.GetCS()!=="limits"){this.i=k}},HandleShove:function(j,i){var k=this.stack.Top();if(k.type!=="multline"||k.data.length){h.Error(["CommandAtTheBeginingOfLine","%1 must come at the beginning of the line",j])}k.data.shove=i},CFrac:function(l){var i=this.trimSpaces(this.GetBrackets(l,"")),k=this.GetArgument(l),m=this.GetArgument(l);var j=b.mfrac(h.Parse("\\strut\\textstyle{"+k+"}",this.stack.env).mml(),h.Parse("\\strut\\textstyle{"+m+"}",this.stack.env).mml());i=({l:b.ALIGN.LEFT,r:b.ALIGN.RIGHT,"":""})[i];if(i==null){h.Error(["IllegalAlign","Illegal alignment specified in %1",l])}if(i){j.numalign=j.denomalign=i}this.Push(j)},Genfrac:function(j,l,q,n,i){if(l==null){l=this.GetDelimiterArg(j)}if(q==null){q=this.GetDelimiterArg(j)}if(n==null){n=this.GetArgument(j)}if(i==null){i=this.trimSpaces(this.GetArgument(j))}var m=this.ParseArg(j);var p=this.ParseArg(j);var k=b.mfrac(m,p);if(n!==""){k.linethickness=n}if(l||q){k=h.fixedFence(l,k.With({texWithDelims:true}),q)}if(i!==""){var o=(["D","T","S","SS"])[i];if(o==null){h.Error(["BadMathStyleFor","Bad math style for %1",j])}k=b.mstyle(k);if(o==="D"){k.displaystyle=true;k.scriptlevel=0}else{k.displaystyle=false;k.scriptlevel=i-1}}this.Push(k)},Multline:function(j,i){this.Push(j);this.checkEqnEnv();return f.multline(i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",width:h.config.MultLineWidth,columnwidth:"100%",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AMSarray:function(k,j,i,m,l){this.Push(k);if(i){this.checkEqnEnv()}m=m.replace(/[^clr]/g,"").split("").join(" ");m=m.replace(/l/g,"left").replace(/r/g,"right").replace(/c/g,"center");return f.AMSarray(k.name,j,i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",columnalign:m,columnspacing:(l||"1em"),rowspacing:"3pt",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AlignedAMSArray:function(i){var j=this.GetBrackets("\\begin{"+i.name+"}");return this.setArrayAlign(this.AMSarray.apply(this,arguments),j)},AlignAt:function(l,j,i){var q,k,p="",o=[];if(!i){k=this.GetBrackets("\\begin{"+l.name+"}")}q=this.GetArgument("\\begin{"+l.name+"}");if(q.match(/[^0-9]/)){h.Error(["PositiveIntegerArg","Argument to %1 must me a positive integer","\\begin{"+l.name+"}"])}while(q>0){p+="rl";o.push("0em 0em");q--}o=o.join(" ");if(i){return this.AMSarray(l,j,i,p,o)}var m=this.AMSarray(l,j,i,p,o);return this.setArrayAlign(m,k)},EquationBegin:function(i,j){this.checkEqnEnv();this.stack.global.forcetag=(j&&a.autoNumber!=="none");return i},EquationStar:function(i,j){this.stack.global.tagged=true;return j},checkEqnEnv:function(){if(this.stack.global.eqnenv){h.Error(["ErroneousNestingEq","Erroneous nesting of equation structures"])}this.stack.global.eqnenv=true},MultiIntegral:function(j,m){var l=this.GetNext();if(l==="\\"){var k=this.i;l=this.GetArgument(j);this.i=k;if(l==="\\limits"){if(j==="\\idotsint"){m="\\!\\!\\mathop{\\,\\,"+m+"}"}else{m="\\!\\!\\!\\mathop{\\,\\,\\,"+m+"}"}}}this.string=m+" "+this.string.slice(this.i);this.i=0},xArrow:function(k,o,n,i){var m={width:"+"+(n+i)+"mu",lspace:n+"mu"};var p=this.GetBrackets(k),q=this.ParseArg(k);var s=b.mo(b.chars(String.fromCharCode(o))).With({stretchy:true,texClass:b.TEXCLASS.REL});var j=b.munderover(s);j.SetData(j.over,b.mpadded(q).With(m).With({voffset:".15em"}));if(p){p=h.Parse(p,this.stack.env).mml();j.SetData(j.under,b.mpadded(p).With(m).With({voffset:"-.24em"}))}this.Push(j.With({subsupOK:true}))},GetDelimiterArg:function(i){var j=this.trimSpaces(this.GetArgument(i));if(j==""){return null}if(j in d.delimiter){return j}h.Error(["MissingOrUnrecognizedDelim","Missing or unrecognized delimiter for %1",i])},GetStar:function(){var i=(this.GetNext()==="*");if(i){this.i++}return i}});f.Augment({autoTag:function(){var j=this.global;if(!j.notag){g.number++;j.tagID=a.formatNumber(g.number.toString());var i=h.Parse("\\text{"+a.formatTag(j.tagID)+"}",{}).mml();j.tag=b.mtd(i).With({id:a.formatID(j.tagID)})}},getTag:function(){var m=this.global,k=m.tag;m.tagged=true;if(m.label){if(a.useLabelIds){k.id=a.formatID(m.label)}g.eqlabels[m.label]={tag:m.tagID,id:k.id}}if(document.getElementById(k.id)||g.IDs[k.id]||g.eqIDs[k.id]){var l=0,j;do{l++;j=k.id+"_"+l}while(document.getElementById(j)||g.IDs[j]||g.eqIDs[j]);k.id=j;if(m.label){g.eqlabels[m.label].id=j}}g.eqIDs[k.id]=1;this.clearTag();return k},clearTag:function(){var i=this.global;delete i.tag;delete i.tagID;delete i.label},fixInitialMO:function(l){for(var k=0,j=l.length;k<j;k++){if(l[k]&&(l[k].type!=="mspace"&&(l[k].type!=="texatom"||(l[k].data[0]&&l[k].data[0].data.length)))){if(l[k].isEmbellished()){l.unshift(b.mi())}break}}}});f.multline=f.array.Subclass({type:"multline",Init:function(j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(j&&a.autoNumber!=="none");this.save={notag:i.global.notag};i.global.tagged=!j&&!i.global.forcetag},EndEntry:function(){if(this.table.length){this.fixInitialMO(this.data)}var i=b.mtd.apply(b,this.data);if(this.data.shove){i.columnalign=this.data.shove}this.row.push(i);this.data=[]},EndRow:function(){if(this.row.length!=1){h.Error(["MultlineRowsOneCol","The rows within the %1 environment must have exactly one column","multline"])}this.table.push(this.row);this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);if(this.table.length){var k=this.table.length-1,n,l=-1;if(!this.table[0][0].columnalign){this.table[0][0].columnalign=b.ALIGN.LEFT}if(!this.table[k][0].columnalign){this.table[k][0].columnalign=b.ALIGN.RIGHT}if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){l=(this.arraydef.side==="left"?0:this.table.length-1);this.table[l]=[this.getTag()].concat(this.table[l])}for(n=0,k=this.table.length;n<k;n++){var j=(n===l?b.mlabeledtr:b.mtr);this.table[n]=j.apply(b,this.table[n])}}this.global.notag=this.save.notag}});f.AMSarray=f.array.Subclass({type:"AMSarray",Init:function(l,k,j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(k&&a.autoNumber!=="none");this.save={notags:i.global.notags,notag:i.global.notag};i.global.notags=(j?null:l);i.global.tagged=!k&&!i.global.forcetag},EndEntry:function(){if(this.row.length){this.fixInitialMO(this.data)}this.row.push(b.mtd.apply(b,this.data));this.data=[]},EndRow:function(){var i=b.mtr;if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){this.row=[this.getTag()].concat(this.row);i=b.mlabeledtr}else{this.clearTag()}if(this.numbered){delete this.global.notag}this.table.push(i.apply(b,this.row));this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);this.global.notags=this.save.notags;this.global.notag=this.save.notag}});f.start.Augment({oldCheckItem:f.start.prototype.checkItem,checkItem:function(k){if(k.type==="stop"){var i=this.mmlData(),j=this.global;if(g.display&&!j.tag&&!j.tagged&&!j.isInner&&(a.autoNumber==="all"||j.forcetag)){this.autoTag()}if(j.tag){var m=[this.getTag(),b.mtd(i)];var l={side:h.config.TagSide,minlabelspacing:h.config.TagIndent,displaystyle:"inherit"};i=b.mtable(b.mlabeledtr.apply(b,m)).With(l)}return f.mml(i)}return this.oldCheckItem.call(this,k)}});h.prefilterHooks.Add(function(i){g.display=i.display;g.number=g.startNumber;g.eqlabels={};g.eqIDs={};g.badref=false;if(g.refUpdate){g.number=i.script.MathJax.startNumber}});h.postfilterHooks.Add(function(i){i.script.MathJax.startNumber=g.startNumber;g.startNumber=g.number;MathJax.Hub.Insert(g.IDs,g.eqIDs);MathJax.Hub.Insert(g.labels,g.eqlabels);if(g.badref&&!i.math.texError){g.refs.push(i.script)}},100);MathJax.Hub.Register.MessageHook("Begin Math Input",function(){g.refs=[];g.refUpdate=false});MathJax.Hub.Register.MessageHook("End Math Input",function(l){if(g.refs.length){g.refUpdate=true;for(var k=0,j=g.refs.length;k<j;k++){g.refs[k].MathJax.state=MathJax.ElementJax.STATE.UPDATE}return MathJax.Hub.processInput({scripts:g.refs,start:new Date().getTime(),i:0,j:0,jax:{},jaxIDs:[]})}return null});h.resetEquationNumbers=function(j,i){g.startNumber=(j||0);if(!i){g.labels={};g.IDs={}}};MathJax.Hub.Startup.signal.Post("TeX AMSmath Ready")});MathJax.Ajax.loadComplete("[MathJax]/extensions/TeX/AMSmath.js");
++MathJax.Extension["TeX/AMSmath"]={version:"2.7.1",number:0,startNumber:0,IDs:{},eqIDs:{},labels:{},eqlabels:{},refs:[]};MathJax.Hub.Register.StartupHook("TeX Jax Ready",function(){var b=MathJax.ElementJax.mml,h=MathJax.InputJax.TeX,g=MathJax.Extension["TeX/AMSmath"];var d=h.Definitions,f=h.Stack.Item,a=h.config.equationNumbers;var c=function(k){var n=[];for(var l=0,j=k.length;l<j;l++){n[l]=h.Parse.prototype.Em(k[l])}return n.join(" ")};var e=(document.getElementsByTagName("base").length===0)?"":String(document.location).replace(/#.*$/,"");d.Add({mathchar0mo:{iiiint:["2A0C",{texClass:b.TEXCLASS.OP}]},macros:{mathring:["Accent","2DA"],nobreakspace:"Tilde",negmedspace:["Spacer",b.LENGTH.NEGATIVEMEDIUMMATHSPACE],negthickspace:["Spacer",b.LENGTH.NEGATIVETHICKMATHSPACE],idotsint:["MultiIntegral","\\int\\cdots\\int"],dddot:["Accent","20DB"],ddddot:["Accent","20DC"],sideset:["Macro","\\mathop{\\mathop{\\rlap{\\phantom{#3}}}\\nolimits#1\\!\\mathop{#3}\\nolimits#2}",3],boxed:["Macro","\\fbox{$\\displaystyle{#1}$}",1],tag:"HandleTag",notag:"HandleNoTag",label:"HandleLabel",ref:"HandleRef",eqref:["HandleRef",true],substack:["Macro","\\begin{subarray}{c}#1\\end{subarray}",1],injlim:["NamedOp","inj lim"],projlim:["NamedOp","proj lim"],varliminf:["Macro","\\mathop{\\underline{\\mmlToken{mi}{lim}}}"],varlimsup:["Macro","\\mathop{\\overline{\\mmlToken{mi}{lim}}}"],varinjlim:["Macro","\\mathop{\\underrightarrow{\\mmlToken{mi}{lim}}}"],varprojlim:["Macro","\\mathop{\\underleftarrow{\\mmlToken{mi}{lim}}}"],DeclareMathOperator:"HandleDeclareOp",operatorname:"HandleOperatorName",SkipLimits:"SkipLimits",genfrac:"Genfrac",frac:["Genfrac","","","",""],tfrac:["Genfrac","","","",1],dfrac:["Genfrac","","","",0],binom:["Genfrac","(",")","0",""],tbinom:["Genfrac","(",")","0",1],dbinom:["Genfrac","(",")","0",0],cfrac:"CFrac",shoveleft:["HandleShove",b.ALIGN.LEFT],shoveright:["HandleShove",b.ALIGN.RIGHT],xrightarrow:["xArrow",8594,5,6],xleftarrow:["xArrow",8592,7,3]},environment:{align:["AMSarray",null,true,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],"align*":["AMSarray",null,false,true,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0])],multline:["Multline",null,true],"multline*":["Multline",null,false],split:["AMSarray",null,false,false,"rl",c([0])],gather:["AMSarray",null,true,true,"c"],"gather*":["AMSarray",null,false,true,"c"],alignat:["AlignAt",null,true,true],"alignat*":["AlignAt",null,false,true],alignedat:["AlignAt",null,false,false],aligned:["AlignedAMSArray",null,null,null,"rlrlrlrlrlrl",c([0,2,0,2,0,2,0,2,0,2,0]),".5em","D"],qaligned:["AlignedAMSArray",null,null,true,"rclrclrclrc",c([0,0,0,0,0,0,0,0,0,0,0]),"0em","D"],gathered:["AlignedAMSArray",null,null,null,"c",null,".5em","D"],subarray:["Array",null,null,null,null,c([0]),"0.1em","S",1],smallmatrix:["Array",null,null,null,"c",c([1/3]),".2em","S",1],equation:["EquationBegin","Equation",true],"equation*":["EquationBegin","EquationStar",false],eqnarray:["AMSarray",null,true,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"],"eqnarray*":["AMSarray",null,false,true,"rcl","0 "+b.LENGTH.THICKMATHSPACE,".5em"]},delimiter:{"\\lvert":["007C",{texClass:b.TEXCLASS.OPEN}],"\\rvert":["007C",{texClass:b.TEXCLASS.CLOSE}],"\\lVert":["2016",{texClass:b.TEXCLASS.OPEN}],"\\rVert":["2016",{texClass:b.TEXCLASS.CLOSE}]}},null,true);h.Parse.Augment({HandleTag:function(k){var m=this.GetStar();var j=this.trimSpaces(this.GetArgument(k)),i=j;if(!m){j=a.formatTag(j)}var l=this.stack.global;l.tagID=i;if(l.notags){h.Error(["CommandNotAllowedInEnv","%1 not allowed in %2 environment",k,l.notags])}if(l.tag){h.Error(["MultipleCommand","Multiple %1",k])}l.tag=b.mtd.apply(b,this.InternalMath(j)).With({id:a.formatID(i)})},HandleNoTag:function(i){if(this.stack.global.tag){delete this.stack.global.tag}this.stack.global.notag=true},HandleLabel:function(j){var k=this.stack.global,i=this.GetArgument(j);if(i===""){return}if(!g.refUpdate){if(k.label){h.Error(["MultipleCommand","Multiple %1",j])}k.label=i;if(g.labels[i]||g.eqlabels[i]){h.Error(["MultipleLabel","Label '%1' multiply defined",i])}g.eqlabels[i]={tag:"???",id:""}}},HandleRef:function(k,m){var j=this.GetArgument(k);var l=g.labels[j]||g.eqlabels[j];if(!l){l={tag:"???",id:""};g.badref=!g.refUpdate}var i=l.tag;if(m){i=a.formatTag(i)}this.Push(b.mrow.apply(b,this.InternalMath(i)).With({href:a.formatURL(l.id,e),"class":"MathJax_ref"}))},HandleDeclareOp:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));if(k.charAt(0)=="\\"){k=k.substr(1)}var l=this.GetArgument(j);l=l.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");h.Definitions.macros[k]=["Macro","\\mathop{\\rm "+l+"}"+i]},HandleOperatorName:function(j){var i=(this.GetStar()?"":"\\nolimits\\SkipLimits");var k=this.trimSpaces(this.GetArgument(j));k=k.replace(/\*/g,"\\text{*}").replace(/-/g,"\\text{-}");this.string="\\mathop{\\rm "+k+"}"+i+" "+this.string.slice(this.i);this.i=0},SkipLimits:function(j){var l=this.GetNext(),k=this.i;if(l==="\\"&&++this.i&&this.GetCS()!=="limits"){this.i=k}},HandleShove:function(j,i){var k=this.stack.Top();if(k.type!=="multline"||k.data.length){h.Error(["CommandAtTheBeginingOfLine","%1 must come at the beginning of the line",j])}k.data.shove=i},CFrac:function(l){var i=this.trimSpaces(this.GetBrackets(l,"")),k=this.GetArgument(l),m=this.GetArgument(l);var j=b.mfrac(h.Parse("\\strut\\textstyle{"+k+"}",this.stack.env).mml(),h.Parse("\\strut\\textstyle{"+m+"}",this.stack.env).mml());i=({l:b.ALIGN.LEFT,r:b.ALIGN.RIGHT,"":""})[i];if(i==null){h.Error(["IllegalAlign","Illegal alignment specified in %1",l])}if(i){j.numalign=j.denomalign=i}this.Push(j)},Genfrac:function(j,l,q,n,i){if(l==null){l=this.GetDelimiterArg(j)}if(q==null){q=this.GetDelimiterArg(j)}if(n==null){n=this.GetArgument(j)}if(i==null){i=this.trimSpaces(this.GetArgument(j))}var m=this.ParseArg(j);var p=this.ParseArg(j);var k=b.mfrac(m,p);if(n!==""){k.linethickness=n}if(l||q){k=h.fixedFence(l,k.With({texWithDelims:true}),q)}if(i!==""){var o=(["D","T","S","SS"])[i];if(o==null){h.Error(["BadMathStyleFor","Bad math style for %1",j])}k=b.mstyle(k);if(o==="D"){k.displaystyle=true;k.scriptlevel=0}else{k.displaystyle=false;k.scriptlevel=i-1}}this.Push(k)},Multline:function(j,i){this.Push(j);this.checkEqnEnv();return f.multline(i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",width:h.config.MultLineWidth,columnwidth:"100%",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AMSarray:function(k,j,i,m,l){this.Push(k);if(i){this.checkEqnEnv()}m=m.replace(/[^clr]/g,"").split("").join(" ");m=m.replace(/l/g,"left").replace(/r/g,"right").replace(/c/g,"center");return f.AMSarray(k.name,j,i,this.stack).With({arraydef:{displaystyle:true,rowspacing:".5em",columnalign:m,columnspacing:(l||"1em"),rowspacing:"3pt",side:h.config.TagSide,minlabelspacing:h.config.TagIndent}})},AlignedAMSArray:function(i){var j=this.GetBrackets("\\begin{"+i.name+"}");return this.setArrayAlign(this.AMSarray.apply(this,arguments),j)},AlignAt:function(l,j,i){var q,k,p="",o=[];if(!i){k=this.GetBrackets("\\begin{"+l.name+"}")}q=this.GetArgument("\\begin{"+l.name+"}");if(q.match(/[^0-9]/)){h.Error(["PositiveIntegerArg","Argument to %1 must me a positive integer","\\begin{"+l.name+"}"])}while(q>0){p+="rl";o.push("0em 0em");q--}o=o.join(" ");if(i){return this.AMSarray(l,j,i,p,o)}var m=this.AMSarray(l,j,i,p,o);return this.setArrayAlign(m,k)},EquationBegin:function(i,j){this.checkEqnEnv();this.stack.global.forcetag=(j&&a.autoNumber!=="none");return i},EquationStar:function(i,j){this.stack.global.tagged=true;return j},checkEqnEnv:function(){if(this.stack.global.eqnenv){h.Error(["ErroneousNestingEq","Erroneous nesting of equation structures"])}this.stack.global.eqnenv=true},MultiIntegral:function(j,m){var l=this.GetNext();if(l==="\\"){var k=this.i;l=this.GetArgument(j);this.i=k;if(l==="\\limits"){if(j==="\\idotsint"){m="\\!\\!\\mathop{\\,\\,"+m+"}"}else{m="\\!\\!\\!\\mathop{\\,\\,\\,"+m+"}"}}}this.string=m+" "+this.string.slice(this.i);this.i=0},xArrow:function(k,o,n,i){var m={width:"+"+(n+i)+"mu",lspace:n+"mu"};var p=this.GetBrackets(k),q=this.ParseArg(k);var s=b.mo(b.chars(String.fromCharCode(o))).With({stretchy:true,texClass:b.TEXCLASS.REL});var j=b.munderover(s);j.SetData(j.over,b.mpadded(q).With(m).With({voffset:".15em"}));if(p){p=h.Parse(p,this.stack.env).mml();j.SetData(j.under,b.mpadded(p).With(m).With({voffset:"-.24em"}))}this.Push(j.With({subsupOK:true}))},GetDelimiterArg:function(i){var j=this.trimSpaces(this.GetArgument(i));if(j==""){return null}if(j in d.delimiter){return j}h.Error(["MissingOrUnrecognizedDelim","Missing or unrecognized delimiter for %1",i])},GetStar:function(){var i=(this.GetNext()==="*");if(i){this.i++}return i}});f.Augment({autoTag:function(){var j=this.global;if(!j.notag){g.number++;j.tagID=a.formatNumber(g.number.toString());var i=h.Parse("\\text{"+a.formatTag(j.tagID)+"}",{}).mml();j.tag=b.mtd(i).With({id:a.formatID(j.tagID)})}},getTag:function(){var m=this.global,k=m.tag;m.tagged=true;if(m.label){if(a.useLabelIds){k.id=a.formatID(m.label)}g.eqlabels[m.label]={tag:m.tagID,id:k.id}}if(document.getElementById(k.id)||g.IDs[k.id]||g.eqIDs[k.id]){var l=0,j;do{l++;j=k.id+"_"+l}while(document.getElementById(j)||g.IDs[j]||g.eqIDs[j]);k.id=j;if(m.label){g.eqlabels[m.label].id=j}}g.eqIDs[k.id]=1;this.clearTag();return k},clearTag:function(){var i=this.global;delete i.tag;delete i.tagID;delete i.label},fixInitialMO:function(l){for(var k=0,j=l.length;k<j;k++){if(l[k]&&(l[k].type!=="mspace"&&(l[k].type!=="texatom"||(l[k].data[0]&&l[k].data[0].data.length)))){if(l[k].isEmbellished()){l.unshift(b.mi())}break}}}});f.multline=f.array.Subclass({type:"multline",Init:function(j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(j&&a.autoNumber!=="none");this.save={notag:i.global.notag};i.global.tagged=!j&&!i.global.forcetag},EndEntry:function(){if(this.table.length){this.fixInitialMO(this.data)}var i=b.mtd.apply(b,this.data);if(this.data.shove){i.columnalign=this.data.shove}this.row.push(i);this.data=[]},EndRow:function(){if(this.row.length!=1){h.Error(["MultlineRowsOneCol","The rows within the %1 environment must have exactly one column","multline"])}this.table.push(this.row);this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);if(this.table.length){var k=this.table.length-1,n,l=-1;if(!this.table[0][0].columnalign){this.table[0][0].columnalign=b.ALIGN.LEFT}if(!this.table[k][0].columnalign){this.table[k][0].columnalign=b.ALIGN.RIGHT}if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){l=(this.arraydef.side==="left"?0:this.table.length-1);this.table[l]=[this.getTag()].concat(this.table[l])}for(n=0,k=this.table.length;n<k;n++){var j=(n===l?b.mlabeledtr:b.mtr);this.table[n]=j.apply(b,this.table[n])}}this.global.notag=this.save.notag}});f.AMSarray=f.array.Subclass({type:"AMSarray",Init:function(l,k,j,i){this.SUPER(arguments).Init.apply(this);this.numbered=(k&&a.autoNumber!=="none");this.save={notags:i.global.notags,notag:i.global.notag};i.global.notags=(j?null:l);i.global.tagged=!k&&!i.global.forcetag},EndEntry:function(){if(this.row.length){this.fixInitialMO(this.data)}this.row.push(b.mtd.apply(b,this.data));this.data=[]},EndRow:function(){var i=b.mtr;if(!this.global.tag&&this.numbered){this.autoTag()}if(this.global.tag&&!this.global.notags){this.row=[this.getTag()].concat(this.row);i=b.mlabeledtr}else{this.clearTag()}if(this.numbered){delete this.global.notag}this.table.push(i.apply(b,this.row));this.row=[]},EndTable:function(){this.SUPER(arguments).EndTable.call(this);this.global.notags=this.save.notags;this.global.notag=this.save.notag}});f.start.Augment({oldCheckItem:f.start.prototype.checkItem,checkItem:function(k){if(k.type==="stop"){var i=this.mmlData(),j=this.global;if(g.display&&!j.tag&&!j.tagged&&!j.isInner&&(a.autoNumber==="all"||j.forcetag)){this.autoTag()}if(j.tag){var m=[this.getTag(),b.mtd(i)];var l={side:h.config.TagSide,minlabelspacing:h.config.TagIndent,displaystyle:"inherit"};i=b.mtable(b.mlabeledtr.apply(b,m)).With(l)}return f.mml(i)}return this.oldCheckItem.call(this,k)}});h.prefilterHooks.Add(function(i){g.display=i.display;g.number=g.startNumber;g.eqlabels={};g.eqIDs={};g.badref=false;if(g.refUpdate){g.number=i.script.MathJax.startNumber}});h.postfilterHooks.Add(function(i){i.script.MathJax.startNumber=g.startNumber;g.startNumber=g.number;MathJax.Hub.Insert(g.IDs,g.eqIDs);MathJax.Hub.Insert(g.labels,g.eqlabels);if(g.badref&&!i.math.texError){g.refs.push(i.script)}},100);MathJax.Hub.Register.MessageHook("Begin Math Input",function(){g.refs=[];g.refUpdate=false});MathJax.Hub.Register.MessageHook("End Math Input",function(l){if(g.refs.length){g.refUpdate=true;for(var k=0,j=g.refs.length;k<j;k++){g.refs[k].MathJax.state=MathJax.ElementJax.STATE.UPDATE}return MathJax.Hub.processInput({scripts:g.refs,start:new Date().getTime(),i:0,j:0,jax:{},jaxIDs:[]})}return null});h.resetEquationNumbers=function(j,i){g.startNumber=(j||0);if(!i){g.labels={};g.IDs={}}};MathJax.Hub.Startup.signal.Post("TeX AMSmath Ready")});MathJax.Ajax.loadComplete("[MathJax]/extensions/TeX/AMSmath.js");
diff -r -u ./node_modules.orig/mathjax/jax/input/TeX/jax.js ./node_modules/mathjax/jax/input/TeX/jax.js
--- ./node_modules.orig/mathjax/jax/input/TeX/jax.js 2017-04-25 10:30:45.000000000 +0200
+++ ./node_modules/mathjax/jax/input/TeX/jax.js 2017-07-13 14:10:01.151263588 +0200
@@ -23,7 +23,7 @@ diff -r -u ./node_modules.orig/mathjax/unpacked/extensions/TeX/AMSmath.js ./node
alignedat: ['AlignAt',null,false,false],
aligned: ['AlignedAMSArray',null,null,null,'rlrlrlrlrlrl',COLS([0,2,0,2,0,2,0,2,0,2,0]),".5em",'D'],
-+ qaligned: ["AlignedAMSArray",null,null,null,"rclrclrclrc",COLS([0,0,0,0,0,0,0,0,0,0,0]),"0em","D"],
++ qaligned: ["AlignedAMSArray",null,null,true,"rclrclrclrc",COLS([0,0,0,0,0,0,0,0,0,0,0]),"0em","D"],
gathered: ['AlignedAMSArray',null,null,null,'c',null,".5em",'D'],
subarray: ['Array',null,null,null,null,COLS([0]),"0.1em",'S',1],
diff --git a/scribblings/adt-pe.scrbl b/scribblings/adt-pe.scrbl
@@ -12,7 +12,7 @@
We extend the metafunctions for paths given
in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${
- \mathop{update}} metafunction is used when using filters to restrict the type
+ @update} metafunction is used when using filters to restrict the type
of a (subpart of a) local variable in the @tt{then} and @tt{else} branches of
a conditional.
@@ -24,12 +24,12 @@ a conditional.
@$${
@aligned{
- \mathop{update}(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
+ @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
&= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
- @${@|ɐ|ⱼ : @${\mathop{update}(τⱼ, υ_π)}}]
+ @${@|ɐ|ⱼ : @${@update(τⱼ, υ_π)}}]
\\
&\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\
- \mathop{update}(@ctor[@κ τ], υ_{π∷@πctor-val})
- &= @ctor[@κ @${\mathop{update}(τ, υ_π)}]
+ @update(@ctor[@κ τ], υ_{π∷@πctor-val})
+ &= @ctor[@κ @${@update(τ, υ_π)}]
}
}
\ No newline at end of file
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -14,7 +14,7 @@
We extend the metafunctions for paths given
in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${
- \mathop{update}} metafunction is used when using filters to restrict the type
+ @update} metafunction is used when using filters to restrict the type
of a (subpart of a) local variable in the @tt{then} and @tt{else} branches of
a conditional.
@@ -26,12 +26,12 @@ a conditional.
@$${
@aligned{
- \mathop{update}(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
+ @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
&= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
- @${@|ɐ|ⱼ : @${\mathop{update}(τⱼ, υ_π)}}]
+ @${@|ɐ|ⱼ : @${@update(τⱼ, υ_π)}}]
\\
&\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\
- \mathop{update}(@ctor[@κ τ], υ_{π∷@πctor-val})
- &= @ctor[@κ @${\mathop{update}(τ, υ_π)}]
+ @update(@ctor[@κ τ], υ_{π∷@πctor-val})
+ &= @ctor[@κ @${@update(τ, υ_π)}]
}
}
\ No newline at end of file
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -21,7 +21,7 @@
]
}
-@${\mathop{@textit{applyfilter}}} is defined
+@${@applyfilter} is defined
in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@htodo{their second (p. 75) definition of applyfilter does not clearly state
@@ -34,7 +34,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
φ_r
- = \mathop{@textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
+ = @applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
@${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Ctor-Pred}}
]
@@ -52,7 +52,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{@textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
@${@textsc{T-Ctor-Val}}
@@ -71,7 +71,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = \mathop{@textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
+ φ_r = @applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Record-Pred}}
@@ -87,7 +87,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{@textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
@${@textsc{T-Record-GetField}}
diff --git a/scribblings/adt-trules.scrbl b/scribblings/adt-trules.scrbl
@@ -21,7 +21,7 @@
]
}
-@${\mathop{\textit{applyfilter}}} is defined
+@${@applyfilter} is defined
in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@htodo{their second (p. 75) definition of applyfilter does not clearly state
@@ -34,17 +34,13 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
φ_r
- = \mathop{\textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
+ = @applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
@${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Ctor-Pred}}
]
}
-@(define & @cond-element[[latex "\\savedamp"] [else "&"]])
-@(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]])
-
@$${
- @cond-element[[latex @list{\let\savedamp&}] [else ""]]
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@κ @${τ'}] \\
o_r = @"\\left\\{" \begin{array}{rl}
@@ -52,7 +48,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
@${@textsc{T-Ctor-Val}}
@@ -71,7 +67,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = \mathop{\textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
+ φ_r = @applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Record-Pred}}
@@ -87,7 +83,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
@${@textsc{T-Record-GetField}}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -109,7 +109,14 @@
(define-syntax num-τ* (defop "num"))
(define num-e @num-e*[n])
(define num-v @num-v*[n])
-(define num-τ @num-τ*[n])
+(define-syntax num-τ
+ (syntax-parser
+ [(_ n) #'@num-τ*[n]]
+ [self:id #'@num-τ*[n]])) ;; n by default
+
+(define-syntax nullv (defop @${@textit{null}}))
+(define-syntax nulle (defop "null"))
+(define-syntax nullτ (defop "null"))
(define-syntax true-e (defop "true"))
(define-syntax true-v (defop @${@textit{true}}))
@@ -149,18 +156,39 @@
@${@(stringify α) \mathbf{…}})
@;(define-syntax →Values (defop "Values"))
(define-syntax-rule (→Values v ...) (spaces (stringify v) ...))
-(define @emptypath @${ϵ} #;@${•})
+(define @emptypath @${ϵ})
(define-syntax-rule (<: a b)
@${⊢ @(stringify a) \mathrel{<:} @(stringify b)})
(define-syntax-rule (<:R a b)
@${⊢ @(stringify a) \mathrel{{<:}_R} @(stringify b)})
-@(define-syntax (Γ stx)
- (syntax-case stx (⊢)
- [(_ more ... ⊢ x τ φ+ φ- o)
- #'@${@(add-between (list "Γ" (stringify more) ...) ", ") ⊢
+@(define-syntax Γ
+ (syntax-parser
+ #:literals (+) #:datum-literals (⊢)
+ [(_ {~and {~not +} more} ... {~optional {~seq + φ}} ⊢ x τ φ⁺ φ⁻ o)
+ #`@${@(add-between (list "Γ" (stringify more) ...) ", ")
+ @#,@(if (attribute φ) @list{+ @#'(stringify φ)} @list{}) ⊢
@(stringify x)
: @(stringify τ)
- ; @(stringify φ+) / @(stringify φ-)
- ; @(stringify o)}]))
-\ No newline at end of file
+ ; @(stringify φ⁺) / @(stringify φ⁻)
+ ; @(stringify o)}]))
+@(define-syntax subst
+ (syntax-parser
+ [(_ {~seq from {~literal ↦} to} ...)
+ #'@$["[" (list (stringify from) "↦" (stringify to)) ... "]"]]))
+@(define-syntax substφo
+ (syntax-parser
+ [(_ from {~literal ↦} to)
+ #'@$["{|}_{{" (stringify from) "}↦{" (stringify to) "}}"]]))
+
+(define update "\\operatorname{update}")
+(define applyfilter "\\operatorname{applyfilter}")
+(define combinefilter "\\operatorname{combinefilter}")
+(define no-overlap "\\operatorname{no-overlap}")
+(define restrict "\\operatorname{restrict}")
+(define remove "\\operatorname{remove}")
+(define loc "\\mathit{loc}")
+(define (! . rest) (list "\\overline{" rest "}"))
+(define metatrue "\\mathrm{true}")
+(define metafalse "\\mathrm{false}")
+\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -48,7 +48,11 @@
textbf
textit
textrm
- text)
+ text
+ &
+ nl
+ tag*
+ tag)
(require racket/stxparam
racket/splicing
@@ -494,14 +498,16 @@ EOTEX
(string->bytes/utf-8
"\\usepackage{mathpartir}"))))
($ (cond-element [html "\\frac{\\begin{gathered}"]
- [else "\\inferrule{"])
- from*
+ [else (string-append "\\ifcsname savedamp\\endcsname"
+ "\\else\\let\\savedamp&\\fi"
+ "\\inferrule{")])
+ (if (eq? from* -) "\\vphantom{x}" from*)
(cond-element [html "\\end{gathered}}{\\begin{gathered}"]
[else "}{"])
- to*
+ (if (eq? to* -) "\\vphantom{x}" to*)
(cond-element [html "\\end{gathered}}"]
[else "}"])
- label))])
+ "\\ " label))])
(define htmldiff-css-experiment #<<EOCSS
.version:after {
@@ -550,7 +556,7 @@ EOCSS
(define (aligned #:valign [valign 'mid] . lines)
(define valign-letter (case valign [(top) "t"] [(mid) "m"] [(bot) "b"]))
- @list{
+ @$${
\begin{aligned}[@valign-letter]
@lines
\end{aligned}
@@ -648,3 +654,41 @@ EOCSS
(define (textit . l) (mathtext "\\textit{" l "}"))
(define (textrm . l) (mathtext "\\textrm{" l "}"))
(define (text . l) (mathtext "\\text{" l "}"))
+
+;; In some cases, LaTeX doesn't like the use of the regular & and \\ because
+;; they were redefined (mostly when placing arrays or cases within an inferrule.
+;; For now, we just use this simple workaround
+(define & @cond-element[[latex "\\savedamp"] [else "&"]])
+(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]])
+
+(define-runtime-path tikztag.sty "../tikztag.sty")
+(define ((tag** starred?) . txt)
+ (cond-element
+ [html (list "\\hphantom{"
+ (text (if starred? "" "(")
+ txt
+ (if starred? "" ")"))
+ "}"
+ "\\tag*{"
+ (mathtext
+ ($ "\\llap{"
+ (text (if starred? "" "(")
+ txt
+ (if starred? "" ")"))
+ "}"))
+ "}")]
+ [latex (elem #:style (style #f (list (tex-addition
+ ;; The \n are important in case the
+ ;; file does not end with a newline
+ ;; but ends with a comment (it gobbles
+ ;; the \makeatother and the following
+ ;; commands if there are no \n.
+ (bytes-append #"\n\\makeatletter\n"
+ (file->bytes tikztag.sty)
+ #"\n\\makeatother\n"))))
+ (list "\\hphantom{\text{" @mathtext[txt] "}}"
+ "\\tikztag{" @mathtext[txt] "}"))]
+ [else (list " (" txt ")")]))
+
+(define tag (tag** #f))
+(define tag* (tag** #t))
diff --git a/tikztag.sty b/tikztag.sty
@@ -0,0 +1,129 @@
+%%%%%%%%%%%%%%%%%%%% tikztag.sty %%%%%%%%%%%%%%%%%%%%
+% This code is released under the CC0 license (i.e. in the Public Domain
+% or under a very permissive license if your country does not recognise
+% dedications to the Public Domain.
+% Author: Georges Dupéron.
+%%%%%%%%%% \documentclass{article}
+%%%%%%%%%% \makeatletter
+\usepackage{amsmath, tikz, hyperref, lipsum}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Parse options into:
+% \if@tikztag@star
+% \if@tikztag@label@
+% \@tikztag@label
+% \if@tikztag@labeltext@
+% \@tikztag@label
+\newif\if@tikztag@star@
+\newif\if@tikztag@label@
+\newif\if@tikztag@labeltext@
+\def\tikztag{\@ifstar\@tikztag@star\@tikztag@nostar}
+\def\@tikztag@star{\@tikztag@star@true\expandafter\@tikztag@common}
+\def\@tikztag@nostar{\@tikztag@star@false\expandafter\@tikztag@common}
+\def\@tikztag@common{\@ifnextchar[{%
+ \@tikztag@label@true\@tikztag@get@label%
+ }{%
+ \@tikztag@label@false\@tikztag%
+ }}
+\def\@tikztag@get@label[#1]{\def\@tikztag@label{#1}\expandafter\@tikztag@get@maybe@labeltext}
+\def\@tikztag@get@maybe@labeltext{\@ifnextchar[{%
+ \@tikztag@labeltext@true\@tikztag@get@labeltext%
+ }{%
+ \@tikztag@labeltext@false\@tikztag%
+ }}
+\def\@tikztag@get@labeltext[#1]{\def\@tikztag@labeltext{#1}\expandafter\@tikztag}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Implementation:
+\edef\tikztagnumber{0}
+\newcommand{\@tikztag}[1]{%
+ % place the marker:
+ \pgfmathtruncatemacro{\tikztagnumber}{\tikztagnumber+1}%
+ \xdef\tikztagnumber{\tikztagnumber}%
+ \tikz[remember picture]\coordinate(tikztagmarker\tikztagnumber){};%
+ % dispatch given the options
+ \if@tikztag@label@%
+ \if@tikztag@labeltext@%
+ \if@tikztag@star@%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{\noexpand#1}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \else%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \fi%
+ \else%
+ \if@tikztag@star@%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\noexpand#1}{\noexpand#1}{\tikztagnumber}{\noexpand\@firstoftwo}}
+ \else
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\noexpand#1}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@firstoftwo}}
+ \fi
+ \fi
+ \else
+ \if@tikztag@star@
+ \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{\noexpand#1}{\tikztagnumber}{\noexpand\@secondoftwo}}
+ \else
+ \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@secondoftwo}}
+ \fi
+ \fi
+ \@@tikztag
+}
+\newcommand{\@@@tikztag}[5]{%
+ \g@addto@macro\accumulatetikztag{\@@@@tikztag{#1}{#2}{#3}{#4}{#5}}%
+}
+% #1=label #2=label text #3=text #4=\tikztagnumber #5=\@firstoftwo or \@secondoftwo to use label or not
+\newcommand{\@@@@tikztag}[5]{%
+ \tikz[overlay,remember picture]%
+ \node[anchor=base east, inner xsep=0pt]%
+ at (tikztagmarker#4 -| current line right)%
+ {#3};%
+ #5{%
+ \tikz[overlay,remember picture]%
+ \node[anchor=base east, inner xsep=0pt]%
+ at (tikztagmarker#4 -| current line left)%
+ {\phantomsection\edef\@currentlabel{#2}\label{#1}};%
+ }{}
+}
+\def\inittikztag{%
+ \noindent\tikz[remember picture]\coordinate(current line left){};%
+ \tikz[overlay,remember picture]%
+ \coordinate[xshift=\linewidth] (current line right) at (current line left){};%
+ \xdef\accumulatetikztag{}%
+}%
+\def\posttikztag{\accumulatetikztag}%
+\let\@tikztag@old@texMathDisplay\texMathDisplay%
+\def\texMathDisplay#1{\inittikztag\@tikztag@old@texMathDisplay{#1\posttikztag}}%
+\newenvironment{taggableequationstar}{%
+ \inittikztag%
+ \begin{equation*}%
+}{%
+ \end{equation*}%
+ \posttikztag
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%\makeatother
+%%%%%%%%%%\begin{document}
+%%%%%%%%%%
+%%%%%%%%%%
+%%%%%%%%%%\lipsum[2]
+%%%%%%%%%%\begin{equation*}
+%%%%%%%%%% \begin{array}{@{}r@{}c@{}l@{}}
+%%%%%%%%%% a&bbbbb&c \\
+%%%%%%%%%% x&y&z \\
+%%%%%%%%%% \end{array}
+%%%%%%%%%%\end{equation*}
+%%%%%%%%%%\lipsum[2]
+%%%%%%%%%%\begin{taggableequationstar}
+%%%%%%%%%% \begin{array}{@{}r@{}c@{}l@{}}
+%%%%%%%%%% a&bbbbb&c \tikztag[eq:foo][abc]{a, b and c} \\
+%%%%%%%%%% x&y&z \tikztag[eq:bar]{other stuff}\\
+%%%%%%%%%% x&y&z \tikztag{more stuff}\\
+%%%%%%%%%% \end{array}
+%%%%%%%%%%\end{taggableequationstar}
+%%%%%%%%%%Foo: \ref{eq:foo}. Bar: \ref{eq:bar}. Baz: \ref{eq:baz}. Quux: \ref{eq:quux}.
+%%%%%%%%%%\lipsum[2]
+%%%%%%%%%%\begin{taggableequationstar}
+%%%%%%%%%% \begin{array}{@{}r@{}c@{}l@{}}
+%%%%%%%%%% a&bbbbb&c \tikztag*[eq:baz][baz]{a, b and c (baz)} \\
+%%%%%%%%%% x&y&z \tikztag*[eq:quux]{other stuff 2}\\
+%%%%%%%%%% x&y&z \tikztag*{more stuff 2}\\
+%%%%%%%%%% \end{array}
+%%%%%%%%%%\end{taggableequationstar}
+%%%%%%%%%%
+%%%%%%%%%%\end{document}
+%%%%%%%%%%%%%%%%%%%% end tikztag.sty %%%%%%%%%%%%%%%%%%%%
+\ No newline at end of file
