(* Content-type: application/vnd.wolfram.mathematica *) (*** Wolfram Notebook File ***) (* http://www.wolfram.com/nb *) (* CreatedBy='Mathematica 8.0' *) (*CacheID: 234*) (* Internal cache information: NotebookFileLineBreakTest NotebookFileLineBreakTest NotebookDataPosition[ 157, 7] NotebookDataLength[ 58050, 1404] NotebookOptionsPosition[ 13852, 441] NotebookOutlinePosition[ 55894, 1336] CellTagsIndexPosition[ 55373, 1318] WindowFrame->Normal*) (* Beginning of Notebook Content *) Notebook[{ Cell[CellGroupData[{ Cell["\<\ Simple Example from Set Theory\ \>", "Title", CellChangeTimes->{{3.616293145520181*^9, 3.616293147863456*^9}, { 3.623004338135836*^9, 3.62300434371999*^9}, {3.62300619670866*^9, 3.623006201026662*^9}}, CellID->795014953], Cell["Suppose we want to prove", "Text", CellChangeTimes->{{3.6161365624812*^9, 3.616136594446863*^9}, { 3.616278360000617*^9, 3.616278372769078*^9}, {3.616539840341612*^9, 3.616539848078095*^9}}, CellID->1098476306], Cell[BoxData[ FormBox[ RowBox[{ RowBox[{ RowBox[{"if", " ", "A"}], "\[SubsetEqual]", RowBox[{"B", ":", " ", RowBox[{"A", "\[Backslash]", "C"}]}]}], "=", RowBox[{"A", "\[Intersection]", RowBox[{"(", RowBox[{"B", "\[Backslash]", "C"}], ")"}]}]}], TraditionalForm]], "DisplayFormula", CellChangeTimes->{{3.605592266056245*^9, 3.605592320234824*^9}, { 3.605592694117099*^9, 3.60559269416293*^9}, 3.611996464064112*^9}, CellID->1336903145], Cell["\<\ In a first step, we need to introduce the set theoretic notions via \ definitions. (Once the set theory prover is ported from Theorema 1.0 to the \ new version, the definitions can be dropped since the prover will then \ recognize all set theory constructs \[Ellipsis])\ \>", "Text", CellChangeTimes->{{3.616310012600455*^9, 3.616310044058996*^9}, { 3.616310079181907*^9, 3.616310190483858*^9}, {3.616539876860092*^9, 3.616539961635605*^9}}, CellID->1576060680], Cell["", "OpenEnvironment", CellID->439790372], Cell[CellGroupData[{ Cell["Definition (Set Theory)", "EnvironmentHeader", CellFrameLabels->{{None, Cell[ BoxData[ ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Common`removeEnvironment[ ButtonNotebook[]]]]]}, {None, None}}, CellChangeTimes->{{3.616293173896672*^9, 3.616293181615853*^9}}, CellID->426252685], Cell[BoxData[ UnderscriptBox["\[ForAll]", RowBox[{"x", ",", "A", ",", "B"}]]], "GlobalDeclaration", ShowCellTags->False, CellChangeTimes->{{3.616293205953051*^9, 3.616293210936397*^9}}, CellTags->{ "ID:1197931704", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->1197931704], Cell[BoxData[ RowBox[{ RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"A", "\[SubsetEqual]", "B"}], TagBox[")", "AutoParentheses"]}], TagBox[ RowBox[{ ":", "\[NegativeThickSpace]\[NegativeThinSpace]", "\[DoubleLongLeftRightArrow]"}], Identity, SyntaxForm->"a\[DoubleLongLeftRightArrow]b"], RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{"x", "\[Element]", "A"}]], RowBox[{"x", "\[Element]", "B"}]}], TagBox[")", "AutoParentheses"]}]}]], "FormalTextInputFormula", CellFrameLabels->{{None, Cell[ BoxData[ RowBox[{ StyleBox["(\[SubsetEqual])", "FrameLabel"], " ", ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Language`Session`Private`removeFormula[{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/\ OneMoreTheorem.nb"}]]}]]]}, {None, None}}, ShowCellTags->False, CellChangeTimes->{ 3.616293190136777*^9, {3.616293226428041*^9, 3.61629327027252*^9}, 3.616296199526304*^9}, CellTags->{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[SubsetEqual]"}, CellID->1841163329], Cell[BoxData[ RowBox[{ RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"x", "\[Element]", RowBox[{"A", "\[Backslash]", "B"}]}], TagBox[")", "AutoParentheses"]}], TagBox[ RowBox[{ ":", "\[NegativeThickSpace]\[NegativeThinSpace]", "\[DoubleLongLeftRightArrow]"}], Identity, SyntaxForm->"a\[DoubleLongLeftRightArrow]b"], RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ RowBox[{"x", "\[Element]", "A"}], "\[And]", RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[Not]", RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"x", "\[Element]", "B"}], TagBox[")", "AutoParentheses"]}]}], TagBox[")", "AutoParentheses"]}]}], TagBox[")", "AutoParentheses"]}]}]], "FormalTextInputFormula", CellFrameLabels->{{None, Cell[ BoxData[ RowBox[{ StyleBox["(\\)", "FrameLabel"], " ", ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Language`Session`Private`removeFormula[{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/\ OneMoreTheorem.nb"}]]}]]]}, {None, None}}, ShowCellTags->False, CellChangeTimes->{{3.616293341498119*^9, 3.616293464461448*^9}}, CellTags->{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\\"}, CellID->790959835], Cell[BoxData[ RowBox[{ RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"x", "\[Element]", RowBox[{"A", "\[Intersection]", "B"}]}], TagBox[")", "AutoParentheses"]}], TagBox[ RowBox[{ ":", "\[NegativeThickSpace]\[NegativeThinSpace]", "\[DoubleLongLeftRightArrow]"}], Identity, SyntaxForm->"a\[DoubleLongLeftRightArrow]b"], RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ RowBox[{"x", "\[Element]", "A"}], "\[And]", RowBox[{"x", "\[Element]", "B"}]}], TagBox[")", "AutoParentheses"]}]}]], "FormalTextInputFormula", CellFrameLabels->{{None, Cell[ BoxData[ RowBox[{ StyleBox["(\[Intersection])", "FrameLabel"], " ", ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Language`Session`Private`removeFormula[{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/\ OneMoreTheorem.nb"}]]}]]]}, {None, None}}, ShowCellTags->False, CellChangeTimes->{{3.616293513244295*^9, 3.616293569917513*^9}}, CellTags->{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[Intersection]"}, CellID->1252989057], Cell["\[GraySquare]", "EndEnvironmentMarker", CellID->1529780747] }, Open ]], Cell["", "CloseEnvironment", CellID->1563925829], Cell["", "OpenEnvironment", CellID->834846774], Cell[CellGroupData[{ Cell["Theorem (Diff / Inter)", "EnvironmentHeader", CellFrameLabels->{{None, Cell[ BoxData[ ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Common`removeEnvironment[ ButtonNotebook[]]]]]}, {None, None}}, CellChangeTimes->{{3.616293640645581*^9, 3.616293649068387*^9}}, CellID->865240769], Cell[BoxData[ UnderscriptBox["\[ForAll]", RowBox[{"A", ",", "B", ",", "C", ",", "x"}]]], "GlobalDeclaration", ShowCellTags->False, CellChangeTimes->{{3.612005990888099*^9, 3.612005993876964*^9}, { 3.616294352151859*^9, 3.616294352184887*^9}, {3.616294691917154*^9, 3.616294700859024*^9}, {3.61629502292695*^9, 3.616295035538314*^9}}, CellTags->{ "ID:862730946", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->862730946], Cell[BoxData[ RowBox[{ RowBox[{"A", "\[SubsetEqual]", "B"}], "\[Implies]", RowBox[{ RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"x", "\[Element]", RowBox[{"A", "\[Backslash]", "C"}]}], TagBox[")", "AutoParentheses"]}], "\[DoubleLongLeftRightArrow]", RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"x", "\[Element]", RowBox[{"A", "\[Intersection]", RowBox[{"(", RowBox[{"B", "\[Backslash]", "C"}], ")"}]}]}], TagBox[")", "AutoParentheses"]}]}]}]], "FormalTextInputFormula", CellFrameLabels->{{None, Cell[ BoxData[ RowBox[{ StyleBox["(2)", "FrameLabel"], " ", ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Language`Session`Private`removeFormula[{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/\ OneMoreTheorem.nb"}]]}]]]}, {None, None}}, ShowCellTags->False, CellChangeTimes->{{3.616293679552341*^9, 3.616293821276466*^9}, { 3.616295026467793*^9, 3.616295030660417*^9}}, CellTags->{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "2"}, CellID->501871624], Cell["\[GraySquare]", "EndEnvironmentMarker", CellID->905092664] }, Open ]], Cell["", "CloseEnvironment", CellID->986882933], Cell[CellGroupData[{ Cell[TextData[{ Cell[BoxData[ StyleBox["\<\"\[CheckmarkedBox]\"\>", StripOnInput->False, ShowStringCharacters->False]]], " Proof of ", Cell[BoxData[ ButtonBox[ TagBox[ TooltipBox[ PaneSelectorBox[{False-> StyleBox["\<\"(2)\"\>", "FormReference", StripOnInput->False], True-> StyleBox["\<\"(2)\"\>", "FormReferenceHover", StripOnInput->False]}, Dynamic[ CurrentValue["MouseOver"]], FrameMargins->0, ImageSize->Automatic], TagBox[ FormBox[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["A", "ExpressionVariable"], ",", StyleBox["B", "ExpressionVariable"], ",", StyleBox["C", "ExpressionVariable"], ",", StyleBox["x", "ExpressionVariable"]}]], RowBox[{ RowBox[{ StyleBox["A", "ExpressionVariable"], "\[SubsetEqual]", StyleBox["B", "ExpressionVariable"]}], "\[Implies]", RowBox[{ RowBox[{"(", RowBox[{ StyleBox["x", "ExpressionVariable"], "\[Element]", RowBox[{ StyleBox["A", "ExpressionVariable"], "\[Backslash]", StyleBox["C", "ExpressionVariable"]}]}], ")"}], "\[DoubleLeftRightArrow]", RowBox[{"(", RowBox[{ StyleBox["x", "ExpressionVariable"], "\[Element]", RowBox[{ StyleBox["A", "ExpressionVariable"], "\[Intersection]", RowBox[{ StyleBox["B", "ExpressionVariable"], "\[Backslash]", StyleBox["C", "ExpressionVariable"]}]}]}], ")"}]}]}]}], TheoremaForm], DisplayForm]], Annotation[#, DisplayForm[ FormBox[ RowBox[{ UnderscriptBox["\[ForAll]", RowBox[{ StyleBox["A", "ExpressionVariable"], ",", StyleBox["B", "ExpressionVariable"], ",", StyleBox["C", "ExpressionVariable"], ",", StyleBox["x", "ExpressionVariable"]}]], RowBox[{ RowBox[{ StyleBox["A", "ExpressionVariable"], "\[SubsetEqual]", StyleBox["B", "ExpressionVariable"]}], "\[Implies]", RowBox[{ RowBox[{"(", RowBox[{ StyleBox["x", "ExpressionVariable"], "\[Element]", RowBox[{ StyleBox["A", "ExpressionVariable"], "\[Backslash]", StyleBox["C", "ExpressionVariable"]}]}], ")"}], "\[DoubleLeftRightArrow]", RowBox[{"(", RowBox[{ StyleBox["x", "ExpressionVariable"], "\[Element]", RowBox[{ StyleBox["A", "ExpressionVariable"], "\[Intersection]", RowBox[{ StyleBox["B", "ExpressionVariable"], "\[Backslash]", StyleBox["C", "ExpressionVariable"]}]}]}], ")"}]}]}]}], TheoremaForm]], "Tooltip"]& ], Appearance->None, ButtonFunction:>NotebookLocate["ID:501871624"], Evaluator->Automatic, Method->"Preemptive"]]], " #1: ", Cell[BoxData[ ButtonBox[ StyleBox["\<\"Show proof\"\>", StripOnInput->False, FontVariations->{"Underline"->True}], Appearance->None, ButtonFunction:>Theorema`Common`displayProof[ ToExpression[ "FileNameJoin[{CurrentValue[\"NotebookDirectory\"], \ FileBaseName[CurrentValue[\"NotebookFileName\"]], \"p501871624-1-po.m\"}]"]], Evaluator->Automatic, ImageSize->Automatic, Method->"Queued"]]] }], "ProofInfo", CellFrameLabels->{{None, Cell[ BoxData[ ButtonBox[ "\[Times]", Evaluator -> Automatic, Appearance -> None, ButtonFunction :> Theorema`Interface`GUI`Private`removeGroup[ ButtonNotebook[], "p501871624-1"]]]]}, {None, None}}, CellTags->{"Proof|ID:501871624", "Proof|ID:501871624-1"}, CellID->1659692279], Cell[BoxData[ DynamicBox[ToBoxes[ Refresh[ ReplaceAll[ Get[ ToExpression[ "FileNameJoin[{CurrentValue[\"NotebookDirectory\"], \ FileBaseName[CurrentValue[\"NotebookFileName\"]], \ \"p501871624-1-display.m\"}]"]], Theorema`Interface`GUI`Private`FORM -> Theorema`Interface`GUI`Private`displayFormulaFromKey], TrackedSymbols :> {Theorema`Common`$tmaEnv}], StandardForm], ImageSizeCache->{770., {32., 40.}}]], "ProofInfoBody", CellID->1129186913] }, Closed]] }, Open ]] }, WindowSize->{860, 998}, WindowMargins->{{-2, Automatic}, {Automatic, -10}}, Magnification->1.5 Inherited, FrontEndVersion->"8.0 for Linux x86 (32-bit) (February 23, 2011)", StyleDefinitions->Notebook[{ Cell[ StyleData[ StyleDefinitions -> FrontEnd`FileName[{"Theorema"}, "TheoremaCore.nb"]]], Cell["Modify the definitions below to change the default appearance of all \ cells in a given style. \nMake modifications to any definition using commands \ in the Format menu.", "Text"], Cell[ CellGroupData[{ Cell["Notebook Options Settings", "Section"], Cell[ "The options defined for the style below will be used at the Notebook \ level.", "Text"], Cell[ CellGroupData[{ Cell[ StyleData["Notebook"], InputAliases -> {"and" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ "\[SelectionPlaceholder]", "\[And]", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "or" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", "\[Or]", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "not" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[Not]", "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "impl" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ "\[SelectionPlaceholder]", "\[Implies]", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "equiv" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ "\[SelectionPlaceholder]", "\[DoubleLongLeftRightArrow]", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "eq" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ "\[SelectionPlaceholder]", "\[Equal]", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], ":equiv" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", TagBox[ RowBox[{ ":", "\[NegativeThickSpace]\[NegativeThinSpace]", "\[DoubleLongLeftRightArrow]"}], Identity, SyntaxForm -> "a\[DoubleLongLeftRightArrow]b"], "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], ":eq" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", ":=", "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "andn" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[And]", "\[Piecewise]", GridBox[{{"\[SelectionPlaceholder]"}, {"\[Placeholder]"}}, ColumnAlignments -> Left]}], TagBox[")", "AutoParentheses"]}], "orn" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[Or]", "\[Piecewise]", GridBox[{{"\[SelectionPlaceholder]"}, {"\[Placeholder]"}}, ColumnAlignments -> Left]}], TagBox[")", "AutoParentheses"]}], "equivn" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[DoubleLeftRightArrow]", "\[Piecewise]", GridBox[{{"\[SelectionPlaceholder]"}, {"\[Placeholder]"}}]}], TagBox[")", "AutoParentheses"]}], "cdist" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[Piecewise]", GridBox[{{ "\[SelectionPlaceholder]", "\[DoubleLeftArrow]", "\[Placeholder]"}, { "\[Placeholder]", "\[DoubleLeftArrow]", "\[Placeholder]"}}]}], TagBox[")", "AutoParentheses"]}], "far" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox["\[ForAll]", "\[Placeholder]"], "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "exr" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox["\[Exists]", "\[Placeholder]"], "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "farc" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox[ UnderscriptBox["\[ForAll]", "\[Placeholder]"], "\[Placeholder]"], "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "exrc" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox[ UnderscriptBox["\[Exists]", "\[Placeholder]"], "\[Placeholder]"], "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "let" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ UnderscriptBox["let", RowBox[{"\[Placeholder]", "=", "\[Placeholder]"}]], "\[SelectionPlaceholder]"}], TagBox[")", "AutoParentheses"]}], "app" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", TagBox["\:293a", Identity, SyntaxForm -> "a*b"], "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "prep" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", TagBox["\:293b", Identity, SyntaxForm -> "a*b"], "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "join" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", TagBox["\:22c8", Identity, SyntaxForm -> "a*b"], "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "elemT" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{"\[SelectionPlaceholder]", TagBox["\:22ff", Identity, SyntaxForm -> "a+b"], "\[Placeholder]"}], TagBox[")", "AutoParentheses"]}], "subop" -> RowBox[{ TagBox["(", "AutoParentheses"], SubscriptBox["\[SelectionPlaceholder]", "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "supop" -> RowBox[{ TagBox["(", "AutoParentheses"], SuperscriptBox["\[SelectionPlaceholder]", "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "subsupop" -> RowBox[{ TagBox["(", "AutoParentheses"], SubsuperscriptBox[ "\[SelectionPlaceholder]", "\[Placeholder]", "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "oop" -> RowBox[{ TagBox["(", "AutoParentheses"], OverscriptBox["\[SelectionPlaceholder]", "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "uoop" -> RowBox[{ TagBox["(", "AutoParentheses"], UnderoverscriptBox[ "\[SelectionPlaceholder]", "\[Placeholder]", "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "osop" -> RowBox[{ TagBox["(", "AutoParentheses"], SubscriptBox[ OverscriptBox["\[SelectionPlaceholder]", "\[Placeholder]"], "\[Placeholder]"], TagBox[")", "AutoParentheses"]}], "op" -> RowBox[{ TagBox["(", "AutoParentheses"], TagBox["\[SelectionPlaceholder]", Identity], TagBox[")", "AutoParentheses"]}], "[]" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:e114", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:e115", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "()" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:fd3e", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:fd3f", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "<>" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:27e8", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:27e9", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "{}" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:e117", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:e118", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "[[]]" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:27e6", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:27e7", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "(())" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:2e28", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:2e29", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "<<>>" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:27ea", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:27eb", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "{{}}" -> RowBox[{ TagBox["(", "AutoParentheses"], RowBox[{ TagBox["\:2983", Identity, SyntaxForm -> "("], "\[SelectionPlaceholder]", TagBox["\:2984", Identity, SyntaxForm -> ")"]}], TagBox[")", "AutoParentheses"]}], "(" -> TagBox["(", "AutoParentheses"], ")" -> TagBox[")", "AutoParentheses"]}, Background -> RGBColor[0.957, 0.96, 0.97]], Cell[ StyleData["Notebook", "Printout"], Background -> None]}, Open]]}, Open]], Cell[ CellGroupData[{ Cell["Style Environment Names", "Section"], Cell[ StyleData[All, "Working"], DockedCells -> { Cell[ "Theorema 2.0", "SBO", FontTracking -> 8, CellMargins -> {{0, 0}, {0, 0}}, CellFrameMargins -> {{0, 50}, {0, 0}}, FontSize -> 28, FontSlant -> "Plain", FontColor -> RGBColor[0.29, 0.46, 0.6], TextAlignment -> Right, Background -> RGBColor[0.36, 0.54, 0.69]]}], Cell[ StyleData[ All, "Layout", StyleDefinitions -> StyleData[All, "Working"]], MenuSortingValue -> 1200]}, Open]], Cell[ CellGroupData[{ Cell["Styles for Title and Section Cells", "Section"], Cell[ CellGroupData[{ Cell["Title", "Subsection"], Cell[ CellGroupData[{ Cell[ StyleData["Title"], CellMargins -> {{27, 27}, {10, 30}}, TextAlignment -> Center, MenuSortingValue -> 1100, MenuCommandKey -> "1", FontFamily -> "Bitstream Charter", FontSize -> 36, FontWeight -> "Bold", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.23, 0.25, 0.34]], Cell[ StyleData["Title", "Printout"], ShowGroupOpener -> False, CellMargins -> {{6, 10}, {5, 30}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Subtitle"], CellMargins -> {{27, 27}, {20, 2}}, TextAlignment -> Center, MenuSortingValue -> 1150, FontFamily -> "Bitstream Charter", FontSize -> 24, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.23, 0.25, 0.34]], Cell[ StyleData["Subtitle", "Printout"], CellMargins -> {{6, 10}, {5, 0}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Subsubtitle"], CellMargins -> {{27, 27}, {8, 2}}, TextAlignment -> Center, MenuSortingValue -> 1200, FontFamily -> "Bitstream Charter", FontSize -> 16, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.23, 0.25, 0.34]], Cell[ StyleData["Subsubtitle", "Printout"], CellMargins -> {{6, 10}, {0, 0}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Author"], CellMargins -> {{27, 27}, {18, 20}}, TextAlignment -> Center, MenuSortingValue -> 1200, FontFamily -> "Bitstream Charter", FontSize -> 16, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.23, 0.25, 0.34]], Cell[ StyleData["Subsubtitle", "Printout"], CellMargins -> {{6, 10}, {0, 0}}]}, Closed]]}, Closed]], Cell[ CellGroupData[{ Cell["Sectioning", "Subsection"], Cell[ CellGroupData[{ Cell[ StyleData["Section"], ShowGroupOpener -> True, MenuSortingValue -> 1250, MenuCommandKey -> "4", FontFamily -> "Bitstream Charter", FontSize -> 20, FontWeight -> "Bold", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.3, 0.3, 0.3]], Cell[ StyleData["Section", "Printout"], ShowGroupOpener -> False, CellMargins -> {{2, 0}, {7, 22}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Subsection"], CellDingbat -> None, ShowGroupOpener -> True, CellMargins -> {{27, Inherited}, {8, 12}}, MenuSortingValue -> 1300, MenuCommandKey -> "5", FontFamily -> "Bitstream Charter", FontSize -> 14, FontWeight -> "Bold", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.3, 0.3, 0.3]], Cell[ StyleData["Subsection", "Printout"], ShowGroupOpener -> False, CellMargins -> {{9, 0}, {7, 22}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Subsubsection"], CellDingbat -> None, ShowGroupOpener -> True, CellMargins -> {{27, Inherited}, {2, 10}}, MenuSortingValue -> 1350, MenuCommandKey -> "6", FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Bold", FontSlant -> "Italic", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.4, 0.4, 0.4]], Cell[ StyleData["Subsubsection", "Printout"], ShowGroupOpener -> False, CellMargins -> {{35, 0}, {7, 14}}]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Subsubsubsection"], CellDingbat -> None, ShowGroupOpener -> True, CellMargins -> {{27, Inherited}, {Inherited, Inherited}}, FontFamily -> "Bitstream Charter", FontSize -> 11, FontWeight -> "Bold", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.4, 0.4, 0.4]], Cell[ StyleData["Subsubsubsection", "Printout"], CellMargins -> {{50, 0}, {7, 14}}]}, Closed]]}, Open]]}, Open]], Cell[ CellGroupData[{ Cell["Styles for Publication\[Hyphen]ready Documents", "Section"], Cell[ CellGroupData[{ Cell[ StyleData["Author"], CellMargins -> {{27, 30}, {20, 5}}, MenuSortingValue -> 1900, FontFamily -> "Helvetica", FontSize -> 14, FontSlant -> "Italic"], Cell[ StyleData["Author", "Printout"], CellMargins -> {{6, 10}, {0, 10}}, FontSize -> 10]}, Closed]], Cell[ CellGroupData[{ Cell[ StyleData["Abstract"], CellFrame -> {{0, 0}, {0.5, 0.5}}, CellMargins -> {{27, 140}, {20, 20}}, LineSpacing -> {0.9, 0}, MenuSortingValue -> 2050, FontFamily -> "Times", FontSize -> 12], Cell[ StyleData["Abstract", "Printout"], Hyphenation -> True, LineSpacing -> {1, 2}, FontSize -> 10]}, Closed]]}, Closed]], Cell[ CellGroupData[{ Cell["Text", "Section"], Cell[ StyleData["Text"], CellMargins -> {{27, 27}, {Inherited, Inherited}}, TextJustification -> 1., ParagraphIndent -> 15, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> False}], Cell[ StyleData["EnvironmentText"], ShowCellBracket -> Automatic, CellMargins -> {{82, Inherited}, {Inherited, Inherited}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, TextJustification -> 1., ParagraphSpacing -> {0.3, 0.}, MenuSortingValue -> 1480, MenuCommandKey -> "T", FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> False}], Cell[ CellGroupData[{ Cell[ StyleData["Item"], CellDingbat -> Cell["\[FilledSmallCircle]", FontWeight -> "Bold"], CellMargins -> {{81, 10}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15000}, CellFrameLabelMargins -> 4, CounterIncrements -> "Item", CounterAssignments -> {{"Subitem", 0}, {"Subsubitem", 0}}, MenuSortingValue -> 1600, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["Item", "Presentation"], CellMargins -> {{140, 10}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["ItemParagraph"], CellMargins -> {{81, 10}, {4, 1}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15000}, DefaultNewCellStyle -> "Item", MenuSortingValue -> 1600, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["ItemParagraph", "Presentation"], CellMargins -> {{140, 10}, {7, 2}}, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["Subitem"], CellDingbat -> Cell["\[FilledSmallCircle]", FontWeight -> "Bold"], CellMargins -> {{105, 12}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15100}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "Item", CounterIncrements -> "Subitem", CounterAssignments -> {{"Subsubitem", 0}}, MenuSortingValue -> 1610, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["Subitem", "Presentation"], CellMargins -> {{176, 12}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["SubitemParagraph"], CellMargins -> {{105, 12}, {4, 1}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15100}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "Subitem", MenuSortingValue -> 1610, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["SubitemParagraph", "Presentation"], CellMargins -> {{176, 12}, {7, 2}}, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["Subsubitem"], CellDingbat -> Cell["\[FilledSmallCircle]", FontWeight -> "Bold"], CellMargins -> {{129, 12}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15200}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "Subsubitem", CounterIncrements -> "Subsubitem", MenuSortingValue -> 1620, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["Subsubitem", "Presentation"], CellMargins -> {{212, 12}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["SubsubitemParagraph"], CellMargins -> {{129, 12}, {4, 1}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15200}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "Subsubitem", CounterIncrements -> "Subsubitem", MenuSortingValue -> 1625, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["SubsubitemParagraph", "Presentation"], CellMargins -> {{212, 12}, {7, 2}}, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["ItemNumbered"], CellDingbat -> Cell[ TextData[{ CounterBox["ItemNumbered"], "."}], FontWeight -> "Bold"], CellMargins -> {{81, 10}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15000}, CellFrameLabelMargins -> 4, CounterIncrements -> "ItemNumbered", CounterAssignments -> {{"SubitemNumbered", 0}, { "SubsubitemNumbered", 0}}, MenuSortingValue -> 1630, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["ItemNumbered", "Presentation"], CellMargins -> {{140, 10}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["SubitemNumbered"], CellDingbat -> Cell[ TextData[{ CounterBox["ItemNumbered"], ".", CounterBox["SubitemNumbered"], "."}], FontWeight -> "Bold"], CellMargins -> {{105, 12}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15100}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "Item", CounterIncrements -> "SubitemNumbered", CounterAssignments -> {{"SubsubitemNumbered", 0}}, MenuSortingValue -> 1640, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["SubitemNumbered", "Presentation"], CellMargins -> {{176, 12}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["SubsubitemNumbered"], CellDingbat -> Cell[ TextData[{ CounterBox["ItemNumbered"], ".", CounterBox["SubitemNumbered"], ".", CounterBox["SubsubitemNumbered"], "."}], FontWeight -> "Bold"], CellMargins -> {{129, 12}, {4, 4}}, CellGroupingRules -> {"GroupTogetherNestedGrouping", 15200}, CellFrameLabelMargins -> 4, DefaultNewCellStyle -> "SubitemNumbered", CounterIncrements -> "SubsubitemNumbered", MenuSortingValue -> 1645, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> { "StrikeThrough" -> False, "Underline" -> False}, $CellContext`ReturnCreatesNewCell -> True], Cell[ StyleData["SubsubitemNumbered", "Presentation"], CellMargins -> {{212, 12}, {7, 7}}, CellFrameLabelMargins -> 6, FontSize -> 24]}, Open]]}, Open]], Cell[ CellGroupData[{ Cell["Theorema", "Section"], Cell[ StyleData["GlobalDeclaration"], CellFrame -> {{0, 2}, {0, 0}}, ShowCellBracket -> Automatic, CellMargins -> {{76, 10}, {2, 2}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, InitializationCell -> True, CellFrameMargins -> 10, CellFrameColor -> RGBColor[0.73, 0.65, 0.61], CellFrameLabelMargins -> 33, ShowAutoStyles -> False, MenuSortingValue -> 1441, MenuCommandKey -> "G", FontSize -> 14], Cell[ StyleData["OpenEnvironment"], Editable -> False, Selectable -> False, CellFrame -> {{False, False}, {True, False}}, ShowCellBracket -> True, CellMargins -> {{76, 6}, {-4, Inherited}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellFrameMargins -> 2, CellFrameColor -> RGBColor[0.4, 0.4, 0.4], MenuSortingValue -> 1485], Cell[ StyleData["EnvironmentHeader"], CellFrame -> {{False, False}, {False, False}}, CellMargins -> {{76, Inherited}, {Inherited, Inherited}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellFrameMargins -> 6, CellFrameColor -> RGBColor[0.4, 0.4, 0.4], ShowAutoStyles -> False, MenuSortingValue -> 1450, FontSize -> 14, FontWeight -> "Bold", FontVariations -> {"CapsType" -> "SmallCaps"}, Background -> RGBColor[0.89, 0.8, 0.69]], Cell[ CellGroupData[{ Cell[ StyleData["FormalTextInputFormula"], ShowCellBracket -> Automatic, CellMargins -> {{96, 10}, {2, 2}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, InitializationCell -> True, CellFrameLabelMargins -> 53, ShowAutoStyles -> False, LimitsPositioningTokens -> {}, MenuSortingValue -> 1470, MenuCommandKey -> "F", FontWeight -> "Bold", FontColor -> RGBColor[0.25, 0.19, 0.2]], Cell[ StyleData["FormalTextInputFormula", "Layout"], Editable -> False], Cell[ StyleData["FormalTextInputFormula", "Presentation"], Editable -> False]}, Open]], Cell[ StyleData["EndEnvironmentMarker"], CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, TextAlignment -> Right, MenuSortingValue -> 1480], Cell[ StyleData["CloseEnvironment"], Editable -> False, Selectable -> False, CellFrame -> {{False, False}, {False, True}}, ShowCellBracket -> True, CellMargins -> {{76, 6}, {Inherited, 0}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellFrameMargins -> 2, CellFrameColor -> RGBColor[0.4, 0.4, 0.4], MenuSortingValue -> 1485], Cell[ CellGroupData[{ Cell[ StyleData["Computation"], CellFrame -> {{1.5, 0}, {0, 0}}, ShowCellBracket -> Automatic, CellMargins -> {{76, 10}, {0, 7}}, CellBracketOptions -> {"Color" -> RGBColor[0.23, 0.25, 0.34]}, CellFrameMargins -> {{8, 8}, {3, 4}}, CellFrameColor -> RGBColor[0.486, 0.33, 0.32], ShowAutoStyles -> False, MenuSortingValue -> 1510, MenuCommandKey -> "C", FontWeight -> "Bold", FontColor -> RGBColor[0.23, 0.25, 0.34], Background -> RGBColor[0.88, 0.88, 0.92]], Cell[ StyleData["Computation", "Layout"], Editable -> False], Cell[ StyleData["Computation", "Presentation"], Editable -> False]}, Open]], Cell[ StyleData["ComputationResult"], CellFrame -> {{1.5, 0}, {0, 0}}, ShowCellBracket -> Automatic, CellMargins -> {{76, 10}, {0, 0}}, CellBracketOptions -> {"Color" -> RGBColor[0.23, 0.25, 0.34]}, CellFrameMargins -> {{8, 8}, {4, 3}}, CellFrameColor -> RGBColor[0.486, 0.33, 0.32], StyleMenuListing -> None, FontColor -> RGBColor[0.23, 0.25, 0.34], Background -> RGBColor[0.88, 0.88, 0.92]], Cell[ StyleData["ComputationInfo"], ShowCellBracket -> False, CellMargins -> {{120, 10}, {10, 2}}, StyleMenuListing -> None, FontFamily -> $CellContext`Arial], Cell[ StyleData["ComputationInfoBody"], ShowCellBracket -> False, CellMargins -> {{144, 10}, {10, 2}}, StyleMenuListing -> None], Cell[ StyleData["ProofInfo"], ShowCellBracket -> False, CellMargins -> {{76, 10}, {6, 6}}, CellFrameLabelMargins -> 15, StyleMenuListing -> None, FontFamily -> "Arial"], Cell[ StyleData["ProofInfoBody"], ShowCellBracket -> False, CellMargins -> {{100, 10}, {0, 0}}, StyleMenuListing -> None], Cell[ CellGroupData[{ Cell[ StyleData["FrameLabel"], LanguageCategory -> None, StyleMenuListing -> None, FontFamily -> "Times New Roman", FontSize -> 10, FontWeight -> "Plain", FontSlant -> "Italic", FontTracking -> "Plain", FontVariations -> { "Masked" -> False, "Outline" -> False, "Shadow" -> False, "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.55, 0.44, 0.42], Background -> None], Cell[ StyleData["FrameLabel", "Printout"]]}, Open]], Cell[ StyleData["OpenArchive"], CellFrame -> {{False, False}, {False, True}}, ShowCellBracket -> Automatic, CellMargins -> {{70, 70}, {0, 10}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellGroupingRules -> {"SectionGrouping", 20}, CellFrameMargins -> 3, CellFrameColor -> RGBColor[0.4, 0.4, 0.4], CellFrameLabelMargins -> 1, DefaultFormatType -> DefaultInputFormatType, ShowAutoStyles -> False, MenuSortingValue -> 1210, FontWeight -> Bold, Background -> RGBColor[0.73, 0.74, 0.84]], Cell[ StyleData["ArchiveInfo"], ShowCellBracket -> Automatic, CellMargins -> {{70, 70}, {0, 0}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellFrameMargins -> 5, CellFrameLabelMargins -> 3, ShowCellTags -> False, ShowAutoStyles -> False, MenuSortingValue -> 1220, FontWeight -> "Bold", Background -> RGBColor[0.88, 0.88, 0.92]], Cell[ StyleData["CloseArchive"], CellFrame -> {{False, False}, {True, False}}, ShowCellBracket -> Automatic, CellMargins -> {{0, 0}, {5, 10}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellGroupingRules -> {"SectionGrouping", 25}, CellFrameMargins -> 2, CellFrameColor -> RGBColor[0.4, 0.4, 0.4], TextAlignment -> Center, MenuSortingValue -> 1230, FontFamily -> "Arial Black", FontSize -> 24, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> False}, Background -> RGBColor[0.73, 0.65, 0.61]], Cell[ StyleData["IncludeArchive"], CellFrame -> {{4, 0}, {False, False}}, ShowCellBracket -> Automatic, CellMargins -> {{81, 100}, {Inherited, Inherited}}, CellBracketOptions -> {"Color" -> RGBColor[0.73, 0.74, 0.84]}, CellFrameColor -> RGBColor[0.55, 0.44, 0.42], CellFrameLabels -> {{"\[RightSkeleton]", None}, {None, None}}, CellFrameLabelMargins -> 25, MenuSortingValue -> 1445], Cell[ StyleData["ExpressionVariable"], SingleLetterItalics -> True, MultiLetterItalics -> True, FontColor -> RGBColor[0.29, 0.46, 0.6]], Cell[ StyleData["ExpressionABF"], SingleLetterItalics -> True, MultiLetterItalics -> True, FontColor -> RGBColor[0.29, 0.46, 0.6]], Cell[ StyleData["ExpressionMeta"], SingleLetterItalics -> True, MultiLetterItalics -> True, FontColor -> RGBColor[0.29, 0.46, 0.6]], Cell[ CellGroupData[{ Cell[ StyleData["AutoParentheses"], SpanMaxSize -> 3, FontOpacity -> 0.15], Cell[ StyleData["AutoParentheses", "Layout"], FontOpacity -> 0], Cell[ StyleData["AutoParentheses", "SlideShow"], FontOpacity -> 0]}, Open]], Cell[ CellGroupData[{ Cell[ StyleData["Emphasized"], MenuCommandKey -> "E", FontSlant -> "Italic"], Cell[ StyleData["Emphasized", "SlideShow"], FontSlant -> "Plain", FontColor -> RGBColor[0.36, 0.54, 0.69]]}, Open]], Cell[ StyleData["GenericButton"], FontFamily -> "Bitstream Charter", FontWeight -> "Plain", FontSlant -> "Italic", FontTracking -> "Plain", FontVariations -> { "Masked" -> False, "Outline" -> False, "Shadow" -> False, "StrikeThrough" -> False, "Underline" -> False}, FontColor -> RGBColor[0.23, 0.25, 0.34]], Cell[ StyleData["TheoremaForm"], "TwoByteSyntaxCharacterAutoReplacement" -> True, LineSpacing -> {1.25, 0, 2}, SingleLetterItalics -> True, StyleMenuListing -> None, FontFamily -> "Courier"], Cell[ StyleData["ComponentActive"], FontFamily -> "Times New Roman"], Cell[ StyleData["ComponentInactive"], FontFamily -> "Times New Roman", FontOpacity -> 0.4], Cell[ StyleData["ComponentEmpty"], FontFamily -> "Times New Roman", FontVariations -> {"StrikeThrough" -> True}], Cell[ StyleData["TabView"], FontFamily -> "Times New Roman", FontSize -> 10], Cell[ StyleData["TabViewLabel"], FontFamily -> "Times New Roman", FontSize -> 10, FontWeight -> "Bold"], Cell[ StyleData["FormReference", StyleDefinitions -> StyleData["Text"]], FontFamily -> "Times New Roman", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> False}], Cell[ StyleData["FormReferenceHover", StyleDefinitions -> StyleData["Text"]], FontFamily -> "Times New Roman", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> True}, FontColor -> RGBColor[0.404, 0.43, 0.545]], Cell[ StyleData["DisplayFormula"], CellMargins -> {{36, 6}, {7, 7}}, ConversionRules :> { "HTML" -> {{"", ""}, {"

", "

"}}}, CellHorizontalScrolling -> True, DefaultFormatType -> TraditionalForm, InputAutoReplacements -> {}, TextAlignment -> Center, FontFamily -> "Bitstream Charter", FontSize -> 12, FontWeight -> "Plain", FontSlant -> "Plain", FontVariations -> {"StrikeThrough" -> False, "Underline" -> False}, ButtonBoxOptions -> {Appearance -> {Automatic, None}}]}, Open]]}, Visible -> False, FrontEndVersion -> "8.0 for Linux x86 (32-bit) (February 23, 2011)", StyleDefinitions -> "StylesheetFormatting.nb"] ] (* End of Notebook Content *) (* Internal cache information *) (*CellTagsOutline CellTagsIndex->{ "ID:1197931704"->{ Cell[2459, 80, 323, 8, 44, "GlobalDeclaration", CellTags->{ "ID:1197931704", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->1197931704]}, "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"->{ Cell[2459, 80, 323, 8, 44, "GlobalDeclaration", CellTags->{ "ID:1197931704", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->1197931704], Cell[2785, 90, 1310, 43, 42, "FormalTextInputFormula", CellTags->{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[SubsetEqual]"}, CellID->1841163329], Cell[4098, 135, 1485, 52, 32, "FormalTextInputFormula", CellTags->{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\\"}, CellID->790959835], Cell[5586, 189, 1272, 41, 32, "FormalTextInputFormula", CellTags->{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[Intersection]"}, CellID->1252989057], Cell[7444, 255, 474, 10, 44, "GlobalDeclaration", CellTags->{ "ID:862730946", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->862730946], Cell[7921, 267, 1265, 39, 32, "FormalTextInputFormula", CellTags->{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "2"}, CellID->501871624]}, "ID:1841163329"->{ Cell[2785, 90, 1310, 43, 42, "FormalTextInputFormula", CellTags->{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[SubsetEqual]"}, CellID->1841163329]}, "\[SubsetEqual]"->{ Cell[2785, 90, 1310, 43, 42, "FormalTextInputFormula", CellTags->{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[SubsetEqual]"}, CellID->1841163329]}, "ID:790959835"->{ Cell[4098, 135, 1485, 52, 32, "FormalTextInputFormula", CellTags->{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\\"}, CellID->790959835]}, "\\"->{ Cell[4098, 135, 1485, 52, 32, "FormalTextInputFormula", CellTags->{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\\"}, CellID->790959835]}, "ID:1252989057"->{ Cell[5586, 189, 1272, 41, 32, "FormalTextInputFormula", CellTags->{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[Intersection]"}, CellID->1252989057]}, "\[Intersection]"->{ Cell[5586, 189, 1272, 41, 32, "FormalTextInputFormula", CellTags->{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[Intersection]"}, CellID->1252989057]}, "ID:862730946"->{ Cell[7444, 255, 474, 10, 44, "GlobalDeclaration", CellTags->{ "ID:862730946", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->862730946]}, "ID:501871624"->{ Cell[7921, 267, 1265, 39, 32, "FormalTextInputFormula", CellTags->{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "2"}, CellID->501871624]}, "2"->{ Cell[7921, 267, 1265, 39, 32, "FormalTextInputFormula", CellTags->{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "2"}, CellID->501871624]}, "Proof|ID:501871624"->{ Cell[9342, 317, 3998, 106, 44, "ProofInfo", CellTags->{"Proof|ID:501871624", "Proof|ID:501871624-1"}, CellID->1659692279]}, "Proof|ID:501871624-1"->{ Cell[9342, 317, 3998, 106, 44, "ProofInfo", CellTags->{"Proof|ID:501871624", "Proof|ID:501871624-1"}, CellID->1659692279]} } *) (*CellTagsIndex CellTagsIndex->{ {"ID:1197931704", 51436, 1204}, {"Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", \ 51705, 1210}, {"ID:1841163329", 52971, 1245}, {"\[SubsetEqual]", 53215, 1252}, {"ID:790959835", 53457, 1259}, {"\\", 53676, 1266}, {"ID:1252989057", 53906, 1273}, {"\[Intersection]", 54153, 1280}, {"ID:862730946", 54397, 1287}, {"ID:501871624", 54608, 1293}, {"2", 54825, 1300}, {"Proof|ID:501871624", 55059, 1307}, {"Proof|ID:501871624-1", 55218, 1311} } *) (*NotebookFileOutline Notebook[{ Cell[CellGroupData[{ Cell[579, 22, 238, 8, 288, "Title", CellID->795014953], Cell[820, 32, 223, 4, 34, "Text", CellID->1098476306], Cell[1046, 38, 478, 13, 43, "DisplayFormula", CellID->1336903145], Cell[1527, 53, 478, 9, 87, "Text", CellID->1576060680], Cell[2008, 64, 47, 1, 18, "OpenEnvironment", CellID->439790372], Cell[CellGroupData[{ Cell[2080, 69, 376, 9, 55, "EnvironmentHeader", CellID->426252685], Cell[2459, 80, 323, 8, 44, "GlobalDeclaration", CellTags->{ "ID:1197931704", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->1197931704], Cell[2785, 90, 1310, 43, 42, "FormalTextInputFormula", CellTags->{ "ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[SubsetEqual]"}, CellID->1841163329], Cell[4098, 135, 1485, 52, 32, "FormalTextInputFormula", CellTags->{ "ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\\"}, CellID->790959835], Cell[5586, 189, 1272, 41, 32, "FormalTextInputFormula", CellTags->{ "ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "\[Intersection]"}, CellID->1252989057], Cell[6861, 232, 66, 1, 33, "EndEnvironmentMarker", CellID->1529780747] }, Open ]], Cell[6942, 236, 49, 1, 24, "CloseEnvironment", CellID->1563925829], Cell[6994, 239, 47, 1, 18, "OpenEnvironment", CellID->834846774], Cell[CellGroupData[{ Cell[7066, 244, 375, 9, 55, "EnvironmentHeader", CellID->865240769], Cell[7444, 255, 474, 10, 44, "GlobalDeclaration", CellTags->{ "ID:862730946", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, CellID->862730946], Cell[7921, 267, 1265, 39, 32, "FormalTextInputFormula", CellTags->{ "ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb", "2"}, CellID->501871624], Cell[9189, 308, 65, 1, 33, "EndEnvironmentMarker", CellID->905092664] }, Open ]], Cell[9269, 312, 48, 1, 24, "CloseEnvironment", CellID->986882933], Cell[CellGroupData[{ Cell[9342, 317, 3998, 106, 44, "ProofInfo", CellTags->{"Proof|ID:501871624", "Proof|ID:501871624-1"}, CellID->1659692279], Cell[13343, 425, 481, 12, 105, "ProofInfoBody", CellID->1129186913] }, Closed]] }, Open ]] } ] *) (* End of internal cache information *)