ProveTriHof1thruN.txt

##################################################################
##ProveTriHof1thruN.txt: This file is made to accompany          #
##Chapter 9 of Nathan Fox's doctoral thesis.                     #
##                                                               #
##Save this file as ProveTriHof1thruN.txt                        #
##To use it, stay in the                                         #
##same directory, start Maple (by typing: maple <Enter> )        #
##and then type:  read ProveTriHof1thruN.txt <Enter>             #
##                                                               #
##This file depends on mapledoc.txt and nonstdhof.txt, which can #
##be found in the same online directory as this file             #
##                                                               #
##Written by Nathan Fox, Rutgers University,                     #
##fox at math dot rutgers dot edu                                #
##Version 1.0.0                                                  #
##################################################################

read(`nonstdhof.txt`):
with(NonStdHof):

printf("%s\n\n%s\n\n%s@math.rutgers.edu\n\n%s\n\n%s\n%s\n%s\n%s\n",
    "This is ProveTriHof1thruN.txt",
    "It accompanies Section 9.2 of \"An Exploration of Nested Recurrences Using Experimental Mathematics\" by Nathan Fox",
    "Please report bugs to fox",
    "The most current version of this package is available from",
    "http://github.com/nhf216/thesis/ProveTriHof1thruN.txt",
    "For a list of the procedures in this package, along with their usage, type HelpProveTriHof();.",
    "For help with a specific procedure, type HelpProveTriHof(procedure_name);.",
    "For a brief description of a specific procedure, type Describe(procedure_name);."):

#mapledoc
Input:=':-Input':
Output:=':-Output':
Note:=':-Note':
__doc:=DocManager():

