patrick/advent-of-code-2021
1
0
Fork 0
mirror of https://github.com/Smaug123/advent-of-code-2021 synced 2025-10-05 03:58:39 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
main
advent-of-code-2021/day24.nb
Patrick Stevens d93eb92b3e Add Day 24 solution in Mathematica (#24)
2023-01-22 01:12:34 +00:00

6118 lines
223 KiB
Mathematica
Raw Permalink Blame History

(* Content-type: application/vnd.wolfram.mathematica *)
(*** Wolfram Notebook File ***)
(* http://www.wolfram.com/nb *)
(* Created By: SaveReadableNotebook *)
(* https://resources.wolframcloud.com/FunctionRepository/resources/SaveReadableNotebook *)
Notebook[
{
Cell[
CellGroupData[
{
Cell["Advent of Code 2021, day 24", "Title"],
Cell["Examine the inputs", "Subtitle"],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"input",
"=",
"\"inp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 10\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 0\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 12\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 6\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 13\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 4\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 13\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 2\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 14\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 9\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -2\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 1\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 11\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 10\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -15\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 6\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -10\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 4\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 1\nadd x 10\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 6\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -10\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 3\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -4\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 9\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -1\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 15\nmul y x\nadd z y\ninp w\nmul x 0\nadd x z\nmod x 26\ndiv z 26\nadd x -1\neql x w\neql x 0\nmul y 0\nadd y 25\nmul y x\nadd y 1\nmul z y\nmul y 0\nadd y w\nadd y 5\nmul y x\nadd z y\""
}
],
";"
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[54]:="
],
Cell[
BoxData[
RowBox[
{
RowBox[{"parseInt", "[", "s_String", "]"}],
":=",
RowBox[
{
RowBox[
{
"ToExpression",
"[",
RowBox[{"s", ",", "StandardForm", ",", "Hold"}],
"]"
}
],
"/.",
RowBox[
{
"{",
RowBox[
{
RowBox[
{RowBox[{"Hold", "[", "i_Integer", "]"}], ":>", "i"}
],
",",
RowBox[{"_", "->", "s"}]
}
],
"}"
}
]
}
]
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[47]:="
],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"parsed",
"=",
RowBox[
{
RowBox[
{
RowBox[
{
"(",
RowBox[
{
"parseInt",
"/@",
RowBox[
{"StringSplit", "[", RowBox[{"#", ",", "\" \""}], "]"}
]
}
],
")"
}
],
"&"
}
],
"/@",
RowBox[
{
"StringSplit",
"[",
RowBox[{"input", ",", "\"\\n\""}],
"]"
}
]
}
]
}
],
";"
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[48]:="
],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"runs",
"=",
RowBox[
{
"Split",
"[",
RowBox[
{
"parsed",
",",
RowBox[
{
RowBox[
{
"#2",
"!=",
RowBox[{"{", RowBox[{"\"inp\"", ",", "\"w\""}], "}"}]
}
],
"&"
}
]
}
],
"]"
}
]
}
],
";"
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[49]:="
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"runs",
"[",
RowBox[{"[", RowBox[{"1", ";;", "2"}], "]"}],
"]"
}
]
],
"Input",
CellLabel -> "In[199]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[{"{", RowBox[{"\"inp\"", ",", "\"w\""}], "}"}],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"x\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"x\"", ",", "\"z\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mod\"", ",", "\"x\"", ",", "26"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"div\"", ",", "\"z\"", ",", "1"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"x\"", ",", "10"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"eql\"", ",", "\"x\"", ",", "\"w\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"eql\"", ",", "\"x\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "25"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "\"x\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "1"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"z\"", ",", "\"y\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "\"w\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "\"x\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"z\"", ",", "\"y\""}], "}"}
]
}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{
RowBox[{"{", RowBox[{"\"inp\"", ",", "\"w\""}], "}"}],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"x\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"x\"", ",", "\"z\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mod\"", ",", "\"x\"", ",", "26"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"div\"", ",", "\"z\"", ",", "1"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"x\"", ",", "12"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"eql\"", ",", "\"x\"", ",", "\"w\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"eql\"", ",", "\"x\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "25"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "\"x\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "1"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"z\"", ",", "\"y\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "0"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "\"w\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"y\"", ",", "6"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"mul\"", ",", "\"y\"", ",", "\"x\""}], "}"}
],
",",
RowBox[
{"{", RowBox[{"\"add\"", ",", "\"z\"", ",", "\"y\""}], "}"}
]
}
],
"}"
}
]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[199]="
]
},
Open
]
],
Cell[
"The only places where the instructions differ:",
"Text"
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"Flatten",
"@",
RowBox[
{
"Position",
"[",
RowBox[
{
RowBox[
{"Equal", "@@@", RowBox[{"Transpose", "[", "runs", "]"}]}
],
",",
"False"
}
],
"]"
}
]
}
]
],
"Input",
CellLabel -> "In[50]:="
],
Cell[
BoxData[
RowBox[{"{", RowBox[{"5", ",", "6", ",", "16"}], "}"}]
],
"Output",
CellLabel -> "Out[50]="
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"reduced",
"=",
RowBox[
{
"MapIndexed",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"#1",
"[",
RowBox[{"[", RowBox[{"5", ",", "3"}], "]"}],
"]"
}
],
",",
RowBox[
{
"#1",
"[",
RowBox[{"[", RowBox[{"6", ",", "3"}], "]"}],
"]"
}
],
",",
RowBox[
{
"#1",
"[",
RowBox[{"[", RowBox[{"16", ",", "3"}], "]"}],
"]"
}
],
",",
RowBox[{"#2", "[", RowBox[{"[", "1", "]"}], "]"}]
}
],
"}"
}
],
"&"
}
],
",",
"runs"
}
],
"]"
}
]
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[50]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
RowBox[
{"{", RowBox[{"1", ",", "10", ",", "0", ",", "1"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "12", ",", "6", ",", "2"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "13", ",", "4", ",", "3"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "13", ",", "2", ",", "4"}], "}"}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "14", ",", "9", ",", "5"}], "}"}
],
",",
RowBox[
{
"{",
RowBox[{"26", ",", RowBox[{"-", "2"}], ",", "1", ",", "6"}],
"}"
}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "11", ",", "10", ",", "7"}], "}"}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "15"}], ",", "6", ",", "8"}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "10"}], ",", "4", ",", "9"}
],
"}"
}
],
",",
RowBox[
{"{", RowBox[{"1", ",", "10", ",", "6", ",", "10"}], "}"}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "10"}], ",", "3", ",", "11"}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "4"}], ",", "9", ",", "12"}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "1"}], ",", "15", ",", "13"}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{"26", ",", RowBox[{"-", "1"}], ",", "5", ",", "14"}
],
"}"
}
]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[50]="
]
},
Open
]
],
Cell["Simplify by hand what happens in that case:", "Text"],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"fCompressed",
"[",
RowBox[
{"a_", ",", "b_", ",", "c_", ",", "state_", ",", "zIn_"}
],
"]"
}
],
":=",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
"x",
"=",
RowBox[
{
"If",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[{"Mod", "[", RowBox[{"zIn", ",", "26"}], "]"}],
"+",
"b"
}
],
"!=",
RowBox[{"w", "[", "state", "]"}]
}
],
",",
"1",
",",
"0"
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[{"Quotient", "[", RowBox[{"zIn", ",", "a"}], "]"}],
" ",
RowBox[{"(", RowBox[{RowBox[{"25", "x"}], "+", "1"}], ")"}]
}
],
"+",
RowBox[
{
RowBox[
{
"(",
RowBox[{RowBox[{"w", "[", "state", "]"}], "+", "c"}],
")"
}
],
"x"
}
]
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[51]:="
],
Cell[
CellGroupData[
{
Cell[
"(optional) Verify that the simplified version is the same",
"Subtitle"
],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"moreParsed",
"=",
RowBox[
{
"parsed",
"/.",
RowBox[
{
"{",
RowBox[
{
RowBox[{"\"add\"", "->", "Plus"}],
",",
RowBox[{"\"div\"", "->", "Quotient"}],
",",
RowBox[{"\"mod\"", "->", "Mod"}],
",",
RowBox[
{
"\"eql\"",
"->",
RowBox[
{
"(",
RowBox[
{
RowBox[{"Boole", "[", RowBox[{"#1", "==", "#2"}], "]"}],
"&"
}
],
")"
}
]
}
],
",",
RowBox[{"\"mul\"", "->", "Times"}]
}
],
"}"
}
]
}
]
}
],
";"
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[52]:="
],
Cell[
BoxData[
RowBox[
{
RowBox[{"evaluateLonghand", "[", "instructions_", "]"}],
":=",
RowBox[
{
RowBox[
{
RowBox[
{
"Last",
"[",
RowBox[
{
"Fold",
"[",
RowBox[
{
RowBox[
{
"Function",
"[",
RowBox[
{
RowBox[{"{", RowBox[{"state", ",", "instruction"}], "}"}],
",",
RowBox[
{
"Switch",
"[",
RowBox[
{
"instruction",
",",
"\[IndentingNewLine]",
RowBox[{"{", RowBox[{"\"inp\"", ",", "\"w\""}], "}"}],
",",
RowBox[
{
"{",
RowBox[
{
RowBox[{RowBox[{"First", "[", "state", "]"}], "+", "1"}],
",",
RowBox[
{
"Append",
"[",
RowBox[
{
RowBox[{"Last", "[", "state", "]"}],
",",
RowBox[
{
"\"w\"",
"->",
RowBox[{"w", "[", RowBox[{"First", "@", "state"}], "]"}]
}
]
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
"_",
",",
RowBox[
{
"{",
RowBox[
{
RowBox[{"state", "[", RowBox[{"[", "1", "]"}], "]"}],
",",
RowBox[
{
"Append",
"[",
RowBox[
{
RowBox[{"state", "[", RowBox[{"[", "2", "]"}], "]"}],
",",
RowBox[
{
RowBox[{"instruction", "[", RowBox[{"[", "2", "]"}], "]"}],
"->",
RowBox[
{
RowBox[{"instruction", "[", RowBox[{"[", "1", "]"}], "]"}],
"[",
RowBox[
{
RowBox[
{
RowBox[{"state", "[", RowBox[{"[", "2", "]"}], "]"}],
"[",
RowBox[{"instruction", "[", RowBox[{"[", "2", "]"}], "]"}],
"]"
}
],
",",
RowBox[
{
"If",
"[",
RowBox[
{
RowBox[
{"StringQ", "[", RowBox[{"Last", "@", "instruction"}], "]"}
],
",",
RowBox[
{
RowBox[{"state", "[", RowBox[{"[", "2", "]"}], "]"}],
"[",
RowBox[{"instruction", "[", RowBox[{"[", "3", "]"}], "]"}],
"]"
}
],
",",
RowBox[{"Last", "@", "instruction"}]
}
],
"]"
}
]
}
],
"]"
}
]
}
]
}
],
"]"
}
]
}
],
"}"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"{",
RowBox[
{
"1",
",",
RowBox[
{
"<|",
RowBox[
{
RowBox[{"\"x\"", "->", "0"}],
",",
RowBox[{"\"y\"", "->", "0"}],
",",
RowBox[{"\"z\"", "->", "0"}]
}
],
"|>"
}
]
}
],
"}"
}
],
",",
"instructions"
}
],
"]"
}
],
"]"
}
],
"[",
"\"z\"",
"]"
}
],
"//",
RowBox[
{
RowBox[
{
"FullSimplify",
"[",
RowBox[
{
"#",
",",
RowBox[
{
"Flatten",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{RowBox[{"w", "[", "#", "]"}], "\[Element]", "Integers"}
],
"&&",
RowBox[
{"1", "<=", RowBox[{"w", "[", "#", "]"}], "<=", "9"}
]
}
],
"&"
}
],
"/@",
RowBox[{"Range", "[", "13", "]"}]
}
],
"]"
}
]
}
],
"]"
}
],
"&"
}
]
}
]
}
]
],
"Input",
CellLabel -> "In[9]:="
],
Cell[
"They do agree, at least for the first seven rounds:",
"Text"
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
RowBox[
{
RowBox[
{
"evaluateLonghand",
"[",
RowBox[
{
"moreParsed",
"[",
RowBox[
{
"[",
RowBox[
{
"1",
";;",
RowBox[
{
"7",
RowBox[{"Length", "@", RowBox[{"First", "@", "runs"}]}]
}
]
}
],
"]"
}
],
"]"
}
],
"]"
}
],
"==",
RowBox[
{
"Fold",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
"fCompressed",
"[",
RowBox[{RowBox[{"Sequence", "@@", "#2"}], ",", "#1"}],
"]"
}
],
"&"
}
],
",",
"0",
",",
RowBox[
{
"reduced",
"[",
RowBox[{"[", RowBox[{"1", ";;", "7"}], "]"}],
"]"
}
]
}
],
"]"
}
]
}
],
"//",
RowBox[
{
RowBox[
{
"FullSimplify",
"[",
RowBox[
{
"#",
",",
RowBox[
{
"Flatten",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{RowBox[{"w", "[", "#", "]"}], "\[Element]", "Integers"}
],
"&&",
RowBox[
{"1", "<=", RowBox[{"w", "[", "#", "]"}], "<=", "9"}
]
}
],
"&"
}
],
"/@",
RowBox[{"Range", "[", "13", "]"}]
}
],
"]"
}
]
}
],
"]"
}
],
"&"
}
]
}
]
],
"Input",
CellLabel -> "In[10]:="
],
Cell[BoxData["True"], "Output", CellLabel -> "Out[10]="]
},
Open
]
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell["Solve", "Subtitle"],
Cell[
TextData[
{
"I\[CloseCurlyQuote]ve used a bunch of user-defined symbols like ",
Cell[
BoxData[FormBox["if", TraditionalForm]],
FormatType -> TraditionalForm
],
" instead of ",
Cell[
BoxData[FormBox["If", TraditionalForm]],
FormatType -> TraditionalForm
],
", to demonstrate that I\[CloseCurlyQuote]m not using any of the Awesome Power of Mathematica. I\[CloseCurlyQuote]m specifically only calling out to Mathematica when there are genuinely numeric quantities to compute with. Notice how I\[CloseCurlyQuote]m not even using Mathematica booleans!"
}
],
"Text"
],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"f",
"[",
RowBox[
{"a_", ",", "b_", ",", "c_", ",", "state_", ",", "zIn_"}
],
"]"
}
],
":=",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
"x",
"=",
RowBox[
{
"if",
"[",
RowBox[
{
RowBox[
{
"not",
"[",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"mod", "[", RowBox[{"zIn", ",", "26"}], "]"}],
",",
"b"
}
],
"]"
}
],
",",
RowBox[{"w", "[", "state", "]"}]
}
],
"]"
}
],
"]"
}
],
",",
"1",
",",
"0"
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"zIn", ",", "a"}], "]"}],
" ",
",",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"times", "[", RowBox[{"25", ",", "x"}], "]"}],
",",
"1"
}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "state", "]"}], ",", "c"}],
"]"
}
],
",",
"x"
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
]
],
"Input",
InitializationCell -> True,
CellLabel -> "In[55]:="
],
Cell[
BoxData[
{
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[{"k_", ",", RowBox[{"w", "[", "_", "]"}]}],
"]"
}
],
",",
"m_"
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"k", ",", "1"}], "]"}],
",",
"m"
}
],
"]"
}
],
",",
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"k", ",", "9"}], "]"}],
",",
"m"
}
],
"]"
}
]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"k", ",", "1"}], "]"}],
",",
"m"
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
"a_",
",",
RowBox[
{
"times",
"[",
RowBox[{RowBox[{"k_", "?", "NumericQ"}], " ", ",", "b_"}],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[{"n_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"n", ">", "1"}],
"&&",
RowBox[
{
"IntegerQ",
"@",
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}]
}
]
}
]
}
],
":=",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a", ",", "n"}], "]"}],
",",
RowBox[
{
"times",
"[",
RowBox[
{
SuperscriptBox[
"n",
RowBox[
{
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}],
"-",
"1"
}
]
],
",",
"b"
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
"a_",
",",
RowBox[
{
"times",
"[",
RowBox[{"b_", ",", RowBox[{"k_", "?", "NumericQ"}]}],
" ",
"]"
}
]
}
],
"]"
}
],
",",
RowBox[{"n_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"n", ">", "1"}],
"&&",
RowBox[
{
"IntegerQ",
"@",
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}]
}
]
}
]
}
],
":=",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a", ",", "n"}], "]"}],
",",
RowBox[
{
"times",
"[",
RowBox[
{
SuperscriptBox[
"n",
RowBox[
{
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}],
"-",
"1"
}
]
],
",",
"b"
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[{"b_", ",", RowBox[{"k_", "?", "NumericQ"}]}],
" ",
"]"
}
],
",",
"a_"
}
],
"]"
}
],
",",
RowBox[{"n_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"n", ">", "1"}],
"&&",
RowBox[
{
"IntegerQ",
"@",
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}]
}
]
}
]
}
],
":=",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a", ",", "n"}], "]"}],
",",
RowBox[
{
"times",
"[",
RowBox[
{
SuperscriptBox[
"n",
RowBox[
{
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}],
"-",
"1"
}
]
],
",",
"b"
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[{RowBox[{"k_", "?", "NumericQ"}], ",", "b_"}],
" ",
"]"
}
],
",",
"a_"
}
],
"]"
}
],
",",
RowBox[{"n_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"n", ">", "1"}],
"&&",
RowBox[
{
"IntegerQ",
"@",
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}]
}
]
}
]
}
],
":=",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a", ",", "n"}], "]"}],
",",
RowBox[
{
"times",
"[",
RowBox[
{
SuperscriptBox[
"n",
RowBox[
{
RowBox[{"Log", "[", RowBox[{"n", ",", "k"}], "]"}],
"-",
"1"
}
]
],
",",
"b"
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a_", ",", "1"}], "]"}],
":=",
"a"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a_", ",", "b_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
":=",
RowBox[
{
"quotient",
"[",
RowBox[
{
"a",
",",
RowBox[{"times", "[", RowBox[{"b", ",", "c"}], "]"}]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "_", "]"}], ",", "b_"}],
"]"
}
],
",",
"c_"
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"9", ",", "b"}], "]"}],
",",
"c"
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"0"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"mod",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"times", "[", RowBox[{"a_", " ", ",", "b_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
",",
"a_"
}
],
"]"
}
],
":=",
"c"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"mod",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"times", "[", RowBox[{"a_", " ", ",", "b_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
",",
"b_"
}
],
"]"
}
],
":=",
"c"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"mod",
"[",
RowBox[
{
RowBox[{"a_", "?", "NumericQ"}],
",",
RowBox[{"b_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[{"Mod", "[", RowBox[{"a", ",", "b"}], "]"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{
"mod",
"[",
RowBox[{RowBox[{"w", "[", "n_", "]"}], ",", "k_"}],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"less", "[", RowBox[{"9", ",", "k"}], "]"}],
"===",
"true"
}
]
}
],
":=",
RowBox[{"w", "[", "n", "]"}]
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"positive", "[", "x_", "]"}],
":=",
RowBox[{"less", "[", RowBox[{"0", ",", "x"}], "]"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{
"positive",
"[",
RowBox[{"mod", "[", RowBox[{"a_", ",", "n_"}], "]"}],
"]"
}
],
"/;",
RowBox[
{RowBox[{"positive", "[", "a", "]"}], "===", "true"}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{"nonnegative", "[", RowBox[{"w", "[", "_", "]"}], "]"}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"nonnegative",
"[",
RowBox[{"mod", "[", RowBox[{"a_", ",", "n_"}], "]"}],
"]"
}
],
"/;",
RowBox[
{RowBox[{"nonnegative", "[", "a", "]"}], "===", "true"}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"nonnegative",
"[",
RowBox[
{
"if",
"[",
RowBox[{"cond_", ",", "trueCase_", ",", "falseCase_"}],
"]"
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"nonnegative", "[", "trueCase", "]"}],
",",
RowBox[{"nonnegative", "[", "falseCase", "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"nonnegative",
"[",
RowBox[{"times", "[", RowBox[{"a_", ",", " ", "b_"}], "]"}],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"nonnegative", "[", "a", "]"}],
",",
RowBox[{"nonnegative", "[", "b", "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"nonnegative",
"[",
RowBox[{"plus", "[", RowBox[{"a_", ",", "b_"}], "]"}],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"nonnegative", "[", "a", "]"}],
",",
RowBox[{"nonnegative", "[", "b", "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"nonnegative",
"[",
RowBox[{"quotient", "[", RowBox[{"a_", ",", "b_"}], "]"}],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"nonnegative", "[", "a", "]"}],
",",
RowBox[{"less", "[", RowBox[{"0", ",", "b"}], "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{"nonnegative", "[", RowBox[{"k_", "?", "NumericQ"}], "]"}
],
":=",
RowBox[
{
"If",
"[",
RowBox[
{
RowBox[{"NonNegative", "[", "k", "]"}],
",",
"true",
",",
"false"
}
],
"]"
}
]
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"a_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
],
" ",
",",
RowBox[
{
"b_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
]
}
],
"]"
}
],
",",
"0"
}
],
"]"
}
],
":=",
RowBox[
{
"or",
"[",
RowBox[
{
RowBox[{"equal", "[", RowBox[{"a", ",", "0"}], "]"}],
",",
RowBox[{"equal", "[", RowBox[{"b", ",", "0"}], "]"}]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"a_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
],
",",
" ",
RowBox[
{
"b_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
]
}
],
"]"
}
],
",",
"0"
}
],
"]"
}
],
":=",
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"equal", "[", RowBox[{"a", ",", "0"}], "]"}],
",",
RowBox[{"equal", "[", RowBox[{"b", ",", "0"}], "]"}]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a_", ",", "n_"}], "]"}],
",",
"0"
}
],
"]"
}
],
":=",
RowBox[{"less", "[", RowBox[{"a", ",", "n"}], "]"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"if",
"[",
RowBox[
{
"cond_",
",",
RowBox[
{
"n_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"positive", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
],
",",
"0"
}
],
"]"
}
],
",",
"0"
}
],
"]"
}
],
":=",
RowBox[{"not", "[", "cond", "]"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"if",
"[",
RowBox[
{
"cond_",
",",
"0",
",",
RowBox[
{
"n_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"positive", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
]
}
],
"]"
}
],
",",
"0"
}
],
"]"
}
],
":=",
"cond"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "_", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{
"n_",
",",
RowBox[
{
"_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
]
}
],
"]"
}
]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"less", "[", RowBox[{"9", ",", "n"}], "]"}],
"===",
"true"
}
]
}
],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[{RowBox[{"w", "[", "_", "]"}], ",", "0"}],
"]"
}
],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "_", "]"}],
",",
RowBox[{"k_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"less", "[", RowBox[{"9", ",", "k"}], "]"}],
"===",
"true"
}
]
}
],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"x_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[{RowBox[{"Head", "[", "#", "]"}], "=!=", "w"}],
"&"
}
],
")"
}
]
}
],
",",
RowBox[{"w", "[", "n_", "]"}]
}
],
"]"
}
],
":=",
RowBox[
{
"equal",
"[",
RowBox[{RowBox[{"w", "[", "n", "]"}], ",", "x"}],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"a_", "?", "NumericQ"}],
",",
RowBox[{"b_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[
{
"If",
"[",
RowBox[
{RowBox[{"a", "==", "b"}], ",", "true", ",", "false"}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "_", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"w", "[", "_", "]"}],
",",
RowBox[{"n_", "?", "NumericQ"}]
}
],
"]"
}
]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"less", "[", RowBox[{"9", ",", "n"}], "]"}],
"===",
"true"
}
]
}
],
":=",
"false"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"_", "?", "nonnegative"}],
",",
RowBox[
{
"times",
"[",
RowBox[
{
"n_",
",",
" ",
RowBox[
{
"_",
"?",
RowBox[
{
"(",
RowBox[
{
RowBox[
{RowBox[{"nonnegative", "[", "#", "]"}], "===", "true"}
],
"&"
}
],
")"
}
]
}
]
}
],
"]"
}
]
}
],
"]"
}
],
",",
"n_"
}
],
"]"
}
],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"a_", "?", "NumericQ"}],
",",
RowBox[{"b_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[
{
"If",
"[",
RowBox[
{RowBox[{"a", "<", "b"}], ",", "true", ",", "false"}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"quotient", "[", RowBox[{"a_", ",", "b_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
":=",
RowBox[
{
"less",
"[",
RowBox[
{
"a",
",",
RowBox[{"times", "[", RowBox[{"b", ",", "c"}], "]"}]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
"a_",
",",
RowBox[{"plus", "[", RowBox[{"b_", ",", "c_"}], "]"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[{"less", "[", RowBox[{"a", ",", "b"}], "]"}],
",",
RowBox[{"less", "[", RowBox[{"0", ",", "c"}], "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"a_", ",", "b_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[
{
"not",
"@",
RowBox[{"less", "[", RowBox[{"a", ",", "c"}], "]"}]
}
],
",",
RowBox[{"nonnegative", "[", "b", "]"}]
}
],
"]"
}
],
"===",
"true"
}
]
}
],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"times", "[", RowBox[{"x_", ",", "c_"}], "]"}],
",",
"c_"
}
],
"]"
}
],
"/;",
RowBox[
{RowBox[{"positive", "[", "c", "]"}], "===", "true"}
]
}
],
":=",
RowBox[{"equal", "[", RowBox[{"x", ",", "0"}], "]"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[{"w", "[", "_", "]"}],
",",
RowBox[{"k_", "?", "NumericQ"}]
}
],
"]"
}
],
"/;",
RowBox[
{
RowBox[{"less", "[", RowBox[{"9", ",", "k"}], "]"}],
"===",
"true"
}
]
}
],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[{"0", ",", RowBox[{"w", "[", "_", "]"}]}],
"]"
}
],
":=",
"true"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{"if", "[", RowBox[{"true", ",", "a_", ",", "_"}], "]"}
],
":=",
"a"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{"if", "[", RowBox[{"false", ",", "_", ",", "a_"}], "]"}
],
":=",
"a"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[
{
"if",
"[",
RowBox[
{RowBox[{"not", "[", "cond_", "]"}], ",", "t_", ",", "f_"}
],
"]"
}
],
":=",
RowBox[
{"if", "[", RowBox[{"cond", ",", "f", ",", "t"}], "]"}
]
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"not", "[", RowBox[{"not", "[", "x_", "]"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{RowBox[{"not", "[", "false", "]"}], "=", "true"}],
";"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[{RowBox[{"not", "[", "true", "]"}], "=", "false"}],
";"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"and", "[", RowBox[{"_", ",", "false"}], "]"}],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"and", "[", RowBox[{"false", ",", "_"}], "]"}],
":=",
"false"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"and", "[", RowBox[{"true", ",", "x_"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[{"and", "[", RowBox[{"x_", ",", "true"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"or", "[", RowBox[{"_", ",", "true"}], "]"}],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"or", "[", RowBox[{"true", ",", "_"}], "]"}],
":=",
"true"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"or", "[", RowBox[{"false", ",", "x_"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[{"or", "[", RowBox[{"x_", ",", "false"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[{"a_", "?", "NumericQ"}],
",",
RowBox[{"b_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[{"a", "+", "b"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[{"a_", "?", "NumericQ"}],
",",
RowBox[{"b_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[{"a", " ", "b"}]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[{"a_", ",", RowBox[{"b_", "?", "NumericQ"}]}],
"]"
}
],
",",
RowBox[{"c_", "?", "NumericQ"}]
}
],
"]"
}
],
":=",
RowBox[
{
"plus",
"[",
RowBox[{"a", ",", RowBox[{"b", "+", "c"}]}],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"times", "[", RowBox[{"0", ",", "_"}], "]"}],
":=",
"0"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"times", "[", RowBox[{"_", ",", "0"}], "]"}],
":=",
"0"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"times", "[", RowBox[{"x_", ",", "1"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"times", "[", RowBox[{"1", ",", "x_"}], "]"}],
":=",
"x"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"plus", "[", RowBox[{"a_", ",", "0"}], "]"}],
":=",
"a"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
RowBox[{"plus", "[", RowBox[{"0", ",", "a_"}], "]"}],
":=",
"a"
}
],
"\[IndentingNewLine]"
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
"x_",
",",
RowBox[
{"if", "[", RowBox[{"cond_", ",", "0", ",", "t_"}], "]"}
]
}
],
"]"
}
],
":=",
RowBox[
{
"if",
"[",
RowBox[
{
"cond",
",",
"0",
",",
RowBox[{"times", "[", RowBox[{"x", ",", "t"}], "]"}]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
"x_",
",",
RowBox[
{"if", "[", RowBox[{"cond_", ",", "t_", ",", "0"}], "]"}
]
}
],
"]"
}
],
":=",
RowBox[
{
"if",
"[",
RowBox[
{
"cond",
",",
RowBox[{"times", "[", RowBox[{"x", ",", "t"}], "]"}],
",",
"0"
}
],
"]"
}
]
}
]
}
],
"Input",
CellLabel -> "In[56]:="
],
Cell["Let\[CloseCurlyQuote]s go!", "Text"],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"condition",
"=",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[
{
"Fold",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
"f",
"[",
RowBox[{RowBox[{"Sequence", "@@", "#2"}], ",", "#1"}],
"]"
}
],
"&"
}
],
",",
"0",
",",
"reduced"
}
],
"]"
}
],
",",
"0"
}
],
"]"
}
]
}
]
],
"Input",
CellLabel -> "In[121]:="
],
Cell[
BoxData[
InterpretationBox[
TagBox[
FrameBox[
GridBox[
{
{
ItemBox[
TagBox[
RowBox[
{
"and",
"[",
RowBox[
{
RowBox[
{
"less",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"quotient",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[{RowBox[{"w", "[", "1", "]"}], ",", "26"}],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "2", "]"}], ",", "6"}],
"]"
}
]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "3", "]"}], ",", "4"}],
"]"
}
]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "4", "]"}], ",", "2"}],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"if",
"[",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "6", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "5", "]"}], ",", "7"}],
"]"
}
]
}
],
"]"
}
],
",",
"0",
",",
"25"
}
],
"]"
}
],
",",
"1"
}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"if",
"[",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "6", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "5", "]"}], ",", "7"}],
"]"
}
]
}
],
"]"
}
],
",",
"0",
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "6", "]"}], ",", "1"}],
"]"
}
]
}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"if",
"[",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "7", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"mod",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
RowBox[
{
RowBox[
{
"plus",
"[",
RowBox[
{
RowBox[
{
"times",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
"11"
}
],
"]"
}
]
}
],
"]"
}
],
",",
"0",
",",
"25"
}
],
"]"
}
],
",",
"1"
}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"if",
"[",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "7", "]"}],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"0",
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
RowBox[
{TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"], ",", "1"}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"if",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"if",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"plus",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
",",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"]
}
],
"]"
}
],
",",
"26"
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
TemplateBox[{"1"}, "OutputSizeLimit`Skeleton"],
"]"
}
]
}
],
"]"
}
],
Short[#1, 5] &
],
BaseStyle -> {Deployed -> False},
StripOnInput -> False
]
},
{
GridBox[
{
{
PaneBox[
TagBox[
TooltipBox[
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource[
"FEStrings",
"sizeBriefExplanation"
],
StandardForm
],
ImageSizeCache -> {59.0, {2.0, 8.0}}
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLText",
StripOnInput -> False
],
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeExplanation"],
StandardForm
]
],
DynamicUpdating -> True,
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0},
LineSpacing -> {1, 2},
StripOnInput -> False
]
],
Function[
Annotation[
#1,
Style[
Dynamic[
FEPrivate`FrontEndResource["FEStrings", "sizeExplanation"]
],
DynamicUpdating -> True,
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0},
LineSpacing -> {1, 2}
],
"Tooltip"
]
]
],
Alignment -> Center,
BaselinePosition -> Baseline,
ImageSize -> {Automatic, {25, Full}}
],
ButtonBox[
PaneSelectorBox[
{
False ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowLess"],
StandardForm
],
ImageSizeCache -> {51.0, {0.0, 8.0}}
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControl",
StripOnInput -> False
],
True ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowLess"],
StandardForm
]
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControlActive",
StripOnInput -> False
]
},
Dynamic[CurrentValue["MouseOver"]],
Alignment -> Center,
FrameMargins -> 0,
ImageSize -> {Automatic, {25, Full}}
],
Appearance -> None,
BaselinePosition -> Baseline,
ButtonFunction :>
OutputSizeLimit`ButtonFunction[
OutputSizeLimit`Defer,
121,
17588487059817799587,
5 / 2
],
Enabled -> True,
Evaluator -> Automatic,
Method -> "Queued"
],
ButtonBox[
PaneSelectorBox[
{
False ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowMore"],
StandardForm
],
ImageSizeCache -> {56.0, {0.0, 8.0}}
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControl",
StripOnInput -> False
],
True ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowMore"],
StandardForm
]
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControlActive",
StripOnInput -> False
]
},
Dynamic[CurrentValue["MouseOver"]],
Alignment -> Center,
FrameMargins -> 0,
ImageSize -> {Automatic, {25, Full}}
],
Appearance -> None,
BaselinePosition -> Baseline,
ButtonFunction :>
OutputSizeLimit`ButtonFunction[
OutputSizeLimit`Defer,
121,
17588487059817799587,
5 * 2
],
Enabled -> True,
Evaluator -> Automatic,
Method -> "Queued"
],
ButtonBox[
PaneSelectorBox[
{
False ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowAll"],
StandardForm
],
ImageSizeCache -> {42.0, {0.0, 8.0}}
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControl",
StripOnInput -> False
],
True ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeShowAll"],
StandardForm
]
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControlActive",
StripOnInput -> False
]
},
Dynamic[CurrentValue["MouseOver"]],
Alignment -> Center,
FrameMargins -> 0,
ImageSize -> {Automatic, {25, Full}}
],
Appearance -> None,
BaselinePosition -> Baseline,
ButtonFunction :>
OutputSizeLimit`ButtonFunction[
OutputSizeLimit`Defer,
121,
17588487059817799587,
Infinity
],
Enabled -> True,
Evaluator -> Automatic,
Method -> "Queued"
],
ButtonBox[
PaneSelectorBox[
{
False ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeChangeLimit"],
StandardForm
],
ImageSizeCache -> {77.0, {0.0, 8.0}}
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControl",
StripOnInput -> False
],
True ->
StyleBox[
StyleBox[
DynamicBox[
ToBoxes[
FEPrivate`FrontEndResource["FEStrings", "sizeChangeLimit"],
StandardForm
]
],
StripOnInput -> False,
DynamicUpdating -> True,
LineSpacing -> {1, 2},
LineIndent -> 0,
LinebreakAdjustments -> {1.0, 100, 0, 0, 0}
],
"OSLControlActive",
StripOnInput -> False
]
},
Dynamic[CurrentValue["MouseOver"]],
Alignment -> Center,
FrameMargins -> 0,
ImageSize -> {Automatic, {25, Full}}
],
Appearance -> None,
BaselinePosition -> Baseline,
ButtonFunction :>
FrontEndExecute[
{
FrontEnd`SetOptions[
FrontEnd`$FrontEnd,
FrontEnd`PreferencesSettings -> {"Page" -> "Advanced"}
],
FrontEnd`FrontEndToken["PreferencesDialog"]
}
],
Evaluator -> None,
Method -> "Preemptive"
]
}
},
AutoDelete -> False,
FrameStyle -> GrayLevel[0.85],
GridBoxDividers -> {"Columns" -> {False, {True}}},
GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{Automatic}}},
GridBoxSpacings -> {"Columns" -> {{2}}}
]
}
},
DefaultBaseStyle -> "Column",
GridBoxAlignment -> {"Columns" -> {{Left}}, "Rows" -> {{Baseline}}},
GridBoxDividers -> {"Columns" -> {{False}}, "Rows" -> {{False}}},
GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{1.0}}},
GridBoxSpacings -> {
"Columns" -> {Offset[0.28], {Offset[0.56]}, Offset[0.28]},
"Rows" -> {Offset[0.2], Offset[1.2], {Offset[0.4]}, Offset[0.2]}
}
],
BaseStyle -> "OutputSizeLimit",
FrameMargins -> {{12, 12}, {0, 15}},
FrameStyle -> GrayLevel[0.85],
RoundingRadius -> 5,
StripOnInput -> False
],
Deploy,
DefaultBaseStyle -> "Deploy"
],
If[ 17588487059817799587 === $SessionID,
Out[121],
Message[MessageName[Syntax, "noinfoker"]];
Missing["NotAvailable"];
]
]
],
"Output",
CellLabel -> "Out[121]="
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell[
BoxData[RowBox[{"LeafCount", "[", "condition", "]"}]],
"Input",
CellLabel -> "In[122]:="
],
Cell[BoxData["279080"], "Output", CellLabel -> "Out[122]="]
},
Open
]
],
Cell[
"Well, there\[CloseCurlyQuote]s a bunch of cases left in here - some `if` clauses we can\[CloseCurlyQuote]t refine because we can\[CloseCurlyQuote]t prove what their inputs are. Extract them all, and condition on them.",
"Text"
],
Cell[
BoxData[
{
RowBox[
{
RowBox[{"caseBash", "[", "exprs_List", "]"}],
":=",
RowBox[
{
"Flatten",
"[",
RowBox[
{
RowBox[
{
RowBox[
{
"Function",
"[",
RowBox[
{
RowBox[{"{", "exprAndRules", "}"}],
",",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"expr",
"=",
RowBox[{"exprAndRules", "[", RowBox[{"[", "2", "]"}], "]"}]
}
],
",",
RowBox[
{
"rules",
"=",
RowBox[{"exprAndRules", "[", RowBox[{"[", "1", "]"}], "]"}]
}
]
}
],
"}"
}
],
",",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
"cases",
"=",
RowBox[
{
"MinimalBy",
"[",
RowBox[
{
RowBox[
{
"Cases",
"[",
RowBox[
{
"expr",
",",
RowBox[
{
RowBox[
{"if", "[", RowBox[{"cond_", ",", "_", ",", "_"}], "]"}
],
":>",
"cond"
}
],
",",
"All"
}
],
"]"
}
],
",",
"LeafCount"
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"If",
"[",
RowBox[
{
RowBox[{"cases", "===", RowBox[{"{", "}"}]}],
",",
RowBox[{"{", "exprAndRules", "}"}],
",",
RowBox[
{
RowBox[
{
"Function",
"[",
RowBox[
{
RowBox[{"{", "case", "}"}],
",",
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{"Append", "[", RowBox[{"rules", ",", "case"}], "]"}
],
",",
RowBox[{"expr", "/.", RowBox[{"case", "->", "true"}]}]
}
],
"}"
}
],
",",
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"Append",
"[",
RowBox[{"rules", ",", RowBox[{"not", "@", "case"}]}],
"]"
}
],
",",
RowBox[{"expr", "/.", RowBox[{"case", "->", "false"}]}]
}
],
"}"
}
]
}
],
"}"
}
]
}
],
"]"
}
],
"@",
RowBox[{"First", "@", "cases"}]
}
]
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"]"
}
]
}
],
"]"
}
],
"/@",
"exprs"
}
],
",",
"1"
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
RowBox[
{
RowBox[{"caseBash", "[", "expr_", "]"}],
":=",
RowBox[
{
"caseBash",
"[",
RowBox[
{
"{",
RowBox[
{"{", RowBox[{RowBox[{"{", "}"}], ",", "expr"}], "}"}
],
"}"
}
],
"]"
}
]
}
]
}
],
"Input",
CellLabel -> "In[123]:="
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"done",
"=",
RowBox[
{
RowBox[
{
"Select",
"[",
RowBox[
{
RowBox[
{
"FixedPoint",
"[",
RowBox[{"caseBash", ",", "condition"}],
"]"
}
],
",",
RowBox[
{
RowBox[
{
RowBox[{"#", "[", RowBox[{"[", "2", "]"}], "]"}],
"=!=",
"false"
}
],
"&"
}
]
}
],
"]"
}
],
"//",
"AbsoluteTiming"
}
]
}
]
],
"Input",
CellLabel -> "In[125]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
"0.270172`",
",",
RowBox[
{
"{",
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "6", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "5", "]"}], ",", "7"}],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "8", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{RowBox[{"w", "[", "7", "]"}], ",", RowBox[{"-", "5"}]}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "9", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{RowBox[{"w", "[", "4", "]"}], ",", RowBox[{"-", "8"}]}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "11", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{RowBox[{"w", "[", "10", "]"}], ",", RowBox[{"-", "4"}]}
],
"]"
}
]
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "12", "]"}],
",",
RowBox[{"w", "[", "3", "]"}]
}
],
"]"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "13", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[{RowBox[{"w", "[", "2", "]"}], ",", "5"}],
"]"
}
]
}
],
"]"
}
]
}
],
"}"
}
],
",",
RowBox[
{
"equal",
"[",
RowBox[
{
RowBox[{"w", "[", "14", "]"}],
",",
RowBox[
{
"plus",
"[",
RowBox[
{RowBox[{"w", "[", "1", "]"}], ",", RowBox[{"-", "1"}]}
],
"]"
}
]
}
],
"]"
}
]
}
],
"}"
}
],
"}"
}
]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[125]="
]
},
Open
]
],
Cell[
"Let\[CloseCurlyQuote]s make it look a bit nicer:",
"Text"
],
Cell[
BoxData[
RowBox[
{
RowBox[
{
"translate",
"=",
RowBox[
{
"{",
RowBox[
{
RowBox[{"equal", "->", "Equal"}],
",",
RowBox[{"plus", "->", "Plus"}]
}
],
"}"
}
]
}
],
";"
}
]
],
"Input",
CellLabel -> "In[126]:="
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"translated",
"=",
RowBox[
{
RowBox[
{
"Flatten",
"[",
RowBox[
{
"done",
"[",
RowBox[{"[", RowBox[{"2", ",", "1"}], "]"}],
"]"
}
],
"]"
}
],
"/.",
"translate"
}
]
}
]
],
"Input",
CellLabel -> "In[133]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
RowBox[
{
RowBox[{"w", "[", "6", "]"}],
"\[Equal]",
RowBox[{"7", "+", RowBox[{"w", "[", "5", "]"}]}]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "8", "]"}],
"\[Equal]",
RowBox[
{RowBox[{"-", "5"}], "+", RowBox[{"w", "[", "7", "]"}]}
]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "9", "]"}],
"\[Equal]",
RowBox[
{RowBox[{"-", "8"}], "+", RowBox[{"w", "[", "4", "]"}]}
]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "11", "]"}],
"\[Equal]",
RowBox[
{RowBox[{"-", "4"}], "+", RowBox[{"w", "[", "10", "]"}]}
]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "12", "]"}],
"\[Equal]",
RowBox[{"w", "[", "3", "]"}]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "13", "]"}],
"\[Equal]",
RowBox[{"5", "+", RowBox[{"w", "[", "2", "]"}]}]
}
],
",",
RowBox[
{
RowBox[{"w", "[", "14", "]"}],
"\[Equal]",
RowBox[
{RowBox[{"-", "1"}], "+", RowBox[{"w", "[", "1", "]"}]}
]
}
]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[133]="
]
},
Open
]
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell["The final answers", "Subtitle"],
Cell[
"Each of the fourteen variables appears exactly once in the list of constraints:",
"Text"
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
RowBox[
{
"Sort",
"[",
RowBox[
{
"Sequence",
"@@@",
RowBox[
{
"Flatten",
"[",
RowBox[
{
RowBox[
{
RowBox[
{"Cases", "[", RowBox[{"#", ",", "_w", ",", "All"}], "]"}
],
"&"
}
],
"/@",
"translated"
}
],
"]"
}
]
}
],
"]"
}
],
"==",
RowBox[{"Range", "[", RowBox[{"1", ",", "14"}], "]"}]
}
]
],
"Input",
CellLabel -> "In[140]:="
],
Cell[BoxData["True"], "Output", CellLabel -> "Out[140]="]
},
Open
]
],
Cell["Each equation has exactly two variables:", "Text"],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"AllTrue",
"[",
RowBox[
{
"translated",
",",
RowBox[
{
RowBox[
{
RowBox[
{
"Length",
"@",
RowBox[
{"Cases", "[", RowBox[{"#", ",", "_w", ",", "All"}], "]"}
]
}
],
"==",
"2"
}
],
"&"
}
]
}
],
"]"
}
]
],
"Input",
CellLabel -> "In[144]:="
],
Cell[BoxData["True"], "Output", CellLabel -> "Out[144]="]
},
Open
]
],
Cell[
"So to maximise, we just maximise the smaller-index variable in each constraint.",
"Text"
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"max",
"=",
RowBox[
{
RowBox[
{
RowBox[
{
"Function",
"[",
RowBox[
{
RowBox[{"{", "constraint", "}"}],
",",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
"vars",
"=",
RowBox[
{
"SortBy",
"[",
RowBox[
{
RowBox[
{
"Cases",
"[",
RowBox[{"constraint", ",", "_w", ",", "All"}],
"]"
}
],
",",
RowBox[{RowBox[{"Sequence", "@@", "#"}], "&"}],
",",
"1"
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"toBeLarger",
"=",
RowBox[{"vars", "[", RowBox[{"[", "1", "]"}], "]"}]
}
],
",",
RowBox[
{
"toBeSmaller",
"=",
RowBox[{"vars", "[", RowBox[{"[", "2", "]"}], "]"}]
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"Thread",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[{"vars", "[", RowBox[{"[", "1", "]"}], "]"}],
",",
RowBox[{"vars", "[", RowBox[{"[", "2", "]"}], "]"}]
}
],
"}"
}
],
"->",
RowBox[
{
"First",
"@",
RowBox[
{
"MaximalBy",
"[",
RowBox[
{
RowBox[
{
"Select",
"[",
RowBox[
{
RowBox[
{
"Tuples",
"[",
RowBox[
{
RowBox[{"Range", "[", RowBox[{"1", ",", "9"}], "]"}],
",",
"2"
}
],
"]"
}
],
",",
RowBox[
{
RowBox[
{
"constraint",
"/.",
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"toBeLarger",
"->",
RowBox[{"#", "[", RowBox[{"[", "1", "]"}], "]"}]
}
],
",",
RowBox[
{
"toBeSmaller",
"->",
RowBox[{"#", "[", RowBox[{"[", "2", "]"}], "]"}]
}
]
}
],
"}"
}
]
}
],
"&"
}
]
}
],
"]"
}
],
",",
"First"
}
],
"]"
}
]
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
],
"]"
}
],
"/@",
"translated"
}
],
"//",
"Flatten"
}
]
}
]
],
"Input",
CellLabel -> "In[160]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
RowBox[{RowBox[{"w", "[", "5", "]"}], "\[Rule]", "2"}],
",",
RowBox[{RowBox[{"w", "[", "6", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "7", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "8", "]"}], "\[Rule]", "4"}],
",",
RowBox[{RowBox[{"w", "[", "4", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "9", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "10", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "11", "]"}], "\[Rule]", "5"}],
",",
RowBox[{RowBox[{"w", "[", "3", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "12", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "2", "]"}], "\[Rule]", "4"}],
",",
RowBox[{RowBox[{"w", "[", "13", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "1", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "14", "]"}], "\[Rule]", "8"}]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[160]="
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
RowBox[{"w", "/@", RowBox[{"Range", "[", "14", "]"}]}],
"/.",
"max"
}
]
],
"Input",
CellLabel -> "In[161]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
"9",
",",
"4",
",",
"9",
",",
"9",
",",
"2",
",",
"9",
",",
"9",
",",
"4",
",",
"1",
",",
"9",
",",
"5",
",",
"9",
",",
"9",
",",
"8"
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[161]="
]
},
Open
]
],
Cell[
"And to minimise, we minimise the smaller-index variable.",
"Text"
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
"min",
"=",
RowBox[
{
RowBox[
{
RowBox[
{
"Function",
"[",
RowBox[
{
RowBox[{"{", "constraint", "}"}],
",",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
"vars",
"=",
RowBox[
{
"SortBy",
"[",
RowBox[
{
RowBox[
{
"Cases",
"[",
RowBox[{"constraint", ",", "_w", ",", "All"}],
"]"
}
],
",",
RowBox[{RowBox[{"Sequence", "@@", "#"}], "&"}],
",",
"1"
}
],
"]"
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"With",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"toBeLarger",
"=",
RowBox[{"vars", "[", RowBox[{"[", "1", "]"}], "]"}]
}
],
",",
RowBox[
{
"toBeSmaller",
"=",
RowBox[{"vars", "[", RowBox[{"[", "2", "]"}], "]"}]
}
]
}
],
"}"
}
],
",",
"\[IndentingNewLine]",
RowBox[
{
"Thread",
"[",
RowBox[
{
RowBox[
{
"{",
RowBox[
{
RowBox[{"vars", "[", RowBox[{"[", "1", "]"}], "]"}],
",",
RowBox[{"vars", "[", RowBox[{"[", "2", "]"}], "]"}]
}
],
"}"
}
],
"->",
RowBox[
{
"First",
"@",
RowBox[
{
"MinimalBy",
"[",
RowBox[
{
RowBox[
{
"Select",
"[",
RowBox[
{
RowBox[
{
"Tuples",
"[",
RowBox[
{
RowBox[{"Range", "[", RowBox[{"1", ",", "9"}], "]"}],
",",
"2"
}
],
"]"
}
],
",",
RowBox[
{
RowBox[
{
"constraint",
"/.",
RowBox[
{
"{",
RowBox[
{
RowBox[
{
"toBeLarger",
"->",
RowBox[{"#", "[", RowBox[{"[", "1", "]"}], "]"}]
}
],
",",
RowBox[
{
"toBeSmaller",
"->",
RowBox[{"#", "[", RowBox[{"[", "2", "]"}], "]"}]
}
]
}
],
"}"
}
]
}
],
"&"
}
]
}
],
"]"
}
],
",",
"First"
}
],
"]"
}
]
}
]
}
],
"]"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
],
"\[IndentingNewLine]",
"]"
}
]
}
],
"]"
}
],
"/@",
"translated"
}
],
"//",
"Flatten"
}
]
}
]
],
"Input",
CellLabel -> "In[162]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
RowBox[{RowBox[{"w", "[", "5", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "6", "]"}], "\[Rule]", "8"}],
",",
RowBox[{RowBox[{"w", "[", "7", "]"}], "\[Rule]", "6"}],
",",
RowBox[{RowBox[{"w", "[", "8", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "4", "]"}], "\[Rule]", "9"}],
",",
RowBox[{RowBox[{"w", "[", "9", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "10", "]"}], "\[Rule]", "5"}],
",",
RowBox[{RowBox[{"w", "[", "11", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "3", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "12", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "2", "]"}], "\[Rule]", "1"}],
",",
RowBox[{RowBox[{"w", "[", "13", "]"}], "\[Rule]", "6"}],
",",
RowBox[{RowBox[{"w", "[", "1", "]"}], "\[Rule]", "2"}],
",",
RowBox[{RowBox[{"w", "[", "14", "]"}], "\[Rule]", "1"}]
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[162]="
]
},
Open
]
],
Cell[
CellGroupData[
{
Cell[
BoxData[
RowBox[
{
RowBox[{"w", "/@", RowBox[{"Range", "[", "14", "]"}]}],
"/.",
"min"
}
]
],
"Input",
CellLabel -> "In[163]:="
],
Cell[
BoxData[
RowBox[
{
"{",
RowBox[
{
"2",
",",
"1",
",",
"1",
",",
"9",
",",
"1",
",",
"8",
",",
"6",
",",
"1",
",",
"1",
",",
"5",
",",
"1",
",",
"1",
",",
"6",
",",
"1"
}
],
"}"
}
]
],
"Output",
CellLabel -> "Out[163]="
]
},
Open
]
]
},
Open
]
]
},
Open
]
]
},
PrivateNotebookOptions -> {
"CloudPublishPath" -> "/Published/advent-of-code-2021-day24.nb"
},
FrontEndVersion -> "13.0 for Mac OS X ARM (64-bit) (February 4, 2022)",
StyleDefinitions -> "Default.nb",
ExpressionUUID -> "23a7649c-1977-44d4-a2ae-d4c1c515d60c"
]
Reference in New Issue View Git Blame Copy Permalink