--- a/Attic/Prefix_subtract.thy Mon Oct 15 13:23:52 2012 +0000
+++ b/Attic/Prefix_subtract.thy Mon Dec 03 08:16:58 2012 +0000
@@ -1,5 +1,5 @@
theory Prefix_subtract
- imports Main "~~/src/HOL/Library/List_Prefix"
+ imports Main "../List_Prefix"
begin
--- a/Journal/Paper.thy Mon Oct 15 13:23:52 2012 +0000
+++ b/Journal/Paper.thy Mon Dec 03 08:16:58 2012 +0000
@@ -337,8 +337,11 @@
then be careful to rename these identities apart whenever connecting two
automata. This results in clunky proofs establishing that properties are
invariant under renaming. Similarly, connecting two automata represented as
- matrices results in very adhoc constructions, which are not pleasant to
- reason about.
+ matrices results in messy constructions, which are not pleasant to
+ formally reason about. \citeN[Page 67]{Braibant12}, for example, writes that there are no
+ problems with reasoning about matrices, but that there is an
+ ``intrinsic difficulty of working with rectangular matrices'' in some
+ parts of his formalisation of formal languages in Coq.
Functions are much better supported in Isabelle/HOL, but they still lead to
similar problems as with graphs. Composing, for example, two
@@ -376,15 +379,23 @@
%\emph{locales} or \emph{type classes}, which are \emph{not} available in all
%HOL-based theorem provers.
- Because of these problems to do with representing automata, there seems to
- be no substantial formalisation of automata theory and regular languages
- carried out in HOL-based theorem provers. \citeN{Nipkow98} establishes
+ Because of these problems to do with representing automata, formalising
+ automata theory is surprisingly not as easy as one might think, despite the
+ sometimes very detailed, but informal, textbook proofs. \citeN{LammichTuerk12}
+ formalised Hopcroft's algorithm using an automata library of 27 kloc in
+ Isabelle/HOL. There they use matrices for representing automata.
+ Functions are used by \citeN{Nipkow98}, who establishes
the link between regular expressions and automata in the context of
- lexing. \citeN{BerghoferReiter09} formalise automata
- working over bit strings in the context of Presburger arithmetic. The only
- larger formalisations of automata theory are carried out in Nuprl by
- \citeN{Constable00} and in Coq by \citeN{Filliatre97}, \citeN{Almeidaetal10}
- and \citeN{Braibant12}.
+ lexing. \citeN{BerghoferReiter09} use functions as well for formalising automata
+ working over bit strings in the context of Presburger arithmetic.
+ A Larger formalisation of automata theory, including the Myhill-Nerode theorem,
+ was carried out in Nuprl by \citeN{Constable00} which also uses functions.
+ Other large formailsations of automata theory in Coq are by
+ \citeN{Filliatre97} who essentially uses graphs and by \citeN{Almeidaetal10}
+ and \citeN{Braibant12}, who both use matrices. Many of these works,
+ like \citeN{Nipkow98} or \citeN{Braibant12}, mention intrinsic problems with
+ their representation of
+ automata which made them `fight' their respective theorem prover.
%Also, one might consider automata as just convenient `vehicles' for
%establishing properties about regular languages. However, paper proofs
@@ -428,7 +439,8 @@
This convenience of regular expressions has
recently been exploited in HOL4 with a formalisation of regular expression
matching based on derivatives by \citeN{OwensSlind08}, and with an equivalence
- checker for regular expressions in Isabelle/HOL by \citeN{KraussNipkow11}. The
+ checker for regular expressions in Isabelle/HOL by \citeN{KraussNipkow11}
+ and in Matida by \citeN{Asperti12} and in Coq by \citeN{CoquandSiles12}. The
main purpose of this paper is to show that a central result about regular
languages---the Myhill-Nerode Theorem---can be recreated by only using
regular expressions. This theorem gives necessary and sufficient conditions
@@ -1196,7 +1208,8 @@
\noindent
Much more interesting, however, are the inductive cases. They seem hard to be solved
- directly. The reader is invited to try.
+ directly. The reader is invited to try.\footnote{The induction hypothesis is not strong enough
+ to make any progress with the TIME and STAR cases.}
In order to see how our proof proceeds consider the following suggestive picture
given by \citeN{Constable00}:
@@ -2080,7 +2093,8 @@
\noindent
and assume @{text B} is any language and @{text A} is regular, then @{term
"Deriv_lang B A"} is regular. To see this consider the following argument
- using partial derivatives: From @{text A} being regular we know there exists
+ using partial derivatives (which we used in Section~\ref{derivatives}): From @{text A}
+ being regular we know there exists
a regular expression @{text r} such that @{term "A = lang r"}. We also know
that @{term "pderivs_lang B r"} is finite for every language @{text B} and
regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition
@@ -2253,8 +2267,8 @@
\begin{proof}[of the First Part of Theorem~\ref{subseqreg}]
By the second part, we know the right-hand side of \eqref{compl}
is regular, which means @{term "- SUBSEQ A"} is regular. But since
- we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
- must be regular.
+ we established already that regularity is preserved under complement (using Myhill-Nerode),
+ also @{term "SUBSEQ A"} must be regular.
\end{proof}
Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing
@@ -2418,6 +2432,8 @@
algorithm is still executable. Given the infrastructure for
executable sets introduced by \citeN{Haftmann09} in Isabelle/HOL, it should.
+ We started out by claiming that in a theorem prover it is eaiser to reason
+ about regular expressions than about automta. Here are some numbers:
Our formalisation of the Myhill-Nerode Theorem consists of 780 lines of
Isabelle/Isar code for the first direction and 460 for the second (the one
based on tagging-functions), plus around 300 lines of standard material
@@ -2430,7 +2446,7 @@
The algorithm for solving equational systems, which we
used in the first direction, is conceptually relatively simple. Still the
use of sets over which the algorithm operates means it is not as easy to
- formalise as one might hope. However, it seems sets cannot be avoided since
+ formalise as one might wish. However, it seems sets cannot be avoided since
the `input' of the algorithm consists of equivalence classes and we cannot
see how to reformulate the theory so that we can use lists or matrices. Lists would be
much easier to reason about, since we can define functions over them by
@@ -2445,29 +2461,35 @@
for their formalisation of the first eleven chapters of the textbook by \citeN{HopcroftUllman69},
which includes the Myhill-Nerode theorem. It is hard to gauge the size of a
formalisation in Nurpl, but from what is shown in the Nuprl Math Library
- about their development it seems substantially larger than ours. We attribute
+ about their development it seems \emph{substantially} larger than ours. We attribute
this to our use of regular expressions, which meant we did not need to `fight'
- the theorem prover.
+ the theorem prover. Recently, \citeN{LammichTuerk12} formalised Hopcroft's
+ algorithm in Isabelle/HOL (in 7000 lines of code) using an automata
+ library of 27000 lines of code.
Also, \citeN{Filliatre97} reports that his formalisation in
Coq of automata theory and Kleene's theorem is ``rather big''.
- More recently, \citeN{Almeidaetal10} reported about another
+ \citeN{Almeidaetal10} reported about another
formalisation of regular languages in Coq. Their
main result is the
correctness of Mirkin's construction of an automaton from a regular
expression using partial derivatives. This took approximately 10600 lines
- of code. Also \citeN{Braibant12} formalised a large part of regular language
+ of code. \citeN{Braibant12} formalised a large part of regular language
theory and Kleene algebras in Coq. While he is mainly interested
in implementing decision procedures for Kleene algebras, his library
includes a proof of the Myhill-Nerode theorem. He reckons that our
``development is more concise'' than his one based on matrices \cite[Page 67]{Braibant12}.
+ He writes that there is no conceptual problems with formally reasoning
+ about matrices for automata, but notes ``intrinsic difficult[ies]'' when working
+ with matrices in Coq, which is the sort of `fighting' one would encounter also
+ in other theorem provers.
+
In terms of time, the estimate for our formalisation is that we
needed approximately 3 months and this included the time to find our proof
arguments. Unlike \citeN{Constable00}, who were able to follow the Myhill-Nerode
proof by \citeN{HopcroftUllman69}, we had to find our own arguments. So for us the
formalisation was not the bottleneck. The code of
- our formalisation can be found in the Archive of Formal Proofs at
- \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}
- \cite{myhillnerodeafp11}.\smallskip
+ our formalisation \cite{myhillnerodeafp11} can be found in the Archive of Formal Proofs at
+ \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}.\smallskip
\noindent
{\bf Acknowledgements:}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/acmtrans.bst Mon Dec 03 08:16:58 2012 +0000
@@ -0,0 +1,1770 @@
+% "ACM Transactions" BibTeX style, acmtrans.bst
+% for BibTeX version 0.99c, LaTeX version 3.141
+% Revised 28-MARCH-1996
+% Revised 30-JUNE-1995
+% Revised 15-JAN-1996
+% $Header: acmtrans.bst,v 1.2 96/01/17 09:05:38 boyland Exp $
+%
+% Hacked by John T. Boyland at University of California, Berkeley
+% (with assistance by John R. Hauser)
+% Hacked by Andrew W. Appel and Rebecca L. Davies at Princeton University,
+% based on a "chicago.bst" by Glenn Paulley at U. Waterloo,
+% which was based on "newapa.bst" found at ymir.claremont.edu.
+%
+% Citation format: [author-last-name year]
+% [author-last-name and author-last-name year]
+% [author-last-name, author-last-name, and author-last-name year]
+% [author-last-name et al. year]
+% [author-last-name]
+% author-last-name [year]
+% [author-last-name and author-last-name]
+% [author-last-name et al.]
+% [year] or [year,year]
+% year or year,year
+%
+% Reference list ordering: alphabetical by author or whatever passes
+% for author in the absence of one.
+%
+% This BibTeX style has support for abbreviated author lists and for
+% year-only citations. This is done by having the citations
+% actually look like
+%
+% \citeauthoryear{full-author-info}{abbrev-author-info}{year}
+%
+% The LaTeX style has to have the following (or similar)
+%
+% \let\@internalcite\cite
+% \def\fullcite{\def\citeauthoryear##1##2##3{##1, ##3}\@internalcite}
+% \def\fullciteA{\def\citeauthoryear##1##2##3{##1}\@internalcite}
+% \def\shortcite{\def\citeauthoryear##1##2##3{##2, ##3}\@internalcite}
+% \def\shortciteA{\def\citeauthoryear##1##2##3{##2}\@internalcite}
+% \def\citeyear{\def\citeauthoryear##1##2##3{##3}\@internalcite}
+%
+% These TeX macro definitions are found in acmtrans.sty. Additional
+% commands to manipulate different components of a citation can be defined
+% so that, for example, you can list author's names without parentheses
+% if using a citation as a noun or object in a sentence.
+%
+% Features of acmtrans.bst:
+% ========================
+%
+% - all authors appear last name first.
+% - all pages are listed xx-xx, (no pp.) and are at the end of the reference
+% - publishers are identified as publisher, address
+% - conferences papers (inproceedings) may give city of conference,
+% date of conference, and journal that the proceedings appear in.
+% - months abbreviated to max four letters (eg. Mar.)
+% - volume of a series indicated after the title of the series
+% - editors appear after edited title and are identified by a trailing "Eds."
+% not in parentheses. Editor names are not given in small caps.
+% (unless there is no author line)
+% - names terminated with a period even if there is no first name.
+% - editions are indicated trailing after the work, not in parentheses.
+% - "et al." citations have a protected period to avoid bad spacing (jrh)
+% - "address" required when publisher given
+% - series (roman) and volume are in a sentence separate from (book-)title
+%
+%
+% Features of chicago.bst:
+% =======================
+%
+% - full names used in citations, but abbreviated citations are available
+% (see above)
+% - if an entry has a "month", then the month and year are also printed
+% as part of that bibitem.
+% - all conjunctions use "and" instead of "\&"
+% - major modification from Chicago Manual of Style (13th ed.) is that
+% only the first author in a reference appears last name first-
+% additional authors appear as J. Q. Public.
+% - pages are listed as "pp. xx-xx" in all entry types except
+% article entries.
+% - book, inbook, and manual use "location: publisher" (or organization)
+% for address and publisher. All other types list publishers separately.
+% - "pp." are used to identify page numbers for all entry types except
+% articles.
+% - organization is used as a citation label if neither author nor editor
+% is present (for manuals).
+% - "et al." is used for long author and editor lists, or when "others"
+% is used.
+%
+% Modifications and bug fixes from newapa.bst:
+% ===========================================
+%
+% - added month, year to bib entries if month is present
+% - fixed bug with In proceedings, added necessary comma after title
+% - all conjunctions changed to "and" from "\&"
+% - fixed bug with author labels in my.full.label: "et al." now is
+% generated when "others" is an author name
+% - major modification from Chicago Manual of Style (13th ed.) is that
+% only the first author in a reference appears last name first-
+% additional authors appear as J. Q. Public.
+% - pages are listed as "pp. xx-xx" in all entry types except
+% article entries. Unnecessary (IMHO) "()" around page numbers
+% were removed, and page numbers now don't end with a period.
+% - created chicago.sty for use with this bibstyle (required).
+% - fixed bugs in FUNCTION {format.vol.num.pages} for missing volume,
+% number, and /or pages. Renamed to format.jour.vol.
+% - fixed bug in formatting booktitles: additional period an error if
+% book has a volume.
+% - fixed bug: editors usually given redundant period before next clause
+% (format.editors.dot) removed.
+% - added label support for organizations, if both author and editor
+% are missing (from alpha.bst). If organization is too long, then
+% the key field is used for abbreviated citations.
+% - In proceedings or books of several volumes, no comma was written
+% between the "Volume x" and the page numbers (this was intentional
+% in newapa.bst). Fixed.
+% - Some journals may not have volumes/numbers, only month/year (eg.
+% IEEE Computer). Fixed bug in article style that assumed volume/number
+% was always present.
+%
+% Original documentation for newapa.sty:
+% =====================================
+%
+% This version was made by modifying the master file made by
+% Oren Patashnik (PATASHNIK@SCORE.STANFORD.EDU), and the 'named' BibTeX
+% style of Peter F. Patel-Schneider.
+%
+% Copyright (C) 1985, all rights reserved.
+% Copying of this file is authorized only if either
+% (1) you make absolutely no changes to your copy, including name, or
+% (2) if you do make changes, you name it something other than 'newapa.bst'.
+% There are undoubtably bugs in this style. If you make bug fixes,
+% improvements, etc. please let me know. My e-mail address is:
+% spencer@cgrg.ohio.state.edu or 71160.3141@compuserve.com
+%
+% This style was made from 'plain.bst', 'named.bst', and 'apalike.bst',
+% with lots of tweaking to make it look like APA style, along with tips
+% from Young Ryu and Brian Reiser's modifications of 'apalike.bst'.
+
+ENTRY
+ { address
+ author
+ booktitle
+ chapter
+ city % jtb: added
+ date % jtb: added
+ edition
+ editor
+ howpublished
+ institution
+ journal
+ key
+ month
+ note
+ number
+ organization
+ pages
+ publisher
+ school
+ series
+ title
+ type
+ volume
+ year
+ }
+ {}
+ { label.year extra.label sort.year sort.label }
+
+INTEGERS { output.state before.all mid.sentence after.sentence after.block }
+
+FUNCTION {init.state.consts}
+{ #0 'before.all :=
+ #1 'mid.sentence :=
+ #2 'after.sentence :=
+ #3 'after.block :=
+}
+
+STRINGS { s t u }
+
+FUNCTION {output.nonnull}
+{ 's :=
+ output.state mid.sentence =
+ { ", " * write$ }
+ { output.state after.block =
+ { add.period$ write$
+ newline$
+ "\newblock " write$
+ }
+ { output.state before.all =
+ 'write$
+ { add.period$ " " * write$ }
+ if$
+ }
+ if$
+ mid.sentence 'output.state :=
+ }
+ if$
+ s
+}
+
+% Use a colon to separate output. Used only for address/publisher
+% combination in book/inbook types, address/institution for manuals,
+% and organization:publisher for proceedings (inproceedings).
+%
+FUNCTION {output.nonnull.colon}
+{ 's :=
+ output.state mid.sentence =
+ { ": " * write$ }
+ { output.state after.block =
+ { add.period$ write$
+ newline$
+ "\newblock " write$
+ }
+ { output.state before.all =
+ 'write$
+ { add.period$ " " * write$ }
+ if$
+ }
+ if$
+ mid.sentence 'output.state :=
+ }
+ if$
+ s
+}
+
+FUNCTION {output}
+{ duplicate$ empty$
+ 'pop$
+ 'output.nonnull
+ if$
+}
+
+FUNCTION {output.colon}
+{ duplicate$ empty$
+ 'pop$
+ 'output.nonnull.colon
+ if$
+}
+
+FUNCTION {output.check}
+{ 't :=
+ duplicate$ empty$
+ { pop$ "empty " t * " in " * cite$ * warning$ }
+ 'output.nonnull
+ if$
+}
+
+FUNCTION {output.check.colon}
+{ 't :=
+ duplicate$ empty$
+ { pop$ "empty " t * " in " * cite$ * warning$ }
+ 'output.nonnull.colon
+ if$
+}
+
+FUNCTION {output.year.check}
+{ year empty$
+ { "empty year in " cite$ * warning$ }
+ { write$
+ " " year * extra.label *
+ mid.sentence 'output.state :=
+ }
+ if$
+}
+
+
+FUNCTION {fin.entry}
+{ add.period$
+ write$
+ newline$
+}
+
+FUNCTION {new.block}
+{ output.state before.all =
+ 'skip$
+ { after.block 'output.state := }
+ if$
+}
+
+FUNCTION {new.sentence}
+{ output.state after.block =
+ 'skip$
+ { output.state before.all =
+ 'skip$
+ { after.sentence 'output.state := }
+ if$
+ }
+ if$
+}
+
+FUNCTION {not}
+{ { #0 }
+ { #1 }
+ if$
+}
+
+FUNCTION {and}
+{ 'skip$
+ { pop$ #0 }
+ if$
+}
+
+FUNCTION {or}
+{ { pop$ #1 }
+ 'skip$
+ if$
+}
+
+FUNCTION {new.block.checka}
+{ empty$
+ 'skip$
+ 'new.block
+ if$
+}
+
+FUNCTION {new.block.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.block
+ if$
+}
+
+FUNCTION {new.sentence.checka}
+{ empty$
+ 'skip$
+ 'new.sentence
+ if$
+}
+
+FUNCTION {new.sentence.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.sentence
+ if$
+}
+
+FUNCTION {field.or.null}
+{ duplicate$ empty$
+ { pop$ "" }
+ 'skip$
+ if$
+}
+
+%
+% Emphasize the top string on the stack.
+%
+FUNCTION {emphasize}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "{\em " swap$ * "}" * }
+ if$
+}
+
+%
+% Emphasize the top string on the stack, but add a trailing space.
+%
+FUNCTION {emphasize.space}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "{\em " swap$ * "\/}" * }
+ if$
+}
+
+%
+% Emphasize the top string on stack, add a trailing comma and space.
+%
+FUNCTION {emphasize.comma}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "{\em " swap$ * ",\/}" * }
+ if$
+}
+
+INTEGERS { nameptr namesleft numnames }
+%
+% Format bibliographical entries with the first author last name first,
+% and subsequent authors with initials followed by last name.
+% All names are formatted in this routine.
+%
+
+FUNCTION {format.names}
+{ 's :=
+ #1 'nameptr := % nameptr = 1;
+ s num.names$ 'numnames := % numnames = num.name$(s);
+ numnames 'namesleft :=
+ { namesleft #0 > }
+
+ { nameptr #1 =
+ {"{\sc " s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ * "}" * 't := }
+ {"{\sc " s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ * "}" * 't := }
+ if$
+ nameptr #1 >
+ { namesleft #1 >
+ { ", " * t * }
+ { numnames #2 >
+ { "," * }
+ 'skip$
+ if$
+ t "{\sc others}" =
+ { " {\sc et~al\mbox{.}}" * } % jrh: avoid spacing problems
+ { " {\sc and} " * t * } % from Chicago Manual of Style
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr := % nameptr += 1;
+ namesleft #1 - 'namesleft := % namesleft =- 1;
+ }
+ while$
+}
+
+FUNCTION {my.full.label}
+{ 's :=
+ #1 'nameptr := % nameptr = 1;
+ s num.names$ 'numnames := % numnames = num.name$(s);
+ numnames 'namesleft :=
+ { namesleft #0 > }
+
+ { s nameptr "{vv~}{ll}" format.name$ 't := % get the next name
+ nameptr #1 >
+ { namesleft #1 >
+ { ", " * t * }
+ { numnames #2 >
+ { "," * }
+ 'skip$
+ if$
+ t "others" =
+ { " et~al\mbox{.}" * } % jrh: avoid spacing problems
+ { " and " * t * } % from Chicago Manual of Style
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr := % nameptr += 1;
+ namesleft #1 - 'namesleft := % namesleft =- 1;
+ }
+ while$
+
+}
+
+FUNCTION {format.names.fml}
+%
+% Format names in "familiar" format, with first initial followed by
+% last name. Like format.names, ALL names are formatted.
+% jtb: The names are NOT put in small caps
+%
+{ 's :=
+ #1 'nameptr := % nameptr = 1;
+ s num.names$ 'numnames := % numnames = num.name$(s);
+ numnames 'namesleft :=
+ { namesleft #0 > }
+
+ { "{" s nameptr "{f.~}{vv~}{ll}{, jj}" format.name$ * "}" * 't :=
+
+ nameptr #1 >
+ { namesleft #1 >
+ { ", " * t * }
+ { numnames #2 >
+ { "," * }
+ 'skip$
+ if$
+ t "{others}" =
+ { " {et~al\mbox{.}}" * }
+ { " {and} " * t * }
+% { " {\&} " * t * }
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr := % nameptr += 1;
+ namesleft #1 - 'namesleft := % namesleft =- 1;
+ }
+ while$
+}
+
+FUNCTION {format.authors}
+{ author empty$
+ { "" }
+ { author format.names add.period$} % jtb: add period if none before
+ if$
+}
+
+FUNCTION {format.key}
+{ empty$
+ { key field.or.null }
+ { "" }
+ if$
+}
+
+%
+% Format editor names for use in the "in" types: inbook, incollection,
+% inproceedings: first initial, then last names. When editors are the
+% LABEL for an entry, then format.editor is used which lists editors
+% by last name first.
+%
+FUNCTION {format.editors.fml}
+{ editor empty$
+ { "" }
+ { editor format.names.fml
+ editor num.names$ #1 >
+ { ", Eds." * } % jtb: removed parentheses
+ { ", Ed." * } % jtb: removed parentheses
+ if$
+ }
+ if$
+}
+
+%
+% Format editor names for use in labels, last names first.
+%
+FUNCTION {format.editors}
+{ editor empty$
+ { "" }
+ { editor format.names
+ editor num.names$ #1 >
+ { ", Eds." * } % jtb: removed parentheses
+ { ", Ed." * } % jtb: removed parentheses
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.title}
+{ title empty$
+ { "" }
+ { title "t" change.case$ }
+ if$
+}
+
+% Note that the APA style requres case changes
+% in article titles. The following does not
+% change cases. If you perfer it, uncomment the
+% following and comment out the above.
+
+%FUNCTION {format.title}
+%{ title empty$
+% { "" }
+% { title }
+% if$
+%}
+
+FUNCTION {n.dashify}
+{ 't :=
+ ""
+ { t empty$ not }
+ { t #1 #1 substring$ "-" =
+ { t #1 #2 substring$ "--" = not
+ { "--" *
+ t #2 global.max$ substring$ 't :=
+ }
+ { { t #1 #1 substring$ "-" = }
+ { "-" *
+ t #2 global.max$ substring$ 't :=
+ }
+ while$
+ }
+ if$
+ }
+ { t #1 #1 substring$ *
+ t #2 global.max$ substring$ 't :=
+ }
+ if$
+ }
+ while$
+}
+
+FUNCTION {format.btitle}
+{ edition empty$
+ { title emphasize }
+ { title empty$
+ { title emphasize } % jtb: what is this supposed to do ?!?
+ { "{\em " title * "\/}, " * edition * " ed." * } % jtb: no parens for ed.
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.emphasize.booktitle}
+{ edition empty$
+ { booktitle emphasize }
+ { booktitle empty$
+ { booktitle emphasize } % jtb: what is this supposed to do ?!?
+ { "{\em " booktitle * "\/}, " * edition * " ed." * } % jtb: no ()s for ed.
+ if$
+ }
+ if$
+ }
+
+% jtb: if the preceding string (the title of the conference) is non-empty,
+% jtb: append the location, otherwise leave empty (so as to trigger the
+% jtb: error message in output.check
+FUNCTION {format.city}
+{ duplicate$ empty$
+ { }
+ { city empty$
+ { date empty$
+ { }
+ { " (" * date * ")" * }
+ if$
+ }
+ { date empty$
+ { " (" * city * ")" * }
+ { " (" * city * ", " * date * ")" * }
+ if$
+ }
+ if$
+ }
+ if$
+}
+
+FUNCTION {tie.or.space.connect}
+{ duplicate$ text.length$ #3 <
+ { "~" }
+ { " " }
+ if$
+ swap$ * *
+}
+
+FUNCTION {either.or.check}
+{ empty$
+ 'pop$
+ { "can't use both " swap$ * " fields in " * cite$ * warning$ }
+ if$
+}
+
+% jtb: If there is a series, this is added and the volume trails after it.
+% jtb: Otherwise, "Vol" is Capitalized.
+FUNCTION {format.bvolume}
+{ volume empty$
+ { "" }
+ { series empty$
+ { "Vol." volume tie.or.space.connect}
+ { series ", " * "vol." volume tie.or.space.connect *}
+ if$
+ "volume and number" number either.or.check
+ }
+ if$
+}
+
+FUNCTION {format.number.series}
+{ volume empty$
+ { number empty$
+ { series field.or.null }
+ { output.state mid.sentence =
+ { "Number" } % gnp - changed to mixed case always
+ { "Number" }
+ if$
+ number tie.or.space.connect
+ series empty$
+ { "there's a number but no series in " cite$ * warning$ }
+ { " in " * series * }
+ if$
+ }
+ if$
+ }
+ { "" }
+ if$
+}
+
+INTEGERS { multiresult }
+
+FUNCTION {multi.page.check}
+{ 't :=
+ #0 'multiresult :=
+ { multiresult not
+ t empty$ not
+ and
+ }
+ { t #1 #1 substring$
+ duplicate$ "-" =
+ swap$ duplicate$ "," =
+ swap$ "+" =
+ or or
+ { #1 'multiresult := }
+ { t #2 global.max$ substring$ 't := }
+ if$
+ }
+ while$
+ multiresult
+}
+
+FUNCTION {format.pages}
+{ pages empty$
+ { "" }
+ { pages multi.page.check
+ { pages n.dashify } % gnp - removed () % jtb: removed pp.
+ { pages }
+ if$
+ }
+ if$
+}
+
+% By Young (and Spencer)
+% GNP - fixed bugs with missing volume, number, and/or pages
+%
+% Format journal, volume, number, pages for article types.
+%
+FUNCTION {format.jour.vol}
+{ journal empty$
+ { "no journal in " cite$ * warning$
+ "" }
+ { journal emphasize.space }
+ if$
+ number empty$
+ { volume empty$
+ { "no number and no volume in " cite$ * warning$
+ "" * }
+ { "~{\em " * Volume * "}" * }
+ if$
+ }
+ { volume empty$
+ {"no volume for " cite$ * warning$
+ "~" * number * }
+ { "~" *
+ volume emphasize.comma
+ "~" * number * * }
+ if$
+ month empty$
+ {}
+ {" (" * month * ")" *}
+ if$
+ }
+ if$
+ pages empty$
+ {"page numbers missing in " cite$ * warning$
+ "" * } % gnp - place a null string on the stack for output
+ { duplicate$ empty$
+ { pop$ format.pages }
+ { ", " * pages n.dashify * } % gnp - removed pp. for articles
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.chapter.pages}
+{ chapter empty$
+ 'format.pages
+ { type empty$
+ { "Chapter" } % gnp - changed to mixed case
+ { type "t" change.case$ }
+ if$
+ chapter tie.or.space.connect
+ pages empty$
+ {"page numbers missing in " cite$ * warning$} % gnp - added check
+ { ", " * format.pages * }
+ if$
+ }
+ if$
+}
+
+% jtb: format for collections or proceedings not appearing in a journal
+FUNCTION {format.in.emphasize.booktitle}
+{ booktitle empty$
+ { "" }
+ { "In " format.emphasize.booktitle * }
+ if$
+}
+
+% jtb: format for proceedings appearing in a journal
+FUNCTION {format.in.booktitle}
+{ booktitle empty$
+ { "" }
+ { "In " booktitle * }
+ if$
+}
+
+FUNCTION {format.in.ed.booktitle}
+{ booktitle empty$
+ { "" }
+ { editor empty$
+ { "In " format.emphasize.booktitle * }
+ % jtb: swapped editor location
+ { "In " format.emphasize.booktitle * ", " * format.editors.fml * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.thesis.type}
+{ type empty$
+ 'skip$
+% {pop$
+ {{ "" }
+ type "t" change.case$}
+ if$
+}
+
+FUNCTION {format.tr.number}
+{ type empty$
+ { "Tech. Rep." }
+ 'type
+ if$
+ number empty$
+ { "t" change.case$ }
+ { number tie.or.space.connect }
+ if$
+}
+
+FUNCTION {format.article.crossref}
+{ "See"
+ "\citeN{" * crossref * "}" *
+}
+
+FUNCTION {format.crossref.editor}
+{ editor #1 "{vv~}{ll}" format.name$
+ editor num.names$ duplicate$
+ #2 >
+ { pop$ " et~al\mbox{.}" * } % jrh: avoid spacing problems
+ { #2 <
+ 'skip$
+ { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+ { " et~al\mbox{.}" * } % jrh: avoid spacing problems
+ { " and " * editor #2 "{vv~}{ll}" format.name$ * }
+ if$
+ }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.book.crossref}
+{ volume empty$
+ { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
+ "In "
+ }
+ { "Volume" volume tie.or.space.connect % gnp - changed to mixed case
+ " of " *
+ }
+ if$
+ editor empty$
+ editor field.or.null author field.or.null =
+ or
+ { key empty$
+ { series empty$
+ { "need editor, key, or series for " cite$ * " to crossref " *
+ crossref * warning$
+ "" *
+ }
+ { "{\em " * series * "\/}" * }
+ if$
+ }
+ { key * }
+ if$
+ }
+ { format.crossref.editor * }
+ if$
+ " \citeN{" * crossref * "}" *
+}
+
+FUNCTION {format.incoll.inproc.crossref}
+{ "See"
+ " \citeN{" * crossref * "}" *
+}
+
+% format.lab.names:
+%
+% determines "short" names for the abbreviated author information.
+% "Long" labels are created in calc.label, using the routine my.full.label
+% to format author and editor fields.
+%
+% There are 4 cases for labels. (n=3 in the example)
+% a) one author Foo
+% b) one to n Foo, Bar and Baz
+% c) use of "and others" Foo, Bar et al.
+% d) more than n Foo et al.
+%
+FUNCTION {format.lab.names}
+{ 's :=
+ s num.names$ 'numnames :=
+ numnames #2 > % change number to number of others allowed before
+ % forcing "et al".
+ { s #1 "{vv~}{ll}" format.name$ " et~al\mbox{.}" * } % jrh: \mbox{} added
+ {
+ numnames #1 - 'namesleft :=
+ #2 'nameptr :=
+ s #1 "{vv~}{ll}" format.name$
+ { namesleft #0 > }
+ { nameptr numnames =
+ { s nameptr "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+ { " et~al\mbox{.}" * } % jrh: avoid spacing problems
+ { " and " * s nameptr "{vv~}{ll}" format.name$ * }
+ if$
+ }
+ { ", " * s nameptr "{vv~}{ll}" format.name$ * }
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+ }
+ if$
+}
+
+FUNCTION {author.key.label}
+{ author empty$
+ { key empty$
+ { "no key, author in " cite$ * warning$
+ cite$ #1 #3 substring$ }
+ 'key
+ if$
+ }
+ { author format.lab.names }
+ if$
+}
+
+FUNCTION {editor.key.label}
+{ editor empty$
+ { key empty$
+ { "no key, editor in " cite$ * warning$
+ cite$ #1 #3 substring$ }
+ 'key
+ if$
+ }
+ { editor format.lab.names }
+ if$
+}
+
+FUNCTION {author.key.organization.label}
+%
+% added - gnp. Provide label formatting by organization if author is null.
+%
+{ author empty$
+ { organization empty$
+ { key empty$
+ { "no key, author or organization in " cite$ * warning$
+ cite$ #1 #3 substring$ }
+ 'key
+ if$
+ }
+ { organization }
+ if$
+ }
+ { author format.lab.names }
+ if$
+}
+
+FUNCTION {editor.key.organization.label}
+%
+% added - gnp. Provide label formatting by organization if editor is null.
+%
+{ editor empty$
+ { organization empty$
+ { key empty$
+ { "no key, editor or organization in " cite$ * warning$
+ cite$ #1 #3 substring$ }
+ 'key
+ if$
+ }
+ { organization }
+ if$
+ }
+ { editor format.lab.names }
+ if$
+}
+
+FUNCTION {author.editor.key.label}
+{ author empty$
+ { editor empty$
+ { key empty$
+ { "no key, author, or editor in " cite$ * warning$
+ cite$ #1 #3 substring$ }
+ 'key
+ if$
+ }
+ { editor format.lab.names }
+ if$
+ }
+ { author format.lab.names }
+ if$
+}
+
+FUNCTION {calc.label}
+%
+% Changed - GNP. See also author.organization.sort, editor.organization.sort
+% Form label for BibTeX entry. The classification of which fields are used
+% for which type of entry (book, inbook, etc.) are taken from alpha.bst.
+% The change here from newapa is to also include organization as a
+% citation label if author or editor is missing.
+%
+{ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.key.label
+ { type$ "proceedings" =
+ 'editor.key.organization.label
+ { type$ "manual" =
+ 'author.key.organization.label
+ 'author.key.label
+ if$
+ }
+ if$
+ }
+ if$
+
+ author empty$ % generate the full label citation information.
+ { editor empty$
+ { organization empty$
+ { "no author, editor, or organization in " cite$ * warning$
+ "??" }
+ { organization }
+ if$
+ }
+ { editor my.full.label }
+ if$
+ }
+ { author my.full.label }
+ if$
+
+% leave label on the stack, to be popped when required.
+
+ "}{" * swap$ * "}{" *
+% year field.or.null purify$ #-1 #4 substring$ *
+%
+% save the year for sort processing afterwards (adding a, b, c, etc.)
+%
+ year field.or.null purify$ #-1 #4 substring$
+ 'label.year :=
+}
+
+FUNCTION {output.bibitem}
+{ newline$
+
+ "\bibitem[\protect\citeauthoryear{" write$
+ calc.label write$
+ sort.year write$
+ "}]{" write$
+
+ cite$ write$
+ "}" write$
+ newline$
+ ""
+ before.all 'output.state :=
+}
+
+FUNCTION {article}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ crossref missing$
+ { format.jour.vol output
+ }
+ { format.article.crossref output.nonnull
+ format.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {book}
+{ output.bibitem
+ author empty$
+ { format.editors
+ "author and editor" output.check }
+ { format.authors
+ output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ output.year.check % added
+ new.block
+ format.btitle
+ "title" output.check
+ crossref missing$
+ { new.sentence % jtb: start a new sentence for series/volume
+ format.bvolume output
+ new.block
+ format.number.series output
+ new.sentence
+ publisher "publisher" output.check
+ address "address" output.check % jtb: require address
+ }
+ { new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {booklet}
+{ output.bibitem
+ format.authors output
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ howpublished output
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {inbook}
+{ output.bibitem
+ author empty$
+ { format.editors
+ "author and editor" output.check
+ }
+ { format.authors output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ output.year.check % added
+ new.block
+ format.btitle
+ "title" output.check
+ crossref missing$
+ { new.sentence % jtb: start a new sentence for series/volume
+ format.bvolume output
+ new.block
+ format.number.series output
+ new.sentence
+ publisher "publisher" output.check
+ address "address" output.check % jtb: require address
+ format.chapter.pages
+ "chapter and pages" output.check % jtb: moved from before publisher
+ }
+ { format.chapter.pages "chapter and pages" output.check
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {incollection}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle
+ "booktitle" output.check
+ new.sentence % jtb: start a new sentence for series/volume
+ format.bvolume output
+ format.number.series output
+ new.sentence
+ publisher "publisher" output.check
+ address "address" output.check % jtb: require address
+ format.chapter.pages output % gnp - was special.output.nonnull
+% left out comma before page numbers
+ % jtb: moved from before publisher
+ }
+ { format.incoll.inproc.crossref
+ output.nonnull
+ format.chapter.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {inproceedings}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ crossref missing$
+ { journal missing$ % jtb: proceedings appearing in journals
+ { format.in.emphasize.booktitle format.city "booktitle" output.check
+ format.editors.fml output
+ new.sentence % jtb: start a new sentence for series/volume
+ format.bvolume output
+ format.number.series output
+ new.sentence
+ organization output
+ publisher "publisher" output.check % jtb: require publisher (?)
+ address "address" output.check % jtb: require address
+ format.pages output % jtb: moved from before publisher
+ }
+ % jtb: new:
+ { format.in.booktitle format.city "booktitle" output.check
+ format.editors.fml output
+ new.sentence
+ format.jour.vol output
+ }
+ if$
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {conference} { inproceedings }
+
+FUNCTION {manual}
+{ output.bibitem
+ author empty$
+ { editor empty$
+ { organization "organization" output.check
+ organization format.key output } % if all else fails, use key
+ { format.editors "author and editor" output.check }
+ if$
+ }
+ { format.authors output.nonnull }
+ if$
+ output.year.check % added
+ new.block
+ format.btitle
+ "title" output.check
+ organization address new.block.checkb
+ % jtb: back to normal style: organization, address
+ organization "organization" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {mastersthesis}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ "M.S.\ thesis" format.thesis.type output.nonnull
+ school "school" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {misc}
+{ output.bibitem
+ format.authors output
+ author format.key output % added
+ output.year.check % added
+ title howpublished new.block.checkb
+ format.title output
+ new.block
+ howpublished output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {phdthesis}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ format.thesis.type "Ph.D. thesis" output.nonnull
+ school "school" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {proceedings}
+{ output.bibitem
+ editor empty$
+ { organization output
+ organization format.key output } % gnp - changed from author format.key
+ { format.editors output.nonnull }
+ if$
+% author format.key output % gnp - removed (should be either
+% editor or organization
+ output.year.check % added (newapa)
+ new.block
+ format.btitle format.city "title" output.check % jtb: added city
+ new.sentence
+ format.bvolume output
+ format.number.series output
+ new.sentence
+ organization output
+ % jtb: normal order: publisher, address
+ publisher output
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {techreport}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ format.tr.number output % jtb: moved month ...
+ institution "institution" output.check
+ address output
+ new.sentence
+ month output % jtb: ... to here (no parens)
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {unpublished}
+{ output.bibitem
+ format.authors
+ "author" output.check
+ author format.key output % added
+ output.year.check % added
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ note "note" output.check
+ fin.entry
+}
+
+FUNCTION {default.type} { misc }
+
+MACRO {jan} {"Jan."}
+
+MACRO {feb} {"Feb."}
+
+MACRO {mar} {"Mar."} % jtb: corrected: was "March"
+
+MACRO {apr} {"Apr."} % jtb: corrected: was "April"
+
+MACRO {may} {"May"}
+
+MACRO {jun} {"June"}
+
+MACRO {jul} {"July"}
+
+MACRO {aug} {"Aug."}
+
+MACRO {sep} {"Sept."}
+
+MACRO {oct} {"Oct."}
+
+MACRO {nov} {"Nov."}
+
+MACRO {dec} {"Dec."}
+
+MACRO {acmcs} {"ACM Comput. Surv."}
+
+MACRO {acmlett} {"ACM Lett. Program. Lang. Syst."}
+
+MACRO {acta} {"Acta Inf."}
+
+MACRO {ai} {"Artificial Intelligence"}
+
+MACRO {al} {"Ada Lett."}
+
+MACRO {acr} {"Adv. Comput. Res."}
+
+MACRO {bit} {"Bit"}
+
+MACRO {cacm} {"Commun. ACM"}
+
+MACRO {cj} {"Comput. J."}
+
+MACRO {cn} {"Comput. Netw."}
+
+MACRO {cl} {"Comput. Lang."}
+
+MACRO {ibmjrd} {"IBM J. Res. and Development"}
+
+MACRO {ibmsj} {"IBM Systems Journal"}
+
+MACRO {ict} {"Inf. Contr."}
+
+MACRO {ieebcs} {"IEE/BCS Softw. Eng. J."}
+
+MACRO {ieees} {"IEEE Softw."}
+
+MACRO {ieeese} {"IEEE Trans. Softw. Eng."}
+
+MACRO {ieeetc} {"IEEE Trans. Comput."}
+
+MACRO {ieeetcad}
+ {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}
+
+MACRO {ieeetpds} {"IEEE Trans. Parall. Distrib. Syst."}
+
+MACRO {ieeetit} {"IEEE Trans. Inf. Theory"}
+
+MACRO {ipl} {"Inf. Process. Lett."}
+
+MACRO {icp} {"Inf. Comput."}
+
+MACRO {ist} {"Inf. Softw. Tech."}
+
+MACRO {ijsa} {"Int. J. Supercomput. Appl."}
+
+MACRO {ijpp} {"Int. J. Parallel Program."}
+
+MACRO {jlp} {"J. Logic Program."}
+
+MACRO {jfp} {"J. Funct. Program."}
+
+MACRO {jcss} {"J. Comput. Syst. Sci."}
+
+MACRO {jsmrp} {"J. Softw. Maint. Res. Pract."}
+
+MACRO {jss} {"J. Syst. Softw."}
+
+MACRO {jlc} {"J. Logic and Comput."}
+
+MACRO {jlsc} {"J. Lisp Symb. Comput."}
+
+MACRO {lpls} {"Lett. Program. Lang. Syst."}
+
+MACRO {mor} {"Math. Oper. Res."}
+
+MACRO {mscs} {"Math. Struct. Comput. Sci."}
+
+MACRO {mst} {"Math. Syst. Theor."} % jtb: was Math. Syst. Theory
+ % jtb: (if you ask me, I prefer the old way)
+MACRO {ngc} {"New Gen. Comput."}
+
+MACRO {scp} {"Sci. Comput. Program."}
+
+MACRO {sicomp} {"SIAM J. Comput."}
+
+MACRO {spe} {"Softw. Pract. Exper."}
+
+MACRO {tocs} {"ACM Trans. Comput. Syst."}
+
+MACRO {tods} {"ACM Trans. Database Syst."}
+
+MACRO {tog} {"ACM Trans. Graphics"}
+
+MACRO {toms} {"ACM Trans. Math. Softw."}
+
+MACRO {toois} {"ACM Trans. Office Inf. Syst."}
+
+MACRO {toplas} {"ACM Trans. Program. Lang. Syst."}
+
+MACRO {tocl} {"ACM Trans. On Comp. Logic"}
+
+MACRO {tcs} {"Theor. Comput. Sci."} % jtb: was Theor. Comp. Sci.
+
+MACRO {tr} {"Tech. Rep."}
+
+READ
+
+FUNCTION {sortify}
+{ purify$
+ "l" change.case$
+}
+
+INTEGERS { len }
+
+FUNCTION {chop.word}
+{ 's :=
+ 'len :=
+ s #1 len substring$ =
+ { s len #1 + global.max$ substring$ }
+ 's
+ if$
+}
+
+
+
+FUNCTION {sort.format.names}
+{ 's :=
+ #1 'nameptr :=
+ ""
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { nameptr #1 >
+ { " " * }
+ 'skip$
+ if$
+ s nameptr "{vv{ } }{ll{ }}{ f{ }}{ jj{ }}" format.name$ 't :=
+ nameptr numnames = t "others" = and
+ { " et~al" * }
+ { t sortify * }
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+}
+
+FUNCTION {sort.format.title}
+{ 't :=
+ "A " #2
+ "An " #3
+ "The " #4 t chop.word
+ chop.word
+ chop.word
+ sortify
+ #1 global.max$ substring$
+}
+
+FUNCTION {author.sort}
+{ author empty$
+ { key empty$
+ { "to sort, need author or key in " cite$ * warning$
+ "" }
+ { key sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+
+FUNCTION {editor.sort}
+{ editor empty$
+ { key empty$
+ { "to sort, need editor or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+}
+
+FUNCTION {author.editor.sort}
+{ author empty$
+ { "missing author in " cite$ * warning$
+ editor empty$
+ { key empty$
+ { "to sort, need author, editor, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+
+FUNCTION {author.organization.sort}
+%
+% added - GNP. Stack author or organization for sorting (from alpha.bst).
+% Unlike alpha.bst, we need entire names, not abbreviations
+%
+{ author empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need author, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { organization sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+
+FUNCTION {editor.organization.sort}
+%
+% added - GNP. Stack editor or organization for sorting (from alpha.bst).
+% Unlike alpha.bst, we need entire names, not abbreviations
+%
+{ editor empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need editor, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { organization sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+}
+
+FUNCTION {presort}
+%
+% Presort creates the bibentry's label via a call to calc.label, and then
+% sorts the entries based on entry type. Chicago.bst adds support for
+% including organizations as the sort key; the following is stolen from
+% alpha.bst.
+%
+{ calc.label sortify % recalculate bibitem label
+ year field.or.null purify$ #-1 #4 substring$ * % add year
+ " "
+ *
+ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.sort
+ { type$ "proceedings" =
+ 'editor.organization.sort
+ { type$ "manual" =
+ 'author.organization.sort
+ 'author.sort
+ if$
+ }
+ if$
+ }
+ if$
+ #1 entry.max$ substring$ % added for newapa
+ 'sort.label := % added for newapa
+ sort.label % added for newapa
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+
+ITERATE {presort}
+
+SORT % by label, year, author/editor, title
+
+STRINGS { last.label next.extra }
+
+INTEGERS { last.extra.num }
+
+FUNCTION {initialize.extra.label.stuff}
+{ #0 int.to.chr$ 'last.label :=
+ "" 'next.extra :=
+ #0 'last.extra.num :=
+}
+
+FUNCTION {forward.pass}
+%
+% Pass through all entries, comparing current entry to last one.
+% Need to concatenate year to the stack (done by calc.label) to determine
+% if two entries are the same (see presort)
+%
+{ last.label
+ calc.label year field.or.null purify$ #-1 #4 substring$ * % add year
+ #1 entry.max$ substring$ = % are they equal?
+ { last.extra.num #1 + 'last.extra.num :=
+ last.extra.num int.to.chr$ 'extra.label :=
+ }
+ { "a" chr.to.int$ 'last.extra.num :=
+ "" 'extra.label :=
+ calc.label year field.or.null purify$ #-1 #4 substring$ * % add year
+ #1 entry.max$ substring$ 'last.label := % assign to last.label
+ }
+ if$
+}
+
+FUNCTION {reverse.pass}
+{ next.extra "b" =
+ { "a" 'extra.label := }
+ 'skip$
+ if$
+ label.year extra.label * 'sort.year :=
+ extra.label 'next.extra :=
+}
+
+EXECUTE {initialize.extra.label.stuff}
+
+ITERATE {forward.pass}
+
+REVERSE {reverse.pass}
+
+FUNCTION {bib.sort.order}
+{ sort.label
+ " "
+ *
+ year field.or.null sortify
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+
+ITERATE {bib.sort.order}
+
+SORT % by sort.label, year, title --- giving final bib. order.
+
+FUNCTION {begin.bib}
+
+{ preamble$ empty$
+ 'skip$
+ { preamble$ write$ newline$ }
+ if$
+ "\begin{thebibliography}{}" write$ newline$
+}
+
+
+EXECUTE {begin.bib}
+
+EXECUTE {init.state.consts}
+
+ITERATE {call.type$}
+
+FUNCTION {end.bib}
+{ newline$
+ "\end{thebibliography}" write$ newline$
+}
+
+EXECUTE {end.bib}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/acmtrans2m.cls Mon Dec 03 08:16:58 2012 +0000
@@ -0,0 +1,1578 @@
+% latex2e by nr 7/3/96
+% acmtrans.cls revised 4/19/96
+% revised again 31-JAN-1996 (see end of file)
+% revised 5-14-1997 :
+% Don't use sans-serif font in categories and descriptors
+% include latexsym by default
+% Define longpage and shortpage
+% Adjusted from the acmtrans2e.cls file to the needs of ACM TOCL by
+% Marco Aiello on June 14, 2000.
+% Further changes made by Frederic Goualard on Sep. 27, 2000
+% to take care of the indentation problem in the bibliography
+% arising without the use of the hyperref package.
+% Modularization to adapt to the needs of ALL Transactions of the ACM,
+% and the Journal of the ACM, by Marco Aiello on June and October 2001.
+% Here is the basic framework that is needed to convert your paper
+% into ACM Transactions format and bibliographic format. For a tutorial
+% introduction, see ``instructions.tex'' (compile it with LaTeX) that
+% accompanies the distribution of this style file.
+%
+% -> \documentclass{acmtrans2m}
+% -> \markboth{}{}
+% takes 2 arguments and it is for the left- and right-page headers:
+% the first set of braces is assigned for author's name(s)
+% and
+% the second set of braces is assigned for the title
+% (if the title is too long, contraction may be needed
+% -> \title{}
+% if the title is too long, it can be separated by \\
+% -> \author{}
+% author1 \\ author1 affiliation
+% \and
+% author2 \\ author2 affiliation
+% -> \begin{abstract}
+% -> \end{abstract}
+%
+% -> \category{}{}{}
+% takes 3 arguments for the Computing Reviews Classification Scheme.
+% ex: \category{D.3.3}{Programming Languages}{Language Constructs and
+% Features}[data types and structures]
+% the last argument, in square brackets, is optional.
+% -> \terms{} (ex: \terms{Human Factors, Languages})
+% -> \keywords{} (in alphabetical order \keywords{document processing, sequences,
+% string searching, subsequences, substrings})
+% -> \begin{document}
+%
+% -> \begin{bottomstuff}
+% similar to \thanks
+% for authors' addresses; research/grant statements
+% -> \end{bottomstuff}
+% -> \maketitle
+%
+% Now you can start the body of the paper; your figures, tables and
+% use all the latex constructs.
+%
+% -> \begin{acks}
+% acknowledgements
+% -> \end{acks}
+%
+% -> \bibliographystyle{acmtrans}
+% -> \bibliography{mybib_file}
+%
+% ****
+% If your paper has been accepted with a separate (electronic only)
+% appendix, you need to add the following control sequence:
+%
+%
+% body of appendix
+%!!!!!! \appendixhead has be cut into two: \appendixhead and \elecappendix
+%!!!!!! See end of file. (jtb)
+%
+% -> \end{document}
+%
+% Do not worry about the other definitions in this style file
+% Remember to compile: latex, bibtex, latex latex
+%
+% Bibliographic cite forms needed:
+%
+% \cite{key}
+% which produces citations with author list and year.
+% eg. [Brown 1978; Jarke, et al. 1985]
+% \citeA{key}
+% which produces citations with only the author list.
+% eg. [Brown; Jarke, et al.]
+% \citeN{key}
+% which produces citations with the author list and year, but
+% can be used as nouns in a sentence; no brackets appear around
+% the author names, but only around the year.
+% eg. Shneiderman [1978] states that......
+% \citeN should only be used for a single citation.
+% \citeNN{refkey1,refkey2} for author [ref1year; ref2year]
+% \citeyear{key}
+% which produces the year information only, within brackets.
+%
+% Abbreviated author lists use the ``et al.'' construct.
+%
+% The above are examples of required ACM bibliographic cite formats needed.
+% *******************
+% Here is the complete list of cite forms from the chicago bibliographic style
+%
+% \cite{key}
+% which produces citations with abbreviated author list and year.
+% \citeNP{key}
+% which produces citations with abbreviated author list and year.
+% \citeA{key}
+% which produces only the abbreviated author list.
+% \citeANP{key}
+% which produces only the abbreviated author list.
+% \citeN{key}
+% which produces the abbreviated author list and year, with only the
+% year in parentheses. Use with only one citation.
+% \citeyear{key}
+% which produces the year information only, within parentheses.
+% \citeyearNP{key}
+% which produces the year information only.
+%
+% Abbreviated author lists use the ``et al.'' construct.
+%
+% `NP' means `no parentheses'
+%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesClass{acmtrans2m} [1996/07/03 ACM Transactions class based on <23 April 96>]
+\RequirePackage{latexsym}
+%aiellom{
+\RequirePackage{url}
+
+% Do not change the following! Use the appropriate acmtocl, acmtods, ...
+% options in the .tex file
+\def\@acmVolume{V} %the volume
+\def\@acmNumber{N} %the number
+\def\@acmYear{YY} %the last two digits of the year,
+\def\@acmMonth{0} %the month number
+\def\@journalName{ACM Journal Name} %the name of the ACM journal
+\def\@journalNameShort{jn} %the acronym of the ACM journal
+\def\@permissionCodeOne{0000-0000} %the permission code of the ACM journal
+\def\@permissionCodeTwo{\acmMonthCode} %the permission code of the ACM journal part 2
+\def\@pageCode{\acmPageCode} %the first page of the article in 4 digits
+
+\newif\if@acmnow \newif\if@acmjacm \newif\if@acmcsur
+\newif\if@acmtissec \newif\if@acmtochi \newif\if@acmtocl
+\newif\if@acmtocs \newif\if@acmtodaes \newif\if@acmtods
+\newif\if@acmtogs \newif\if@acmtois \newif\if@acmtoit
+\newif\if@acmtomacs \newif\if@acmtoms \newif\if@acmtoplas
+\newif\if@acmtosem
+
+\DeclareOption{acmnow}{
+ \typeout{Directly generating the Month and Year for footers from the clock.}
+ \def\@acmYear{\yearTwoDigits}
+ \def\@acmMonth{\the\month}
+}
+
+\DeclareOption{acmjacm}{
+ \typeout{}
+ \typeout{Using ACM JACM option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ %\global\@acmjacmfalse
+ \global\@acmcsurfalse \global\@acmtissecfalse \global\@acmtochifalse
+ \global\@acmtoclfalse \global\@acmtocsfalse \global\@acmtodaesfalse
+ \global\@acmtodsfalse \global\@acmtogsfalse \global\@acmtoisfalse
+ \global\@acmtoitfalse \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmjacmtrue
+ \def\@journalName{Journal of the ACM}
+ \def\@journalNameShort{jacm}
+ \def\@permissionCodeOne{0004-5411}
+}
+
+\DeclareOption{acmcsur}{
+ \typeout{}
+ \typeout{Using ACM CSUR option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse % \global\@acmcsurfalse
+ \global\@acmtissecfalse \global\@acmtochifalse \global\@acmtoclfalse
+ \global\@acmtocsfalse \global\@acmtodaesfalse \global\@acmtodsfalse
+ \global\@acmtogsfalse \global\@acmtoisfalse \global\@acmtoitfalse
+ \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmcsurtrue
+ \def\@journalName{ACM Computing Surveys}
+ \def\@journalNameShort{csur}
+ \def\@permissionCodeOne{0360-0300}
+}
+
+\DeclareOption{acmtissec}{
+ \typeout{}
+ \typeout{Using ACM TISSEC option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse %\global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ \global\@acmtomsfalse \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtissectrue
+ \def\@journalName{ACM Transactions on Information Systems and Security}
+ \def\@journalNameShort{tissec}
+ \def\@permissionCodeOne{1094-9224}
+}
+
+\DeclareOption{acmtochi}{
+ \typeout{}
+ \typeout{Using ACM TOCHI option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ %\global\@acmtochifalse
+ \global\@acmtoclfalse \global\@acmtocsfalse \global\@acmtodaesfalse
+ \global\@acmtodsfalse \global\@acmtogsfalse \global\@acmtoisfalse
+ \global\@acmtoitfalse \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtochitrue
+ \def\@journalName{ACM Transactions on Computer-Human Interaction}
+ \def\@journalNameShort{tochi}
+ \def\@permissionCodeOne{1073-0516}
+}
+
+\DeclareOption{acmtocl}{
+ \typeout{}
+ \typeout{Using ACM TOCL option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse %\global\@acmtoclfalse
+ \global\@acmtocsfalse \global\@acmtodaesfalse \global\@acmtodsfalse
+ \global\@acmtogsfalse \global\@acmtoisfalse \global\@acmtoitfalse
+ \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtocltrue
+ \def\@journalName{ACM Transactions on Computational Logic}
+ \def\@journalNameShort{tocl}
+ \def\@permissionCodeOne{1529-3785}
+}
+
+\DeclareOption{acmtocs}{
+ \typeout{}
+ \typeout{Using ACM TOCS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse
+ %\global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ \global\@acmtomsfalse \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtocstrue
+ \def\@journalName{ACM Transactions on Computer Systems}
+ \def\@journalNameShort{tocs}
+ \def\@permissionCodeOne{0734-2071}
+}
+
+\DeclareOption{acmtodaes}{
+ \typeout{}
+ \typeout{Using ACM TODAES option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ %\global\@acmtodaesfalse
+ \global\@acmtodsfalse \global\@acmtogsfalse \global\@acmtoisfalse
+ \global\@acmtoitfalse \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtodaestrue
+ \def\@journalName{ACM Transactions on Design Automation of Electronic Systems}
+ \def\@journalNameShort{todaes}
+ \def\@permissionCodeOne{1084-4309}
+}
+
+\DeclareOption{acmtods}{
+ \typeout{}
+ \typeout{Using ACM TODS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse
+ %\global\@acmtodsfalse
+ \global\@acmtogsfalse \global\@acmtoisfalse \global\@acmtoitfalse
+ \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtodstrue
+ \def\@journalName{ACM Transactions on Database Systems}
+ \def\@journalNameShort{tods}
+ \def\@permissionCodeOne{0362-5915}
+}
+
+\DeclareOption{acmtogs}{
+ \typeout{}
+ \typeout{Using ACM TOGS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse
+ %\global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ \global\@acmtomsfalse \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtogstrue
+ \def\@journalName{ACM Transactions on Graphics}
+ \def\@journalNameShort{togs}
+ \def\@permissionCodeOne{0730-0301}
+}
+
+\DeclareOption{acmtois}{
+ \typeout{}
+ \typeout{Using ACM TOIS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ %\global\@acmtoisfalse
+ \global\@acmtoitfalse \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtoistrue
+ \def\@journalName{ACM Transactions on Information Systems}
+ \def\@journalNameShort{tois}
+ \def\@permissionCodeOne{1046-8188}
+}
+
+\DeclareOption{acmtoit}{
+ \typeout{}
+ \typeout{Using ACM TOIT option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse
+ %\global\@acmtoitfalse
+ \global\@acmtomacsfalse \global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtoittrue
+ \def\@journalName{ACM Transactions on Internet Technology}
+ \def\@journalNameShort{toit}
+ \def\@permissionCodeOne{1533-5399}
+}
+
+\DeclareOption{acmtomacs}{
+ \typeout{}
+ \typeout{Using ACM TOMACS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse
+ %\global\@acmtomacsfalse
+ \global\@acmtomsfalse \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtomacstrue
+ \def\@journalName{ACM Transactions on Modeling and Computer Simulation}
+ \def\@journalNameShort{tomacs}
+ \def\@permissionCodeOne{1049-3301}
+}
+
+\DeclareOption{acmtoms}{
+ \typeout{}
+ \typeout{Using ACM TOMS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ %\global\@acmtomsfalse
+ \global\@acmtoplasfalse \global\@acmtosemfalse
+ \global\@acmtomstrue
+ \def\@journalName{ACM Transactions on Mathematical Software}
+ \def\@journalNameShort{toms}
+ \def\@permissionCodeOne{0098-3500}
+}
+
+\DeclareOption{acmtoplas}{
+ \typeout{}
+ \typeout{Using ACM TOPLAS option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ \global\@acmtomsfalse
+ %\global\@acmtoplasfalse
+ \global\@acmtosemfalse
+ \global\@acmtoplastrue
+ \def\@journalName{ACM Transactions on Programming Languages and Systems}
+ \def\@journalNameShort{toplas}
+ \def\@permissionCodeOne{0164-0925}
+}
+
+\DeclareOption{acmtosem}{
+ \typeout{}
+ \typeout{Using ACM, TOSEM option: 2001/06/01 by Marco Aiello et al.}
+ \typeout{}
+ \global\@acmjacmfalse \global\@acmcsurfalse \global\@acmtissecfalse
+ \global\@acmtochifalse \global\@acmtoclfalse \global\@acmtocsfalse
+ \global\@acmtodaesfalse \global\@acmtodsfalse \global\@acmtogsfalse
+ \global\@acmtoisfalse \global\@acmtoitfalse \global\@acmtomacsfalse
+ \global\@acmtomsfalse \global\@acmtoplasfalse
+ %\global\@acmtosemfalse
+ \global\@acmtosemtrue
+ \def\@journalName{ACM Transactions on Software Engineering and Methodology}
+ \def\@journalNameShort{tosem}
+ \def\@permissionCodeOne{1049-331X}
+}
+%}aiellom
+
+
+
+\if@compatibility\else
+\DeclareOption{a4paper}
+ {\setlength\paperheight {297mm}%
+ \setlength\paperwidth {210mm}%
+ \def\special@paper{210mm,297mm}}
+\DeclareOption{a5paper}
+ {\setlength\paperheight {210mm}%
+ \setlength\paperwidth {148mm}%
+ \def\special@paper{148mm,210mm}}
+\DeclareOption{b5paper}
+ {\setlength\paperheight {250mm}%
+ \setlength\paperwidth {176mm}%
+ \setlength\voffset {-15mm}%
+ \setlength\hoffset {-20mm}%
+ \def\special@paper{176mm,250mm}}
+\DeclareOption{letterpaper}
+ {\setlength\paperheight {11in}%
+ \setlength\paperwidth {8.5in}%
+ \def\special@paper{8.5in,11in}}
+\DeclareOption{legalpaper}
+ {\setlength\paperheight {14in}%
+ \setlength\paperwidth {8.5in}%
+ \def\special@paper{8.5in,14in}}
+\DeclareOption{executivepaper}
+ {\setlength\paperheight {10.5in}%
+ \setlength\paperwidth {7.25in}%
+ \def\special@paper{7.25in,10.5in}}
+\DeclareOption{landscape}
+ {\setlength\@tempdima {\paperheight}%
+ \setlength\paperheight {\paperwidth}%
+ \setlength\paperwidth {\@tempdima}}
+\fi
+
+\DeclareOption{checkMargin}{\setlength\overfullrule{5pt}}
+\DeclareOption{final}{\setlength\overfullrule{0pt}}
+
+\DeclareOption{oneside}{\@twosidefalse \@mparswitchfalse}
+\DeclareOption{twoside}{\@twosidetrue \@mparswitchtrue}
+
+\DeclareOption{10pt}{\def\@ptsize{0}} %needed for amssymbols.sty
+\DeclareOption{11pt}{\ClassError{acmtrans}{11pt style not supported}
+ {ACM transactions documents can be set in 10pt only}}
+\DeclareOption{12pt}{\ClassError{acmtrans}{11pt style not supported}
+ {ACM transactions documents can be set in 10pt only}}
+\newif\if@hyperref
+\DeclareOption{hyperref}{%
+ \def\pages{\pageref{@firstpg}--\pageref{@lastpg}}%
+ \def\mypage{\thepage}%
+ \def\@getpagenum#1#2#3#4{#2}%
+ \def\pdfinfo#1#2{\pdfmark{pdfmark=/DOCINFO,Title=#1,Author=#2}}
+ \global\@hyperreftrue
+ }
+\DeclareOption{nohyperref}{
+ \def\pages{\pageref{@firstpg}--\pageref{@lastpg}}%
+ \def\@getpagenum#1#2{#2}%
+ \def\mypage{\thepage}%
+ \def\pdfinfo#1#2{}%
+ \def\pdfbookmark#1#2{}%
+ \global\@hyperreffalse
+ }
+\DeclareOption{notfinal}{
+ \def\pages{BD}%
+ \def\mypage{TBD}%
+ \def\@getpagenum#1#2{#2}%
+ \def\pdfinfo#1#2{}%
+ \def\pdfbookmark#1#2{}%
+ }
+\DeclareOption{omitline}{\def\@abstractbottom{\relax}}
+\DeclareOption{dontomitline}{\def\@abstractbottom{\if@acmjacm\else\hbox{\vrule height .2pt width 30pc}\fi}}
+\ExecuteOptions{twoside,notfinal,10pt,dontomitline,nohyperref,letterpaper} % defaults
+
+
+
+\ProcessOptions
+
+%{aiellom to automatize the issue specific data
+\def\acmVolume#1{\def\@acmVolume{#1}}
+\def\acmNumber#1{\def\@acmNumber{#1}}
+\if@acmnow\else
+\def\acmYear#1{\def\@acmYear{#1}}
+\def\acmMonth#1{\def\@acmMonth{#1}}
+\fi
+\def\@acmMonthName{\ifnum\@acmMonth=1 January\fi\ifnum\@acmMonth=2 February\fi\ifnum\@acmMonth=3 March\fi\ifnum\@acmMonth=4 April\fi\ifnum\@acmMonth=5 May\fi\ifnum\@acmMonth=6 June\fi\ifnum\@acmMonth=7 July\fi\ifnum\@acmMonth=8 August\fi\ifnum\@acmMonth=9 September\fi\ifnum\@acmMonth=10 October\fi\ifnum\@acmMonth=11 November\fi\ifnum\@acmMonth=12 December\fi}
+
+
+
+% Command to get the year from the system and display the last two digits
+\newcommand{\ignoretwo}[2]{}
+\newcommand{\yearTwoDigits}{\expandafter\ignoretwo\the\year}
+% overright the \@setref definition, so that if a reference is undefined
+% then it returns a number 0 and then the usual double boldface
+% question marks ??
+% this is necessary for the \acmPageCode command, otherwise it gives an error
+% everytime the aux file is not there
+\def\@setref#1#2#3{%
+ \ifx#1\relax
+ \number 0\relax
+ \protect\G@refundefinedtrue
+ \nfss@text{\reset@font\bfseries ??}%
+ \@latex@warning{Reference `#3' on page \thepage \space undefined}%
+ \else
+ \expandafter#2#1\null
+ \fi}
+%make the code a four digits string based on the first page number
+\newcommand{\acmPageCode}{\bgroup
+ \newcount\c@tempo
+ \setcounter{tempo}{\number\pageref{@firstpg}}\ifnum \c@tempo<1000 0\fi\ifnum \c@tempo<100 0\fi\ifnum \c@tempo<10 0\fi\ifnum \c@tempo<1 0\fi\pageref{@firstpg}
+ \egroup
+}
+\newcommand{\acmMonthCode}{\bgroup
+ \newcount\c@tempo
+ \setcounter{tempo}{\number\@acmMonth}\ifnum \c@tempo<10 0\fi\number\@acmMonth00\egroup
+}%}aiellom
+
+
+
+\lineskip 1pt \normallineskip 1pt
+\def\baselinestretch{1}
+
+\renewcommand\normalsize{%
+ \@setfontsize\normalsize\@xpt\@xiipt
+ \abovedisplayskip 6pt plus2pt minus1pt\belowdisplayskip \abovedisplayskip
+ \abovedisplayshortskip 6pt plus0pt minus 3pt
+ \belowdisplayshortskip 6pt plus0pt minus3pt\let\@listi\@listI}
+
+\newcommand\small{%
+ \@setfontsize\small\@ixpt{11pt}%
+ \abovedisplayskip 5pt plus 2pt minus 1pt\belowdisplayskip \abovedisplayskip
+ \abovedisplayshortskip 5pt plus0pt minus2pt\belowdisplayshortskip 5pt plus0pt
+ minus 2pt
+ \def\@listi{\leftmargin\leftmargini \topsep 5pt plus 2pt minus 1pt\parsep 0pt
+ plus .7pt
+ \itemsep 1.6pt plus .8pt}}
+\newcommand\footnotesize{%
+% \@setfontsize\footnotesize\@viiipt{10pt}
+ \@setsize\footnotesize{10pt}\viiipt\@viiipt
+ \abovedisplayskip 4pt plus 1pt minus 0pt\belowdisplayskip \abovedisplayskip
+ \abovedisplayshortskip 4pt plus 0pt minus 1pt\belowdisplayshortskip 4pt plus
+ 0pt minus 1pt
+ \def\@listi{\leftmargin\leftmargini \topsep 4pt plus 1pt minus
+ 0pt\parsep 0pt plus .5pt
+ \itemsep 1pt plus .7pt}}
+
+\newcommand\scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt}
+\newcommand\tiny{\@setfontsize\tiny\@vpt\@vipt}
+\newcommand\large{\@setfontsize\large\@xiipt{14}}
+\newcommand\Large{\@setfontsize\Large\@xivpt{18}}
+\newcommand\LARGE{\@setfontsize\LARGE\@xviipt{20}}
+\newcommand\huge{\@setfontsize\huge\@xxpt{25}}
+\newcommand\Huge{\@setfontsize\Huge\@xxvpt{30}}
+
+\normalsize
+
+ \oddsidemargin .75in \evensidemargin .75in \marginparwidth .5in
+ \marginparsep .125in
+ \topmargin .25in \headheight 12pt\headsep 16pt
+ %% not in latex2e \footheight 10pt
+ \footskip 15pt
+
+\textheight 47pc \textwidth 30pc \columnsep 10pt \columnseprule 0pt
+% next five lines added by K.R. Apt, March 20, 01
+\advance\textheight-2.6pt
+\newdimen\normaltextheight
+\setlength\normaltextheight{\textheight}
+%\renewcommand\rmdefault{pnc}
+%\renewcommand\sfdefault{phv}
+
+
+\footnotesep 7pt
+\skip\footins 15pt plus 4pt minus 3pt
+\floatsep 12pt plus 2pt minus 2pt
+\textfloatsep \floatsep
+\intextsep 1pc plus 1pc
+%%% not in 2e %% \@maxsep 1pc
+%%% not in 2e %% \@dblmaxsep 20pt
+\dblfloatsep 12pt plus 2pt minus 2pt
+\dbltextfloatsep 20pt plus 2pt minus 4pt
+\@fptop 0pt plus 1fil \@fpsep 1pc plus 2fil \@fpbot 0pt plus 1fil
+\@dblfptop 0pt plus 1fil \@dblfpsep 8pt plus 2fil \@dblfpbot 0pt plus 1fil
+\marginparpush 6pt
+
+\parskip 0pt plus .1pt \parindent 10pt \partopsep 0pt
+\@lowpenalty 51 \@medpenalty 151 \@highpenalty 301
+\@beginparpenalty -\@lowpenalty \@endparpenalty -\@lowpenalty \@itempenalty
+-\@lowpenalty
+
+
+\def\part{\@ucheadtrue
+ \@startsection{part}{9}{\z@}{-10pt plus -4pt minus
+ -2pt}{4pt}{\reset@font\normalsize\sffamily}}
+\def\section{\@ucheadtrue
+ \@startsection{section}{1}{\z@}{-10pt plus -4pt minus
+ -2pt}{4pt}{\reset@font\normalsize\sffamily}}
+\def\subsection{\@ucheadfalse
+ \@startsection{subsection}{2}{\z@}{-8pt plus -2pt minus
+ -1pt}{4pt}{\reset@font\normalsize\sffamily}}
+\def\subsubsection{\@ucheadfalse
+ \@startsection{subsubsection}{3}{\parindent}{6pt plus
+1pt}{-5pt}{\reset@font\normalsize\itshape}}
+\def\paragraph{\@ucheadfalse
+ \@startsection{paragraph}{3}{\parindent}{6pt plus
+1pt}{-5pt}{\reset@font\normalsize\itshape}}
+
+\renewcommand{\@seccntformat}[1]{\textup{\csname the#1\endcsname}}
+
+\gdef\@period{.}
+\def\@trivlist{\@topsepadd\topsep
+\if@noskipsec \gdef\@period{}\leavevmode\gdef\@period{.}\fi
+ \ifvmode \advance\@topsepadd\partopsep \else \unskip\par\fi
+ \if@inlabel \@noparitemtrue \@noparlisttrue
+ \else \@noparlistfalse \@topsep\@topsepadd \fi
+ \advance\@topsep \parskip
+ \leftskip\z@\rightskip\@rightskip \parfillskip\@flushglue
+ \@setpar{\if@newlist\else{\@@par}\fi} \global\@newlisttrue
+\@outerparskip\parskip}
+
+
+\def\@startsection#1#2#3#4#5#6{%
+ \if@noskipsec \leavevmode \fi
+ \par
+ \@tempskipa #4\relax
+ \@afterindenttrue
+ \ifdim \@tempskipa <\z@
+ \@tempskipa -\@tempskipa \@afterindentfalse
+ \fi
+ \if@nobreak
+ \everypar{}%
+ \else
+ \addpenalty\@secpenalty\addvspace\@tempskipa
+ \fi
+ \@ifstar
+ {\@ssect{#3}{#4}{#5}{#6}}%
+ {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}}
+\def\@sect#1#2#3#4#5#6[#7]#8{%
+ \ifnum #2>\c@secnumdepth
+ \let\@svsec\@empty
+ \else
+ \refstepcounter{#1}%
+ \if@uchead%
+ \protected@edef\@svsec{\@seccntformat{#1}.\quad\relax}%
+ \else%
+ \protected@edef\@svsec{\@seccntformat{#1}\quad\relax}%
+ \fi%
+ \fi
+ \@tempskipa #5\relax
+ \ifdim \@tempskipa>\z@
+ \begingroup
+ #6{%
+ \@hangfrom{\hskip #3\relax\@svsec}%
+ \interlinepenalty \@M \if@uchead\MakeUppercase{#8}\else#8\fi \@@par}%
+ \endgroup
+ \csname #1mark\endcsname{#7}%
+ \addcontentsline{toc}{#1}{%
+ \ifnum #2>\c@secnumdepth \else
+ \protect\numberline{\csname the#1\endcsname}%
+ \fi
+ #7}%
+ \else
+ \def\@svsechd{%
+ #6{\hskip #3\relax
+ \@svsec \if@uchead\Makeuppercase{#8}\else#8\fi}%
+ \csname #1mark\endcsname{#7}%
+ \addcontentsline{toc}{#1}{%
+ \ifnum #2>\c@secnumdepth \else
+ \protect\numberline{\csname the#1\endcsname}%
+ \fi
+ #7}}%
+ \fi
+ \@xsect{#5}}
+
+\def\@xsect#1{\@tempskipa #1\relax
+ \ifdim \@tempskipa>\z@
+ \par \nobreak
+ \vskip \@tempskipa
+ \@afterheading
+ \else \global\@nobreakfalse \global\@noskipsectrue
+ \everypar{\if@noskipsec \global\@noskipsecfalse
+ \clubpenalty\@M \hskip -\parindent
+ \begingroup \@svsechd\@period \endgroup \unskip
+ \hskip -#1
+ \else \clubpenalty \@clubpenalty
+ \everypar{}\fi}\fi\ignorespaces}
+\newif\if@uchead\@ucheadfalse
+
+
+\setcounter{secnumdepth}{3}
+\newcounter{secnumbookdepth}
+\setcounter{secnumbookdepth}{3}
+
+\newfont{\apbf}{cmbx9}
+
+\def\@withappendix#1{App--\number #1}
+
+\newcommand{\elecappendix}{
+}
+
+\def\appenheader{\global\@topnum\z@ \global\@botroom \textheight \begin{figure}
+\newfont{\sc}{cmcsc10}
+\parindent\z@
+\hbox{}
+\vskip -\textfloatsep
+\vskip 11pt
+\hrule height .2pt width 30pc
+\vskip 2pt\rule{0pt}{10pt}\ignorespaces}
+\def\endappenheader{\end{figure}\gdef\appendixhead{}}
+
+\def\@appsec{}
+
+\def\appendix{\par
+ \setcounter{section}{0}
+ \setcounter{subsection}{0}
+ \def\@appsec{APPENDIX }
+ \def\thesection{\Alph{section}}
+ \def\theHsection{\Alph{section}}}
+
+
+
+\labelsep 5pt
+\settowidth{\leftmargini}{(9)} \addtolength\leftmargini\labelsep
+\settowidth{\leftmarginii}{(b)} \addtolength\leftmarginii\labelsep
+\leftmarginiii \leftmarginii
+\leftmarginiv \leftmarginii
+\leftmarginv \leftmarginii
+\leftmarginvi \leftmarginii
+\leftmargin\leftmargini
+\labelwidth\leftmargini\advance\labelwidth-\labelsep
+\def\@listI{\leftmargin\leftmargini \parsep 0pt plus 1pt\topsep 6pt plus 2pt
+minus 2pt\itemsep 2pt plus 1pt minus .5pt}
+\let\@listi\@listI
+\@listi
+\def\@listii{\leftmargin\leftmarginii
+ \labelwidth\leftmarginii\advance\labelwidth-\labelsep
+ \topsep 0pt plus 1pt
+ \parsep 0pt plus .5pt
+ \itemsep \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
+ \topsep 0pt plus 1pt
+ \parsep 0pt plus .5pt
+ \itemsep \parsep}
+\def\@listiv{\leftmargin\leftmarginiv
+ \labelwidth\leftmarginiv\advance\labelwidth-\labelsep}
+\def\@listv{\leftmargin\leftmarginv
+ \labelwidth\leftmarginv\advance\labelwidth-\labelsep}
+\def\@listvi{\leftmargin\leftmarginvi
+ \labelwidth\leftmarginvi\advance\labelwidth-\labelsep}
+
+
+
+
+\def\enumerate{\ifnum \@enumdepth >3 \@toodeep\else
+ \advance\@enumdepth \@ne
+ \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list
+ {\csname label\@enumctr\endcsname}{\usecounter
+ {\@enumctr}\def\makelabel##1{##1\hss}}\fi}
+\def\longenum{\ifnum \@enumdepth >3 \@toodeep\else
+ \advance\@enumdepth \@ne
+ \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list
+ {\csname label\@enumctr\endcsname}{\usecounter
+ {\@enumctr}\labelwidth\z@}\fi}
+%\leftmargin\z@ \itemindent\parindent}\fi} - this indents each item in enumerate
+\let\endlongenum\endlist
+%%--------------------CHANGED: always roman parentheses. dave ---------------%%
+\def\labelenumi{{\rm (}\arabic{enumi}\/{\rm )}}
+\def\theenumi{\arabic{enumi}}
+\def\labelenumii{{\rm (}\alph{enumii}\rm{)}}
+\def\theenumii{\alph{enumii}}
+\def\p@enumii{\theenumi}
+\def\labelenumiii{\roman{enumiii}.}
+\def\theenumiii{\roman{enumiii}}
+\def\p@enumiii{\theenumi{\rm (}\theenumii{\rm )}}
+\def\labelenumiv{\Alph{enumiv}.}
+\def\theenumiv{\Alph{enumiv}}
+\def\p@enumiv{\p@enumiii\theenumiii}
+
+\def\p@enumiv{\p@enumiii\theenumiii}
+
+\def\itemize{\list{---\hskip -\labelsep}{\settowidth
+ {\leftmargin}{---}\labelwidth\leftmargin
+ \addtolength{\labelwidth}{-\labelsep}}}
+\let\enditemize\endlist
+\def\longitem{\list{---}{\labelwidth\z@
+ \leftmargin\z@ \itemindent\parindent \advance\itemindent\labelsep}}
+\let\endlongitem\endlist
+\def\verse{\let\\=\@centercr
+ \list{}{\leftmargin 2pc
+ \itemindent -1.5em\listparindent \itemindent
+ \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
+\let\endverse\endlist
+\def\quotation{\list{}{\leftmargin 2pc \listparindent .5em
+ \itemindent\listparindent
+ \rightmargin\leftmargin \parsep 0pt plus 1pt}\item[]}
+\let\endquotation=\endlist
+\def\quote{\list{}{\leftmargin 2pc \rightmargin\leftmargin}\item[]}
+\let\endquote=\endlist
+
+\def\description{\list{}{\listparindent\parindent\labelwidth\z@
+ \leftmargin\z@ \itemindent\parindent\advance\itemindent\labelsep
+ \def\makelabel##1{\it ##1.}}}
+\let\enddescription\endlist
+
+\def\describe#1{\list{}{\listparindent\parindent\settowidth{\labelwidth}{#1}\leftmargin
+ \labelwidth\addtolength\leftmargin\labelsep\def\makelabel##1{##1\hfil}}}
+\let\enddescribe\endlist
+
+ \def\program{\ifx\@currsize\normalsize\small \else \rm \fi\tabbing}
+ \let\endprogram\endtabbing
+ \def\@begintheorem#1#2{\trivlist \item[\hskip 10pt\hskip
+ \labelsep{\sc{#1}\hskip 5pt\relax #2.}] \itshape}
+ % aiellom{: this is what makes the theorem environment with names
+ % ABOVE #1 is the word example, corollary, etc.
+ % #2 is the number
+ % \def\@opargbegintheorem#1#2#3{\trivlist
+ % \item[\hskip 10pt \hskip \labelsep{\sc #1\savebox\@tempboxa{#3}\ifdim
+ % \wd\@tempboxa>\z@ \hskip 5pt\relax \box\@tempboxa\fi.}] \itshape}
+ % is been changed to
+ % #1 is the word theorem, lemma, etc.
+ % #2 is the number
+ % #3 is the name of the theorem, lemma, etc.
+ \def\@opargbegintheorem#1#2#3{\trivlist
+ \item[\hskip 10pt \hskip
+\labelsep{\sc{#1}\savebox\@tempboxa{\sc{#3}}\ifdim
+ \wd\@tempboxa>\z@ \hskip 5pt\relax \sc{#2} \box\@tempboxa\fi.}]
+\itshape}
+ % aiellom}
+
+
+
+\newif\if@qeded\global\@qededfalse
+\def\proof{\global\@qededfalse\@ifnextchar[{\@xproof}{\@proof}}
+\def\endproof{\if@qeded\else\qed\fi\endtrivlist}
+\def\qed{\unskip\kern 10pt{\unitlength1pt\linethickness{.4pt}\framebox(6,6){}}
+\global\@qededtrue}
+\def\@proof{\trivlist \item[\hskip 10pt\hskip
+ \labelsep{\sc Proof.}]\ignorespaces}
+\def\@xproof[#1]{\trivlist \item[\hskip 10pt\hskip
+ \labelsep{\sc Proof #1.}]\ignorespaces}
+
+\def\newdef#1#2{\expandafter\@ifdefinable\csname #1\endcsname
+{\@definecounter{#1}\expandafter\xdef\csname
+the#1\endcsname{\@thmcounter{#1}}\global
+ \@namedef{#1}{\@defthm{#1}{#2}}\global
+ \@namedef{end#1}{\@endtheorem}}}
+\def\@defthm#1#2{\refstepcounter
+ {#1}\@ifnextchar[{\@ydefthm{#1}{#2}}{\@xdefthm{#1}{#2}}}
+\def\@xdefthm#1#2{\@begindef{#2}{\csname the#1\endcsname}\ignorespaces}
+\def\@ydefthm#1#2[#3]{\trivlist \item[\hskip 10pt\hskip
+ \labelsep{\it #2\savebox\@tempboxa{#3}\ifdim
+ \wd\@tempboxa>\z@ \ \box\@tempboxa\fi.}]\ignorespaces}
+\def\@begindef#1#2{\trivlist \item[\hskip 10pt\hskip
+ \labelsep{\it #1\ \rm #2.}]}
+
+\def\theequation{\arabic{equation}}
+
+\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \else \newpage \fi \thispagestyle{empty}\c@page\z@}
+\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi}
+
+\arraycolsep 2.5pt \tabcolsep 6pt \arrayrulewidth .4pt \doublerulesep 2pt
+\tabbingsep \labelsep
+
+\skip\@mpfootins = \skip\footins
+\fboxsep = 3pt \fboxrule = .4pt
+
+\newcounter{part}
+\newcounter{section}
+\newcounter{subsection}[section]
+\newcounter{subsubsection}[subsection]
+\newcounter{paragraph}[subsubsection]
+
+\def\thepart{\Roman{part}}
+\def\thesection {\arabic{section}}
+\def\thesubsection {\thesection.\arabic{subsection}}
+\def\thesubsubsection {\thesubsection.\arabic{subsubsection}}
+\def\theparagraph {\thesubsubsection.\arabic{paragraph}}
+
+\def\@pnumwidth{1.55em}
+\def\@tocrmarg {2.55em}
+\def\@dotsep{4.5}
+\setcounter{tocdepth}{3}
+
+\def\tableofcontents{\section*{Contents\@mkboth{CONTENTS}{CONTENTS}}
+ \@starttoc{toc}}
+\def\l@part#1#2{\addpenalty{\@secpenalty}
+ \addvspace{2.25em plus 1pt} \begingroup
+ \@tempdima 3em \parindent \z@ \rightskip \@pnumwidth \parfillskip
+-\@pnumwidth
+ {\large \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
+ \nobreak \endgroup}
+\def\l@section#1#2{\addpenalty{\@secpenalty} \addvspace{1.0em plus 1pt}
+\@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@pnumwidth
+ \parfillskip -\@pnumwidth
+ \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}\par
+ \endgroup}
+\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
+\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
+\def\listoffigures{\section*{List of Figures\@mkboth
+ {LIST OF FIGURES}{LIST OF FIGURES}}\@starttoc{lof}}
+\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
+\def\listoftables{\section*{List of Tables\@mkboth
+ {LIST OF TABLES}{LIST OF TABLES}}\@starttoc{lot}}
+\let\l@table\l@figure
+
+
+\def\thebibliography#1{\par\footnotesize
+\@ucheadfalse
+\@startsection{subsection}{2}{\z@}{16pt plus 2pt minus
+ 1pt}{2pt}{\sf}*{REFERENCES}%
+\list{\arabic{enumi}.}{%
+ \settowidth{\labelwidth}{99.}%
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep \topsep \z@ \parsep 0pt plus .1pt
+ \itemsep \parsep
+ \usecounter{enumi}}%
+ \def\newblock{\hskip .11em plus .33em minus .07em}
+ \sloppy
+ \widowpenalty=4500
+ \clubpenalty=4500
+ \sfcode`\.=1000\relax}
+\let\endthebibliography=\endlist
+
+
+\newif\if@restonecol
+\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
+\columnseprule \z@
+\columnsep 35pt\twocolumn[\section*{Index}]
+ \@mkboth{INDEX}{INDEX}\thispagestyle{plain}\parindent\z@
+ \parskip\z@ plus .3pt\relax\let\item\@idxitem}
+\def\@idxitem{\par\hangindent 40pt}
+\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
+\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
+\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
+\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}
+
+\def\footnoterule{\kern-3\p@
+ \hrule \@height 0.2\p@ \@width 47\p@
+ \kern 2.6\p@
+}
+
+\long\def\@makefntext#1{\parindent 1em\noindent
+ $^{\@thefnmark}$#1}
+
+
+\setcounter{topnumber}{3}
+\def\topfraction{.99}
+\setcounter{bottomnumber}{1}
+\def\bottomfraction{.5}
+\setcounter{totalnumber}{3}
+\def\textfraction{.01}
+\def\floatpagefraction{.85}
+\setcounter{dbltopnumber}{2}
+\def\dbltopfraction{.7}
+\def\dblfloatpagefraction{.5}
+
+\long\def\@makecaption#1#2{\vskip 1pc \setbox\@tempboxa\hbox{#1.\hskip
+1em\relax #2}
+ \ifdim \wd\@tempboxa >\hsize #1. #2\par \else \hbox
+to\hsize{\hfil\box\@tempboxa\hfil}
+ \fi}
+
+\def\nocaption{\refstepcounter\@captype \par
+ \vskip 1pc \hbox to\hsize{\hfil \footnotesize Figure \thefigure
+ \hfil}}
+
+
+\newcounter{figure}
+\def\thefigure{\@arabic\c@figure}
+\def\fps@figure{tbp}
+\def\ftype@figure{1}
+\def\ext@figure{lof}
+\def\fnum@figure{Fig.\ \thefigure}
+\def\figure{\let\normalsize\footnotesize \normalsize \@float{figure}}
+\let\endfigure\end@float
+\@namedef{figure*}{\@dblfloat{figure}}
+\@namedef{endfigure*}{\end@dblfloat}
+
+\newcounter{table}
+\def\thetable{\@Roman\c@table}
+\def\fps@table{tbp}
+\def\ftype@table{2}
+\def\ext@table{lot}
+\def\fnum@table{Table \thetable}
+\def\table{\let\normalsize\footnotesize \normalsize\@float{table}}
+\let\endtable\end@float
+\@namedef{table*}{\@dblfloat{table}}
+\@namedef{endtable*}{\end@dblfloat}
+\def\acmtable#1{\@narrowfig #1\relax
+ \let\caption\@atcap \let\nocaption\@atnocap
+ \def\@tmpnf{}\@ifnextchar[{\@xntab}{\@ntab}}
+\def\endacmtable{\hbox to \textwidth{\hfil
+\vbox{\hsize \@narrowfig
+\box\@nfcapbox
+{\baselineskip 4pt \hbox{\vrule height .4pt width \hsize}}
+\vskip -1pt
+\box\@nfigbox\vskip -1pt
+{\baselineskip 4pt \hbox{\vrule height .4pt width \hsize}}}\hfil}
+\end@float}
+\def\@xntab[#1]{\def\@tmpnf{[#1]}\@ntab}
+\def\@ntab{\expandafter\table\@tmpnf
+ \setbox\@nfigbox\vbox\bgroup
+ \hsize \@narrowfig \@parboxrestore}
+\def\@atmakecap #1#2{\setbox\@tempboxa\hbox{#1.\hskip 1em\relax #2}
+ \ifdim \wd\@tempboxa >\hsize \sloppy #1.\hskip 1em\relax #2 \par \else \hbox
+to\hsize{\hfil\box\@tempboxa\hfil}
+ \fi}
+\def\@atcap{\par\egroup\refstepcounter\@captype
+ \@dblarg{\@atcapx\@captype}}
+\long\def\@atcapx#1[#2]#3{\setbox\@nfcapbox\vbox {\hsize \wd\@nfigbox
+ \@parboxrestore
+ \@atmakecap{\csname fnum@#1\endcsname}{\ignorespaces #3}\par}}
+\def\@atnocap{\egroup \refstepcounter\@captype
+ \setbox\@nfcapbox\vbox {\hsize \wd\@nfigbox
+ \hbox to\hsize{\hfil \footnotesize Table \thetable\hfil}}}
+
+%
+%% Narrow figures
+%
+\def\narrowfig#1{\@narrowfig #1\relax
+ \let\caption\@nfcap \let\nocaption\@nfnocap
+ \def\@tmpnf{}\@ifnextchar[{\@xnfig}{\@nfig}}
+\def\endnarrowfig{\hbox to \textwidth{\if@nfeven
+ \box\@nfcapbox\hfil\box\@nfigbox
+ \else \box\@nfigbox\hfil\box\@nfcapbox\fi}\end@float}
+\def\@xnfig[#1]{\def\@tmpnf{[#1]}\@nfig}
+\def\@nfig{\expandafter\figure\@tmpnf
+ \setbox\@nfigbox\vbox\bgroup
+ \hsize \@narrowfig \@parboxrestore}
+\def\@nfmakecap #1#2{\setbox\@tempboxa\hbox{#1.\hskip 1em\relax #2}
+ \ifdim \wd\@tempboxa >\hsize \sloppy #1.\hskip 1em\relax #2 \par \else \hbox
+to\hsize{\if@nfeven\else\hfil\fi\box\@tempboxa\if@nfeven\hfil\fi}
+ \fi}
+\def\@nfcap{\par\egroup\refstepcounter\@captype
+ \@dblarg{\@nfcapx\@captype}}
+\long\def\@nfcapx#1[#2]#3{\@seteven
+ \setbox\@nfcapbox\vbox to \ht\@nfigbox
+ {\hsize \textwidth \advance\hsize -2pc \advance\hsize -\wd\@nfigbox
+ \@parboxrestore
+ \vfil
+ \@nfmakecap{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+ \vfil}}
+\def\@nfnocap{\egroup \refstepcounter\@captype \@seteven
+ \setbox\@nfcapbox\vbox to \ht\@nfigbox
+ {\hsize \textwidth \advance\hsize -2pc \advance\hsize -\wd\@nfigbox
+ \@parboxrestore
+ \vfil
+ \hbox to\hsize{\if@nfeven\else\hfil\fi
+ \footnotesize Figure \thefigure
+ \if@nfeven\hfil\fi}
+ \vfil}}
+\def\@seteven{\@nfeventrue
+ \@ifundefined{r@@nf\thefigure}{}{%
+ \edef\@tmpnf{\csname r@@nf\thefigure\endcsname}%
+ \edef\@tmpnf{\expandafter\@getpagenum\@tmpnf}%
+ \ifodd\@tmpnf\relax\@nfevenfalse\fi}%
+\label{@nf\thefigure}\edef\@tmpnfx{\if@nfeven e\else o\fi}
+\edef\@tmpnf{\write\@unused {\noexpand\ifodd \noexpand\c@page
+ \noexpand\if \@tmpnfx e\noexpand\@nfmsg{\thefigure} \noexpand\fi
+ \noexpand\else
+ \noexpand\if \@tmpnfx o\noexpand\@nfmsg{\thefigure}\noexpand\fi
+ \noexpand\fi }}\@tmpnf}
+\def\@nfmsg#1{Bad narrowfig: Figure #1 on page \thepage}
+
+\newdimen\@narrowfig
+\newbox\@nfigbox
+\newbox\@nfcapbox
+\newif\if@nfeven
+
+\def\and{\\ and\\}
+\def\maketitle{\newpage \thispagestyle{titlepage}\par
+ \begingroup \lineskip = \z@\null \vskip -30pt\relax
+ \parindent\z@ \LARGE {\raggedright \hyphenpenalty\@M
+ %\sf \@title \par
+ \@title \par
+ \global\firstfoot %aiellom
+ \global\runningfoot %aiellom
+}
+\label{@firstpg}
+{ \vskip 13.5pt\relax \normalsize \sf %vskip 13.5pt between title and author
+ \begingroup \addtolength{\baselineskip}{2pt}
+ \@author\par \vskip -2pt
+ \endgroup }
+ {\ifx \@categories\@empty
+ \else
+ \baselineskip 17pt\relax
+ \if@acmjacm\else\hbox{\vrule height .2pt width 30pc}\fi%to eliminate the lines for jacm
+ }
+ \vskip 8.5pt \footnotesize \box\@abstract \vskip 4pt\relax %vskip8.5 space above abstract
+ {\def\and{\unskip\/{\rm ; }}
+ Categories and Subject Descriptors: \@categories \fi}\par\vskip 4pt\relax
+ \box\@terms \vskip 4pt\relax
+ \box\@keywords \par
+ {\baselineskip 14pt\relax
+ \@abstractbottom
+ }
+ \vskip 23pt\relax
+ \endgroup
+\let\maketitle\relax
+ % \gdef\@author{}\gdef\@title{}
+ \gdef\@categories{}}
+
+
+\newbox\@abstract
+\newbox\@terms
+\newbox\@keywords
+\def\abstract{\global\setbox\@abstract=\vbox\bgroup \everypar{}
+ \footnotesize \hsize 30pc \parindent 10pt \noindent
+ \rule{0pt}{10pt}\ignorespaces}
+\def\endabstract{\egroup}
+
+\def\terms#1{\setbox\@terms=\vbox{\everypar{}
+ \footnotesize \hsize 30pc \parindent 0pt \noindent
+ General Terms: \ignorespaces #1}}
+\def\keywords#1{\setbox\@keywords=\vbox{\everypar{}
+ \footnotesize \hsize 30pc \parindent 0pt \noindent
+ Additional Key Words and Phrases: \ignorespaces #1}
+}
+
+\def\category#1#2#3{\@ifnextchar
+ [{\@category{#1}{#2}{#3}}{\@xcategory{#1}{#2}{#3}}}
+\def\@category#1#2#3[#4]{\edef\@tempa{\ifx \@categories\@empty
+ \else ; \fi}{\def\protect{\noexpand\protect
+ \noexpand}\def\and{\noexpand\and}\xdef\@categories{\@categories\@tempa #1
+[{\bf #2}]:
+ #3\kern\z@---\hskip\z@{\it #4}}}}
+\def\@xcategory#1#2#3{\edef\@tempa{\ifx \@categories\@empty \else ;
+\fi}{\def\protect{\noexpand\protect\noexpand}\def\and{\noexpand
+ \and}\xdef\@categories{\@categories\@tempa #1 [{\bf #2}]: #3}}}
+\def\@categories{}
+\def\bottomstuff{\global\@topnum\z@ \global\@botroom \textheight \begin{figure}
+\parindent\z@
+\hbox{}
+\vskip -\textfloatsep
+\vskip 10pt
+\hrule height .2pt width 30pc
+\vskip 2pt\rule{0pt}{10pt}\ignorespaces}
+\def\endbottomstuff{\permission\end{figure}\gdef\permission{}}
+
+\newenvironment{ackslike}[1]
+ {\par \footnotesize
+ \@ucheadfalse
+ \@startsection{subsection}{2}{\z@}{-16pt plus -2pt minus -1pt}{2pt}{\sf}*
+ {\uppercase{#1}}\par\normalsize
+ \pdfbookmark{Acknowledgments}{Ack}
+ }
+ {\par}
+\newenvironment{acks}{\begin{ackslike}{ACKNOWLEDGMENTS}}{\end{ackslike}}
+
+\def\received{\par\footnotesize\addvspace{18pt plus 0pt minus
+4pt}\parindent\z@}
+%the line below replaced by the line that follows (K.R. Apt, July 11, 2000
+%\def\endreceived{\label{@lastpg}\hskip-2pt\par}
+\def\endreceived{\label{@lastpg}\hskip-2pt\par\normalsize}
+
+\mark{{}{}}
+
+\def\ps@myheadings{\let\@mkboth\@gobbletwo
+\def\@oddhead{\hbox{}\hfill \small\sf \rightmark\hskip
+19pt{\Large$\cdot$}\hskip 17pt\mypage}
+\def\@oddfoot{\hbox{}\hfill\tiny\@runningfoot}
+\def\@evenhead{\small\sf\mypage \hskip 17pt{\Large$\cdot$}\hskip 19pt\leftmark\hfill \hbox{}}
+\def\@evenfoot{\tiny\@runningfoot\hfill\hbox{}}
+\def\sectionmark##1{}\def\subsectionmark##1{}}
+\def\@runningfoot{}
+\def\runningfoot{\def\@runningfoot{\@journalName, Vol.\ \@acmVolume, No.\ \@acmNumber, \@acmMonthName\ 20\@acmYear.}}
+\def\@firstfoot{}
+\def\firstfoot{\def\@firstfoot{\@journalName, Vol.\ \@acmVolume, No.\ \@acmNumber, \@acmMonthName\ 20\@acmYear, Pages \pages.}}
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+\def\@oddhead{}\def\@oddfoot{\hbox{}\hfill
+\tiny\@firstfoot}\def\@evenhead{}\def\@evenfoot{\tiny\@firstfoot\hfill\hbox{}}}
+
+\def\today{\ifcase\month\or
+ January\or February\or March\or April\or May\or June\or
+ July\or August\or September\or October\or November\or December\fi
+ \space\number\day, \number\year}
+\def\@marrayclassiv{\@addtopreamble{$\displaystyle \@nextchar$}}
+\def\@marrayclassz{\ifcase \@lastchclass \@acolampacol \or \@ampacol \or
+ \or \or \@addamp \or
+ \@acolampacol \or \@firstampfalse \@acol \fi
+\edef\@preamble{\@preamble
+ \ifcase \@chnum
+ \hfil$\relax\displaystyle\@sharp$\hfil \or $\relax\displaystyle\@sharp$\hfil
+ \or \hfil$\relax\displaystyle\@sharp$\fi}}
+\def\marray{\arraycolsep 2.5pt\let\@acol\@arrayacol \let\@classz\@marrayclassz
+ \let\@classiv\@marrayclassiv \let\\\@arraycr\def\@halignto{}\@tabarray}
+\def\endmarray{\crcr\egroup\egroup}
+
+
+\ps@myheadings \pagenumbering{arabic} \onecolumn
+
+%-----------------------BIBLIOGRAPHY STUFF-------------------------
+% this is adapted (November 1993) by Andrew Appel and Rebecca Davies from
+%
+%%% filename = "chicago.sty",
+%%% version = "4", % MODIFIED!
+%%% date = "31 August 1992",
+%%% time = "09:42:44 199",
+%%% author = "Glenn Paulley",
+%%% address = "Data Structuring Group
+%%% Department of Computer Science
+%%% University of Waterloo
+%%% Waterloo, Ontario, Canada
+%%% N2L 3G1",
+%%% telephone = "(519) 885-1211",
+%%% FAX = "(519) 885-1208",
+%%% email = "gnpaulle@bluebox.uwaterloo.ca",
+
+%%% ====================================================================
+%
+% this file: Modification of chicago.sty for new ACM bibliography
+% style, which is similar (but not identical) to the ``Chicago'' style.
+%
+% chicago.sty: Style file for use with bibtex style chicago.bst, for
+% bibliographies formatted according to the 13th Edition of the Chicago
+% Manual of Style.
+%
+% 'newapa.bst' was made from 'plain.bst', 'named.bst', and 'apalike.bst',
+% with lots of tweaking to make it look like APA style, along with tips
+% from Young Ryu and Brian Reiser's modifications of 'apalike.bst'.
+% newapa.sty formed the basis of this style, chicago.sty. Author-date
+% references in newapa.bst formed the basis for chicago.bst. Chicagoa.bst
+% supports annotations.
+%
+% Version 4 (August, 1992):
+% - fixed chicago.bst and chicagoa.bst to handle long author lists in
+% sorting
+% - fixed chicago.bst and chicagoa.bst so that missing page numbers in
+% ``article'' entries are handled correctly
+% - modified chicago.sty to format entries with 2nd and subsequent lines
+% indented.
+%
+% Citation format: (author-last-name year)
+% (author-last-name and author-last-name year)
+% (author-last-name et al. year)
+% (author-last-name)
+% author-last-name
+% author-last-name (year)
+% (author-last-name and author-last-name)
+% (author-last-name et al.)
+% (year) or (year,year)
+% year or year,year
+%
+% Reference list ordering: alphabetical by author or whatever passes
+% for author in the absence of one.
+%
+% This BibTeX style has support for abbreviated author lists and for
+% year-only citations. This is done by having the citations
+% actually look like
+%
+% \citeauthoryear{full-author-info}{abbrev-author-info}{year}
+%
+% The LaTeX style has to have the following (or similar)
+%
+% \let\@internalcite\cite
+% \def\fullcite{\def\citeauthoryear##1##2##3{##1, ##3}\@internalcite}
+% \def\fullciteA{\def\citeauthoryear##1##2##3{##1}\@internalcite}
+% \def\shortcite{\def\citeauthoryear##1##2##3{##2, ##3}\@internalcite}
+% \def\shortciteA{\def\citeauthoryear##1##2##3{##2}\@internalcite}
+% \def\citeyear{\def\citeauthoryear##1##2##3{##3}\@internalcite}
+%
+%
+% -------------------------------------------------------------------------
+%
+% Citation macros.
+%
+\let\@internalcite\cite
+
+\def\cite{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{[##1\if@tempswa , ##2\fi]}%
+ \def\citeauthoryear##1##2##3{##2 ##3}\@internalcite}
+\def\citeXNP#1#2{%
+ \def\@cite@label{#2}%
+ \def\@cite##1##2{##1\if@tempswa , ##2\fi}%
+ \def\citeauthoryear##1##2##3{\@cite@label}\@internalcite{#1}}
+% \def\@citeseppen{-1000}%
+% \def\@cite@label{#1}
+% \def\@cite##1##2{\if@tempswa ##2\fi}%
+% \def\citeauthoryear##1##2##3{##2 ##3}\@internalcite}
+\def\citeNP{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{##1\if@tempswa , ##2\fi}%
+ \def\citeauthoryear##1##2##3{##2 ##3}\@internalcite}
+\def\citeN{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{##1\if@tempswa , ##2]\else{]}\fi}%
+ \def\citeauthoryear##1##2##3{##2 [##3}\@citedata}
+\def\shortcite#1{\citeyear{#1}}
+\def\citeS#1{[\citeANP{#1} \citeyearNP{#1}]}
+\def\citeNS#1{\citeANP{#1} \citeyear{#1}}
+\def\citeNPS#1{\citeANP{#1} \citeyearNP{#1}}
+%testing year,year
+\def\citeNN{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{[##1\if@tempswa , ##2\fi]}%
+ \def\citeauthoryear##1##2##3{##3}\@citedata}
+
+\def\citeA{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{[##1\if@tempswa , ##2\fi]}%
+ \def\citeauthoryear##1##2##3{##2}\@internalcite}
+\def\citeANP{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{##1\if@tempswa , ##2\fi}%
+ \def\citeauthoryear##1##2##3{##2}\@internalcite}
+
+\def\citeyear{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{[##1\if@tempswa , ##2\fi]}%
+ \def\citeauthoryear##1##2##3{##3}\@citedata}
+\def\citeyearNP{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{##1\if@tempswa , ##2\fi}%
+ \def\citeauthoryear##1##2##3{##3}\@citedata}
+
+%
+% \@citedata and \@citedatax:
+%
+% Place commas in-between citations in the same \citeyear, \citeyearNP,
+% or \citeN command.
+% Use something like \citeN{ref1,ref2,ref3} and \citeN{ref4} for a list.
+%
+\def\@citedata{%
+ \@ifnextchar [{\@tempswatrue\@citedatax}%
+ {\@tempswafalse\@citedatax[]}%
+}
+
+\def\@citedatax[#1]#2{%
+\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi%
+ \def\@citea{}\@cite{\@for\@citeb:=#2\do%
+ {\@citea\def\@citea{; }\@ifundefined% by Young
+ {b@\@citeb}{{\bf ?}%
+ \@warning{Citation `\@citeb' on page \thepage \space undefined}}%
+{\csname b@\@citeb\endcsname}}}{#1}}%
+
+% don't box citations, separate with ; and a space
+% also, make the penalty between citations negative: a good place to break.
+%
+\def\@citex[#1]#2{%
+\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi%
+ \def\@citea{}\@cite{\@for\@citeb:=#2\do%
+ {\@citea\def\@citea{; }\@ifundefined% by Young
+ {b@\@citeb}{{\bf ?}%
+ \@warning{Citation `\@citeb' on page \thepage \space undefined}}%
+{\csname b@\@citeb\endcsname}}}{#1}}%
+
+% (from apalike.sty)
+% No labels in the bibliography.
+%
+\def\@biblabel#1{}
+
+% (from apalike.sty)
+% Set length of hanging indentation for bibliography entries.
+%
+\newlength{\bibhang}
+\setlength{\bibhang}{2em}
+
+% Indent second and subsequent lines of bibliographic entries. Stolen
+% from openbib.sty: \newblock is set to {}.
+
+\newdimen\bibindent
+\bibindent=1em
+\@ifundefined{refname}%
+ {\@ifundefined{chapter}%
+ {\newcommand{\refname}{\footnotesize REFERENCES}}%
+ {\newcommand{\refname}{\footnotesize BIBLIOGRAPHY}}%
+ }%
+ {}%
+\@ifundefined{chapter}%
+ {\def\thebibliography#1{\footnotesize \section*{\refname\@mkboth
+ {\uppercase{\refname}}{\uppercase{\refname}}}\list
+ {[\arabic{enumi}]}{
+ \settowidth\labelwidth{[#1]}
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \usecounter{enumi}}
+ \def\newblock{}
+ \sloppy
+ \sfcode`\.=1000\relax}}
+ {\def\thebibliography#1{\footnotesize \chapter*{\refname\@mkboth
+ {\uppercase{\refname}}{\uppercase{\refname}}}\list
+ {[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \usecounter{enumi}}
+ \def\newblock{}
+ \sloppy
+ \sfcode`\.=1000\relax}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% fixes to acm trans macro package
+% 31-JAN-1996
+% John Tang Boyland
+
+% newdef need to take the optional parameters of newtheorem
+\def\newdef#1{\@ifnextchar[{\@xnewdef{#1}}{\@ynewdef{#1}}}
+\def\@xnewdef#1[#2]#3{\newtheorem{italic@#1}[#2]{{\em #3}}\@newdef{#1}}
+\def\@ynewdef#1#2{\@ifnextchar[{\@xynewdef{#1}{#2}}{\@yynewdef{#1}{#2}}}
+\def\@xynewdef#1#2[#3]{\newtheorem{italic@#1}{{\em #2}}[#3]\@newdef{#1}}
+\def\@yynewdef#1#2{\newtheorem{italic@#1}{{\em #2}}\@newdef{#1}}
+% and now fix up definition, to change body to use roman font:
+\def\@newdef#1{\newenvironment{#1}{\@ifnextchar[{\@xstartdef{#1}}{\@ystartdef{#1}}}{\end{italic@#1}}}
+%changed by K.R. Apt on Sep. 27, 2000. It was: \def\@xstartdef#1[#2]{\begin{italic@#1}[#2]\rm}
+\def\@xstartdef#1[#2]{\begin{italic@#1}[{\em #2}]\rm}
+\def\@ystartdef#1{\begin{italic@#1}\rm}
+
+% footers produced too small (vpt), when ACM typsets them at 7.5pt (!).
+% A better compromise is viipt.
+\def\@oddfoot{\hbox{}\hfill\scriptsize\@runningfoot}
+\def\@evenfoot{\scriptsize\@runningfoot\hfill\hbox{}}
+
+% first footer was set to (vpt), when ACM typesets them at 6.5pt (!).
+% A better compromise is vipt.
+\def\firstfootsize{\@setsize\firstfootsize{7pt}\vipt\@vipt}
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+\def\@oddhead{}\def\@oddfoot{\hbox{}\hfill\firstfootsize\@firstfoot}%
+\def\@evenhead{}\def\@evenfoot{\firstfootsize\@firstfoot\hfill\hbox{}}}
+
+% new permission statement
+\long\def\permission{\par
+% linebreaks added to conform to the current style
+Permission to make digital/hard copy of all or part of this material without
+fee
+for personal or classroom use
+provided that the copies are not made or distributed for profit
+or commercial advantage, the ACM copyright/server notice, the title of the
+publication, and its date appear, and notice is given that copying is by
+permission of the ACM, Inc. To copy
+otherwise, to republish, to post on servers, or to redistribute to lists
+requires prior specific
+permission and/or a fee.\par
+\copyright\ 20\@acmYear\
+ACM \@permissionCodeOne/\@acmYear/\@permissionCodeTwo-\@pageCode\$5.00 % aiellom
+}
+
+% make sure \permission doesn't get trashed
+\def\endbottomstuff{\permission\end{figure}}
+
+% alternate way of using citeyear
+% \def\shortcite#1{\citeyear{#1}
+% enumerations and longenums are wrong
+% 1. the second line in a paragraph of an enumerations in theorems
+% (or other trivlists) doesn't line up under the first
+% 1. the second line of a longenum doesn't properly wrap around
+% back to the left margin.
+
+% the original definition of \@listI doesn't set labelwidth
+\def\@listI{\leftmargin\leftmargini
+ \labelwidth\leftmargini\advance\labelwidth-\labelsep
+ \parsep 0pt plus 1pt
+ \topsep 6pt plus 2pt minus 2pt
+ \itemsep 2pt plus 1pt minus .5pt}
+\let\@listi\@listI
+\@listi
+
+% add set of \labelwidth and \itemindent
+\def\longenum{\ifnum \@enumdepth >3 \@toodeep\else
+ \advance\@enumdepth \@ne
+ \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list
+ {\csname label\@enumctr\endcsname}{\usecounter
+ {\@enumctr}\labelwidth\z@\leftmargin\z@
+ \itemindent\parindent \advance\itemindent\labelsep}\fi}
+
+% split electronic appendix into two parts:
+
+
+%aiellom{
+\def\appendixhead#1{\appendix
+\section*{ELECTRONIC APPENDIX}
+The electronic appendix for this article can be accessed in
+ the ACM Digital Library by visiting the following URL:$\;$
+ \url{http://www.acm.org/pubs/citations/journals/}{\tt \@journalNameShort /20\@acmYear-\@acmVolume-\@acmNumber/p\pageref{@firstpg}-#1}.
+% \quad \href{http://www.acm.org/tocl}{{\small http://www.acm.org/tocl} }
+}
+%aiellom}
+
+\long\def\elecappendix{
+\clearpage
+\makeatletter
+\pagenumbering{withappendix}
+\makeatother
+\appendix
+\par\noindent{\sc This document is the online-only appendix to:}\hfill \vskip 1em
+{\vbox{\Large\sf \parindent0pt\@title{}}}\vskip .5em
+\vbox{\sf \parindent0pt\@author{}}\vskip .5em\noindent
+\vskip 10pt\noindent
+{\firstfootsize
+\@journalName, Vol.\ \@acmVolume, No.\ \@acmNumber, \@acmMonthName\ 20\@acmYear, Pages \pages.}
+\vskip 11pt\noindent
+\hrule height .2pt
+\par
+\bottomstuff
+\endbottomstuff
+}
+
+% provide for a single acknowledgment
+\def\ack{ \par \footnotesize
+\@ucheadfalse
+\@startsection{subsection}{2}{\z@}{-16pt plus -2pt minus
+ -1pt}{2pt}{\sf}*{ACKNOWLEDGMENT}\par\normalsize
+\pdfbookmark{Acknowledgment}{Ack}
+}
+\def\endack{\par}
+
+% provide both spellings of Acknowledgment(s)
+\let\acknowledgments\acks
+\let\endacknowledgments\endacks
+\let\acknowledgment\ack
+\let\endacknowledgment\endack
+
+\newcommand{\longpage}{\enlargethispage{\baselineskip}}
+\newcommand{\shortpage}{\enlargethispage{-\baselineskip}}
+
+
+% Don't indent bibliography and
+% override \refname (which sets fontsize):
+\def\thebibliography#1{
+ \footnotesize\section*{\footnotesize\sf{REFERENCES}\@mkboth
+ {\uppercase{\refname}}{\uppercase{\refname}}}%
+ \pdfbookmark{References}{Ref}
+ \list
+ {\@biblabel{\arabic{enumiv}}}{%
+ %\settowidth\labelwidth{[#1]}
+ \labelwidth 0pt
+ \leftmargin \bibindent
+ \labelsep 0pt
+ \if@hyperref
+ \itemindent -\bibindent
+ \fi
+ \listparindent -\bibindent
+ \labelsep -\bibindent
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \def\theenumiv{\arabic{enumiv}}}%
+ \def\newblock{\hskip .11em plus.33em minus.07em}%
+ \sloppy
+ \clubpenalty=4500
+ \widowpenalty=4500
+ \frenchspacing}
+\def\endthebibliography{%
+ \def\@noitemerr{\@warning{Empty `thebibliography' environment}}%
+ \endlist}
+\def\@lbibitem[#1]#2{\item[]\if@filesw
+ {\def\protect##1{\string ##1\space}\immediate
+ \write\@auxout{\string\bibcite{#2}{#1}}}\fi\hskip-1em\ignorespaces}
+% Fix cite so it doesn't repeat author lists in citations:
+
+\def\cite{\def\@citeseppen{-1000}%
+ \def\@cite##1##2{[##1\if@tempswa , ##2\fi]}%
+ \let\@lastauthor=\@noauthor
+ \let\citeauthoryear=\citeauthoryear@no@repeats\@internalcite}
+ %\def\citeauthoryear##1##2##3{##2 ##3}\@internalcite
+
+\def\@noauthor={\relax}
+\let\@lastauthor=\@noauthor
+\let\@currauthor=\@noauthor
+
+\def\citeauthoryear@no@repeats#1#2#3{%
+ \def\@currauthor{\csname @author #1\endcsname}%
+ \ifx\@lastauthor\@currauthor{#3}\else{#2 #3}\fi%
+ \let\@lastauthor=\@currauthor}
+
+\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
+\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
+\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
+\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
+\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
+\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
+\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
+\DeclareRobustCommand*\cal{\@fontswitch\relax\mathcal}
+\DeclareRobustCommand*\mit{\@fontswitch\relax\mathnormal}
+
+
+\if@hyperref
+ \let\pdfbookmark=\relax
+ \RequirePackage[pdfmark]{hyperref}
+\fi
+
+% \renewcommand{\thefootnote}{\arabic{footnote}\hspace{-3pt}}
+
+
--- a/Journal/document/root.bib Mon Oct 15 13:23:52 2012 +0000
+++ b/Journal/document/root.bib Mon Dec 03 08:16:58 2012 +0000
@@ -1,4 +1,32 @@
+@InProceedings{CoquandSiles12,
+ author = {T.~Coquand and V.~Siles},
+ title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+ booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs},
+ pages = {119--134},
+ year = {2011},
+ volume = {7086},
+ series = {LNCS}
+}
+@InProceedings{Asperti12,
+ author = {A.~Asperti},
+ title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ pages = {283--298},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS}
+}
+
+@InProceedings{LammichTuerk12,
+ author = {P.~Lammich and T.~Tuerk},
+ title = {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS},
+ pages = {166--182}
+}
@PhdThesis{Braibant12,
author = {T.~Braibant},
@@ -120,11 +148,14 @@
-@Unpublished{KraussNipkow11,
+@article{KraussNipkow11,
author = {A.~Krauss and T.~Nipkow},
title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
- note = {To appear in the Journal of Automated Reasoning},
- year = {2012}
+ journal = {Journal of Automated Reasoning},
+ volume = 49,
+ number = {1},
+ year = {2012},
+ pages = {95--106}
}
@Book{Kozen97,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/List_Prefix.thy Mon Dec 03 08:16:58 2012 +0000
@@ -0,0 +1,382 @@
+(* Title: HOL/Library/List_Prefix.thy
+ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+*)
+
+header {* List prefixes and postfixes *}
+
+theory List_Prefix
+imports List Main
+begin
+
+subsection {* Prefix order on lists *}
+
+instantiation list :: (type) "{order, bot}"
+begin
+
+definition
+ prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
+
+definition
+ strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
+
+definition
+ "bot = []"
+
+instance proof
+qed (auto simp add: prefix_def strict_prefix_def bot_list_def)
+
+end
+
+lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
+ unfolding prefix_def by blast
+
+lemma prefixE [elim?]:
+ assumes "xs \<le> ys"
+ obtains zs where "ys = xs @ zs"
+ using assms unfolding prefix_def by blast
+
+lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
+ unfolding strict_prefix_def prefix_def by blast
+
+lemma strict_prefixE' [elim?]:
+ assumes "xs < ys"
+ obtains z zs where "ys = xs @ z # zs"
+proof -
+ from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
+ unfolding strict_prefix_def prefix_def by blast
+ with that show ?thesis by (auto simp add: neq_Nil_conv)
+qed
+
+lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
+ unfolding strict_prefix_def by blast
+
+lemma strict_prefixE [elim?]:
+ fixes xs ys :: "'a list"
+ assumes "xs < ys"
+ obtains "xs \<le> ys" and "xs \<noteq> ys"
+ using assms unfolding strict_prefix_def by blast
+
+
+subsection {* Basic properties of prefixes *}
+
+theorem Nil_prefix [iff]: "[] \<le> xs"
+ by (simp add: prefix_def)
+
+theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])"
+ by (induct xs) (simp_all add: prefix_def)
+
+lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)"
+proof
+ assume "xs \<le> ys @ [y]"
+ then obtain zs where zs: "ys @ [y] = xs @ zs" ..
+ show "xs = ys @ [y] \<or> xs \<le> ys"
+ by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
+next
+ assume "xs = ys @ [y] \<or> xs \<le> ys"
+ then show "xs \<le> ys @ [y]"
+ by (metis order_eq_iff order_trans prefixI)
+qed
+
+lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
+ by (auto simp add: prefix_def)
+
+lemma less_eq_list_code [code]:
+ "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+ by simp_all
+
+lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
+ by (induct xs) simp_all
+
+lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])"
+ by (metis append_Nil2 append_self_conv order_eq_iff prefixI)
+
+lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs"
+ by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI)
+
+lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
+ by (auto simp add: prefix_def)
+
+theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
+ by (cases xs) (auto simp add: prefix_def)
+
+theorem prefix_append:
+ "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))"
+ apply (induct zs rule: rev_induct)
+ apply force
+ apply (simp del: append_assoc add: append_assoc [symmetric])
+ apply (metis append_eq_appendI)
+ done
+
+lemma append_one_prefix:
+ "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys"
+ unfolding prefix_def
+ by (metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj
+ eq_Nil_appendI nth_drop')
+
+theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
+ by (auto simp add: prefix_def)
+
+lemma prefix_same_cases:
+ "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
+ unfolding prefix_def by (metis append_eq_append_conv2)
+
+lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
+ by (auto simp add: prefix_def)
+
+lemma take_is_prefix: "take n xs \<le> xs"
+ unfolding prefix_def by (metis append_take_drop_id)
+
+lemma map_prefixI: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
+ by (auto simp: prefix_def)
+
+lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
+ by (auto simp: strict_prefix_def prefix_def)
+
+lemma strict_prefix_simps [simp, code]:
+ "xs < [] \<longleftrightarrow> False"
+ "[] < x # xs \<longleftrightarrow> True"
+ "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
+ by (simp_all add: strict_prefix_def cong: conj_cong)
+
+lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
+ apply (induct n arbitrary: xs ys)
+ apply (case_tac ys, simp_all)[1]
+ apply (metis order_less_trans strict_prefixI take_is_prefix)
+ done
+
+lemma not_prefix_cases:
+ assumes pfx: "\<not> ps \<le> ls"
+ obtains
+ (c1) "ps \<noteq> []" and "ls = []"
+ | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"
+ | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
+proof (cases ps)
+ case Nil then show ?thesis using pfx by simp
+next
+ case (Cons a as)
+ note c = `ps = a#as`
+ show ?thesis
+ proof (cases ls)
+ case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
+ next
+ case (Cons x xs)
+ show ?thesis
+ proof (cases "x = a")
+ case True
+ have "\<not> as \<le> xs" using pfx c Cons True by simp
+ with c Cons True show ?thesis by (rule c2)
+ next
+ case False
+ with c Cons show ?thesis by (rule c3)
+ qed
+ qed
+qed
+
+lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
+ assumes np: "\<not> ps \<le> ls"
+ and base: "\<And>x xs. P (x#xs) []"
+ and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
+ and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
+ shows "P ps ls" using np
+proof (induct ls arbitrary: ps)
+ case Nil then show ?case
+ by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
+next
+ case (Cons y ys)
+ then have npfx: "\<not> ps \<le> (y # ys)" by simp
+ then obtain x xs where pv: "ps = x # xs"
+ by (rule not_prefix_cases) auto
+ show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)
+qed
+
+
+subsection {* Parallel lists *}
+
+definition
+ parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where
+ "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
+
+lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
+ unfolding parallel_def by blast
+
+lemma parallelE [elim]:
+ assumes "xs \<parallel> ys"
+ obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
+ using assms unfolding parallel_def by blast
+
+theorem prefix_cases:
+ obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
+ unfolding parallel_def strict_prefix_def by blast
+
+theorem parallel_decomp:
+ "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
+proof (induct xs rule: rev_induct)
+ case Nil
+ then have False by auto
+ then show ?case ..
+next
+ case (snoc x xs)
+ show ?case
+ proof (rule prefix_cases)
+ assume le: "xs \<le> ys"
+ then obtain ys' where ys: "ys = xs @ ys'" ..
+ show ?thesis
+ proof (cases ys')
+ assume "ys' = []"
+ then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
+ next
+ fix c cs assume ys': "ys' = c # cs"
+ then show ?thesis
+ by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI
+ same_prefix_prefix snoc.prems ys)
+ qed
+ next
+ assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
+ with snoc have False by blast
+ then show ?thesis ..
+ next
+ assume "xs \<parallel> ys"
+ with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
+ and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
+ by blast
+ from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
+ with neq ys show ?thesis by blast
+ qed
+qed
+
+lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
+ apply (rule parallelI)
+ apply (erule parallelE, erule conjE,
+ induct rule: not_prefix_induct, simp+)+
+ done
+
+lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
+ by (simp add: parallel_append)
+
+lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
+ unfolding parallel_def by auto
+
+
+subsection {* Postfix order on lists *}
+
+definition
+ postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where
+ "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
+
+lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"
+ unfolding postfix_def by blast
+
+lemma postfixE [elim?]:
+ assumes "xs >>= ys"
+ obtains zs where "xs = zs @ ys"
+ using assms unfolding postfix_def by blast
+
+lemma postfix_refl [iff]: "xs >>= xs"
+ by (auto simp add: postfix_def)
+lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"
+ by (auto simp add: postfix_def)
+lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys"
+ by (auto simp add: postfix_def)
+
+lemma Nil_postfix [iff]: "xs >>= []"
+ by (simp add: postfix_def)
+lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"
+ by (auto simp add: postfix_def)
+
+lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"
+ by (auto simp add: postfix_def)
+lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"
+ by (auto simp add: postfix_def)
+
+lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
+ by (auto simp add: postfix_def)
+lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"
+ by (auto simp add: postfix_def)
+
+lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs"
+proof -
+ assume "xs >>= ys"
+ then obtain zs where "xs = zs @ ys" ..
+ then show ?thesis by (induct zs) auto
+qed
+
+lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys"
+proof -
+ assume "x#xs >>= y#ys"
+ then obtain zs where "x#xs = zs @ y#ys" ..
+ then show ?thesis
+ by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
+qed
+
+lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
+proof
+ assume "xs >>= ys"
+ then obtain zs where "xs = zs @ ys" ..
+ then have "rev xs = rev ys @ rev zs" by simp
+ then show "rev ys <= rev xs" ..
+next
+ assume "rev ys <= rev xs"
+ then obtain zs where "rev xs = rev ys @ zs" ..
+ then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp
+ then have "xs = rev zs @ ys" by simp
+ then show "xs >>= ys" ..
+qed
+
+lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys"
+ by (clarsimp elim!: postfixE)
+
+lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys"
+ by (auto elim!: postfixE intro: postfixI)
+
+lemma postfix_drop: "as >>= drop n as"
+ unfolding postfix_def
+ apply (rule exI [where x = "take n as"])
+ apply simp
+ done
+
+lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
+ by (clarsimp elim!: postfixE)
+
+lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
+ by blast
+
+lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"
+ by blast
+
+lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
+ unfolding parallel_def by simp
+
+lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
+ unfolding parallel_def by simp
+
+lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
+ by auto
+
+lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
+ by (metis Cons_prefix_Cons parallelE parallelI)
+
+lemma not_equal_is_parallel:
+ assumes neq: "xs \<noteq> ys"
+ and len: "length xs = length ys"
+ shows "xs \<parallel> ys"
+ using len neq
+proof (induct rule: list_induct2)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a as b bs)
+ have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
+ show ?case
+ proof (cases "a = b")
+ case True
+ then have "as \<noteq> bs" using Cons by simp
+ then show ?thesis by (rule Cons_parallelI2 [OF True ih])
+ next
+ case False
+ then show ?thesis by (rule Cons_parallelI1)
+ qed
+qed
+
+end
--- a/Myhill_1.thy Mon Oct 15 13:23:52 2012 +0000
+++ b/Myhill_1.thy Mon Dec 03 08:16:58 2012 +0000
@@ -1,3 +1,4 @@
+(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
theory Myhill_1
imports "Folds"
"~~/src/HOL/Library/While_Combinator"
@@ -201,29 +202,12 @@
lemma finite_Trn:
assumes fin: "finite rhs"
shows "finite {r. Trn Y r \<in> rhs}"
-proof -
- have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
- by (rule rev_finite_subset[OF fin]) (auto)
- then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})"
- by (simp add: image_Collect)
- then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}"
- by (erule_tac finite_imageD) (simp add: inj_on_def)
- then show "finite {r. Trn Y r \<in> rhs}"
- by (erule_tac f="snd" in finite_surj) (auto simp add: image_def)
-qed
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
lemma finite_Lam:
assumes fin: "finite rhs"
shows "finite {r. Lam r \<in> rhs}"
-proof -
- have "finite {Lam r | r. Lam r \<in> rhs}"
- by (rule rev_finite_subset[OF fin]) (auto)
- then show "finite {r. Lam r \<in> rhs}"
- apply(simp add: image_Collect[symmetric])
- apply(erule finite_imageD)
- apply(auto simp add: inj_on_def)
- done
-qed
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
lemma trm_soundness:
assumes finite:"finite rhs"
@@ -286,21 +270,21 @@
assume in_X: "x \<in> X"
{ assume empty: "x = []"
then have "x \<in> lang_rhs rhs" using X_in_eqs in_X
- unfolding Init_def Init_rhs_def
+ unfolding Init_def Init_rhs_def
by auto
}
moreover
{ assume not_empty: "x \<noteq> []"
then obtain s c where decom: "x = s @ [c]"
- using rev_cases by blast
+ using rev_cases by blast
have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
then obtain Y where "Y \<in> UNIV // \<approx>A" "Y \<cdot> {[c]} \<subseteq> X" "s \<in> Y"
using decom in_X every_eqclass_has_transition by metis
then have "x \<in> lang_rhs {Trn Y (Atom c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
unfolding transition_def
- using decom by (force simp add: conc_def)
+ using decom by (force simp add: conc_def)
then have "x \<in> lang_rhs rhs" using X_in_eqs in_X
- unfolding Init_def Init_rhs_def by simp
+ unfolding Init_def Init_rhs_def by simp
}
ultimately show "x \<in> lang_rhs rhs" by blast
qed
@@ -315,18 +299,7 @@
fixes CS::"(('a::finite) lang) set"
assumes finite: "finite CS"
shows "finite (Init_rhs CS X)"
-proof-
- def S \<equiv> "{(Y, c)| Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}"
- def h \<equiv> "\<lambda> (Y, c::'a). Trn Y (Atom c)"
- have "finite (CS \<times> (UNIV::('a::finite) set))" using finite by auto
- then have "finite S" using S_def
- by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto)
- moreover have "{Trn Y (Atom c) |Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X} = h ` S"
- unfolding S_def h_def image_def by auto
- ultimately
- have "finite {Trn Y (Atom c) |Y c. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}" by auto
- then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp
-qed
+using assms unfolding Init_rhs_def transition_def by simp
lemma Init_ES_satisfies_invariant:
@@ -444,15 +417,7 @@
lemma Subst_all_preserves_finite:
assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
-proof -
- def eqns \<equiv> "{(X::'a lang, rhs) |X rhs. (X, rhs) \<in> ES}"
- def h \<equiv> "\<lambda>(X::'a lang, rhs). (X, Subst rhs Y yrhs)"
- have "finite (h ` eqns)" using finite h_def eqns_def by auto
- moreover
- have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
- ultimately
- show "finite (Subst_all ES Y yrhs)" by simp
-qed
+using assms unfolding Subst_all_def by simp
lemma Subst_all_preserves_finite_rhs:
"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
--- a/Myhill_2.thy Mon Oct 15 13:23:52 2012 +0000
+++ b/Myhill_2.thy Mon Dec 03 08:16:58 2012 +0000
@@ -1,6 +1,6 @@
(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
theory Myhill_2
- imports Myhill_1 "~~/src/HOL/Library/List_Prefix"
+ imports Myhill_1 List_Prefix
begin
section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *}
--- a/Regular_Set.thy Mon Oct 15 13:23:52 2012 +0000
+++ b/Regular_Set.thy Mon Dec 03 08:16:58 2012 +0000
@@ -11,6 +11,9 @@
definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
+text {* checks the code preprocessor for set comprehensions *}
+export_code conc checking SML
+
overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
begin
primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
@@ -18,6 +21,18 @@
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
end
+text {* for code generation *}
+
+definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
+ lang_pow_code_def [code_abbrev]: "lang_pow = compow"
+
+lemma [code]:
+ "lang_pow (Suc n) A = A @@ (lang_pow n A)"
+ "lang_pow 0 A = {[]}"
+ by (simp_all add: lang_pow_code_def)
+
+hide_const (open) lang_pow
+
definition star :: "'a lang \<Rightarrow> 'a lang" where
"star A = (\<Union>n. A ^^ n)"
@@ -54,6 +69,9 @@
and "UNION I M @@ A = UNION I (%i. M i @@ A)"
by auto
+lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
+by(fastforce simp: conc_def in_lists_conv_set)
+
subsection{* @{term "A ^^ n"} *}
@@ -72,15 +90,21 @@
lemma length_lang_pow_ub:
"ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
-by(induct n arbitrary: w) (fastsimp simp: conc_def)+
+by(induct n arbitrary: w) (fastforce simp: conc_def)+
lemma length_lang_pow_lb:
"ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
-by(induct n arbitrary: w) (fastsimp simp: conc_def)+
+by(induct n arbitrary: w) (fastforce simp: conc_def)+
+
+lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
+by(induction n)(auto simp: conc_subset_lists[OF assms])
subsection{* @{const star} *}
+lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
+unfolding star_def by(blast dest: lang_pow_subset_lists)
+
lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"
by (auto simp: star_def)
@@ -161,7 +185,7 @@
qed
lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"
-by (fastsimp simp: in_star_iff_concat)
+by (fastforce simp: in_star_iff_concat)
lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
proof-
@@ -180,6 +204,68 @@
shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
using a by (induct rule: star_induct) (blast)+
+
+subsection {* Left-Quotients of languages *}
+
+definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Deriv x A = { xs. x#xs \<in> A }"
+
+definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Derivs xs A = { ys. xs @ ys \<in> A }"
+
+abbreviation
+ Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
+where
+ "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
+
+
+lemma Deriv_empty[simp]: "Deriv a {} = {}"
+ and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
+ and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})"
+ and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
+ and Deriv_inter[simp]: "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B"
+ and Deriv_compl[simp]: "Deriv a (-A) = - Deriv a A"
+ and Deriv_Union[simp]: "Deriv a (Union M) = Union(Deriv a ` M)"
+ and Deriv_UN[simp]: "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
+by (auto simp: Deriv_def)
+
+lemma Der_conc [simp]: "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
+unfolding Deriv_def conc_def
+by (auto simp add: Cons_eq_append_conv)
+
+lemma Deriv_star [simp]: "Deriv c (star A) = (Deriv c A) @@ star A"
+proof -
+ have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
+ unfolding Deriv_def conc_def
+ apply(auto simp add: Cons_eq_append_conv)
+ apply(drule star_decom)
+ apply(auto simp add: Cons_eq_append_conv)
+ done
+
+ have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
+ by (simp only: star_unfold_left[symmetric])
+ also have "... = Deriv c (A @@ star A)"
+ by (simp only: Deriv_union) (simp)
+ also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
+ by simp
+ also have "... = (Deriv c A) @@ star A"
+ using incl by auto
+ finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
+qed
+
+lemma Deriv_diff[simp]: "Deriv c (A - B) = Deriv c A - Deriv c B"
+by(auto simp add: Deriv_def)
+
+lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S"
+by(auto simp add: Deriv_def)
+
+lemma Derivs_simps [simp]:
+ shows "Derivs [] A = A"
+ and "Derivs (c # s) A = Derivs s (Deriv c A)"
+ and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
+unfolding Derivs_def Deriv_def by auto
+
+
subsection {* Arden's Lemma *}
lemma arden_helper:
@@ -290,5 +376,4 @@
using eq by blast
qed
-
end