register(__doc, "FastTriHof(ic, terms, {failure, largestnumber})",
    Input::"ic: A list of integers, specifiying an initial condition",
    Input::"terms: A nonnegative integer, specifying how ",
    "many terms to generate",
    Input::"failure: Should we consider weak (true) or strong ",
    "(false) death? (default is false)",
    Input::"largestnumber: Treat any number larger than ",
    "largestnumber as infinity going forward (default is infinity). ",
    "This is helpful if terms grow exponentially.",
    Output::"The first terms terms (or as many as exist if it ",
    "dies first) of the sequence generated by the B-",
    "recurrence B(n)=B(n-B(n-1))+B(n-B(n-2))+B(n-B(n-3) ",
    "with initial conditions ic.  This procedure ",
    "is much faster than SeqQg, but it doesn't handle more general ",
    "recurrences.",
    Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
FastTriHof:=proc(ic, terms, {failure:=false, largestnumber:=infinity})
description "A faster procedure than SeqQg for calculating terms of sequences that satisfy the B-recurrence. (TRI_HOF)":
local L, n, i, TL, trm:
    L:=Array(ic):
    TL:=Array([0$3]):
    for n from nops(ic)+1 to terms do
        TL[1]:=n-L[-1]:
        TL[2]:=n-L[-2]:
        TL[3]:=n-L[-3]:
        trm:=0:
        for i from 1 to 3 do
            if TL[i] > 0 and TL[i] < n then
                trm:=trm + L[TL[i]]:
            elif failure then
                trm:=-infinity:
            fi:
        od:
        if trm = -infinity then
            break:
        elif trm > largestnumber then
            trm:=infinity:
        fi:
        L(n):=trm:
        if trm = 0 then
            break:
        fi:
    od:
    return convert(L, list):
end:

register(__doc, "ProveStuff({start, cap, terms, S, storelast, failure})",
    Input::"start: a positive integer indicating where to start ",
    "the exploration (default is 3, which is the smallest ",
    "sporadic N value)",
    Input::"cap: a positive integer indicating where to end the ",
    "exploration (default is 32471, which is the largest ",
    "sporadic N value)",
    Input::"terms: a positive integer indicating how many terms ",
    "to generate while exploring each sequence (default is 100000)",
    Input::"S: a set of specific values to explore, or NULL to ",
    "explore all sporadic N values start<=N<=cap (default is NULL)",
    Input::"storelast: a nonnegative integer indicating how many ",
    "of the last terms of each sequence should be stored and ",
    "returned (default is 0)",
    Input::"failure: Should we consider weak (true) or strong ",
    "(false) death? (default is false)",
    Output::"A report about about the relevant sporadic N values "
    "(see Theorem 9.8 for listing of non-sporadic values)",
    Example::["start=4300, cap=4400", "returns [[4301, 13030], [4303, 17493], [4308, 12417], [4310, 9420], [4317, 9368], [4324, 14768], [4331, 13118], [4338, 14211], [4345, 11076], [4352, 9368], [4359, 9518], [4366, 15533], [4373, 9403], [4380, 13839], [4387, 9557], [4394, 14228]], [\"4301 dies after 13030 terms.\", \"4303 dies after 17493 terms.\", \"4308 dies after 12417 terms.\", \"4310 dies after 9420 terms.\", \"4317 dies after 9368 terms.\", \"4324 dies after 14768 terms.\", \"4331 dies after 13118 terms.\", \"4338 dies after 14211 terms.\", \"4345 dies after 11076 terms.\", \"4352 dies after 9368 terms.\", \"4359 dies after 9518 terms.\", \"4366 dies after 15533 terms.\", \"4373 dies after 9403 terms.\", \"4380 dies after 13839 terms.\", \"4387 dies after 9557 terms.\", \"4394 dies after 14228 terms.\"]"]
):
ProveStuff:=proc({start:=3, cap:=32471, terms:=100000, S:=NULL, storelast:=0, failure:=false})
description "Analyze sporadic cases of the B-recurrence with initial conditions 1 through N":
local N, i, L, ret, ret2, ret3, st:
    ret:=[]:
    ret2:=[]:
    ret3:=[]:
    for N from start to cap do
        if (S <> NULL and N in S) or S = NULL then
            #196
            if (N mod 7 = 0 and N < 196) or
            #2087
            (N mod 7 = 1 and N < 2087) or
            #3201
            (N mod 7 = 2 and N < 3201) or
            #4315
            (N mod 7 = 3 and N < 4315) or
            #200
            (N mod 7 = 4 and N < 200) or
            #32478
            (N mod 7 = 5) or
            #118
            (N mod 7 = 6 and N < 118) then  
                #L:=SeqQg(terms, ic=[seq(i, i=1..N)], rec=TRI_HOF):
                L:=FastTriHof([seq(i, i=1..N)], terms, failure):
                if nops(L) = terms then
                    st:=sprintf("%d lives for at least %d terms.", N, terms):
                    if storelast > 0 then
                        ret3:=[op(ret3), L[-storelast..]]:
                    fi:
                else
                    st:=sprintf("%d dies after %d terms.", N, nops(L)):
                fi:
                printf("%s\n", st):
                ret:=[op(ret), [N, nops(L)]]:
                ret2:=[op(ret2), st]:
            fi:
        fi:
    od:
    if storelast > 0 then
        return ret, ret2, ret3:
    else
        return ret, ret2:
    fi:
end:

#100K
#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 20, 21, 23, 26, 27, 29, 30, 32, 34, 70, 81, 182, 193, 429, 646, 822, 988, 1031, 1164, 1185, 1892, 2756, 2789, 2935, 3442, 7292, 13263, 14992, 19129, 19395, 19493, 20207, 20375, 20396, 20501, 20592, 20676, 20830, 21523, 22699, 22923, 23126, 23378, 23511, 23700, 24624, 24862, 24876, 25163, 25373, 25632, 25884, 26262, 26360, 26724, 26745, 26801, 27263, 27298, 27592, 27620, 27634, 27732, 27767, 27837, 27844, 27851, 27886, 27935, 27991, 28201, 28383, 28593, 28614, 28691, 29111, 29223, 29412, 29475, 29818, 29930, 30007, 30154, 30308, 30378, 30595, 30609, 30700, 30875, 31078, 31120, 31260, 31435, 31477, 31526, 31666, 31694, 31736, 31764, 32058, 32191, 32247, 32261, 32324, 32352, 32408, 32415, 32450, 32457, 32471]

#200K
#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 20, 23, 26, 27, 30, 32, 34, 81, 182, 193, 429, 822, 1031, 1892, 2756, 2789, 2935, 3442, 7292, 13263, 14992, 19395, 20501, 20592, 20830, 22699, 23378, 23511, 25163, 27298, 31526, 32471]

#500K
#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 20, 23, 34, ...]

#Candidates (unknown eventual behavior)
#[4, 7, 8, 9, 10, 11, 12, 13, 14, 15, 18]

#Lives forever
#[5, 6, 81, 182, 193, 429, 822, 1892, 2789, 3442, 7292, 23511, 25163]

#Permanent ones (patterns happen when hit a 2 or 3 instead of a 0)
#5: SlowTriHof
#6: SlowTriHof
#81: Pattern starts in index 528, alternating between 2's and 565*2^k
#182: Pattern starts in index 391, alternating between 2's and 461*2^k
#429: Pattern starts in index 1269, alternating between 2's and 1313*2^k
#822: Pattern starts in index 3690, alternating between 2's and 4161*2^k
#1892: Pattern starts in index 5873, alternating between 2's and 6103*2^k
#2789: Pattern starts in index 9235, alternating between 2's and 10510*2^k
#7292: Pattern starts in index 22136, alternating between 2's and 22948*2^k
#23511: Pattern starts in index 69984, alternating between 2's and 70559*2^k
#25163: Pattern starts in index 75662, alternating between 2's and 82457*2^k

#3's and 5's
#193: 3, n, K+3k, 5, K+3k+2 pattern with ~470 length kinks (actually, they're length 441, and it lives forever)
#3442: 3, n, K+3k, 5, K+3k+2 pattern, lives forever
#20592: 3, n, K+3k, 5, K+3k+2 pattern, ends at some point but this sequence keeps going
#23378: 3, n, K+3k, 5, K+3k+2 pattern, eventually goes into period 3 thing, then dies after 1190843 terms
#32471: 3, n, K+3k, 5, K+3k+2 pattern, ends at some point and dies after 449436 terms

#Long deaths
#2756 has a 3, n, K+3k, 5, K+3k+2 pattern but dies after 221868 terms
#2935 dies after 1550992 terms (25 more) (see p. 1435 of notes)
#13263 has some weird stuff going on.  Looks like period 84, legit quasiperiodic.  But no, it dies after 780784 terms.
#14992 dies after 833558 terms (96 more)
#19395 dies after 80444792 terms (132 more)
#22699 dies after 11971312 terms (77 more)
#27298 dies after 141895479 terms (198 more)

#Other comments
#1031 dies after 213520 terms
#20501 keeps having period 3 for awhile, but dies after 276406 terms
#20830 has a similar pattern to the long deaths, but then something else happens.  It lives for more than 9050775 terms.  The something else has period 16, and has parts that grow by 7 per period.  These parts are enormous, though, meaning this sequence lives for an absurdly long time. SOLVED! (see p. 1443 of notes)
#31526 dies after 283520 terms

UpdateFile:=proc(fil, strs) local fin, fout, outstr, strs2, i, lin, spindex:
    fin:=fopen(fil, READ):
    i:=1:
    outstr:="":
    strs2:=[op(strs), cat("x"$100, " ")]:
    spindex:=StringTools[Search](" ", strs[i]):
    while true do
        lin:=readline(fin):
        #print(lin):
        if lin = 0 then
            break:
        fi:
        if lin[..spindex] = strs2[i][..spindex] then
            lin:=strs2[i]:
            i:=i+1:
            #if i <= nops(strs) then
            spindex:=StringTools[Search](" ", strs2[i]):
            #fi:
        fi:
        outstr:=cat(outstr, sprintf("%s\n", lin)):
    od:
    fclose(fin):
    fout:=fopen(fil, WRITE):
    fprintf(fout, "%s", outstr):
    fclose(fout):
    print("Done"):
end:

ExtractMaxes:=proc(L, cap) local ret, i:
    ret:={}:
    for i from 1 to nops(L) do
        if L[i][2] = cap then
            ret:=ret union {L[i][1]}:
        fi:
    od:
    return ret:
end:

GeneratePeriod:=proc(threePos, {k:=':-h', N:=':-N'})
    if threePos = 0 then
        return [3, 5*k+1, 3*k+N+1, 5, 3*k+N+3]:
    elif threePos = 1 then
        return [3*k+N, 3, 5*k+2, 3*k+N+1, 5]:
    elif threePos = 2 then
        return [5, 3*k+N, 3, 5*k+3, 3*k+N+1]:
    elif threePos = 3 then
        return [3*k+N-2, 5, 3*k+N, 3, 5*k+4]:
    elif threePos = 4 then
        return [5*k, 3*k+N-2, 5, 3*k+N, 3]:
    fi:
end:

#L is the first some number of terms of the sequence (need 14k for 3442, 500 for 193)
AnalyzeTransitions:=proc(L, {lm:=1000, k:=':-h', N:=':-N', only01:=false}) local ret, a, b, ic, nic, lastblock, retstrings, st, newa, newb, Nexpr, bcap:
    retstrings:=[]:
    bcap:=9:
    if only01 then
        bcap:=1:
    fi:
    ret:=Matrix(5, bcap+1):
    for a from 0 to 4 do
        ic:=[[1..nops(L), L, []], [nops(L)+1..nops(L)+100, [], GeneratePeriod(a)]]:
        for b from 0 to bcap do
            print(sprintf("Now studying (%d, %d)", a, b)):
            nic:=ProveLongTermEventualSolution(ic, rec=TRI_HOF, iters=2, icsym=k, bigsymbols=[N], lmin=lm, bigsymbolmods={[N,b,10]}, belazy=true);
            lastblock:=nic[1][-1]:
            #print("hi"):
            #print(lastblock[-1]):
            if nops(lastblock[-1]) = 5 then
                newa:=ListTools[Search](3, lastblock[-1])-1:
                if newa = 0 then
                    Nexpr:=lastblock[-1][-1]-3*k-3:
                else
                    Nexpr:=lastblock[-1][newa]-3*k:
                fi:
                #print(Nexpr):
                newb:=specialmod(Nexpr, 10, [N], {[N,b,10]}):
                st:=sprintf("(%d, %d) goes to (%d, %d), %a, after a kink of length %d", a, b, newa, newb, Nexpr, nops(lastblock[2])):
                ret[a+1, b+1]:=[newa, newb]:
            elif nops(lastblock[-1]) = 0 then
                st:=sprintf("(%d, %d) dies", a, b):
            else
                st:=sprintf("(%d, %d) gets weird", a, b):
                ret[a+1, b+1]:=-1:
            fi:
            print(st):
            retstrings:=[op(retstrings), st]:
        od:
    od:
    return retstrings, ret:
end:

register(__doc, "KExplore193({icl, icsym, K, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 1000)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"K: A symbol to be treated as \"large\" (default is K)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 500)",
    Output::"A completion of the proof of Proposition 9.11. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
KExplore193:=proc({icl:=1000, icsym:=k, K:=':-K', lm:=500})#M:=':-M'
description "Complete the proof of Proposition 9.11, which analyzes initial conditions [1,2,3,...,193]":
local ic1, ic1K, a, i, mm, M, nic, nextK, nextM, L, sporadics:
    M:=2*K-89:
    ic1:=FastTriHof([seq(i, i=1..193)], icl):
    ic1K:=[[1..icl, ic1, []], [icl+1..K, [], [a[icsym]]], [K+1..K+5, [K+M, 3, K+3, K+M+1, 5], []]]:
    sporadics:={}:
    for mm from 0 to 4 do
        nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
        printf("K >= %d\n\n", op(1, op(nic[2]))):
        nic:=nic[1]:
        nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
        L:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
        for i from 2 to nops(L) do
            if L[i] = 3 then
                nextK:=nextK+i-3:
                nextM:=L[i-1]-nextK:
                break:
            fi:
        od:
        printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
        sporadics:=sporadics union {nic[-1][2]}:
    od:
    return sporadics:
end:

register(__doc, "KExplore3442({icl, icsym, K, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 13889)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"K: A symbol to be treated as \"large\" (default is K)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 12000)",
    Output::"A completion of the proof of Proposition 9.12. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
KExplore3442:=proc({icl:=13889, icsym:=k, K:=':-K', lm:=12000})#M:=':-M'
description "Complete the proof of Proposition 9.12, which analyzes initial conditions [1,2,3,...,3442]":
local ic1, ic1K, a, i, mm, M, nic, nextK, nextM, L, sporadics:
    M:=2*K-89:
    ic1:=FastTriHof([seq(i, i=1..3442)], icl):
    ic1K:=[[1..icl, ic1, []], [icl+1..K, [], [a[icsym]]], [K+1..K+5, [K+M, 3, K+3, K+M+1, 5], []]]:
    sporadics:={}:
    for mm from 0 to 4 do
        nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
        printf("K >= %d\n\n", op(1, op(nic[2]))):
        nic:=nic[1]:
        nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
        L:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
        for i from 2 to nops(L) do
            if L[i] = 3 then
                nextK:=nextK+i-3:
                nextM:=L[i-1]-nextK:
                break:
            fi:
        od:
        printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
        sporadics:=sporadics union {nic[-1][2]}:
    od:
    return sporadics:
end:

register(__doc, "Explore19395({icl, icsym, L, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 77734)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"L: A symbol to be treated as \"large\", representing lambda in Lemma 9.14 (default is L)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 150)",
    Output::"A completion of the proof of Lemma 9.14. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
Explore19395:=proc({icl:=77734, icsym:=k, L:=':-L', lm:=150})#M:=':-M'
description "Complete the proof of Lemma 9.14, which analyzes initial conditions [1,2,3,...,19395]":
local ic1, ic1K, a, i, nic, M1, M2, N, LL, sporadics:
    #M:=2*K-89:
    M1:=321833900:
    M2:=310800:
    N:=402278561:
    ic1:=FastTriHof([seq(i, i=1..19395)], icl):
    ic1K:=[[1..icl, ic1, []], [icl+1..L, [], [M2*2^(icsym-4859), 16, M2*2^(icsym-4858), 16, M2*2^(icsym-4859), 25, M1*2^(icsym-4859)+N-M1, L, 7, M2*2^(icsym-4858), 16, M2*2^(icsym-4858), 16, M1*2^(icsym-4858), L, 7]]]:
    #return ic1K:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    nic:=ProveEventualSolution(ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], lmin=lm, bigsymbolmods={[L,4,16]}):
    #nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,4,16]}, includeassumptions=true, Nmin=L+1):
    printf("L >= %d\n", op(1, op(nic[2]))):
    printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    return nic[1][-1]:
    #return nic[1]:
end:

register(__doc, "Explore27298({icl, icsym, L, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 112949)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"L: A symbol to be treated as \"large\", representing lambda in Lemma 9.15 (default is L)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 200)",
    Output::"A completion of the proof of Lemma 9.15. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
Explore27298:=proc({icl:=112949, icsym:=k, L:=':-L', lm:=200})#M:=':-M'
description "Complete the proof of Lemma 9.15, which analyzes initial conditions [1,2,3,...,27298]":
local ic1, ic1K, a, i, nic, M1, M2, N, LL, sporadics:
    #M:=2*K-89:
    M1:=1135082696:
    M2:=903192:
    N:=1276977978:
    ic1:=FastTriHof([seq(i, i=1..27298)], icl):
    ic1K:=[[1..icl, ic1, []], [icl+1..L, [], [16, M2*2^(icsym-7059), 16, M2*2^(icsym-7060), 25, M1*2^(icsym-7060)+N-M1, L, 7, M2*2^(icsym-7059), 16, M2*2^(icsym-7059), 16, M1*2^(icsym-7059), L, 7, M2*2^(icsym-7059)]]]:
    #return ic1K:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    nic:=ProveEventualSolution(ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], lmin=lm, bigsymbolmods={[L,1,16]}):
    #nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,4,16]}, includeassumptions=true, Nmin=L+1):
    printf("L >= %d\n", op(1, op(nic[2]))):
    printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    return nic[1][-1]:
    #return nic[1]:
end:

Explore20830:=proc({icl:=85009, icsym:=k, L:=':-L', M1:=':-M1', M2:=':-M2', N:=':-N', K:=':-K', lm:=100})#M:=':-M'
local ic1, ic1K, a, i, nic, LL, sporadics:
    #M:=2*K-89:
    #M1:=1135082696:
    #M2:=903192:
    #N:=1276977978:
    ic1:=FastTriHof([seq(i, i=1..20830)], icl):
    ic1K:=[[1..icl, ic1, []], [icl+1..K, [], [a[icsym]]], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]]]:
    #return ic1K:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    #nic:=ProveEventualSolution(ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], lmin=lm, bigsymbolmods={[L,1,16]}):
    nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[K, M2, L, M1, N], bigsymbolmods={[K,1,16], [L,7,16]}, includeassumptions=true, Nmin=L+1):
    printf("%a\n", nic[2]):
    #printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    #return nic[1][-1]:
    return nic[1]:
end:

register(__doc, "Explore20830a({icl, icsym, L, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 85009)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"L: A symbol to be treated as \"large\", representing lambda in Lemma 9.17 (default is L)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 100)",
    Output::"Prove the first behaviorial chunk of Lemma 9.17. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
Explore20830a:=proc({icl:=85009, icsym:=k, L:=':-L', lm:=100})#M:=':-M'
description "Continue the proof of Lemma 9.17, which analyzes initial conditions [1,2,3,...,20830]":
local ic1, ic1K, a, i, nic, M1, M2, N, K, LL, sporadics:
    #M:=2*K-89:
    M1:=36128364:
    M2:=339900:
    N:=45179140:
    K:=icl:
    ic1:=FastTriHof([seq(i, i=1..20830)], icl):
    #ic1K:=[[1..icl, ic1, []], [icl+1..L, [], [16, M2*2^(icsym-7059), 16, M2*2^(icsym-7060), 25, M1*2^(icsym-7060)+N-M1, L, 7, M2*2^(icsym-7059), 16, M2*2^(icsym-7059), 16, M1*2^(icsym-7059), L, 7, M2*2^(icsym-7059)]]]:
    ic1K:=[[1..icl, ic1, []], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]]]:
    #return ic1K:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    #nic:=ProveEventualSolution(ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], lmin=lm, bigsymbolmods={[L,1,16]}):
    nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,7,16]}, includeassumptions=true, Nmin=L+1):
    printf("L >= %d\n", op(1, op(nic[2]))):
    #printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    #return nic[1][-1]:
    return nic[1]:
