Theorema`Common`buiActComputation["AbsValue"] = True Theorema`Common`buiActComputation["And"] = True Theorema`Common`buiActComputation["AnElement"] = True Theorema`Common`buiActComputation["appendElem"] = True Theorema`Common`buiActComputation["ArgMax"] = True Theorema`Common`buiActComputation["ArgMin"] = True Theorema`Common`buiActComputation["Cardinality"] = True Theorema`Common`buiActComputation["CartesianProduct"] = True Theorema`Common`buiActComputation["CaseDistinction"] = True Theorema`Common`buiActComputation["Componentwise"] = True Theorema`Common`buiActComputation["Delete"] = True Theorema`Common`buiActComputation["DeleteAt"] = True Theorema`Common`buiActComputation["Difference"] = True Theorema`Common`buiActComputation["Do"] = True Theorema`Common`buiActComputation["elemTuple"] = True Theorema`Common`buiActComputation["Equal"] = True Theorema`Common`buiActComputation["Exists"] = True Theorema`Common`buiActComputation["Factorial"] = True Theorema`Common`buiActComputation["For"] = True Theorema`Common`buiActComputation["Forall"] = True Theorema`Common`buiActComputation["Greater"] = True Theorema`Common`buiActComputation["GreaterEqual"] = True Theorema`Common`buiActComputation["Iff"] = True Theorema`Common`buiActComputation["Implies"] = True Theorema`Common`buiActComputation["Insert"] = True Theorema`Common`buiActComputation["IntegerInterval"] = True Theorema`Common`buiActComputation["IntegerQuotientRing"] = True Theorema`Common`buiActComputation["IntegerQuotientRingPM"] = True Theorema`Common`buiActComputation["Intersection"] = True Theorema`Common`buiActComputation["IntersectionOf"] = True Theorema`Common`buiActComputation["isComplex"] = True Theorema`Common`buiActComputation["isComplexP"] = True Theorema`Common`buiActComputation["IsElement"] = True Theorema`Common`buiActComputation["isInteger"] = True Theorema`Common`buiActComputation["isRational"] = True Theorema`Common`buiActComputation["isReal"] = True Theorema`Common`buiActComputation["isSet"] = True Theorema`Common`buiActComputation["isTuple"] = True Theorema`Common`buiActComputation["joinTuples"] = True Theorema`Common`buiActComputation["Length"] = True Theorema`Common`buiActComputation["Less"] = True Theorema`Common`buiActComputation["LessEqual"] = True Theorema`Common`buiActComputation["Let"] = True Theorema`Common`buiActComputation["Max"] = True Theorema`Common`buiActComputation["MaximumElementSet"] = True Theorema`Common`buiActComputation["MaximumOf"] = True Theorema`Common`buiActComputation["Min"] = True Theorema`Common`buiActComputation["MinimumElementSet"] = True Theorema`Common`buiActComputation["MinimumOf"] = True Theorema`Common`buiActComputation["Minus"] = True Theorema`Common`buiActComputation["Module"] = True Theorema`Common`buiActComputation["MultInverse"] = True Theorema`Common`buiActComputation["Nand"] = True Theorema`Common`buiActComputation["Nor"] = True Theorema`Common`buiActComputation["Not"] = True Theorema`Common`buiActComputation["Or"] = True Theorema`Common`buiActComputation["Plus"] = True Theorema`Common`buiActComputation["Power"] = True Theorema`Common`buiActComputation["PowerSet"] = True Theorema`Common`buiActComputation["prependElem"] = True Theorema`Common`buiActComputation["ProductOf"] = True Theorema`Common`buiActComputation["Radical"] = True Theorema`Common`buiActComputation["RationalInterval"] = True Theorema`Common`buiActComputation["RealInterval"] = True Theorema`Common`buiActComputation["Replace"] = True Theorema`Common`buiActComputation["ReplacePart"] = True Theorema`Common`buiActComputation["SetEqual"] = True Theorema`Common`buiActComputation["Subscript"] = True Theorema`Common`buiActComputation["Subset"] = True Theorema`Common`buiActComputation["SubsetEqual"] = True Theorema`Common`buiActComputation["Such"] = True Theorema`Common`buiActComputation["SuchUnique"] = True Theorema`Common`buiActComputation["SumOf"] = True Theorema`Common`buiActComputation["Superset"] = True Theorema`Common`buiActComputation["SupersetEqual"] = True Theorema`Common`buiActComputation["Switch"] = True Theorema`Common`buiActComputation["SymmetricDifference"] = True Theorema`Common`buiActComputation["TheArgMax"] = True Theorema`Common`buiActComputation["TheArgMin"] = True Theorema`Common`buiActComputation["Times"] = True Theorema`Common`buiActComputation["TupleEqual"] = True Theorema`Common`buiActComputation["Union"] = True Theorema`Common`buiActComputation["UnionOf"] = True Theorema`Common`buiActComputation["Which"] = True Theorema`Common`buiActComputation["While"] = True Theorema`Common`buiActComputation["Xnor"] = True Theorema`Common`buiActComputation["Xor"] = True Theorema`Common`buiActComputation["\[DoubleStruckCapitalC]"] = True Theorema`Common`buiActComputation["\[DoubleStruckCapitalC]P"] = True Theorema`Common`kbSelectCompute[{"ID:1701005634", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}] = True Theorema`Common`kbSelectCompute[{"ID:513702898", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}] = True Theorema`Common`kbSelectCompute[{"ID:972178751", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}] = True Theorema`Common`kbSelectCompute[_] := False Theorema`Common`$traceUserDef = False Theorema`Interface`GUI`Private`$allCurrentComputationContexts = {"Theorema`Computation`Knowledge`"} Theorema`Common`$tmaEnv = {Theorema`Common`FML$[{"ID:972178751", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]]], True, Theorema`Language`EqualDef$TM[Theorema`Language`DomainOperation$TM[ Theorema`Knowledge`Poly$TM[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Knowledge`deg$TM][ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]], Theorema`Language`Subtract$TM[Theorema`Language`BracketingBar$TM[ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]], 1]]], "deg"], Theorema`Common`FML$[{"ID:513702898", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`i$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Language`DomainOperation$TM[Theorema`Knowledge`Poly$TM[ Theorema`Language`VAR$[Theorema`Knowledge`K$TM]], Theorema`Knowledge`coef$TM][Theorema`Language`VAR$[ Theorema`Knowledge`p$TM], Theorema`Language`VAR$[ Theorema`Knowledge`i$TM]], Theorema`Language`Piecewise$TM[ Theorema`Language`Tuple$TM[Theorema`Language`Tuple$TM[ Theorema`Language`Subscript$TM[Theorema`Language`VAR$[ Theorema`Knowledge`p$TM], Theorema`Language`Plus$TM[ Theorema`Language`VAR$[Theorema`Knowledge`i$TM], 1]], Theorema`Language`LessEqual$TM[0, Theorema`Language`VAR$[ Theorema`Knowledge`i$TM], Theorema`Language`DomainOperation$TM[ Theorema`Knowledge`Poly$TM[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Knowledge`deg$TM][ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]]]], Theorema`Language`Tuple$TM[0, True]]]]], "coef"], Theorema`Common`FML$[{"ID:1701005634", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`q$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Language`DomainOperation$TM[Theorema`Knowledge`Poly$TM[ Theorema`Language`VAR$[Theorema`Knowledge`K$TM]], Theorema`Language`Times$TM][Theorema`Language`VAR$[ Theorema`Knowledge`p$TM], Theorema`Language`VAR$[ Theorema`Knowledge`q$TM]], Theorema`Language`TupleOf$TM[ Theorema`Language`RNG$[Theorema`Language`STEPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`j$TM], 0, Theorema`Language`Plus$TM[Theorema`Language`DomainOperation$TM[ Theorema`Knowledge`Poly$TM[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Knowledge`deg$TM][ Theorema`Language`VAR$[Theorema`Knowledge`p$TM]], Theorema`Language`DomainOperation$TM[Theorema`Knowledge`Poly$TM[ Theorema`Language`VAR$[Theorema`Knowledge`K$TM]], Theorema`Knowledge`deg$TM][Theorema`Language`VAR$[ Theorema`Knowledge`q$TM]]], 1]], True, Theorema`Language`SumOf$TM[Theorema`Language`RNG$[ Theorema`Language`STEPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`i$TM], 0, Theorema`Language`VAR$[ Theorema`Knowledge`j$TM], 1]], True, Theorema`Language`DomainOperation$TM[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM], Theorema`Language`Times$TM][ Theorema`Language`DomainOperation$TM[Theorema`Knowledge`Poly$TM[ Theorema`Language`VAR$[Theorema`Knowledge`K$TM]], Theorema`Knowledge`coef$TM][Theorema`Language`VAR$[ Theorema`Knowledge`p$TM], Theorema`Language`VAR$[ Theorema`Knowledge`i$TM]], Theorema`Language`DomainOperation$TM[ Theorema`Knowledge`Poly$TM[Theorema`Language`VAR$[ Theorema`Knowledge`K$TM]], Theorema`Knowledge`coef$TM][ Theorema`Language`VAR$[Theorema`Knowledge`q$TM], Theorema`Language`Subtract$TM[Theorema`Language`VAR$[ Theorema`Knowledge`j$TM], Theorema`Language`VAR$[ Theorema`Knowledge`i$TM]]]]]]]], "mult"]} Theorema`Common`$kbStruct = {"/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb" -> {{Cell["Theorema 2.0\nTheorem Proving in Mathematica", "Title", CellID -> 807905043], {Cell["What is Theorema?", "Section", CellID -> 752004855]}, {Cell["Realization of Theorema / System Architecture", "Section", CellID -> 389053381]}, {Cell["System Demo", "Section", CellID -> 474999417], {Cell["Definition (Univariate Polynomial Domain)", "EnvironmentHeader", CellID -> 1655106554], Cell[ BoxData[\(\(deg\+P[p]\) := \(\(\[LeftBracketingBar] p \[RightBracketingBar]\) - 1\)\)], "FormalTextInputFormula", CellTags -> {"ID:972178751", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb", "deg"}, CellID -> 972178751], Cell[ BoxData[\(\(coef\+P[\(p, i\)]\) := \(\[Piecewise] \*GridBox[{{\(p\_\(i + 1\)\), "\[DoubleLeftArrow]", \(0 \[LessEqual] i \[LessEqual] \(deg\+P[p]\)\)}, {"0", "\[DoubleLeftArrow]", "otherwise"}}]\)\)], "FormalTextInputFormula", CellTags -> {"ID:513702898", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb", "coef"}, CellID -> 513702898], Cell[ BoxData[\(\(p \(*\+P\) q\) := \(\[LeftAngleBracket] \( \(\[Sum]\+\(\(i = 0\), \[Ellipsis], j\) \(\(coef\+P[\(p, i\)]\) \(*\+K\) \(coef\+P[\(q, \(j - i\)\)]\)\)\) \(|\+\(\(j = 0\), \[Ellipsis], \(\(deg\+P[p]\) + \(deg\+P[q]\)\)\)\)\) \[RightAngleBracket]\)\)], "FormalTextInputFormula", CellTags -> {"ID:1701005634", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb", "mult"}, CellID -> 1701005634]}}}}} Theorema`Interface`GUI`Private`$tcKBBrowseSelection["compute"] = "/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb" Theorema`Interface`GUI`Private`$tcKBBrowseSelection["prove"] = "/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb" Theorema`Interface`GUI`Private`$tcKBBrowseSelection["solve"] = "/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"