# code for Theorem 14:
def pdp "(p>=1) & (n>=1) & (p<=n) & (At (t+p<n) => PD[t] = PD[t+p])":
eval pdmat n "$pdp(n,p)":
def pdlp "$pdp(n,p) & (Aq (q>=1&q<p) => ~$pdp(n,q))":

# code for Theorem 15:
def tmper "(p>=1) & (n>=1) & (p<=n) & (At (t+p<n) => T[t] = T[t+p])":
def tmleastper "$tmper(n,p) & (Aq (q>=1&q<p) => ~$tmper(n,q))":

# every period p of the prefix of length n satisifes p >= (3/5) n
def tmp1 "Ap $tmper(n,p) => (5*p>=3*n)":
# exists a length-m prefix, m <= n, with period p satisfying p = (3/5)n
def tmp2 "Em Ep (m<=n) & $tmper(m,p) & (5*p = 3*m)":
def thm15a "$tmp1(n) & $tmp2(n)":
# this proves that ice = 5/3 for every prefix of length >= 5

def thm15b "Ap $tmper(n,p) & $tmleastper(n,p)":
# those n for which every period is a least period (in other words only one period)

# the matrices for Thue-Morse
eval tmmat n "$tmper(n,p)":