end:

Explore20830b:=proc({icl:=85009, icsym:=k, L:=':-L', lm:=100})#M:=':-M'
local ic1, ic1K, ic1KK, a, i, nica, nic, M1, M2, N, K, LL, Lp, M1p, M2p, N1p, N2p, N3p, Kp:
    #M:=2*K-89:
    M1:=36128364:
    M2:=339900:
    N:=45179140:
    K:=icl:
    ic1:=FastTriHof([seq(i, i=1..20830)], icl):
    #ic1K:=[[1..icl, ic1, []], [icl+1..L, [], [16, M2*2^(icsym-7059), 16, M2*2^(icsym-7060), 25, M1*2^(icsym-7060)+N-M1, L, 7, M2*2^(icsym-7059), 16, M2*2^(icsym-7059), 16, M1*2^(icsym-7059), L, 7, M2*2^(icsym-7059)]]]:
    ic1K:=[[1..icl, ic1, []], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]]]:
    nica:=SeqQg(41, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,7,16]}, Nmin=L+1):
    Lp:=nica[25+5]:
    M1p:=nica[25+9]:
    M2p:=nica[25+2]:
    N1p:=nica[25+16]:
    N2p:=nica[25+4]:
    N3p:=nica[25+11]:
    Kp:=L+25:
    ic1KK:=[[1..icl, ic1, []], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]], [L+1..L+25, nica[..25], []], [L+26..Lp, [],
    [N1p+(2^(icsym-Kp/16)-2)*M1p, 16, M2p*2^(icsym-Kp/16), 7, 7*(icsym-Kp/16)+N2p, Lp, 16, Lp, 16, M1p*2^(icsym-Kp/16), 10, 16*(icsym-Kp/16)+N3p, M2p*2^(icsym-Kp/16), 7, Lp, 16]
    ]]:
    #return ic1KK:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    nic:=ProveEventualSolution(ic1KK, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], lmin=lm, bigsymbolmods={[L,7,16]}):
    #nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,7,16]}, includeassumptions=true, Nmin=Lp+1):
    #printf("L >= %d\n", op(1, op(nic[2]))):
    printf("L >= %d\n", op(1, op(nic[2]))):
    printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    return nic[1][-1]:
    #return nic[1]:
