(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 5.2' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 77641, 2400]*) (*NotebookOutlinePosition[ 160015, 5203]*) (* CellTagsIndexPosition[ 159932, 5197]*) (*WindowFrame->Normal*) Notebook[{ Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["\<\ Practical Reflection for Formal Mathematics\ \>", "Title"], Cell["Martin Giese", "Subtitle"], Cell["\<\ RICAM, Austrian Acad. of Sciences, Linz Theorema Group\ \>", "Subsubtitle"], Cell[BoxData[""], "Input"], Cell[CellGroupData[{ Cell["Workshop on Formal Groebner Bases Theory, Linz, 2006", "Subsubtitle"], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Mathematical Theory Exploration", "Section"], Cell["Mathematical Theory Exploration consists of:", "Text", CellDingbat->"\[FilledSquare]"], Cell["invention of concepts", "Outline1", CellDingbat->"\[FilledSquare]"], Cell["invention of propositions about concepts", "Outline1", CellDingbat->"\[FilledSquare]"], Cell[CellGroupData[{ Cell["proving these propositions", "Outline1", CellDingbat->"\[FilledSquare]"], Cell["But also:", "Text", CellDingbat->None] }, Open ]], Cell["invention of problems formulated in terms of concepts", "Outline1", CellDingbat->"\[FilledSquare]"], Cell["invention of algorithms to solve these problems", "Outline1", CellDingbat->"\[FilledSquare]"], Cell[CellGroupData[{ Cell["verifying these algorithms", "Outline1", CellDingbat->"\[FilledSquare]"], Cell["And even:", "Text", CellDingbat->None] }, Open ]], Cell["invention of new techniques to reason about concepts", "Outline1", CellDingbat->"\[FilledSquare]"], Cell["verification of the new techniques", "Outline1", CellDingbat->"\[FilledSquare]"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Idea", "Section"], Cell["Found a new reasoning technique?", "Text"], Cell["Normally:", "Text"], Cell[TextData[{ "Implement/extend a theorem prover in C, Java, ", StyleBox["Mathematica\[Ellipsis]", FontSlant->"Italic"] }], "Outline1"], Cell[CellGroupData[{ Cell["Skip verification because no useful verifier is available", "Outline1"], Cell["\<\ Idea: \ \>", "Text"] }, Open ]], Cell["Allow formulation of new reasoners in Theorema language", "Outline1"], Cell["Support verification of reasoners using Theorema", "Outline1"], Cell["\<\ Make it possible to use new reasoners like the \"built-in\" ones.\ \ \>", "Outline1"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Credits", "Section"], Cell[CellGroupData[{ Cell["\<\ This line of work has been initiated by Bruno Buchberger, based on the ideas presented in:\ \>", "Outline1", TextAlignment->Left], Cell["\<\ Proving by First and Intermediate Principles Invited talk at TYPES Workshop, Nov 1-2, 2004 University of Nijmegen,The Netherlands\ \>", "Text", CellMargins->{{109.5, Inherited}, {Inherited, Inherited}}, TextAlignment->AlignmentMarker] }, Open ]], Cell["It is joint work with Temur Kutsia", "Outline1"], Cell[CellGroupData[{ Cell["Many ideas have been contributed in discussions by", "Outline1"], Cell["Markus Rosenkranz", "Outline2"], Cell["Tudor Jebelean", "Outline2"], Cell["\[Ellipsis]", "Outline2"] }, Open ]] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Workflow", "Section"], Cell["\"ordinary\" reasoning:", "Text"], Cell["Axiomatize natrual numbers, ", "Outline1"], Cell["Define addition", "Outline1"], Cell[CellGroupData[{ Cell[TextData[{ "Prove things about addition: ", StyleBox["x+0=x, x+y=y+x, \[Ellipsis]", "Input"] }], "Outline1"], Cell["\"meta\" reasoning:", "Text"] }, Open ]], Cell["Discover a smarter way of proving things about addition", "Outline1", CellMargins->{{132.5, Inherited}, {Inherited, Inherited}}, TextAlignment->AlignmentMarker], Cell["Formalize the new reasoning technique", "Outline1", CellMargins->{{132.5, Inherited}, {Inherited, Inherited}}, TextAlignment->AlignmentMarker], Cell["Verify it", "Outline1", CellMargins->{{132.5, Inherited}, {Inherited, Inherited}}, TextAlignment->AlignmentMarker], Cell[CellGroupData[{ Cell["Add it to the System's collection of reasoners", "Outline1", CellMargins->{{132.5, Inherited}, {Inherited, Inherited}}, TextAlignment->AlignmentMarker], Cell["\"ordinary\" reasoning:", "Text"] }, Open ]], Cell["Prove more things, using the new reasoning technique", "Outline1"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Reflection", "Section"], Cell["\<\ Formulation of Reasoners means writing programs that manipulate \ terms and formulae\ \>", "Text"], Cell["\<\ Therefore, the logic for the \"meta\" reasoning must contain \ representations of the syntactic entities of the logic used for the \ \"ordinary\" reasoning.\ \>", "Text"], Cell["\<\ We want to use the same logic for \"meta\" and \"ordinary\" \ reasoning, so our logic will contain representations of its own syntax.\ \>", \ "Text"], Cell["\<\ The term \"Reflection\" refers to a language that contains a \ representation of its own syntax.\ \>", "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Term Representation: Symbols", "Section"], Cell["Many term representations are possible. ", "Text"], Cell["\<\ We decided to have a 'quoted' symbol in the logic as representation \ for every symbol.\ \>", "Text"], Cell["\<\ In this talk, we represent quoted symbols for the term \ representation. So\ \>", "Text"], Cell[BoxData[GridBox[{ { StyleBox[\(the\ symbol ... \), "Text"], StyleBox[\(represents\ the\ symbol ... \), "Text"]}, {\(\(\ \)\(a\+_\)\(\ \)\), "a"}, {\(\(\ \)\(0\+_\)\(\ \)\), "0"}, {\(\(\ \)\(\(a\+_\)\+_\)\(\ \)\), \(\(\ \)\(a\+_\)\(\ \)\)}, {"\[Ellipsis]", "\[Ellipsis]"} }, GridFrame->True, RowLines->True, ColumnLines->True]], "Input", TextAlignment->Center], Cell["Alternatives:", "Text"], Cell["Enumerate symbols:", "Text"], Cell[BoxData[GridBox[{ { RowBox[{\(sym[zero]\), StyleBox[" ", "Text"], StyleBox["represents", "Text"], StyleBox[" ", "Text"], StyleBox["the", "Text"], StyleBox[" ", "Text"], StyleBox["symbol", "Text"], StyleBox[" ", "Input"], StyleBox["a", "Input"]}]}, { RowBox[{\(sym[succ[0]]\), StyleBox[" ", "Text"], StyleBox["represents", "Text"], StyleBox[" ", "Text"], StyleBox["the", "Text"], StyleBox[" ", "Text"], StyleBox["symbol", "Text"], StyleBox[" ", "Input"], StyleBox["b", "Input"]}]} }]], "Input"], Cell["Or use character codes:", "Text"], Cell[BoxData[GridBox[{ { RowBox[{\(sym[\[LeftAngleBracket]97\[RightAngleBracket]]\), StyleBox[" ", "Text"], StyleBox["represents", "Text"], StyleBox[" ", "Text"], StyleBox["the", "Text"], StyleBox[" ", "Text"], StyleBox["symbol", "Text"], StyleBox[" ", "Input"], "a"}]}, { RowBox[{\(sym[\[LeftAngleBracket]97, 98, 99\[RightAngleBracket]]\), StyleBox[" ", "Text"], StyleBox["represents", "Text"], StyleBox[" ", "Text"], StyleBox["the", "Text"], StyleBox[" ", "Text"], StyleBox["symbol", "Text"], StyleBox[" ", "Input"], "abc"}]} }]], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Term Representation: Variables", "Section"], Cell["\<\ Assume that variables are different from other (constant) \ symbols.\ \>", "Text"], Cell["Also represent variables by underined symbols:", "Text"], Cell[BoxData[GridBox[{ { StyleBox[\(the\ symbol ... \), "Text"], StyleBox[\(represents\ the\ variable ... \), "Text"]}, {\(\(\ \)\(x\+_\)\(\ \)\), "x"}, {\(\(\ \)\(y\+_\)\(\ \)\), "y"}, {"\[Ellipsis]", "\[Ellipsis]"} }, GridFrame->True, RowLines->True, ColumnLines->True]], "Input", TextAlignment->Center], Cell["\<\ Note that a quoted variable is a constant symbol and not a \ variable.\ \>", "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Term Representation: Compound Terms", "Section"], Cell[TextData[{ "We also decided to reuse ", StyleBox["\[Ellipsis][\[Ellipsis]]", "Input"], " for construction of compound terms." }], "Text"], Cell[BoxData[GridBox[{ { StyleBox[\(the\ term ... \), "Text"], StyleBox[\(represents\ the\ term ... \), "Text"]}, {\(\(\ \)\(a\+_\)\(\ \)\), "a"}, {\(f\+_[b\+_]\), \(f[b]\)}, {GridBox[{ {\(f\+_[t]\)}, { RowBox[{ StyleBox["where", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["t", "Input", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["represents", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["a", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["term", "Text", FontSize->12]}]} }], GridBox[{ {\(f[s]\)}, { RowBox[{ StyleBox["where", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["s", "Input", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["is", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["the", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["term", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["represented", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["by", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["t", "Input", FontSize->12]}]} }]}, { RowBox[{" ", GridBox[{ {\(t[a\+_]\)}, { RowBox[{ StyleBox["where", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["t", "Input", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["represents", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["a", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["term", "Text", FontSize->12]}]} }]}], GridBox[{ {\(s[a]\)}, { RowBox[{ StyleBox["where", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["s", "Input", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["is", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["the", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["term", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["represented", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["by", "Text", FontSize->12], StyleBox[" ", "Text", FontSize->12], StyleBox["t", "Input", FontSize->12]}]} }]}, {\(\((f\+_\( + \+_\)g\+_)\)[x\+_]\), \(\((f + g)\)[x]\)} }, GridFrame->True, RowLines->True, ColumnLines->True]], "Input", TextAlignment->Center], Cell[TextData[{ "If ", StyleBox["f", "Input"], " and ", StyleBox["t", "Input"], " are term representations, ", StyleBox["f[t]", "Input"], " is a compound term.\nOtherwise, ", StyleBox["f[t]", "Input"], " is the result of a function application." }], "Text"], Cell["Alternatives:", "Text"], Cell[BoxData[ \(f\+_\([\+_\)b\+_\(]\+_\)\)], "Input"], Cell[BoxData[ \(MkTerm[f\+_, b\+_]\)], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["An Example Exploration: Arithmetic of Natural Numbers", "Section"], Cell[BoxData[ RowBox[{"Axioms", "[", RowBox[{ "\"\\"", ",", \(any[n]\), ",", "\[IndentingNewLine]", GridBox[{ {\(0 \[Element] \[DoubleStruckCapitalN]\)}, {\(n \[Element] \[DoubleStruckCapitalN] \[Implies] \(n\^+\) \ \[Element] \[DoubleStruckCapitalN]\)} }]}], "]"}]], "Input"], Cell[BoxData[ RowBox[{"Axioms", "[", RowBox[{ "\"\\"", ",", \(any[m \[Element] \[DoubleStruckCapitalN], n \[Element] \[DoubleStruckCapitalN]]\), ",", "\[IndentingNewLine]", GridBox[{ {\(m + 0 := m\)}, {\(m + \(n\^+\) := \(\((m + n)\)\^+\)\)} }]}], "]"}]], "Input"], Cell[BoxData[ \(Proposition["\<0 left unit\>", any[n \[Element] \[DoubleStruckCapitalN]], \[IndentingNewLine]0 + n = n]\)], "Input"], Cell[BoxData[ \(Prove[Proposition["\<0 left unit\>"], using \[Rule] \[Ellipsis], by \[Rule] \[Ellipsis]]\)], "Input"], Cell["and eventually...", "Text"], Cell[BoxData[ \(Proposition["\<+ associative\>", any[l \[Element] \[DoubleStruckCapitalN], m \[Element] \[DoubleStruckCapitalN], n \[Element] \[DoubleStruckCapitalN]], \[IndentingNewLine]\((l + m)\) + n = l + \((m + n)\)]\)], "Input"], Cell[BoxData[ \(Prove[Proposition["\<+ associative\>"], using \[Rule] \[Ellipsis], by \[Rule] \[Ellipsis]]\)], "Input"], Cell[BoxData[""], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Exploration continues: Multiplication", "Section"], Cell["Define multiplication of natural numbers:", "Text"], Cell[BoxData[ RowBox[{"Axioms", "[", RowBox[{ "\"\\"", ",", \(any[m \[Element] \[DoubleStruckCapitalN], n \[Element] \[DoubleStruckCapitalN]]\), ",", "\[IndentingNewLine]", GridBox[{ {\(m\[CenterDot]0 := 0\)}, {\(m\[CenterDot]\(n\^+\) := m + \((m\[CenterDot]n)\)\)} }]}], "]"}]], "Input"], Cell["\<\ Now go on to show things about multiplication, using knowledge \ about addition:\ \>", "Text"], Cell[BoxData[ \(Proposition["\<\[CenterDot] associative\>", any[l \[Element] \[DoubleStruckCapitalN], m \[Element] \[DoubleStruckCapitalN], n \[Element] \[DoubleStruckCapitalN]], \[IndentingNewLine]\((l\ \[CenterDot]m)\)\[CenterDot]n = l\[CenterDot]\((m\[CenterDot]n)\)]\)], "Input"], Cell[BoxData[ \(Prove[Proposition["\<\[CenterDot] associative\>"], using \[Rule] {\[Ellipsis]Proposition["\<+ associative\>"] \ \[Ellipsis]}, by \[Rule] \[Ellipsis]]\)], "Input"], Cell[TextData[{ "Probably the knowledge about ", StyleBox["+", "Input"], ", like associativity is used quite heavily." }], "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["An Idea for a Reasoner", "Section"], Cell["\<\ After doing some proofs involving addition, you might find out that it's always possible, and often a good idea to write sums in \ right-associative form: For instance, to take\ \>", "Text"], Cell[BoxData[ \(\((\((a + b)\) + \((c + d)\))\) + e\)], "Input"], Cell["and rewrite it to ", "Text"], Cell[BoxData[ \(a + \((b + \((c + \((d + e)\))\))\)\)], "Input"], Cell["\<\ You now would like to write a reasoner that can do this for \ you.\ \>", "Text"], Cell["\<\ Reasoner just takes a term and simplifies it, so we call it a \ simplifier.\ \>", "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["An implementation", "Section"], Cell["\<\ Here is a formulation of the algorithm in the Theorema language \ with quoting:\ \>", "Text"], Cell[BoxData[ RowBox[{"Algorithm", "[", RowBox[{ "\"\\"", ",", \(any[t, t1, t2, l, acc]\), ",", "\[IndentingNewLine]", GridBox[{ {\(\(simplify[t] := sumList[collect[t, {}]]\)\(\[IndentingNewLine]\) \)}, {\(collect[t1\( + \+_\)t2, acc] := collect[t1, collect[t2, acc]]\)}, {\(\(collect[t, acc] := t\[Cup]acc\)\(\[IndentingNewLine]\) \)}, {\(sumList[{}] := 0\+_\)}, {\(sumList[{t}] := t\)}, {\(sumList[t\[Cup]l] := t\( + \+_\)sumList[l]\)} }]}], "]"}]], "Input", GridBoxOptions->{ColumnAlignments->{":="}}] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Formulating Soundness", "Section"], Cell["When is such a simplifier sound?", "Text"], Cell["First: it sends terms to terms:", "Text"], Cell[BoxData[ \(Proposition["\", any[t], \[IndentingNewLine]t \[Element] \[DoubleStruckCapitalT] \ \[Implies] simplify[t\ ] \[Element] \[DoubleStruckCapitalT]]\)], "Input"], Cell["Second: the result still means the same.", "Text"], Cell["Two possibilities:", "Text"], Cell[CellGroupData[{ Cell[TextData[{ "Reflection of Syntax:\nwhat is provable with ", StyleBox["simplify", "Input"], " is provable without" }], "Outline1"], Cell[BoxData[ \(\(\(\[RightTee]\)\(\[ForAll] \+\(t \[Element] \ \[DoubleStruckCapitalT]\)rewritable[t, simplify[t], KB]\)\)\)], "Input"] }, Open ]], Cell[CellGroupData[{ Cell[TextData[{ "Reflection of Semantics:\nwhat is provable with ", StyleBox["simplify", "Input"], " is true" }], "Outline1"], Cell[BoxData[ RowBox[{ RowBox[{"KB", "\[RightTee]", RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ {\(t \[Element] \[DoubleStruckCapitalT]\)}, {\(\[Beta] \[Element] \[DoubleStruckCapitalA]\)} }]], \(eval[t, \[Beta]]\)}]}], "=", \(eval[simplify[t], \[Beta]]\)}]], "Input"] }, Open ]] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Reflection of Syntax/Semantics", "Section"], Cell["Problems with Reflection of Syntax:", "Text"], Cell["\<\ Need to axiomatize whole calculus, rewriting\[Ellipsis]\ \>", \ "Outline1"], Cell["Also axiomatize knowledge base", "Outline1"], Cell["Axiomatization must be good for your prover", "Outline1"], Cell[CellGroupData[{ Cell["Reasoning power on \"ordinary\" level hard to lift", "Outline1"], Cell["Reflection of Semantics avoids this, but:", "Text"] }, Open ]], Cell["Some care necessary in axiomatizing evaluation", "Outline1"], Cell["Only for a logic with model semantics", "Outline1"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Axioms for symbols and terms", "Section"], Cell[TextData[{ "Axiom Schemata for symbols. Let's use ", StyleBox["\[DoubleStruckCapitalS]", "Input"], " for the set of (quoted) symbols in the T'ma language, ", StyleBox["\[DoubleStruckCapitalV]", "Input"], " for the variable symbols and ", StyleBox["\[DoubleStruckCapitalT]", "Input"], " for the terms." }], "Text"], Cell[BoxData[ StyleBox[GridBox[{ { RowBox[{"\[RightTee]", RowBox[{\(a\+_\), "\[Element]", RowBox[{"\[DoubleStruckCapitalS]", " ", StyleBox["for", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["all", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["symbols", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["a", "Input", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}]}]}]}]}, { RowBox[{ RowBox[{"\[RightTee]", RowBox[{\(x\+_\), "\[Element]", RowBox[{"\[DoubleStruckCapitalV]", " ", StyleBox["for", "Text"], StyleBox[" ", "Text"], StyleBox["all", "Text"], StyleBox[" ", "Text"], StyleBox["variables", "Text"], " ", "x"}]}]}], "\[IndentingNewLine]", \(\(\(\[RightTee]\)\(\ \[DoubleStruckCapitalS] \[Intersection] \[DoubleStruckCapitalV]\)\) = \ \[EmptySet]\)}]}, { RowBox[{"\[RightTee]", RowBox[{"0", "\[NotElement]", RowBox[{"\[DoubleStruckCapitalS]", "\[Union]", RowBox[{"\[DoubleStruckCapitalV]", " ", StyleBox[\(\(etc\)\(.\)\), "Text"]}]}]}]}]}, {\(\(\[RightTee]\)\(t \[Element] \[DoubleStruckCapitalT] \[And] a \[Element] \[DoubleStruckCapitalT] \[Implies] t[a] \[NotElement] \[DoubleStruckCapitalS] \[Union] \ \[DoubleStruckCapitalV]\)\)}, {\(\(\[RightTee]\)\(\[DoubleStruckCapitalS] \[Union] \ \[DoubleStruckCapitalV] \[SubsetEqual] \[DoubleStruckCapitalT]\)\)}, {\(\(\[RightTee]\)\(0 \[NotElement] \[DoubleStruckCapitalT]\)\)}, {\(\(\[RightTee]\)\(t \[Element] \[DoubleStruckCapitalT] \[And] a \[Element] \[DoubleStruckCapitalT] \[Implies] t[a] \[Element] \[DoubleStruckCapitalT]\)\)} }, ColumnAlignments->{Left}], FontSize->16]], "Input"], Cell["To prove inequalities between terms:", "Text"], Cell[BoxData[ StyleBox[GridBox[{ { RowBox[{"\[RightTee]", RowBox[{\(a\+_\), "\[NotEqual]", RowBox[{\(b\+_\), " ", StyleBox["for", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["all", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[\(symbols/variables\), "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox[" ", "Text", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["a", "Input", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}]}], StyleBox["\[NotEqual]", "Input", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}], StyleBox["b", "Input", GridBoxOptions->{ColumnSpacings->0.8, ColumnAlignments->{Left}}]}]}]}, {\(\(\[RightTee]\)\(t \[Element] \[DoubleStruckCapitalT] \[And] a \[Element] \[DoubleStruckCapitalT] \[And] s \[Element] \[DoubleStruckCapitalS] \[Union] \ \[DoubleStruckCapitalV] \[Implies] t[a] \[NotEqual] s\)\)}, {\(\(\(\[RightTee]\)\(t\_1 \[Element] \[DoubleStruckCapitalT] \ \[And] a\_1 \[Element] \[DoubleStruckCapitalT] \[And] t\_2 \[Element] \[DoubleStruckCapitalT] \[And] a\_2 \[Element] \[DoubleStruckCapitalT] \[And] t\_1[a\_1]\)\) = \(t\_2[a\_2] \[Implies] t\_1 = \(t\_2 \[And] a\_1 = a\_2\)\)\)} }, ColumnAlignments->{Left}], FontSize->16]], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Term Induction", "Section"], Cell["\<\ No fixed type system or signatures \[Implies] don't know arity of \ functions in advance.\ \>", "Text"], Cell["\<\ Higher order terms \[Implies] might not know head symbol of a term.\ \ \>", "Text"], Cell["Therefore terms are inductive in 2 \"dimensions\"", "Text"], Cell["Dimension 1: the nesting of terms", "Text"], Cell[BoxData[ \(a\+_, \ f\+_[a\+_], \ f\+_[f\+_[a\+_]], \ \[Ellipsis]\)], "Input"], Cell["Dimension 2: argument lists", "Text"], Cell[BoxData[ \(\(\(f\+_[], \ f\+_[a\+_], \ f\+_[a\+_, a\+_], \ f\+_[a\+_, a\+_, a\+_]\)\(\[IndentingNewLine]\) \)\)], "Input"], Cell[BoxData[GridBox[{ {\(\[ForAll] \+\(s \[Element] \[DoubleStruckCapitalS]\)P[s]\)}, {\(\[ForAll] \+\(v \[Element] \[DoubleStruckCapitalV]\)P[v]\)}, {\(\[ForAll] \+\(head \[Element] \[DoubleStruckCapitalT]\)P[ head] \[Implies] P[head[]]\)}, { UnderscriptBox[ RowBox[{ RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ {\(head \[Element] \[DoubleStruckCapitalT]\)}, {\(t \[Element] \[DoubleStruckCapitalT]\)}, {\(tail\&_ \[Element] \ \[DoubleStruckCapitalT]\[Dash]tuple\)} }]], \((P[t] \[And] P[head[tail\&_]])\)}], "\[Implies]", \(P[head[t, tail\&_]]\)}], "_"]}, {\(\[ForAll] \+\(t \[Element] \[DoubleStruckCapitalT]\)P[t]\)} }]], "Input"], Cell[BoxData[""], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Axioms for evaluation function", "Section"], Cell[TextData[{ StyleBox["eval", "Input"], " function mimics evaluation function of model semantics." }], "Text"], Cell["Axioms like:", "Text"], Cell[BoxData[ \(\(\(\[RightTee]\)\(v \[Element] \[DoubleStruckCapitalV] \[Implies] eval[v, \[Beta]]\)\) = \[Beta][v]\)], "Input"], Cell[BoxData[ RowBox[{\(\(\[RightTee]\)\(eval[a\+_, \[Beta]]\)\), "=", RowBox[{"a", " ", StyleBox["for", "Text"], StyleBox[" ", "Text"], StyleBox["all", "Text"], StyleBox[" ", "Text"], StyleBox["symbols", "Text"], StyleBox[" ", "Text"], StyleBox["a", "Input"]}]}]], "Input"], Cell[BoxData[ \(\(\(\[RightTee]\)\(t \[Element] \[DoubleStruckCapitalT] \[And] a \[Element] \[DoubleStruckCapitalT] \[Implies] \((eval[ t[a], \[Beta]] = \(eval[t, \[Beta]]\)[ eval[a, \[Beta]]])\)\)\)\)], "Input"], Cell["which implies", "Text"], Cell[BoxData[GridBox[{ {\(eval[ t\_1\( + \+_\)t\_2, \[Beta]] = \ \(eval[\(+\+_\(\(,\)\(\[Beta]\)\)\)]\)[eval[t\_1, \[Beta]], eval[t\_2, \[Beta]]]\)}, {\(\(=\)\(eval[t\_1, \[Beta]] + eval[t\_2, \[Beta]]\)\)} }, ColumnAlignments->{"="}]], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Eval Caveat", "Section"], Cell["Danger:", "Text"], Cell[BoxData[ \(\(\(\[RightTee]\)\(eval[eval\+_, \[Beta]]\)\) = eval\)], "Input"], Cell["so:", "Text"], Cell[BoxData[{ \(\(\(\[RightTee]\)\(t\_1 \[Element] \[DoubleStruckCapitalT] \[And] t\_2 \[Element] \[DoubleStruckCapitalT]\)\)\), "\[IndentingNewLine]", \ \(\t\(\(\[Implies]\)\(eval[eval\+_[t\_1, t\_2], \[Beta]]\)\) = eval[eval\+_[t\_1, \[Beta]], eval\+_[t\_2, \[Beta]]]\)}], "Input"], Cell["is no good as definition and leads to inconsistency", "Text"], Cell[TextData[{ "\[DoubleLongRightArrow] avoid defining ", Cell[BoxData[ \(eval[eval\+_]\)]], " at all for the time being." }], "Text"], Cell[TextData[{ "Later maybe have layers of eval: ", Cell[BoxData[ \(TraditionalForm\`eval\_1\ can\ evaluate\ \(eval\_0\)\+_\)]], ", ", Cell[BoxData[ \(TraditionalForm\`eval\_2\ can\ evaluate\ \(eval\_1\)\+_\)]], ",\[Ellipsis]" }], "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Proving Soundness", "Section"], Cell["Let's prove:", "Text"], Cell[BoxData[ \(\[ForAll] \+\(t \[Element] \[DoubleStruckCapitalT]\)eval[simplify[t]] = eval[t]\)], "Input"], Cell[TextData[{ "Strenghten induction: for all terms ", StyleBox["t", "Input"], " and list of terms ", StyleBox["acc", "Input"], ":" }], "Text"], Cell[BoxData[ \(eval[sumList[collect[t, acc]]] = eval[t\( + \+_\)sumList[acc]]\)], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["The Proof", "Section"], Cell[TextData[{ "Induction step: Statement holds for ", Cell[BoxData[ \(t\_1\)]], " and ", Cell[BoxData[ \(t\_2\)]], ", show it for ", Cell[BoxData[ \(t\_1\( + \+_\)t\_2\)]], "." }], "Text"], Cell[BoxData[{ \(eval[sumList[collect[t\_1\( + \+_\)t\_2, acc]]]\), "\n", \(\(\(=\)\(\ \)\(eval[ sumList[collect[t\_1, collect[t\_2, acc]]]]\)\)\), "\n", \(\(\( = \&\(I . H . \)\)\(\ \)\(eval[ t\_1\( + \+_\)sumList[collect[t\_2, acc]]]\)\)\), "\n", \(\(\(=\)\(\ \)\(eval[t\_1] + eval[sumList[collect[t\_2, acc]]]\)\)\), "\n", \(\(\( = \&\(I . H . \)\)\(\ \)\(eval[t\_1] + eval[t\_2\( + \+_\)sumList[acc]]\)\)\), "\n", \(\(\(=\)\(eval[ t\_1] + \((eval[t\_2] + eval[sumList[acc]])\)\)\)\), "\[IndentingNewLine]", \(\(\(=\)\(\((eval[t\_1] + eval[t\_2])\) + eval[sumList[acc]]\)\)\), "\[IndentingNewLine]", \(\(\(=\)\(eval[t\_1\( + \+_\)t\_2] + eval[sumList[acc]]\)\)\), "\[IndentingNewLine]", \(\(\(=\)\(eval[\((t\_1\( + \+_\)t\_2)\)\( + \+_\)sumList[ acc]]\)\)\)}], "Input"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Putting the simplifier to work:", "Section"], Cell["Now we can use the simplifier:", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ simplify[\((\((a\+_\( + \+_\)b\+_)\)\( + \+_\)\((c\+_\( + \+_\)d\+_)\))\ \)\( + \+_\)e\+_], using \[Rule] Algorithm["\"]]\)], "Input"], Cell[BoxData[ \(\(\(\ \)\(a\+_\( + \+_\)\((b\+_\( + \+_\)\((c\+_\( + \+_\)\((d\+_\( + \ \+_\)e\+_)\))\))\)\)\)\)], "Output"] }, Open ]], Cell["To use it like other reasoners, make it known to the system:", "Text"], Cell[BoxData[ \(DeclareSimplifier[ShiftParens, simplify, using \[Rule] Algorithm["\"]]\)], "Input"], Cell["Now use it like other simplifiers", "Text"], Cell[CellGroupData[{ Cell[BoxData[ RowBox[{"Compute", "[", RowBox[{ RowBox[{\((\((a + b)\) + \((c + d)\))\), "+", StyleBox["e", FontColor->GrayLevel[0]]}], StyleBox[",", FontColor->GrayLevel[0]], \(by \[Rule] ShiftParens\)}], StyleBox["]", FontColor->GrayLevel[0]]}]], "Input"], Cell[BoxData[ \(a + \((b + \((c + \((d + e)\))\))\)\)], "Output"] }, Open ]], Cell[TextData[{ "Note: no mention of ", StyleBox["using->Proposition[\"+ associative\"]", "Input"], "." }], "Text"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Related Work", "Section"], Cell["Most closely related:", "Text"], Cell["Meta-reasoning in NqThm and ACL2 (Boyer, Moore):", "Text"], Cell["\<\ Can extend ACL2 theorem prover with simplifiers, prove their soundness by Reflection of Semantics\ \>", "Text"], Cell["Novelties in Theorema:", "Text"], Cell["Use predicate logic with quoting instead of LISP", "Outline1"], Cell["New challenges from higher order logic and quantification", "Outline1"], Cell["Also full provers, not only simplifiers", "Outline1"], Cell["More emphasis on practicality", "Outline1"], Cell["Also thinking of proving other properties of reasoners", "Outline1"] }, Open ]], Cell[TextData[Cell[BoxData[GridBox[{ { ButtonBox[ StyleBox["\[FirstPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageFirst"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"First Slide"], ButtonBox[ StyleBox["\[LeftPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPagePrevious"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Previous Slide"], ButtonBox[ StyleBox["\[RightPointer]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageNext"]}], ButtonStyle->"SlideHyperlink", ButtonNote->"Next Slide"], ButtonBox[ StyleBox["\[LastPage]", "SR"], ButtonFunction:>FrontEndExecute[ { FrontEndToken[ FrontEnd`SelectedNotebook[ ], "ScrollPageLast"]}], ButtonStyle->"SlideHyperlink"], " ", ButtonBox[ StyleBox[ RowBox[{ CounterBox["SlideShowNavigationBar"], \(\(\ \)\(of\)\(\ \)\), CounterBox["SlideShowNavigationBar", {None, "SlideShowHeader", -1}]}], "SR"], ButtonFrame->"None"]} }]]]], "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell["Conclusion", "Section"], Cell["\<\ Theory exploration involves inventing new reasoning \ techniques\ \>", "Outline1"], Cell["It should be possible to formalize them inside the system", "Outline1"], Cell["Requires a reflective term representation in the logic", "Outline1"], Cell["\<\ For soundness proofs, reflection of semantics often \ preferrable\ \>", "Outline1"], Cell[CellGroupData[{ Cell["Implementation of Compute with Quoting works", "Outline1"], Cell["Next steps:", "Text"] }, Open ]], Cell["Do Proving, not only computation", "Outline1"], Cell["Try it out in case studies", "Outline1"], Cell["\<\ Try to describe most of Theorema as extension of one small basic prover\ \>", "Outline1"] }, Open ]] }, Open ]] }, Open ]] }, FrontEndVersion->"5.2 for X", ScreenRectangle->{{0, 1400}, {0, 1050}}, ScreenStyleEnvironment->"Working", PrintingStyleEnvironment->"SlideShow", WindowToolbars->"RulerBar", WindowSize->{1154, 668}, WindowMargins->{{55, Automatic}, {Automatic, 22}}, ScrollingOptions->{"PagewiseScrolling"->False}, PrintingPageRange->{Automatic, Automatic}, PrintingOptions->{"PrintingMargins"->{{54, 54}, {72, 72}}, "PaperSize"->{597.562, 842.375}, "PaperOrientation"->"Landscape", "PrintCellBrackets"->False, "PrintRegistrationMarks"->True, "PrintMultipleHorizontalPages"->False, "PostScriptOutputFile":>FrontEnd`FileName[{$RootDirectory, "home", "giese", \ "work", "talks", "FormGroeb06"}, "GieseGroebC.ps", CharacterEncoding -> \ "iso8859-1"], "Magnification"->1}, Magnification->2, StyleDefinitions -> Notebook[{ Cell[CellGroupData[{ Cell["Style Definitions", "Title"], Cell["\<\ Modify the definitions below to change the default appearance of \ all cells in a given style. Make modifications to any definition using \ commands in the Format menu.\ \>", "Text"], Cell[CellGroupData[{ Cell["Style Environment Names", "Section"], Cell[StyleData[All, "Working"], PageWidth->WindowWidth, CellBracketOptions->{"Color"->RGBColor[0.269993, 0.308507, 0.6]}, CellLabelMargins->{{12, Inherited}, {Inherited, Inherited}}, ScriptMinSize->9], Cell[StyleData[All, "Presentation"], PageWidth->WindowWidth, CellLabelMargins->{{24, Inherited}, {Inherited, Inherited}}, ScriptMinSize->12], Cell[StyleData[All, "Condensed"], PageWidth->WindowWidth, CellLabelMargins->{{8, Inherited}, {Inherited, Inherited}}, ScriptMinSize->8], Cell[StyleData[All, "SlideShow"], PageWidth->WindowWidth, ScrollingOptions->{"PagewiseDisplay"->True, "VerticalScrollRange"->Fit}, ShowCellBracket->False, ScriptMinSize->9], Cell[StyleData[All, "Printout"], PageWidth->PaperWidth, CellLabelMargins->{{2, Inherited}, {Inherited, Inherited}}, ScriptMinSize->5, PrivateFontOptions->{"FontType"->"Outline"}] }, Closed]], Cell[CellGroupData[{ Cell["Notebook Options", "Section"], Cell["\<\ The options defined for the style below will be used at the \ Notebook level.\ \>", "Text"], Cell[StyleData["Notebook"], PageHeaders->{{Cell[ TextData[ { CounterBox[ "Page"]}], "PageNumber"], None, Cell[ TextData[ { ValueBox[ "FileName"]}], "Header"]}, {Cell[ TextData[ { ValueBox[ "FileName"]}], "Header"], None, Cell[ TextData[ { CounterBox[ "Page"]}], "PageNumber"]}}, CellFrameLabelMargins->6, StyleMenuListing->None] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Headings", "Section"], Cell[CellGroupData[{ Cell[StyleData["Title"], CellMargins->{{27, Inherited}, {10, 30}}, CellGroupingRules->{"TitleGrouping", 0}, PageBreakBelow->False, DefaultNewInlineCellStyle->"None", InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, TextAlignment->Center, LineSpacing->{1, 11}, LanguageCategory->"NaturalLanguage", CounterIncrements->"Title", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}, { "Subtitle", 0}, {"Subsubtitle", 0}}, FontFamily->"Helvetica", FontSize->36, FontWeight->"Bold"], Cell[StyleData["Title", "Presentation"], CellMargins->{{27, 10}, {10, 30}}, LineSpacing->{1, 0}, FontSize->44], Cell[StyleData["Title", "Condensed"], CellMargins->{{8, 10}, {4, 8}}, FontSize->20], Cell[StyleData["Title", "SlideShow"]], Cell[StyleData["Title", "Printout"], CellMargins->{{2, 10}, {12, 30}}, FontSize->24] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subtitle"], CellMargins->{{27, Inherited}, {20, 40}}, CellGroupingRules->{"TitleGrouping", 10}, PageBreakBelow->False, DefaultNewInlineCellStyle->"None", InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, TextAlignment->Center, LanguageCategory->"NaturalLanguage", CounterIncrements->"Subtitle", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}, { "Subsubtitle", 0}}, FontFamily->"Helvetica", FontSize->24], Cell[StyleData["Subtitle", "Presentation"], CellMargins->{{27, 10}, {20, 2}}, LineSpacing->{1, 0}, FontSize->36], Cell[StyleData["Subtitle", "Condensed"], CellMargins->{{8, 10}, {4, 4}}, FontSize->14], Cell[StyleData["Subtitle", "SlideShow"]], Cell[StyleData["Subtitle", "Printout"], CellMargins->{{2, 10}, {12, 8}}, FontSize->18] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsubtitle"], CellMargins->{{27, Inherited}, {8, 2}}, CellGroupingRules->{"TitleGrouping", 20}, PageBreakBelow->False, DefaultNewInlineCellStyle->"None", InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, TextAlignment->Center, LanguageCategory->"NaturalLanguage", CounterIncrements->"Subsubtitle", CounterAssignments->{{"Section", 0}, {"Equation", 0}, {"Figure", 0}}, FontFamily->"Helvetica", FontSize->16], Cell[StyleData["Subsubtitle", "Presentation"], CellMargins->{{24, 10}, {20, 20}}, LineSpacing->{1, 0}, FontSize->24], Cell[StyleData["Subsubtitle", "Condensed"], CellMargins->{{8, 10}, {8, 8}}, FontSize->12], Cell[StyleData["Subsubtitle", "SlideShow"]], Cell[StyleData["Subsubtitle", "Printout"], CellMargins->{{2, 10}, {12, 8}}, FontSize->14] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Section"], CellFrame->{{0, 0}, {4, 0}}, CellMargins->{{24, 24}, {8, 20}}, CellGroupingRules->{"SectionGrouping", 30}, PageBreakBelow->False, CellFrameMargins->4, CellFrameColor->RGBColor[1, 0.299992, 0], DefaultNewInlineCellStyle->"None", LineSpacing->{1, 2}, LanguageCategory->"NaturalLanguage", CounterIncrements->"Section", CounterAssignments->{{"Subsection", 0}, {"Subsubsection", 0}}, FontFamily->"Helvetica", FontSize->20, FontWeight->"Bold"], Cell[StyleData["Section", "Presentation"], CellMargins->{{40, 10}, {11, 32}}, LineSpacing->{1, 0}, FontSize->24], Cell[StyleData["Section", "Condensed"], CellMargins->{{18, Inherited}, {6, 12}}, FontSize->12], Cell[StyleData["Section", "SlideShow"]], Cell[StyleData["Section", "Printout"], CellMargins->{{2, 0}, {7, 22}}, FontSize->14] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsection"], CellDingbat->"\[FilledSmallSquare]", CellMargins->{{60, Inherited}, {8, 12}}, CellGroupingRules->{"SectionGrouping", 40}, PageBreakBelow->False, DefaultNewInlineCellStyle->"None", InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, LanguageCategory->"NaturalLanguage", CounterIncrements->"Subsection", CounterAssignments->{{"Subsubsection", 0}}, FontFamily->"Helvetica", FontSize->14, FontWeight->"Bold"], Cell[StyleData["Subsection", "Presentation"], CellMargins->{{36, 10}, {11, 32}}, LineSpacing->{1, 0}, FontSize->22], Cell[StyleData["Subsection", "Condensed"], CellMargins->{{16, Inherited}, {6, 12}}, FontSize->12], Cell[StyleData["Subsection", "SlideShow"]], Cell[StyleData["Subsection", "Printout"], CellMargins->{{9, 0}, {7, 22}}, FontSize->12] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Subsubsection"], CellDingbat->"\[FilledSmallSquare]", CellMargins->{{60, Inherited}, {2, 10}}, CellGroupingRules->{"SectionGrouping", 50}, PageBreakBelow->False, DefaultNewInlineCellStyle->"None", InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, LanguageCategory->"NaturalLanguage", CounterIncrements->"Subsubsection", FontFamily->"Helvetica", FontWeight->"Bold"], Cell[StyleData["Subsubsection", "Presentation"], CellMargins->{{34, 10}, {11, 26}}, LineSpacing->{1, 0}, FontSize->18], Cell[StyleData["Subsubsection", "Condensed"], CellMargins->{{17, Inherited}, {6, 12}}, FontSize->10], Cell[StyleData["Subsubsection", "SlideShow"]], Cell[StyleData["Subsubsection", "Printout"], CellMargins->{{9, 0}, {7, 14}}, FontSize->11] }, Closed]] }, Open ]], Cell[CellGroupData[{ Cell["Styles for Body Text", "Section", FontSize->14], Cell[CellGroupData[{ Cell[StyleData["Text"], CellMargins->{{60, 10}, {7, 7}}, InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, LineSpacing->{1, 3}, CounterIncrements->"Text", FontFamily->"Helvetica", FontSize->14], Cell[StyleData["Text", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}], Cell[StyleData["Text", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}], Cell[StyleData["Text", "SlideShow"]], Cell[StyleData["Text", "Printout"], CellMargins->{{2, 2}, {6, 6}}, TextJustification->0.5, Hyphenation->True] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SmallText"], CellMargins->{{60, 10}, {6, 6}}, DefaultNewInlineCellStyle->"None", LineSpacing->{1, 3}, LanguageCategory->"NaturalLanguage", CounterIncrements->"SmallText", FontFamily->"Helvetica", FontSize->14], Cell[StyleData["SmallText", "Presentation"], CellMargins->{{24, 10}, {8, 8}}, LineSpacing->{1, 5}], Cell[StyleData["SmallText", "Condensed"], CellMargins->{{8, 10}, {5, 5}}, LineSpacing->{1, 2}], Cell[StyleData["SmallText", "SlideShow"]], Cell[StyleData["SmallText", "Printout"], CellMargins->{{2, 2}, {5, 5}}, TextJustification->0.5, Hyphenation->True] }, Closed]] }, Open ]], Cell[CellGroupData[{ Cell["Styles for Input/Output", "Section"], Cell["\<\ The cells in this section define styles used for input and output \ to the kernel. Be careful when modifying, renaming, or removing these \ styles, because the front end associates special meanings with these style \ names. Some attributes for these styles are actually set in FormatType Styles \ (in the last section of this stylesheet). \ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Input"], CellMargins->{{66, 10}, {5, 7}}, Evaluatable->True, CellGroupingRules->"InputGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GroupPageBreakWithin->False, DefaultFormatType->DefaultInputFormatType, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, AutoItalicWords->{}, LanguageCategory->"Mathematica", FormatType->InputForm, ShowStringCharacters->True, NumberMarks->True, LinebreakAdjustments->{0.85, 2, 10, 0, 1}, CounterIncrements->"Input", FontSize->14, FontWeight->"Bold"], Cell[StyleData["Input", "Presentation"], CellMargins->{{72, Inherited}, {8, 10}}, LineSpacing->{1, 0}, FontSize->16], Cell[StyleData["Input", "Condensed"], CellMargins->{{40, 10}, {2, 3}}, FontSize->11], Cell[StyleData["Input", "SlideShow"]], Cell[StyleData["Input", "Printout"], CellMargins->{{39, 0}, {4, 6}}, LinebreakAdjustments->{0.85, 2, 10, 1, 1}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["InputOnly"], CellMargins->{{66, 10}, {7, 7}}, Evaluatable->True, CellGroupingRules->"InputGrouping", CellHorizontalScrolling->True, DefaultFormatType->DefaultInputFormatType, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, AutoItalicWords->{}, LanguageCategory->"Mathematica", FormatType->InputForm, ShowStringCharacters->True, NumberMarks->True, LinebreakAdjustments->{0.85, 2, 10, 0, 1}, CounterIncrements->"Input", StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["InputOnly", "Presentation"], CellMargins->{{72, Inherited}, {8, 10}}, LineSpacing->{1, 0}, FontSize->16], Cell[StyleData["InputOnly", "Condensed"], CellMargins->{{40, 10}, {2, 3}}, FontSize->11], Cell[StyleData["InputOnly", "SlideShow"]], Cell[StyleData["InputOnly", "Printout"], CellMargins->{{39, 0}, {4, 6}}, LinebreakAdjustments->{0.85, 2, 10, 1, 1}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Output"], CellMargins->{{66, 10}, {7, 5}}, CellEditDuplicate->True, CellGroupingRules->"OutputGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, DefaultFormatType->DefaultOutputFormatType, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, AutoItalicWords->{}, LanguageCategory->None, FormatType->InputForm, CounterIncrements->"Output"], Cell[StyleData["Output", "Presentation"], CellMargins->{{72, Inherited}, {10, 8}}, LineSpacing->{1, 0}, FontSize->16], Cell[StyleData["Output", "Condensed"], CellMargins->{{41, Inherited}, {3, 2}}, FontSize->11], Cell[StyleData["Output", "SlideShow"]], Cell[StyleData["Output", "Printout"], CellMargins->{{39, 0}, {6, 4}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Message"], CellMargins->{{66, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"OutputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, DefaultFormatType->DefaultOutputFormatType, "TwoByteSyntaxCharacterAutoReplacement"->True, AutoStyleOptions->{"UnmatchedBracketStyle"->None}, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, AutoItalicWords->{}, LanguageCategory->None, FormatType->InputForm, CounterIncrements->"Message", StyleMenuListing->None, FontFamily->"Helvetica", FontSize->10, FontColor->RGBColor[0.6, 0.100008, 0.100008]], Cell[StyleData["Message", "Presentation"], CellMargins->{{72, Inherited}, {Inherited, Inherited}}, LineSpacing->{1, 0}, FontSize->16], Cell[StyleData["Message", "Condensed"], CellMargins->{{41, Inherited}, {Inherited, Inherited}}, FontSize->11], Cell[StyleData["Message", "SlideShow"]], Cell[StyleData["Message", "Printout"], CellMargins->{{39, Inherited}, {Inherited, Inherited}}, FontSize->7, FontColor->GrayLevel[0]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Print"], CellMargins->{{66, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"OutputGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GroupPageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, DefaultFormatType->DefaultOutputFormatType, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, AutoItalicWords->{}, LanguageCategory->None, FormatType->InputForm, CounterIncrements->"Print", StyleMenuListing->None], Cell[StyleData["Print", "Presentation"], CellMargins->{{72, Inherited}, {Inherited, Inherited}}, LineSpacing->{1, 0}, FontSize->16], Cell[StyleData["Print", "Condensed"], CellMargins->{{41, Inherited}, {Inherited, Inherited}}, FontSize->11], Cell[StyleData["Print", "SlideShow"]], Cell[StyleData["Print", "Printout"], CellMargins->{{39, Inherited}, {Inherited, Inherited}}, FontSize->8] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Graphics"], CellMargins->{{4, Inherited}, {Inherited, Inherited}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, PageBreakWithin->False, GeneratedCell->True, CellAutoOverwrite->True, ShowCellLabel->False, DefaultFormatType->DefaultOutputFormatType, LanguageCategory->None, FormatType->InputForm, CounterIncrements->"Graphics", ImageMargins->{{43, Inherited}, {Inherited, 0}}, StyleMenuListing->None, FontFamily->"Courier", FontSize->10], Cell[StyleData["Graphics", "Presentation"], ImageMargins->{{62, Inherited}, {Inherited, 0}}], Cell[StyleData["Graphics", "Condensed"], ImageMargins->{{38, Inherited}, {Inherited, 0}}, Magnification->0.6], Cell[StyleData["Graphics", "SlideShow"]], Cell[StyleData["Graphics", "Printout"], ImageMargins->{{30, Inherited}, {Inherited, 0}}, Magnification->0.8] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["CellLabel"], LanguageCategory->None, StyleMenuListing->None, FontFamily->"Helvetica", FontSize->9, FontColor->RGBColor[0.269993, 0.308507, 0.6]], Cell[StyleData["CellLabel", "Presentation"], FontSize->12], Cell[StyleData["CellLabel", "Condensed"], FontSize->9], Cell[StyleData["CellLabel", "SlideShow"]], Cell[StyleData["CellLabel", "Printout"], FontFamily->"Courier", FontSize->8, FontSlant->"Italic", FontColor->GrayLevel[0]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["FrameLabel"], LanguageCategory->None, StyleMenuListing->None, FontFamily->"Helvetica", FontSize->9], Cell[StyleData["FrameLabel", "Presentation"], FontSize->12], Cell[StyleData["FrameLabel", "Condensed"], FontSize->9], Cell[StyleData["FrameLabel", "SlideShow"]], Cell[StyleData["FrameLabel", "Printout"], FontFamily->"Courier", FontSize->8, FontSlant->"Italic", FontColor->GrayLevel[0]] }, Closed]] }, Open ]], Cell[CellGroupData[{ Cell["Inline Formatting", "Section"], Cell["\<\ These styles are for modifying individual words or letters in a \ cell exclusive of the cell tag.\ \>", "Text"], Cell[StyleData["RM"], StyleMenuListing->None, FontWeight->"Plain", FontSlant->"Plain"], Cell[StyleData["BF"], StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["IT"], StyleMenuListing->None, FontSlant->"Italic"], Cell[StyleData["TR"], StyleMenuListing->None, FontFamily->"Times", FontWeight->"Plain", FontSlant->"Plain"], Cell[StyleData["TI"], StyleMenuListing->None, FontFamily->"Times", FontWeight->"Plain", FontSlant->"Italic"], Cell[StyleData["TB"], StyleMenuListing->None, FontFamily->"Times", FontWeight->"Bold", FontSlant->"Plain"], Cell[StyleData["TBI"], StyleMenuListing->None, FontFamily->"Times", FontWeight->"Bold", FontSlant->"Italic"], Cell[StyleData["MR"], "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, StyleMenuListing->None, FontFamily->"Courier", FontWeight->"Plain", FontSlant->"Plain"], Cell[StyleData["MO"], "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, StyleMenuListing->None, FontFamily->"Courier", FontWeight->"Plain", FontSlant->"Italic"], Cell[StyleData["MB"], "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, StyleMenuListing->None, FontFamily->"Courier", FontWeight->"Bold", FontSlant->"Plain"], Cell[StyleData["MBO"], "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, StyleMenuListing->None, FontFamily->"Courier", FontWeight->"Bold", FontSlant->"Italic"], Cell[StyleData["SR"], StyleMenuListing->None, FontFamily->"Helvetica", FontWeight->"Plain", FontSlant->"Plain"], Cell[StyleData["SO"], StyleMenuListing->None, FontFamily->"Helvetica", FontWeight->"Plain", FontSlant->"Italic"], Cell[StyleData["SB"], StyleMenuListing->None, FontFamily->"Helvetica", FontWeight->"Bold", FontSlant->"Plain"], Cell[StyleData["SBO"], StyleMenuListing->None, FontFamily->"Helvetica", FontWeight->"Bold", FontSlant->"Italic"], Cell[CellGroupData[{ Cell[StyleData["SO10"], StyleMenuListing->None, FontFamily->"Helvetica", FontSize->10, FontWeight->"Plain", FontSlant->"Italic"], Cell[StyleData["SO10", "Printout"], StyleMenuListing->None, FontFamily->"Helvetica", FontSize->7, FontWeight->"Plain", FontSlant->"Italic"] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Inert"], StyleMenuListing->None, Background->RGBColor[0.870588, 0.905882, 0.972549]], Cell[StyleData["Inert", "Printout"], StyleMenuListing->None, Background->GrayLevel[1]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Formulas and Programming", "Section"], Cell[CellGroupData[{ Cell[StyleData["InlineFormula"], CellMargins->{{10, 4}, {0, 8}}, CellHorizontalScrolling->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Formula", ScriptLevel->1, SingleLetterItalics->True], Cell[StyleData["InlineFormula", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}, FontSize->16], Cell[StyleData["InlineFormula", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}, FontSize->11], Cell[StyleData["InlineFormula", "SlideShow"]], Cell[StyleData["InlineFormula", "Printout"], CellMargins->{{2, 0}, {6, 6}}, FontSize->10] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DisplayFormula"], CellMargins->{{60, Inherited}, {Inherited, Inherited}}, CellHorizontalScrolling->True, DefaultFormatType->DefaultInputFormatType, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Formula", ScriptLevel->0, SingleLetterItalics->True, UnderoverscriptBoxOptions->{LimitsPositioning->True}], Cell[StyleData["DisplayFormula", "Presentation"], LineSpacing->{1, 5}, FontSize->16], Cell[StyleData["DisplayFormula", "Condensed"], LineSpacing->{1, 1}, FontSize->11], Cell[StyleData["DisplayFormula", "SlideShow"]], Cell[StyleData["DisplayFormula", "Printout"], FontSize->10] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Program"], CellFrame->{{0, 0}, {0.5, 0.5}}, CellMargins->{{60, 4}, {0, 8}}, CellHorizontalScrolling->True, Hyphenation->False, LanguageCategory->"Formula", ScriptLevel->1, FontFamily->"Courier"], Cell[StyleData["Program", "Presentation"], CellMargins->{{24, 10}, {10, 10}}, LineSpacing->{1, 5}, FontSize->16], Cell[StyleData["Program", "Condensed"], CellMargins->{{8, 10}, {6, 6}}, LineSpacing->{1, 1}, FontSize->11], Cell[StyleData["Program", "SlideShow"]], Cell[StyleData["Program", "Printout"], CellMargins->{{2, 0}, {6, 6}}, FontSize->9] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Outline Styles", "Section"], Cell[CellGroupData[{ Cell[StyleData["Outline1"], CellDingbat->"\[FilledSquare]", CellMargins->{{90, 10}, {7, 7}}, CellGroupingRules->{"SectionGrouping", 50}, ParagraphIndent->-38, CounterIncrements->"Outline1", CounterAssignments->{{"Outline2", 0}, {"Outline3", 0}, {"Outline4", 0}}, FontFamily->"Helvetica", FontSize->14, FontWeight->"Plain", FontSlant->"Plain", FontTracking->"Plain", FontVariations->{"Underline"->False, "Outline"->False, "Shadow"->False, "StrikeThrough"->False, "Masked"->False, "CompatibilityType"->0, "RotationAngle"->0}, CounterBoxOptions->{CounterFunction:>CapitalRomanNumeral}], Cell[StyleData["Outline1", "SlideShow"]], Cell[StyleData["Outline1", "Printout"], CounterBoxOptions->{CounterFunction:>CapitalRomanNumeral}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Outline2"], CellDingbat->"\[FilledSmallSquare]", CellMargins->{{120, 10}, {7, 7}}, CellGroupingRules->{"SectionGrouping", 60}, ParagraphIndent->-27, CounterIncrements->"Outline2", CounterAssignments->{{"Outline3", 0}, {"Outline4", 0}}, FontFamily->"Helvetica", FontSize->14, FontWeight->"Plain", FontSlant->"Plain", FontTracking->"Plain", FontVariations->{"Underline"->False, "Outline"->False, "Shadow"->False, "StrikeThrough"->False, "Masked"->False, "CompatibilityType"->0, "RotationAngle"->0}, CounterBoxOptions->{CounterFunction:>(Part[ CharacterRange[ "A", "Z"], #]&)}], Cell[StyleData["Outline2", "SlideShow"]], Cell[StyleData["Outline2", "Printout"], CounterBoxOptions->{CounterFunction:>(Part[ CharacterRange[ "A", "Z"], #]&)}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Outline3"], CellMargins->{{150, 10}, {7, 7}}, CellGroupingRules->{"SectionGrouping", 70}, ParagraphIndent->-21, CounterIncrements->"Outline3", CounterAssignments->{{"Outline4", 0}}, FontFamily->"Helvetica", FontSize->14, CounterBoxOptions->{CounterFunction:>Identity}], Cell[StyleData["Outline3", "SlideShow"]], Cell[StyleData["Outline3", "Printout"], CounterBoxOptions->{CounterFunction:>Identity}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Outline4"], CellMargins->{{180, 10}, {7, 7}}, CellGroupingRules->{"SectionGrouping", 80}, ParagraphIndent->-18, CounterIncrements->"Outline4", FontFamily->"Helvetica", FontSize->14, CounterBoxOptions->{CounterFunction:>(Part[ CharacterRange[ "a", "z"], #]&)}], Cell[StyleData["Outline4", "SlideShow"]], Cell[StyleData["Outline4", "Printout"]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Hyperlink Styles", "Section"], Cell["\<\ The cells below define styles useful for making hypertext \ ButtonBoxes. The \"Hyperlink\" style is for links within the same Notebook, \ or between Notebooks.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Hyperlink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookLocate[ #2]}]&), Active->True, ButtonFrame->"None", ButtonNote->ButtonData}], Cell[StyleData["Hyperlink", "Presentation"], FontSize->16], Cell[StyleData["Hyperlink", "Condensed"], FontSize->11], Cell[StyleData["Hyperlink", "SlideShow"]], Cell[StyleData["Hyperlink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell["\<\ The following styles are for linking automatically to the on-line \ help system.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["MainBookLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "MainBook", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["MainBookLink", "Presentation"], FontSize->16], Cell[StyleData["MainBookLink", "Condensed"], FontSize->11], Cell[StyleData["MainBookLink", "SlideShow"]], Cell[StyleData["MainBookLink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["AddOnsLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontFamily->"Courier", FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "AddOns", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["AddOnsLink", "Presentation"], FontSize->16], Cell[StyleData["AddOnsLink", "Condensed"], FontSize->11], Cell[StyleData["AddOnsLink", "SlideShow"]], Cell[StyleData["AddOnsLink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["RefGuideLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontFamily->"Courier", FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "RefGuide", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["RefGuideLink", "Presentation"], FontSize->16], Cell[StyleData["RefGuideLink", "Condensed"], FontSize->11], Cell[StyleData["RefGuideLink", "SlideShow"]], Cell[StyleData["RefGuideLink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["RefGuideLinkText"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "RefGuide", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["RefGuideLinkText", "Presentation"], FontSize->16], Cell[StyleData["RefGuideLinkText", "Condensed"], FontSize->11], Cell[StyleData["RefGuideLinkText", "SlideShow"]], Cell[StyleData["RefGuideLinkText", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["GettingStartedLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "GettingStarted", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["GettingStartedLink", "Presentation"], FontSize->16], Cell[StyleData["GettingStartedLink", "Condensed"], FontSize->11], Cell[StyleData["GettingStartedLink", "SlideShow"]], Cell[StyleData["GettingStartedLink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DemosLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "Demos", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["DemosLink", "SlideShow"]], Cell[StyleData["DemosLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["TourLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "Tour", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["TourLink", "SlideShow"]], Cell[StyleData["TourLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["OtherInformationLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "OtherInformation", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["OtherInformationLink", "Presentation"], FontSize->16], Cell[StyleData["OtherInformationLink", "Condensed"], FontSize->11], Cell[StyleData["OtherInformationLink", "SlideShow"]], Cell[StyleData["OtherInformationLink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["MasterIndexLink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontColor->RGBColor[0.269993, 0.308507, 0.6], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`HelpBrowserLookup[ "MasterIndex", #]}]&), Active->True, ButtonFrame->"None"}], Cell[StyleData["MasterIndexLink", "SlideShow"]], Cell[StyleData["MasterIndexLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Styles for Headers and Footers", "Section"], Cell[StyleData["Header"], CellMargins->{{0, 0}, {4, 1}}, DefaultNewInlineCellStyle->"None", LanguageCategory->"NaturalLanguage", StyleMenuListing->None, FontSize->10, FontSlant->"Italic"], Cell[StyleData["Footer"], CellMargins->{{0, 0}, {0, 4}}, DefaultNewInlineCellStyle->"None", LanguageCategory->"NaturalLanguage", StyleMenuListing->None, FontSize->9, FontSlant->"Italic"], Cell[StyleData["PageNumber"], CellMargins->{{0, 0}, {4, 1}}, StyleMenuListing->None, FontFamily->"Times", FontSize->10] }, Closed]], Cell[CellGroupData[{ Cell["Palette Styles", "Section"], Cell["\<\ The cells below define styles that define standard \ ButtonFunctions, for use in palette buttons.\ \>", "Text"], Cell[StyleData["Paste"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, Placeholder]}]&)}], Cell[StyleData["Evaluate"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionEvaluate[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["EvaluateCell"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionMove[ FrontEnd`InputNotebook[ ], All, Cell, 1], FrontEnd`SelectionEvaluateCreateCell[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["CopyEvaluate"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`SelectionCreateCell[ FrontEnd`InputNotebook[ ], All], FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionEvaluate[ FrontEnd`InputNotebook[ ], All]}]&)}], Cell[StyleData["CopyEvaluateCell"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`SelectionCreateCell[ FrontEnd`InputNotebook[ ], All], FrontEnd`NotebookApply[ FrontEnd`InputNotebook[ ], #, All], FrontEnd`SelectionEvaluateCreateCell[ FrontEnd`InputNotebook[ ], All]}]&)}] }, Closed]], Cell[CellGroupData[{ Cell["Placeholder Styles", "Section"], Cell["\<\ The cells below define styles useful for making placeholder \ objects in palette templates.\ \>", "Text"], Cell[CellGroupData[{ Cell[StyleData["Placeholder"], Placeholder->True, StyleMenuListing->None, FontSlant->"Italic", FontColor->RGBColor[0.890623, 0.864698, 0.384756], TagBoxOptions->{Editable->False, Selectable->False, StripWrapperBoxes->False}], Cell[StyleData["Placeholder", "Presentation"]], Cell[StyleData["Placeholder", "Condensed"]], Cell[StyleData["Placeholder", "SlideShow"]], Cell[StyleData["Placeholder", "Printout"]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["PrimaryPlaceholder"], StyleMenuListing->None, DrawHighlighted->True, FontSlant->"Italic", Background->RGBColor[0.912505, 0.891798, 0.507774], TagBoxOptions->{Editable->False, Selectable->False, StripWrapperBoxes->False}], Cell[StyleData["PrimaryPlaceholder", "Presentation"]], Cell[StyleData["PrimaryPlaceholder", "Condensed"]], Cell[StyleData["PrimaryPlaceholder", "SlideShow"]], Cell[StyleData["PrimaryPlaceholder", "Printout"]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["FormatType Styles", "Section"], Cell["\<\ The cells below define styles that are mixed in with the styles \ of most cells. If a cell's FormatType matches the name of one of the styles \ defined below, then that style is applied between the cell's style and its \ own options. This is particularly true of Input and Output.\ \>", "Text"], Cell[StyleData["CellExpression"], PageWidth->Infinity, CellMargins->{{6, Inherited}, {Inherited, Inherited}}, ShowCellLabel->False, ShowSpecialCharacters->False, AllowInlineCells->False, Hyphenation->False, AutoItalicWords->{}, StyleMenuListing->None, FontFamily->"Courier", FontSize->12, Background->GrayLevel[1]], Cell[StyleData["InputForm"], InputAutoReplacements->{}, AllowInlineCells->False, Hyphenation->False, StyleMenuListing->None, FontFamily->"Courier"], Cell[StyleData["OutputForm"], PageWidth->Infinity, TextAlignment->Left, LineSpacing->{0.6, 1}, StyleMenuListing->None, FontFamily->"Courier"], Cell[StyleData["StandardForm"], InputAutoReplacements->{ "->"->"\[Rule]", ":>"->"\[RuleDelayed]", "<="->"\[LessEqual]", ">="->"\[GreaterEqual]", "!="->"\[NotEqual]", "=="->"\[Equal]", Inherited}, "TwoByteSyntaxCharacterAutoReplacement"->True, LineSpacing->{1.25, 0}, StyleMenuListing->None, FontFamily->"Courier"], Cell[StyleData["TraditionalForm"], InputAutoReplacements->{ "->"->"\[Rule]", ":>"->"\[RuleDelayed]", "<="->"\[LessEqual]", ">="->"\[GreaterEqual]", "!="->"\[NotEqual]", "=="->"\[Equal]", Inherited}, "TwoByteSyntaxCharacterAutoReplacement"->True, LineSpacing->{1.25, 0}, SingleLetterItalics->True, TraditionalFunctionNotation->True, DelimiterMatching->None, StyleMenuListing->None], Cell["\<\ The style defined below is mixed in to any cell that is in an \ inline cell within another.\ \>", "Text"], Cell[StyleData["InlineCell"], LanguageCategory->"Formula", ScriptLevel->1, StyleMenuListing->None], Cell[StyleData["InlineCellEditing"], StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216]] }, Closed]], Cell[CellGroupData[{ Cell["Automatic Styles", "Section"], Cell["\<\ The cells below define styles that are used to affect the display \ of certain types of objects in typeset expressions. For example, \ \"UnmatchedBracket\" style defines how unmatched bracket, curly bracket, and \ parenthesis characters are displayed (typically by coloring them to make them \ stand out).\ \>", "Text"], Cell[StyleData["UnmatchedBracket"], StyleMenuListing->None, FontColor->RGBColor[0.760006, 0.330007, 0.8]], Cell[StyleData["Completions"], StyleMenuListing->None, FontFamily->"Courier"] }, Closed]], Cell[CellGroupData[{ Cell["Styles from HelpBrowser", "Section"], Cell[CellGroupData[{ Cell[StyleData["MathCaption"], CellFrame->{{0, 0}, {0, 0.5}}, CellMargins->{{66, 12}, {2, 24}}, PageBreakBelow->False, CellFrameMargins->{{8, 8}, {8, 2}}, CellFrameColor->GrayLevel[0.700008], CellFrameLabelMargins->4, LineSpacing->{1, 1}, ParagraphSpacing->{0, 8}, StyleMenuListing->None, FontColor->GrayLevel[0.2]], Cell[StyleData["MathCaption", "Presentation"], FontSize->18], Cell[StyleData["MathCaption", "SlideShow"]], Cell[StyleData["MathCaption", "Printout"], CellMargins->{{39, 0}, {0, 14}}, Hyphenation->True, FontSize->9, FontColor->GrayLevel[0]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["ObjectName"], ShowCellBracket->True, CellMargins->{{66, 4}, {8, 8}}, Evaluatable->True, CellGroupingRules->"InputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, CellLabelAutoDelete->False, CellLabelMargins->{{14, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultInputFormatType, ShowSpecialCharacters->Automatic, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Mathematica", FormatType->StandardForm, ShowStringCharacters->True, NumberMarks->True, StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["ObjectName", "Presentation"], FontSize->18], Cell[StyleData["ObjectName", "SlideShow"]], Cell[StyleData["ObjectName", "Printout"], ShowCellBracket->False, CellMargins->{{39, 0}, {6, 6}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Usage"], ShowCellBracket->True, CellMargins->{{66, 4}, {8, 8}}, Evaluatable->True, CellGroupingRules->"InputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, CellLabelAutoDelete->False, CellLabelMargins->{{14, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultInputFormatType, ShowSpecialCharacters->Automatic, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Mathematica", FormatType->StandardForm, ShowStringCharacters->True, NumberMarks->True, StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["Usage", "Presentation"], FontSize->18], Cell[StyleData["Usage", "SlideShow"]], Cell[StyleData["Usage", "Printout"], ShowCellBracket->False, CellMargins->{{39, 0}, {6, 6}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Notes"], ShowCellBracket->True, CellMargins->{{66, 4}, {8, 8}}, Evaluatable->True, CellGroupingRules->"InputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, CellLabelAutoDelete->False, CellLabelMargins->{{14, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultInputFormatType, ShowSpecialCharacters->Automatic, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Mathematica", FormatType->StandardForm, ShowStringCharacters->True, NumberMarks->True, StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["Notes", "Presentation"], FontSize->18], Cell[StyleData["Notes", "SlideShow"]], Cell[StyleData["Notes", "Printout"], ShowCellBracket->False, CellMargins->{{39, 0}, {6, 6}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["InlineOutput"], ShowCellBracket->True, CellMargins->{{66, 4}, {8, 8}}, Evaluatable->True, CellGroupingRules->"InputGrouping", PageBreakWithin->False, GroupPageBreakWithin->False, CellLabelAutoDelete->False, CellLabelMargins->{{14, Inherited}, {Inherited, Inherited}}, DefaultFormatType->DefaultInputFormatType, ShowSpecialCharacters->Automatic, "TwoByteSyntaxCharacterAutoReplacement"->True, HyphenationOptions->{"HyphenationCharacter"->"\[Continuation]"}, LanguageCategory->"Mathematica", FormatType->StandardForm, ShowStringCharacters->True, NumberMarks->True, StyleMenuListing->None, FontWeight->"Bold"], Cell[StyleData["InlineOutput", "Presentation"], FontSize->18], Cell[StyleData["InlineOutput", "SlideShow"]], Cell[StyleData["InlineOutput", "Printout"], ShowCellBracket->False, CellMargins->{{39, 0}, {6, 6}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell["Emphasis Boxes and Pictures", "Subsection"], Cell[CellGroupData[{ Cell[StyleData["Box"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnSpacings->1}], Cell[StyleData["Box", "Presentation"], FontSize->18], Cell[StyleData["Box", "SlideShow"]], Cell[StyleData["Box", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DoubleBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnSpacings->2, RowAlignments->Top}], Cell[StyleData["DoubleBox", "Presentation"], FontSize->18], Cell[StyleData["DoubleBox", "SlideShow"]], Cell[StyleData["DoubleBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["1ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnSpacings->1}], Cell[StyleData["1ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["1ColumnBox", "SlideShow"]], Cell[StyleData["1ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["2ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], SingleLetterItalics->False, LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->{0.31, 0.67}}], Cell[StyleData["2ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["2ColumnBox", "SlideShow"]], Cell[StyleData["2ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->9, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["2ColumnEvenBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->0.46}], Cell[StyleData["2ColumnEvenBox", "Presentation"], FontSize->18], Cell[StyleData["2ColumnEvenBox", "SlideShow"]], Cell[StyleData["2ColumnEvenBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["2ColumnSmallBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnSpacings->1.5, ColumnWidths->0.35, ColumnAlignments->{Right, Left}}], Cell[StyleData["2ColumnSmallBox", "Presentation"], FontSize->18], Cell[StyleData["2ColumnSmallBox", "SlideShow"]], Cell[StyleData["2ColumnSmallBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["3ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->0.32}], Cell[StyleData["3ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["3ColumnBox", "SlideShow"]], Cell[StyleData["3ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["3ColumnSmallBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnSpacings->1.5, ColumnWidths->0.24, ColumnAlignments->{Right, Center, Left}}], Cell[StyleData["3ColumnSmallBox", "Presentation"], FontSize->18], Cell[StyleData["3ColumnSmallBox", "SlideShow"]], Cell[StyleData["3ColumnSmallBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["4ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], SingleLetterItalics->False, LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->{0.13, 0.35, 0.13, 0.35}}], Cell[StyleData["4ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["4ColumnBox", "SlideShow"]], Cell[StyleData["4ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["5ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->0.202}], Cell[StyleData["5ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["5ColumnBox", "SlideShow"]], Cell[StyleData["5ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->9, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["6ColumnBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxFrame->0.5, BoxMargins->True}, GridBoxOptions->{ColumnWidths->{0.12, 0.22, 0.12, 0.12, 0.22, 0.12}}], Cell[StyleData["6ColumnBox", "Presentation"], FontSize->18], Cell[StyleData["6ColumnBox", "SlideShow"]], Cell[StyleData["6ColumnBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["FramedBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnAlignments->{Left}}], Cell[StyleData["FramedBox", "Presentation"], FontSize->18], Cell[StyleData["FramedBox", "SlideShow"]], Cell[StyleData["FramedBox", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DefinitionBox"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.4, 0.6}, ColumnAlignments->{Left}}], Cell[StyleData["DefinitionBox", "Presentation"], FontSize->18], Cell[StyleData["DefinitionBox", "SlideShow"]], Cell[StyleData["DefinitionBox", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DefinitionBox3Col"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.35, 0.2, 0.45}, ColumnAlignments->{Left}}], Cell[StyleData["DefinitionBox3Col", "Presentation"], FontSize->18], Cell[StyleData["DefinitionBox3Col", "SlideShow"]], Cell[StyleData["DefinitionBox3Col", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DefinitionBox4Col"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.15, 0.35, 0.15, 0.35}, ColumnAlignments->{Left}}], Cell[StyleData["DefinitionBox4Col", "Presentation"], FontSize->18], Cell[StyleData["DefinitionBox4Col", "SlideShow"]], Cell[StyleData["DefinitionBox4Col", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DefinitionBox5Col"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->0.2, ColumnAlignments->{Left}}], Cell[StyleData["DefinitionBox5Col", "Presentation"], FontSize->18], Cell[StyleData["DefinitionBox5Col", "SlideShow"]], Cell[StyleData["DefinitionBox5Col", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["DefinitionBox6Col"], CellFrame->0.5, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakWithin->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.13, 0.24, 0.13, 0.13, 0.24, 0.13}, ColumnAlignments->{Left}}], Cell[StyleData["DefinitionBox6Col", "Presentation"], FontSize->18], Cell[StyleData["DefinitionBox6Col", "SlideShow"]], Cell[StyleData["DefinitionBox6Col", "Printout"], CellMargins->{{2, 4}, {0, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["TopBox"], CellFrame->{{0.5, 0.5}, {0, 0.5}}, CellMargins->{{27, 12}, {0, 8}}, CellHorizontalScrolling->True, PageBreakBelow->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.31, 0.62}, ColumnAlignments->{Left}}], Cell[StyleData["TopBox", "Presentation"], FontSize->18], Cell[StyleData["TopBox", "SlideShow"]], Cell[StyleData["TopBox", "Printout"], CellMargins->{{2, 0}, {0, 8}}, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["MiddleBox"], CellFrame->{{0.5, 0.5}, {0, 0}}, CellMargins->{{27, 12}, {0, -7}}, CellHorizontalScrolling->True, PageBreakAbove->False, PageBreakBelow->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.31, 0.62}, ColumnAlignments->{Left}}], Cell[StyleData["MiddleBox", "Presentation"], FontSize->18], Cell[StyleData["MiddleBox", "SlideShow"]], Cell[StyleData["MiddleBox", "Printout"], CellMargins->{{2, 0}, {0, 2}}, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["BottomBox"], CellFrame->{{0.5, 0.5}, {0.5, 0}}, CellMargins->{{27, 12}, {0, -7}}, CellHorizontalScrolling->True, PageBreakAbove->False, PageBreakBelow->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.31, 0.62}, ColumnAlignments->{Left}}], Cell[StyleData["BottomBox", "Presentation"], FontSize->18], Cell[StyleData["BottomBox", "SlideShow"]], Cell[StyleData["BottomBox", "Printout"], CellMargins->{{2, 0}, {0, -5}}, FontSize->10, Background->GrayLevel[1], GridBoxOptions->{RowMinHeight->2.2}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["TopSpanBox"], CellFrame->{{0.5, 0.5}, {0, 0.5}}, CellMargins->{{27, 12}, {-2, 8}}, CellHorizontalScrolling->True, PageBreakBelow->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.9, 0.03}, ColumnAlignments->{Left}}], Cell[StyleData["TopSpanBox", "Presentation"], FontSize->18], Cell[StyleData["TopSpanBox", "SlideShow"]], Cell[StyleData["TopSpanBox", "Printout"], CellMargins->{{2, 0}, {-2, 8}}, FontSize->10, Background->GrayLevel[1]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["MiddleSpanBox"], CellFrame->{{0.5, 0.5}, {0, 0}}, CellMargins->{{27, 12}, {0, 0}}, CellHorizontalScrolling->True, PageBreakAbove->False, PageBreakBelow->False, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], AutoIndent->False, AutoSpacing->False, LineIndent->0, StyleMenuListing->None, FontWeight->"Plain", Background->RGBColor[0.964706, 0.929412, 0.839216], GridBoxOptions->{RowSpacings->1.5, ColumnSpacings->1, ColumnWidths->{0.9, 0.03}, ColumnAlignments->{Left}}], Cell[StyleData["MiddleSpanBox", "Presentation"], FontSize->18], Cell[StyleData["MiddleSpanBox", "SlideShow"]], Cell[StyleData["MiddleSpanBox", "Printout"], CellMargins->{{2, 0}, {-5, 0}}, FontSize->10, Background->GrayLevel[1], GridBoxOptions->{RowMinHeight->1.8}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Picture"], CellMargins->{{27, Inherited}, {4, 4}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, StyleMenuListing->None], Cell[StyleData["Picture", "Presentation"], FontSize->18], Cell[StyleData["Picture", "SlideShow"]], Cell[StyleData["Picture", "Printout"], CellMargins->{{2, Inherited}, {4, 4}}, Magnification->0.65] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["OpenCloseItemizedPicture"], CellMargins->{{88, 4}, {4, 4}}, PrivateCellOptions->{"DefaultCellGroupOpen"->False}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, StyleMenuListing->None], Cell[StyleData["OpenCloseItemizedPicture", "Presentation"], FontSize->18], Cell[StyleData["OpenCloseItemizedPicture", "SlideShow"]], Cell[StyleData["OpenCloseItemizedPicture", "Printout"], CellMargins->{{76, 2}, {0, 0}}, CellElementSpacings->{"CellMinHeight"->1, "ClosedCellHeight"->0}, CellOpen->False] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["ItemizedPicture"], CellMargins->{{88, 4}, {4, 4}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, StyleMenuListing->None], Cell[StyleData["ItemizedPicture", "Presentation"], FontSize->18], Cell[StyleData["ItemizedPicture", "SlideShow"]], Cell[StyleData["ItemizedPicture", "Printout"], CellMargins->{{77, 2}, {4, -4}}, Magnification->0.5] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["ListGraphic"], CellMargins->{{88, 4}, {4, 4}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, StyleMenuListing->None], Cell[StyleData["ListGraphic", "Presentation"], FontSize->18], Cell[StyleData["ListGraphic", "SlideShow"]], Cell[StyleData["ListGraphic", "Printout"], CellMargins->{{77, 2}, {4, -4}}, Magnification->0.5] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["ListNoteBox"], CellFrame->0.5, CellMargins->{{88, 12}, {8, 8}}, CellHorizontalScrolling->True, CellFrameColor->RGBColor[0.74902, 0.694118, 0.552941], LineIndent->0, StyleMenuListing->None, Background->RGBColor[0.964706, 0.929412, 0.839216], FrameBoxOptions->{BoxMargins->{{1, 1}, {1.5, 1.5}}}, GridBoxOptions->{ColumnSpacings->1}], Cell[StyleData["ListNoteBox", "Presentation"], FontSize->18], Cell[StyleData["ListNoteBox", "SlideShow"]], Cell[StyleData["ListNoteBox", "Printout"], CellMargins->{{77, 4}, {6, 2}}, FontSize->10, Background->GrayLevel[0.900008]] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["PictureGroup"], CellMargins->{{41, 4}, {0, 4}}, CellGroupingRules->"GraphicsGrouping", CellHorizontalScrolling->True, StyleMenuListing->None], Cell[StyleData["PictureGroup", "Presentation"], FontSize->18], Cell[StyleData["PictureGroup", "SlideShow"]], Cell[StyleData["PictureGroup", "Printout"], CellMargins->{{76, 2}, {0, 0}}, CellElementSpacings->{"CellMinHeight"->1, "ClosedCellHeight"->0}, CellOpen->False] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["Sound"], ShowCellBracket->True, CellMargins->{{27, Inherited}, {0, 8}}, StyleMenuListing->None], Cell[StyleData["Sound", "Presentation"], FontSize->18], Cell[StyleData["Sound", "SlideShow"]], Cell[StyleData["Sound", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->10] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Tables", "Subsection"], Cell[CellGroupData[{ Cell[StyleData["2ColumnTable"], CellMargins->{{35, 4}, {0, 8}}, CellHorizontalScrolling->True, LineIndent->0, StyleMenuListing->None, GridBoxOptions->{ColumnWidths->{0.34, 0.64}, ColumnAlignments->{Left}}], Cell[StyleData["2ColumnTable", "Presentation"], FontSize->18], Cell[StyleData["2ColumnTable", "SlideShow"]], Cell[StyleData["2ColumnTable", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["2ColumnEvenTable"], CellMargins->{{35, 4}, {0, 8}}, CellHorizontalScrolling->True, LineIndent->0, StyleMenuListing->None, GridBoxOptions->{ColumnWidths->0.49, ColumnAlignments->{Left}}], Cell[StyleData["2ColumnEvenTable", "Presentation"], FontSize->18], Cell[StyleData["2ColumnEvenTable", "SlideShow"]], Cell[StyleData["2ColumnEvenTable", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->9] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["3ColumnTable"], CellMargins->{{35, 4}, {0, 8}}, CellHorizontalScrolling->True, LineIndent->0, StyleMenuListing->None, GridBoxOptions->{ColumnWidths->{0.28, 0.28, 0.43}, ColumnAlignments->{Left}}], Cell[StyleData["3ColumnTable", "Presentation"], FontSize->18], Cell[StyleData["3ColumnTable", "SlideShow"]], Cell[StyleData["3ColumnTable", "Printout"], CellMargins->{{2, 0}, {0, 8}}, FontSize->9] }, Closed]] }, Closed]] }, Closed]], Cell[CellGroupData[{ Cell["Slide Show Styles", "Section"], Cell[CellGroupData[{ Cell[StyleData["SlideShowNavigationBar"], Editable->False, CellFrame->True, CellMargins->{{0, 0}, {3, 3}}, CellElementSpacings->{"CellMinHeight"->0.8125}, CellGroupingRules->{"SectionGrouping", 30}, CellFrameMargins->False, CellFrameColor->GrayLevel[1], CellFrameLabelMargins->False, TextAlignment->Center, CounterIncrements->"SlideShowNavigationBar", StyleMenuListing->None, FontSize->10, Background->GrayLevel[0.8], Magnification->1, GridBoxOptions->{GridBaseline->Center, RowSpacings->0, ColumnSpacings->0, ColumnWidths->{3.5, 3.5, 3.5, 3.5, 13, 5, 4}, RowAlignments->Baseline, ColumnAlignments->{ Center, Center, Center, Center, Center, Center, Right, Center}}], Cell[StyleData["SlideShowNavigationBar", "Presentation"]], Cell[StyleData["SlideShowNavigationBar", "SlideShow"], Deletable->False, ShowCellBracket->False, CellMargins->{{-1, -1}, {-1, -1}}, PageBreakAbove->True, CellFrameMargins->{{1, 1}, {0, 0}}], Cell[StyleData["SlideShowNavigationBar", "Printout"], CellMargins->{{18, 4}, {4, 4}}, LineSpacing->{1, 3}, FontSize->10] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SlideShowSection"], CellFrame->{{0, 0}, {0, 0.5}}, CellMargins->{{0, 0}, {10, 0}}, CellGroupingRules->{"SectionGrouping", 40}, PageBreakBelow->False, CellFrameMargins->{{12, 4}, {6, 12}}, InputAutoReplacements->{"TeX"->StyleBox[ RowBox[ {"T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "LaTeX"->StyleBox[ RowBox[ {"L", StyleBox[ AdjustmentBox[ "A", BoxMargins -> {{-0.35999999999999999, \ -0.10000000000000001}, {0, 0}}, BoxBaselineShift -> -0.20000000000000001], FontSize -> Smaller], "T", AdjustmentBox[ "E", BoxMargins -> {{-0.074999999999999997, \ -0.085000000000000006}, {0, 0}}, BoxBaselineShift -> 0.5], "X"}]], "mma"->"Mathematica", "Mma"->"Mathematica", "MMA"->"Mathematica", "gridMathematica"->FormBox[ RowBox[ {"grid", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.175, 0}, {0, 0}}]}], TextForm], "webMathematica"->FormBox[ RowBox[ {"web", AdjustmentBox[ StyleBox[ "Mathematica", FontSlant -> "Italic"], BoxMargins -> {{-0.17499999999999999, 0}, {0, 0}}]}], TextForm], Inherited}, CounterIncrements->"Section", CounterAssignments->{{"Subsection", 0}, {"Subsubsection", 0}}, StyleMenuListing->None, FontFamily->"Helvetica", FontSize->18, FontWeight->"Plain", FontColor->GrayLevel[1], Background->RGBColor[0.408011, 0.440726, 0.8]], Cell[StyleData["SlideShowSection", "Presentation"], CellFrameMargins->{{20, 10}, {10, 18}}, FontSize->27], Cell[StyleData["SlideShowSection", "SlideShow"], ShowCellBracket->False, PageBreakAbove->True], Cell[StyleData["SlideShowSection", "Printout"], CellMargins->{{18, 30}, {0, 30}}, CellFrameMargins->5, FontSize->14] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SlideHyperlink"], StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontSize->26, FontColor->GrayLevel[0.400015], ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookLocate[ #2]}]&), Active->True, ButtonMinHeight->0.85, ButtonMargins->0.5, ButtonNote->None}], Cell[StyleData["SlideHyperlink", "Presentation"], CellMargins->{{14, 10}, {6, 12}}, FontSize->36], Cell[StyleData["SlideHyperlink", "SlideShow"]], Cell[StyleData["SlideHyperlink", "Printout"], FontSize->10, FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SlideTOCLink"], CellMargins->{{24, Inherited}, {Inherited, Inherited}}, StyleMenuListing->None, ButtonStyleMenuListing->Automatic, FontFamily->"Helvetica", ButtonBoxOptions->{ButtonFunction:>(FrontEndExecute[ { FrontEnd`NotebookLocate[ #2]}]&), Active->True, ButtonMargins->1.5, ButtonNote->ButtonData}], Cell[StyleData["SlideTOCLink", "Presentation"], CellMargins->{{35, 10}, {8, 8}}, FontSize->18], Cell[StyleData["SlideTOCLink", "SlideShow"]], Cell[StyleData["SlideTOCLink", "Printout"], FontColor->GrayLevel[0], FontVariations->{"Underline"->False}] }, Closed]], Cell[CellGroupData[{ Cell[StyleData["SlideTOC"], CellDingbat->"\[Bullet]", CellMargins->{{18, Inherited}, {Inherited, Inherited}}, StyleMenuListing->None, FontFamily->"Helvetica"], Cell[StyleData["SlideTOC", "Presentation"], CellMargins->{{25, 10}, {10, 5}}, FontSize->18], Cell[StyleData["SlideTOC", "SlideShow"], FontSize->14], Cell[StyleData["SlideTOC", "Printout"], FontSize->10, FontColor->GrayLevel[0]] }, Closed]] }, Closed]] }, Open ]] }] ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{ "SlideShowHeader"->{ Cell[1754, 51, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[3781, 117, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[6568, 207, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[8933, 287, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[11383, 368, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[14222, 458, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[16549, 531, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[21149, 692, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[23587, 770, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[31549, 1025, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[34824, 1121, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[37799, 1208, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[40137, 1283, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[42700, 1357, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[45716, 1453, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[48041, 1526, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[55737, 1718, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[58988, 1814, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[62077, 1911, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[64758, 1995, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[66928, 2064, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[69806, 2148, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[72819, 2245, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[75183, 2317, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"]} } *) (*CellTagsIndex CellTagsIndex->{ {"SlideShowHeader", 157568, 5144} } *) (*NotebookFileOutline Notebook[{ Cell[1754, 51, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[3458, 99, 68, 3, 306, "Title"], Cell[3529, 104, 32, 0, 182, "Subtitle"], Cell[3564, 106, 85, 3, 102, "Subsubtitle"], Cell[3652, 111, 26, 0, 56, "Input"], Cell[CellGroupData[{ Cell[3703, 115, 75, 0, 61, "Subsubtitle"], Cell[3781, 117, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[5485, 165, 50, 0, 126, "Section"], Cell[5538, 167, 94, 1, 69, "Text"], Cell[5635, 170, 75, 1, 65, "Outline1"], Cell[5713, 173, 94, 1, 65, "Outline1"], Cell[CellGroupData[{ Cell[5832, 178, 80, 1, 65, "Outline1"], Cell[5915, 181, 46, 1, 69, "Text"] }, Open ]], Cell[5976, 185, 107, 1, 65, "Outline1"], Cell[6086, 188, 101, 1, 65, "Outline1"], Cell[CellGroupData[{ Cell[6212, 193, 80, 1, 65, "Outline1"], Cell[6295, 196, 46, 1, 69, "Text"] }, Open ]], Cell[6356, 200, 106, 1, 65, "Outline1"], Cell[6465, 203, 88, 1, 65, "Outline1"] }, Open ]], Cell[6568, 207, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[8272, 255, 23, 0, 126, "Section"], Cell[8298, 257, 48, 0, 69, "Text"], Cell[8349, 259, 25, 0, 69, "Text"], Cell[8377, 261, 145, 4, 65, "Outline1"], Cell[CellGroupData[{ Cell[8547, 269, 77, 0, 65, "Outline1"], Cell[8627, 271, 32, 3, 110, "Text"] }, Open ]], Cell[8674, 277, 75, 0, 65, "Outline1"], Cell[8752, 279, 68, 0, 65, "Outline1"], Cell[8823, 281, 95, 3, 65, "Outline1"] }, Open ]], Cell[8933, 287, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[10637, 335, 26, 0, 126, "Section"], Cell[CellGroupData[{ Cell[10688, 339, 142, 4, 102, "Outline1"], Cell[10833, 345, 248, 6, 151, "Text"] }, Open ]], Cell[11096, 354, 54, 0, 65, "Outline1"], Cell[CellGroupData[{ Cell[11175, 358, 70, 0, 65, "Outline1"], Cell[11248, 360, 37, 0, 65, "Outline2"], Cell[11288, 362, 34, 0, 65, "Outline2"], Cell[11325, 364, 31, 0, 65, "Outline2"] }, Open ]] }, Open ]], Cell[11383, 368, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[13087, 416, 27, 0, 126, "Section"], Cell[13117, 418, 39, 0, 69, "Text"], Cell[13159, 420, 48, 0, 65, "Outline1"], Cell[13210, 422, 35, 0, 65, "Outline1"], Cell[CellGroupData[{ Cell[13270, 426, 117, 3, 65, "Outline1"], Cell[13390, 431, 35, 0, 69, "Text"] }, Open ]], Cell[13440, 434, 170, 2, 65, "Outline1"], Cell[13613, 438, 152, 2, 65, "Outline1"], Cell[13768, 442, 124, 2, 65, "Outline1"], Cell[CellGroupData[{ Cell[13917, 448, 161, 2, 65, "Outline1"], Cell[14081, 452, 39, 0, 69, "Text"] }, Open ]], Cell[14135, 455, 72, 0, 65, "Outline1"] }, Open ]], Cell[14222, 458, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[15926, 506, 29, 0, 126, "Section"], Cell[15958, 508, 108, 3, 69, "Text"], Cell[16069, 513, 180, 4, 110, "Text"], Cell[16252, 519, 159, 4, 110, "Text"], Cell[16414, 525, 120, 3, 69, "Text"] }, Open ]], Cell[16549, 531, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[18253, 579, 47, 0, 126, "Section"], Cell[18303, 581, 56, 0, 69, "Text"], Cell[18362, 583, 111, 3, 69, "Text"], Cell[18476, 588, 100, 3, 69, "Text"], Cell[18579, 593, 477, 14, 234, "Input"], Cell[19059, 609, 29, 0, 69, "Text"], Cell[19091, 611, 34, 0, 69, "Text"], Cell[19128, 613, 974, 37, 98, "Input"], Cell[20105, 652, 39, 0, 69, "Text"], Cell[20147, 654, 987, 35, 98, "Input"] }, Open ]], Cell[21149, 692, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[22853, 740, 49, 0, 126, "Section"], Cell[22905, 742, 92, 3, 69, "Text"], Cell[23000, 747, 62, 0, 69, "Text"], Cell[23065, 749, 410, 13, 194, "Input"], Cell[23478, 764, 94, 3, 69, "Text"] }, Open ]], Cell[23587, 770, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[25291, 818, 54, 0, 126, "Section"], Cell[25348, 820, 148, 4, 69, "Text"], Cell[25499, 826, 5611, 176, 348, "Input"], Cell[31113, 1004, 275, 10, 110, "Text"], Cell[31391, 1016, 29, 0, 69, "Text"], Cell[31423, 1018, 57, 1, 62, "Input"], Cell[31483, 1021, 51, 1, 57, "Input"] }, Open ]], Cell[31549, 1025, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[33253, 1073, 72, 0, 126, "Section"], Cell[33328, 1075, 357, 8, 134, "Input"], Cell[33688, 1085, 356, 9, 135, "Input"], Cell[34047, 1096, 152, 3, 91, "Input"], Cell[34202, 1101, 128, 2, 56, "Input"], Cell[34333, 1105, 33, 0, 69, "Text"], Cell[34369, 1107, 278, 5, 91, "Input"], Cell[34650, 1114, 130, 2, 56, "Input"], Cell[34783, 1118, 26, 0, 56, "Input"] }, Open ]], Cell[34824, 1121, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[36528, 1169, 56, 0, 126, "Section"], Cell[36587, 1171, 57, 0, 69, "Text"], Cell[36647, 1173, 384, 9, 135, "Input"], Cell[37034, 1184, 104, 3, 69, "Text"], Cell[37141, 1189, 312, 5, 91, "Input"], Cell[37456, 1196, 189, 3, 91, "Input"], Cell[37648, 1201, 136, 4, 69, "Text"] }, Open ]], Cell[37799, 1208, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[39503, 1256, 41, 0, 126, "Section"], Cell[39547, 1258, 201, 4, 151, "Text"], Cell[39751, 1264, 68, 1, 56, "Input"], Cell[39822, 1267, 34, 0, 69, "Text"], Cell[39859, 1269, 68, 1, 56, "Input"], Cell[39930, 1272, 90, 3, 69, "Text"], Cell[40023, 1277, 99, 3, 69, "Text"] }, Open ]], Cell[40137, 1283, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[41841, 1331, 36, 0, 126, "Section"], Cell[41880, 1333, 103, 3, 69, "Text"], Cell[41986, 1338, 699, 16, 394, "Input"] }, Open ]], Cell[42700, 1357, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[44404, 1405, 40, 0, 126, "Section"], Cell[44447, 1407, 48, 0, 69, "Text"], Cell[44498, 1409, 47, 0, 69, "Text"], Cell[44548, 1411, 211, 3, 91, "Input"], Cell[44762, 1416, 56, 0, 69, "Text"], Cell[44821, 1418, 34, 0, 69, "Text"], Cell[CellGroupData[{ Cell[44880, 1422, 140, 4, 102, "Outline1"], Cell[45023, 1428, 140, 2, 70, "Input"] }, Open ]], Cell[CellGroupData[{ Cell[45200, 1435, 131, 4, 102, "Outline1"], Cell[45334, 1441, 355, 8, 98, "Input"] }, Open ]] }, Open ]], Cell[45716, 1453, 1679, 44, 30, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[47420, 1501, 49, 0, 126, "Section"], Cell[47472, 1503, 51, 0, 69, "Text"], Cell[47526, 1505, 85, 3, 65, "Outline1"], Cell[47614, 1510, 50, 0, 65, "Outline1"], Cell[47667, 1512, 63, 0, 65, "Outline1"], Cell[CellGroupData[{ Cell[47755, 1516, 70, 0, 65, "Outline1"], Cell[47828, 1518, 57, 0, 69, "Text"] }, Open ]], Cell[47900, 1521, 66, 0, 65, "Outline1"], Cell[47969, 1523, 57, 0, 65, "Outline1"] }, Open ]], Cell[48041, 1526, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[49745, 1574, 47, 0, 126, "Section"], Cell[49795, 1576, 332, 8, 110, "Text"], Cell[50130, 1586, 3107, 71, 365, "Input"], Cell[53240, 1659, 52, 0, 69, "Text"], Cell[53295, 1661, 2427, 54, 145, "Input"] }, Open ]], Cell[55737, 1718, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[57441, 1766, 33, 0, 126, "Section"], Cell[57477, 1768, 113, 3, 69, "Text"], Cell[57593, 1773, 93, 3, 69, "Text"], Cell[57689, 1778, 65, 0, 69, "Text"], Cell[57757, 1780, 49, 0, 69, "Text"], Cell[57809, 1782, 86, 1, 57, "Input"], Cell[57898, 1785, 43, 0, 69, "Text"], Cell[57944, 1787, 140, 3, 92, "Input"], Cell[58087, 1792, 857, 17, 340, "Input"], Cell[58947, 1811, 26, 0, 56, "Input"] }, Open ]], Cell[58988, 1814, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[60692, 1862, 49, 0, 126, "Section"], Cell[60744, 1864, 117, 3, 69, "Text"], Cell[60864, 1869, 28, 0, 69, "Text"], Cell[60895, 1871, 144, 2, 56, "Input"], Cell[61042, 1875, 423, 16, 57, "Input"], Cell[61468, 1893, 255, 4, 56, "Input"], Cell[61726, 1899, 29, 0, 69, "Text"], Cell[61758, 1901, 304, 7, 88, "Input"] }, Open ]], Cell[62077, 1911, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[63781, 1959, 30, 0, 126, "Section"], Cell[63814, 1961, 23, 0, 69, "Text"], Cell[63840, 1963, 85, 1, 57, "Input"], Cell[63928, 1966, 19, 0, 69, "Text"], Cell[63950, 1968, 309, 5, 92, "Input"], Cell[64262, 1975, 67, 0, 69, "Text"], Cell[64332, 1977, 147, 5, 69, "Text"], Cell[64482, 1984, 261, 8, 70, "Text"] }, Open ]], Cell[64758, 1995, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[66462, 2043, 36, 0, 126, "Section"], Cell[66501, 2045, 28, 0, 69, "Text"], Cell[66532, 2047, 119, 2, 70, "Input"], Cell[66654, 2051, 154, 6, 69, "Text"], Cell[66811, 2059, 102, 2, 57, "Input"] }, Open ]], Cell[66928, 2064, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[68632, 2112, 28, 0, 126, "Section"], Cell[68663, 2114, 222, 11, 69, "Text"], Cell[68888, 2127, 903, 18, 351, "Input"] }, Open ]], Cell[69806, 2148, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[71510, 2196, 50, 0, 126, "Section"], Cell[71563, 2198, 46, 0, 69, "Text"], Cell[CellGroupData[{ Cell[71634, 2202, 197, 4, 92, "Input"], Cell[71834, 2208, 128, 2, 53, "Output"] }, Open ]], Cell[71977, 2213, 76, 0, 69, "Text"], Cell[72056, 2215, 131, 2, 91, "Input"], Cell[72190, 2219, 49, 0, 69, "Text"], Cell[CellGroupData[{ Cell[72264, 2223, 332, 9, 56, "Input"], Cell[72599, 2234, 69, 1, 52, "Output"] }, Open ]], Cell[72683, 2238, 121, 4, 69, "Text"] }, Open ]], Cell[72819, 2245, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[74523, 2293, 31, 0, 126, "Section"], Cell[74557, 2295, 37, 0, 69, "Text"], Cell[74597, 2297, 64, 0, 69, "Text"], Cell[74664, 2299, 121, 3, 110, "Text"], Cell[74788, 2304, 38, 0, 69, "Text"], Cell[74829, 2306, 68, 0, 65, "Outline1"], Cell[74900, 2308, 77, 0, 65, "Outline1"], Cell[74980, 2310, 59, 0, 65, "Outline1"], Cell[75042, 2312, 49, 0, 65, "Outline1"], Cell[75094, 2314, 74, 0, 65, "Outline1"] }, Open ]], Cell[75183, 2317, 1679, 44, 22, "SlideShowNavigationBar", CellTags->"SlideShowHeader"], Cell[CellGroupData[{ Cell[76887, 2365, 29, 0, 126, "Section"], Cell[76919, 2367, 92, 3, 65, "Outline1"], Cell[77014, 2372, 77, 0, 65, "Outline1"], Cell[77094, 2374, 74, 0, 65, "Outline1"], Cell[77171, 2376, 93, 3, 65, "Outline1"], Cell[CellGroupData[{ Cell[77289, 2383, 64, 0, 65, "Outline1"], Cell[77356, 2385, 27, 0, 69, "Text"] }, Open ]], Cell[77398, 2388, 52, 0, 65, "Outline1"], Cell[77453, 2390, 46, 0, 65, "Outline1"], Cell[77502, 2392, 99, 3, 102, "Outline1"] }, Open ]] }, Open ]] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)