end:

register(__doc, "Explore20830c({icl, icsym, L, Lp, M1p, M2p, N1p, N2p, N3p, lm})",
    Input::"icl: A positive integer, specifying the initial ",
    "condition length to consider (default is 85009)",
    Input::"icsym: A symbol to use as icsym in nonstdhof.txt ",
    "(default is k)",
    Input::"L: A symbol to be treated as \"large\", representing lambda in Lemma 9.17 (default is L)",
    Input::"Lp: A symbol to represent lambda' in Lemma 9.17 ",
    "(default is Lp)",
    Input::"M1p: A symbol to represent mu_1' in Lemma 9.17 ",
    "(default is M1p)",
    Input::"M2p: A symbol to represent mu_2' in Lemma 9.17 ",
    "(default is M2p)",
    Input::"N1p: A symbol to represent nu_1' in Lemma 9.17 ",
    "(default is N1p)",
    Input::"N2p: A symbol to represent nu_2' in Lemma 9.17 ",
    "(default is N2p)",
    Input::"N3p: A symbol to represent nu_3' in Lemma 9.17 ",
    "(default is N3p)",
    Input::"lm: A positive integer, a tuning parameter specifying ",
    "how many terms to generate when calling ProveLongTermEventualSolution ",
    "as a subroutine (default is 100)",
    Output::"Prove the second behaviorial chunk of Lemma 9.17. Print ",
    "out relevant info as it runs, and return an exhaustive list ",
    "of terms, thereby serving as a proof certificate. ",
    "Of course, this proof is only valid given the results of ",
    "Explore20830a."
    #Example::["[1,1,1], 20", "returns [1, 1, 1, 3, 7, 8, 3, 8, 10, 4, 5, 12, 19, 11, 4, 19, 27, 11, 8, 22]"],
    #Example::["[1,2,3,4,5], 20", "returns [1, 2, 3, 4, 5, 6, 6, 7, 8, 9, 9, 10, 11, 12, 12, 13, 14, 15, 15, 16]"]
):
Explore20830c:=proc({icl:=85009, icsym:=k, L:=':-L', Lp:=':-Lp', M1p:=':-M1p', M2p:=':-M2p', N1p:=':-N1p', N2p:=':-N2p', N3p:=':-N3p', lm:=100})#M:=':-M'
description "Complete the proof of Lemma 9.17, which analyzes initial conditions [1,2,3,...,20830]":
local ic1, ic1K, ic1KK, a, i, nica, nic, M1, M2, N, K, LL, Kp:
    #M:=2*K-89:
    M1:=36128364:
    M2:=339900:
    N:=45179140:
    K:=icl:
    ic1:=FastTriHof([seq(i, i=1..20830)], icl):
    #ic1K:=[[1..icl, ic1, []], [icl+1..L, [], [16, M2*2^(icsym-7059), 16, M2*2^(icsym-7060), 25, M1*2^(icsym-7060)+N-M1, L, 7, M2*2^(icsym-7059), 16, M2*2^(icsym-7059), 16, M1*2^(icsym-7059), L, 7, M2*2^(icsym-7059)]]]:
    ic1K:=[[1..icl, ic1, []], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]]]:
    nica:=SeqQg(41, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,7,16]}, Nmin=L+1):
    #Lp:=nica[25+5]:
    #M1p:=nica[25+9]:
    #M2p:=nica[25+2]:
    #N1p:=nica[25+16]:
    #N2p:=nica[25+4]:
    #N3p:=nica[25+11]:
    Kp:=L+25:
    ic1KK:=[[1..icl, ic1, []], [K+1..L, [], [25, M1*2^(icsym-(K+15)/16)+N-M1, L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-1)/16), 16, M1*2^(icsym-(K-1)/16), L, 7, M2*2^(icsym-(K-1)/16), 16, M2*2^(icsym-(K-17)/16), 16, M2*2^(icsym-(K-1)/16)]], [L+1..L+25, nica[..25], []], [L+26..Lp, [],
    [N1p+(2^(icsym-Kp/16)-2)*M1p, 16, M2p*2^(icsym-Kp/16), 7, 7*(icsym-Kp/16)+N2p, Lp, 16, Lp, 16, M1p*2^(icsym-Kp/16), 10, 16*(icsym-Kp/16)+N3p, M2p*2^(icsym-Kp/16), 7, Lp, 16]
    ]]:
    #return ic1KK:
    #sporadics:={}:
    #for mm from 0 to 4 do
    #    nic:=ProveLongTermEventualSolution(ic1K, rec=TRI_HOF, iters=2, icsym=':-icsym', bigsymbols=[K], lmin=lm, bigsymbolmods={[K,mm,5]}):
    #    printf("K >= %d\n\n", op(1, op(nic[2]))):
    #    nic:=nic[1]:
    #    nextK:=nops(nic[-1][2]) + op(2, nic[-2][1])-1:
    #    LL:=SeqQg(6, Nmin=nextK, ic=nic, icsym=':-icsym', bigsymbols=[K], bigsymbolmods={[K,mm,5]}, rec=TRI_HOF):
    #    for i from 2 to nops(LL) do
    #        if L[i] = 3 then
    #            nextK:=nextK+i-3:
    #            nextM:=LL[i-1]-nextK:
    #            break:
    #        fi:
    #    od:
    #    printf("K = %d mod %d:\nPersists through %a\nNext K: %a\nNext M: %a\n\n", mm, 5, op(2, nic[-2][1]), nextK, nextM):
    #    sporadics:=sporadics union {nic[-1][2]}:
    #od:
    #return sporadics:
    nic:=ProveEventualSolution(ic1KK, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L, Lp, N2p, M2p, M1p, N1p, N3p], lmin=lm, bigsymbolmods={[L,7,16], [Lp, 0, 16]}):
    #nic:=SeqQg(lm, ic=ic1K, rec=TRI_HOF, ':-icsym'=icsym, bigsymbols=[L], bigsymbolmods={[L,7,16]}, includeassumptions=true, Nmin=Lp+1):
    #printf("L >= %d\n", op(1, op(nic[2]))):
    printf(cat(StringTools[Join](["%a"$nops(nic[2])], ", "), "\n"), op(nic[2])):
    printf("Died after %a terms\n", sort(op(2, nic[1][-1][1]))):
    #printf("Died after %d more terms\n", nops(nic[1])):
    return nic[1][-1]:
    #return nic[1]:
end:

CollapseTermsFile:=proc(fil, L, {startind:=1, Q:="B193"}) local f1, i:
    f1:=fopen(fil, WRITE):
    for i from 1 to nops(L) do
        fprintf(f1, "%s(%a) = %a\n", Q, sort(startind + i - 1), sort(L[i])):
    od:
    fclose(f1):
end:

#Help procedure
HelpProveTriHof:=getHelp(__doc):