# ProvingGround

We formalize (in code) the combinatorial group theory part of the spltting lemma of the paper Homogenous length functions on Groups. This is based on an implementation (in scala) of a large part of Homotopy type theory equipped with symbolic algebra in this project.

## The statement

Assume we are given the following:

• A group $G$.
• A (length) function $l: G \to \mathbb{Q}$ such that
• For $g, h \in G$, $l(gh) \leq l(g) + l(h)$,
• For $g, h\in G$, $l(ghg^{-1}) = l(g$).
• Elements $x, y, z, w \in G$ such that
• $x \sim yw$ (here $\sim$ means conjugate in $G$),
• $x \sim zw^{-1}$.

Then we have the following:

Theorem: There exists a constant $A\in\mathbb{Q}$ so that for $n \in \mathbb{N}$,

$l(x^{2n}) \leq n(l(y) + l(z)) +A.$

In the above paper, homogeneity is used to deduce a bound for $l(x)$, and on taking the limit we get $l(x) \leq \frac{l(y) + l(z)}{2}$.

## Preliminaries

We start with some imports. This is a bit ugly due to avoiding variable name collisions.

scala>

scala> import provingground._, HoTT._

import provingground._, HoTT._

scala>

scala> import scalahott._, andrewscurtis.FreeGroups._

import scalahott._, andrewscurtis.FreeGroups._

scala> import spire.implicits._

import spire.implicits._

scala>
import NatRing.{ x=>_,  Literal => nat, _}, QField.{w => _, x =>_, y=>_, z=>_, Literal => rat, _}, FreeGroup.{Literal => elem, _}

import NatRing.{ x=>_,  Literal => nat, _}, QField.{w => _, x =>_, y=>_, z=>_, Literal => rat, _}, FreeGroup.{Literal => elem, _}

scala> import Theorems.{PowerDistributive, ConjPower}

import Theorems.{PowerDistributive, ConjPower}


## The Setup

We introduce terms for the length function $l$, as well as witnesses for the assumptions on $l$.

scala> val l = "l" :: FreeGroup ->: QTyp

l: Func[RepTerm[Word], RepTerm[spire.math.Rational]] with Subs[Func[RepTerm[Word], RepTerm[spire.math.Rational]]] = l

scala>

scala> val g = "g" :: FreeGroup

g: RepTerm[Word] with Subs[RepTerm[Word]] = g

scala> val h = "h" :: FreeGroup

h: RepTerm[Word] with Subs[RepTerm[Word]] = h

scala> val n = "n" :: NatTyp

n: RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]] = n

scala>

scala> val triang =
"triangle-inequality" :: (
g ~>: (h ~>: (
(leq(l(g |+| h))(l(g) + l(h)))
))
)

triang: FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], PosWit]] with Subs[FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], PosWit]]] = triangle-inequality

scala>

scala> val conjInv =
"conjugacy-invariance" :: (
g ~>: (
h ~>: (
(l(h) =:= (l(g |+| h |+| g.inverse)))
)
)
)

conjInv: FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], Equality[RepTerm[spire.math.Rational]]]] with Subs[FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], FuncLike[RepTerm[Word] with Subs[RepTerm[Word]], Equality[RepTerm[spire.math.Rational]]]]] = conjugacy-invariance

scala>


Next, we introduce variables for $x, y, z, s, t \in G$, where $s, t \in G$ are the elements so that the conjugacies $x \sim wy$ and $x \sim zw^{-1}$ are given by the equations $x = swys^{-1}$ and $x = tzw^{-1}t^{-1}$.

scala> val w = "w" :: FreeGroup

w: RepTerm[Word] with Subs[RepTerm[Word]] = w

scala> val y = "y" :: FreeGroup

y: RepTerm[Word] with Subs[RepTerm[Word]] = y

scala> val z = "z" :: FreeGroup

z: RepTerm[Word] with Subs[RepTerm[Word]] = z

scala> val s = "s" :: FreeGroup

s: RepTerm[Word] with Subs[RepTerm[Word]] = s

scala> val t = "t" :: FreeGroup

t: RepTerm[Word] with Subs[RepTerm[Word]] = t


So far these are all independent. We shall introduce terms as witnesses for the above equations later, as we first prove a lemma not involving $x$.

## Statement of lemma

The main internal repetition trick is captured the bound

$l((wy)^ns^{-1}t(zw^{-1})^n)\leq n(l(y) + l(z)) + l(s^{-1}) + l(t).$

We define $c(n) = (wy)^ns^{-1}t(zw^{-1})^n$ and $f(n) = n(l(y) + l(z)) + l(s^{-1}) + l(t)$, so the inequality is $l(c(n))\leq(f(n))$. We encode this below as the main lemma.

scala> val wy = w |+| y

wy: LocalTerm = ((mul) (w)) (y)

scala> val zwbar = z |+| w.inverse

zwbar: LocalTerm = ((mul) (z)) ((inv) (w))

scala> val wyn = FreeGroup.power(wy)(n)

wyn: RepTerm[Word] = (<function1>) (n)

scala> val zwbarn = FreeGroup.power(zwbar)(n)

zwbarn: RepTerm[Word] = (<function1>) (n)

scala>

scala> val c = n :-> (wyn |+| s.inverse |+| t |+| zwbarn) // this is the function we have to bound.

c: Func[RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]], LocalTerm] = (n :  Nat.Typ) ↦ (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))

scala>

scala> val r = incl(QField)

r: Rec[LocalTerm] = <function1>

scala>

scala> val f = n :-> (l(s.inverse) + l(t) + ((l(y) + l(z)) * r(n) ) )

f: Func[RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]], LocalTerm] = (n :  Nat.Typ) ↦ (((l) (t) + (l) ((inv) (s)) + ((l) (z) * (<function1>) (n)) + ((<function1>) (n) * (l) (y))))

scala>

scala> val lemma = n :-> (leq (l(c(n)) )(f(n) ) )

lemma: Func[RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]], Pos] = (n :  Nat.Typ) ↦ (Pos((((<function1>) (n) * (l) (y)) + ((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + ((<function1>) (n) * (l) (z)) + (l) ((inv) (s)) + (l) (t))))


## Proving the lemma

Let $d(n) = (wy)(wy)^ns^{-1}t(zw^{-1})^n(zw)$. Note that by definition $g^{n+1} = g^n g$, so we need to prove $d(n) = c(n+1)$. We use $g^ng^m = g^{n+m}$ (proved in our code) to prove this. The proof is given by the term dIsc.

scala> val d = n :-> (wy |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| zwbar)

d: Func[RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]], LocalTerm] = (n :  Nat.Typ) ↦ (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))

scala> val dIsc = FreeGroup.rm(s.inverse |+| t |+| zwbarn |+| zwbar) *: (PowerDistributive.pf(wy)(nat(1))(n))

dIsc: Equality[LocalTerm] = (ind{($dpmt : FreeGroup) ↦ (($dpmu :  FreeGroup) ↦ ($dpmt =$dpmu))(((mul) (w)) (((mul) (y)) ((<function1>) (n))))(((mul) ((<function1>) (n))) (((mul) (w)) (y)))}{($adxw : FreeGroup) ↦ (($adxx :  FreeGroup) ↦ ((_ : ($adxw =$adxx) :  $adxw =$adxx) ↦ (((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))) = ((mul) ($adxx)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}(($adxw : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ((<function1>) (n) : (((mul) (w)) (((mul) (y)) ((<function1>) (n))) = ((mul) ((<function1>) (n))) (((mul) (w)) (y)))) : (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))) = ((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))

scala> assert(dIsc.typ == (d(n) =:= c(succ(n))))


Next, let $b(n) = y(wy)^ns^{-1}t(zw^{-1})^nz$ be the conjugacy-reduced form of $d(n)$. Using $d(n) = c(n+1)$ and conjugacy invariance, we show that $l(c(n+1)) = l(b(n))$. The term bIsc is the proof of l(c(n+1)) = l(b(n)).

scala> val b = n :-> (y |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| z)

b: Func[RepTerm[spire.math.SafeLong] with Subs[RepTerm[spire.math.SafeLong]], LocalTerm] = (n :  Nat.Typ) ↦ (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))

scala> val lbIsld = conjInv(w)(y |+| c(n) |+| z)

lbIsld: Equality[RepTerm[spire.math.Rational]] = ((conjugacy-invariance) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))

scala> val bIsc = lbIsld && (l *: dIsc)

bIsc: Equality[RepTerm[spire.math.Rational] with Subs[RepTerm[spire.math.Rational]]] = ((ind{($stxr : Q.Typ) ↦ (($stxs :  Q.Typ) ↦ ($stxr =$stxs))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($hjcl : Q.Typ) ↦ (($hjcm :  Q.Typ) ↦ ((_ : ($hjcl =$hjcm) :  $hjcl =$hjcm) ↦ (($hjcm = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) → ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))}(($hjcl : Q.Typ) ↦ (($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) :$hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ↦ ($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))) (((conjugacy-invariance) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))) ((ind{($stxu : FreeGroup) ↦ (($stxv :  FreeGroup) ↦ ($stxu =$stxv))(((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))(((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}{($dtua : FreeGroup) ↦ (($dtub :  FreeGroup) ↦ ((_ : ($dtua =$dtub) :  $dtua =$dtub) ↦ ((l) ($dtua) = (l) ($dtub))))}(($dtua : FreeGroup) ↦ (Refl(Q.Typ,(l) ($dtua))))) ((ind{($dpmt : FreeGroup) ↦ (($dpmu :  FreeGroup) ↦ ($dpmt =$dpmu))(((mul) (w)) (((mul) (y)) ((<function1>) (n))))(((mul) ((<function1>) (n))) (((mul) (w)) (y)))}{($adxw : FreeGroup) ↦ (($adxx :  FreeGroup) ↦ ((_ : ($adxw =$adxx) :  $adxw =$adxx) ↦ (((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))) = ((mul) ($adxx)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}(($adxw : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ((<function1>) (n) : (((mul) (w)) (((mul) (y)) ((<function1>) (n))) = ((mul) ((<function1>) (n))) (((mul) (w)) (y)))) : (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))) = ((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) : ((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))) = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))

scala> assert(bIsc.typ == (l(b(n)) =:= l(c(succ(n))) ))


With these preliminaries, we can prove the lemma by induction. First note the base case.

scala> val baseCase = triang(inv(s))(t) !: (lemma(0))

baseCase: PosWit = ((triangle-inequality) ((inv) (s))) (t) : (Pos((((prod) (-1)) ((l) (((mul) ((inv) (s))) (t))) + (l) ((inv) (s)) + (l) (t))))


The induction step takes more work. We first assume the induction hypothesis.

scala> val hyp = "hyp" :: lemma(n)

hyp: PosWit with Subs[PosWit] = hyp : (Pos((((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y)))))


Next, we bound $l(b(n))$ (which we know is $l(c(n+ 1)))$ in terms of $l(c(n))$.

scala> val lbnBoundedlcnlylz = triang(y)(c(n)) + triang(y |+| c(n))(z)

lbnBoundedlcnlylz: PosWitSum = PosWitSum(((triangle-inequality) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (y) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))))),((triangle-inequality) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) (z) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))) + (l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) (z)))))

scala> assert(lbnBoundedlcnlylz.typ == (leq(l(b(n)))(l(c(n)) + l(y) + l(z))))


Now, using the induction hypothesis, we get a bound on $l(b(n))$.

scala> val lbnBounded = lbnBoundedlcnlylz + hyp

lbnBounded: PosWitSum = PosWitSum(PosWitSum(((triangle-inequality) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (y) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))))),((triangle-inequality) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) (z) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))) + (l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) (z))))),hyp : (Pos((((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))

scala> assert(lbnBounded.typ == leq(l(b(n)) )(f(succ(n))) )


Next, we put together $l(c(n+1)) = l(b(n))$ and the bound on $l(b(n))$ to get the required bound on $l(c(n+1))$.

scala> val bnd = "bound" :: QField.LocalTyp

bnd: RepTerm[spire.math.Rational] with Subs[RepTerm[spire.math.Rational]] = bound

scala> val cbnd = bIsc.lift(bnd :-> (leq(bnd)(f(succ(n)) ) ))

cbnd: Func[PosWit, PosWit] = (ind{($ciyea : Q.Typ) ↦ (($ciyeb :  Q.Typ) ↦ ($ciyea =$ciyeb))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($tghe : Q.Typ) ↦ (($tghf :  Q.Typ) ↦ ((_ : ($tghe =$tghf) :  $tghe =$tghf) ↦ ((Pos(((l) (z) + (l) (y) + ((prod) (-1)) ($tghe) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (z) + (l) (y) + (l) ((inv) (s)) + ((prod) (-1)) ($tghf) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))}(($tghe : Q.Typ) ↦ (($anlea : (Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) : Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) ↦ ($anlea : (Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))) (((ind{($stxr : Q.Typ) ↦ (($stxs :  Q.Typ) ↦ ($stxr =$stxs))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($hjcl : Q.Typ) ↦ (($hjcm :  Q.Typ) ↦ ((_ : ($hjcl =$hjcm) :  $hjcl =$hjcm) ↦ (($hjcm = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) → ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))}(($hjcl : Q.Typ) ↦ (($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) :$hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ↦ ($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))) (((conjugacy-invariance) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))) ((ind{($stxu : FreeGroup) ↦ (($stxv :  FreeGroup) ↦ ($stxu =$stxv))(((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))(((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}{($dtua : FreeGroup) ↦ (($dtub :  FreeGroup) ↦ ((_ : ($dtua =$dtub) :  $dtua =$dtub) ↦ ((l) ($dtua) = (l) ($dtub))))}(($dtua : FreeGroup) ↦ (Refl(Q.Typ,(l) ($dtua))))) ((ind{($dpmt : FreeGroup) ↦ (($dpmu :  FreeGroup) ↦ ($dpmt =$dpmu))(((mul) (w)) (((mul) (y)) ((<function1>) (n))))(((mul) ((<function1>) (n))) (((mul) (w)) (y)))}{($adxw : FreeGroup) ↦ (($adxx :  FreeGroup) ↦ ((_ : ($adxw =$adxx) :  $adxw =$adxx) ↦ (((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))) = ((mul) ($adxx)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}(($adxw : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ((<function1>) (n) : (((mul) (w)) (((mul) (y)) ((<function1>) (n))) = ((mul) ((<function1>) (n))) (((mul) (w)) (y)))) : (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))) = ((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) : ((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))) = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul...

scala> val step = cbnd(lbnBounded)

step: PosWit = ((ind{($ciyea : Q.Typ) ↦ (($ciyeb :  Q.Typ) ↦ ($ciyea =$ciyeb))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($tghe : Q.Typ) ↦ (($tghf :  Q.Typ) ↦ ((_ : ($tghe =$tghf) :  $tghe =$tghf) ↦ ((Pos(((l) (z) + (l) (y) + ((prod) (-1)) ($tghe) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (z) + (l) (y) + (l) ((inv) (s)) + ((prod) (-1)) ($tghf) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))}(($tghe : Q.Typ) ↦ (($anlea : (Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) : Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) ↦ ($anlea : (Pos(((l) (z) + ((prod) (-1)) ($tghe) + (l) (y) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))) (((ind{($stxr : Q.Typ) ↦ (($stxs :  Q.Typ) ↦ ($stxr =$stxs))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($hjcl : Q.Typ) ↦ (($hjcm :  Q.Typ) ↦ ((_ : ($hjcl =$hjcm) :  $hjcl =$hjcm) ↦ (($hjcm = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) → ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))}(($hjcl : Q.Typ) ↦ (($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) :$hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ↦ ($hjrb : ($hjcl = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))))) (((conjugacy-invariance) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))))) ((ind{($stxu : FreeGroup) ↦ (($stxv :  FreeGroup) ↦ ($stxu =$stxv))(((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))(((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}{($dtua : FreeGroup) ↦ (($dtub :  FreeGroup) ↦ ((_ : ($dtua =$dtub) :  $dtua =$dtub) ↦ ((l) ($dtua) = (l) ($dtub))))}(($dtua : FreeGroup) ↦ (Refl(Q.Typ,(l) ($dtua))))) ((ind{($dpmt : FreeGroup) ↦ (($dpmu :  FreeGroup) ↦ ($dpmt =$dpmu))(((mul) (w)) (((mul) (y)) ((<function1>) (n))))(((mul) ((<function1>) (n))) (((mul) (w)) (y)))}{($adxw : FreeGroup) ↦ (($adxx :  FreeGroup) ↦ ((_ : ($adxw =$adxx) :  $adxw =$adxx) ↦ (((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))) = ((mul) ($adxx)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}(($adxw : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($adxw)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ((<function1>) (n) : (((mul) (w)) (((mul) (y)) ((<function1>) (n))) = ((mul) ((<function1>) (n))) (((mul) (w)) (y)))) : (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))) = ((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) : ((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))) = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mu...

scala> assert(step.typ == lemma(succ(n)))


Finally, the lemma is proved by induction.

scala> val lemmaProof = Induc(lemma, baseCase, n :~> (hyp :-> step))

lemmaProof: Induc[PosWit with Subs[PosWit]] = <function1>

scala> assert(lemmaProof.typ == (n ~>: (lemma(n))) )


## Rest of the proof of the theorem

Some work remains, essentially to use symbolic algebra for equations such as $x^{2n} = x^nx^n$ and to put together equations and inequalities. We introduce terms witnessing the hypotheses $x=swys^{-1}$ and $x=tzw^{-1}t^{-1}$

scala> val x = "x" :: FreeGroup

x: RepTerm[Word] with Subs[RepTerm[Word]] = x

scala> val g = "g" :: FreeGroup

g: RepTerm[Word] with Subs[RepTerm[Word]] = g

scala> val pown = g :-> FreeGroup.power(g)(n)

pown: Func[RepTerm[Word] with Subs[RepTerm[Word]], RepTerm[Word]] = (g :  FreeGroup) ↦ ((<function1>) (n))

scala>

scala> val c1 = "x ~ wy" :: (x =:= (s |+| w |+| y |+| s.inverse))

c1: Equality[RepTerm[Word] with Subs[RepTerm[Word]]] with Subs[Equality[RepTerm[Word] with Subs[RepTerm[Word]]]] = x ~ wy : (x = ((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))

scala> val c2 = "x ~ zw^{-1}" :: (x =:= (t |+| z |+| w.inverse |+| t.inverse))

c2: Equality[RepTerm[Word] with Subs[RepTerm[Word]]] with Subs[Equality[RepTerm[Word] with Subs[RepTerm[Word]]]] = x ~ zw^{-1} : (x = ((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))


We deduce using a theorem (in our code) about powers of conjugates that $x^n = s(wy)^ns^{-1} = t(zw^{-1})^nt^{-1}$.

scala> val xnConjwyn = (pown *: c1) && ConjPower.pf(s)(wy)(n)

xnConjwyn: Equality[RepTerm[Word] with Subs[RepTerm[Word]]] = ((ind{($cnmhm : FreeGroup) ↦ (($cnmhn :  FreeGroup) ↦ ($cnmhm =$cnmhn))((<function1>) (n))((<function1>) (n))}{($cmgsz : FreeGroup) ↦ (($cmgta :  FreeGroup) ↦ ((_ : ($cmgsz =$cmgta) :  $cmgsz =$cmgta) ↦ (($cmgta = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) → ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))}(($cmgsz : FreeGroup) ↦ (($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) :$cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) ↦ ($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))) ((ind{($cmkam : FreeGroup) ↦ (($cmkan :  FreeGroup) ↦ ($cmkam =$cmkan))(x)(((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))}{($ckpkx : FreeGroup) ↦ (($ckpky :  FreeGroup) ↦ ((_ : ($ckpkx =$ckpky) :  $ckpkx =$ckpky) ↦ ((<function1>) (n) = (<function1>) (n))))}(($ckpkx : FreeGroup) ↦ (Refl(FreeGroup,(<function1>) (n))))) (x ~ wy : (x = ((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))) : ((<function1>) (n) = (<function1>) (n)))) ((<function1>) (n) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) scala> val xnConjzwbarn= (pown *: c2) && ConjPower.pf(t)(zwbar)(n) xnConjzwbarn: Equality[RepTerm[Word] with Subs[RepTerm[Word]]] = ((ind{($cpikk :  FreeGroup) ↦ (($cpikl : FreeGroup) ↦ ($cpikk = $cpikl))((<function1>) (n))((<function1>) (n))}{($cobrd :  FreeGroup) ↦ (($cobre : FreeGroup) ↦ ((_ : ($cobrd = $cobre) :$cobrd = $cobre) ↦ (($cobre = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) → ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))}(($cobrd :  FreeGroup) ↦ (($cocft : ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) :  $cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) ↦ ($cocft : ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))) ((ind{($coeyq :  FreeGroup) ↦ (($coeyr : FreeGroup) ↦ ($coeyq = $coeyr))(x)(((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))}{($cnmhp :  FreeGroup) ↦ (($cnmhq : FreeGroup) ↦ ((_ : ($cnmhp = $cnmhq) :$cnmhp = $cnmhq) ↦ ((<function1>) (n) = (<function1>) (n))))}(($cnmhp :  FreeGroup) ↦ (Refl(FreeGroup,(<function1>) (n))))) (x ~ zw^{-1} : (x = ((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))) : ((<function1>) (n) = (<function1>) (n)))) ((<function1>) (n) : ((<function1>) (n) = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))) : ((<function1>) (n) = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))

scala> assert(xnConjwyn.typ == (pown(x) =:= (s |+| pown(wy)  |+| s.inverse  ) ) )

scala> assert(xnConjzwbarn.typ == (pown(x) =:= (t |+| pown(zwbar)  |+| t.inverse  ) ) )


We use the above equations to show that $x^nx^n = s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

scala> val t1 = s |+| pown(wy)  |+| s.inverse

t1: LocalTerm = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))

scala> val t2 = t |+| pown(zwbar)  |+| t.inverse

t2: LocalTerm = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))

scala> val xnxnExpr = (FreeGroup.rm(pown(x)) *: xnConjwyn) && (FreeGroup.lm(t1) *: xnConjzwbarn)

xnxnExpr: Equality[LocalTerm with Subs[LocalTerm]] = ((ind{($cyhqn : FreeGroup) ↦ (($cyhqo :  FreeGroup) ↦ ($cyhqn =$cyhqo))(((mul) ((<function1>) (n))) ((<function1>) (n)))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n)))))}{($ctiow : FreeGroup) ↦ (($ctiox :  FreeGroup) ↦ ((_ : ($ctiow =$ctiox) :  $ctiow =$ctiox) ↦ (($ctiox = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($ctiow : FreeGroup) ↦ (($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) :$ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) ↦ ($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))) ((ind{($ctpfz : FreeGroup) ↦ (($ctpga :  FreeGroup) ↦ ($ctpfz =$ctpga))((<function1>) (n))(((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))}{($cpipx : FreeGroup) ↦ (($cpipy :  FreeGroup) ↦ ((_ : ($cpipx =$cpipy) :  $cpipx =$cpipy) ↦ (((mul) ($cpipx)) ((<function1>) (n)) = ((mul) ($cpipy)) ((<function1>) (n)))))}(($cpipx : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($cpipx)) ((<function1>) (n)))))) (((ind{($cnmhm : FreeGroup) ↦ (($cnmhn :  FreeGroup) ↦ ($cnmhm =$cnmhn))((<function1>) (n))((<function1>) (n))}{($cmgsz : FreeGroup) ↦ (($cmgta :  FreeGroup) ↦ ((_ : ($cmgsz =$cmgta) :  $cmgsz =$cmgta) ↦ (($cmgta = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) → ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))}(($cmgsz : FreeGroup) ↦ (($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) :$cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) ↦ ($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))) ((ind{($cmkam : FreeGroup) ↦ (($cmkan :  FreeGroup) ↦ ($cmkam =$cmkan))(x)(((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))}{($ckpkx : FreeGroup) ↦ (($ckpky :  FreeGroup) ↦ ((_ : ($ckpkx =$ckpky) :  $ckpkx =$ckpky) ↦ ((<function1>) (n) = (<function1>) (n))))}(($ckpkx : FreeGroup) ↦ (Refl(FreeGroup,(<function1>) (n))))) (x ~ wy : (x = ((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))) : ((<function1>) (n) = (<function1>) (n)))) ((<function1>) (n) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))) : (((mul) ((<function1>) (n))) ((<function1>) (n)) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n))))))) ((ind{($cyhqq :  FreeGroup) ↦ (($cyhqr : FreeGroup) ↦ ($cyhqq = $cyhqr))((<function1>) (n))(((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))}{($cqxma :  FreeGroup) ↦ (($cqxmb : FreeGroup) ↦ ((_ : ($cqxma = $cqxmb) :$cqxma = $cqxmb) ↦ (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxma))) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxmb))))))}(($cqxma :  FreeGroup) ↦ (Refl(FreeGroup,((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxma))))))) (((ind{($cpikk :  FreeGroup) ↦ (($cpikl : FreeGroup) ↦ ($cpikk = $cpikl))((<function1>) (n))((<function1>) (n))}{($cobrd :  FreeGroup) ↦ (($cobre : FreeGroup) ↦ ((_ : ($cobrd = $cobre) :$cobrd = $cobre) ↦ (($cobre = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) → ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))}(($cobrd :  FreeGroup) ↦ (($cocft : ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) :  $cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) ↦ ($cocft : ($cobrd = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))) ((ind{($coeyq :  FreeGroup) ↦ (($coeyr : FreeGroup) ↦ ($coeyq = $coeyr))(x)(((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))}{($cnmhp :  FreeGroup) ↦ (($cnmhq : FreeGroup) ↦ ((_ : ($cnmhp = $cnmhq) :$cnmhp = $cnmhq) ↦ ((<function1>) (n) = (<function1>) (n))))}(($cnmhp :  FreeGroup) ↦ (Refl(FreeGroup,(<function1>) (n))))) (x ~ zw^{-1} : (x = ((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))) : ((<function1>) (n) = (<function1>) (n)))) ((<function1>) (n) : ((<function1>) (n) = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))) : ((<function1>) (n) = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))) : (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n)))) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))) : (((mul) ((<function1>) (n))) ((<function1>) (n)) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))

scala> assert(xnxnExpr.typ == ((pown(x) |+| pown(x)) =:= (t1 |+| t2 )   ))


Using $x^nx^n = x^{2n}$, we get the formula $x^{2n} = s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

scala> val x2nExpr =PowerDistributive.pf(x)(n)(n).sym && xnxnExpr

x2nExpr: Equality[LocalTerm with Subs[LocalTerm] with Subs[LocalTerm with Subs[LocalTerm]]] = ((ind{($dawxw : FreeGroup) ↦ (($dawxx :  FreeGroup) ↦ ($dawxw =$dawxx))((<function1>) (((prod) (2)) (n)))(((mul) ((<function1>) (n))) ((<function1>) (n)))}{($cywvb : FreeGroup) ↦ (($cywvc :  FreeGroup) ↦ ((_ : ($cywvb =$cywvc) :  $cywvb =$cywvc) ↦ (($cywvc = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($cywvb : FreeGroup) ↦ (($cyxjr : ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) :$cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) ↦ ($cyxjr : ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))) ((ind{($czaqz : FreeGroup) ↦ (($czara :  FreeGroup) ↦ ($czaqz =$czara))(((mul) ((<function1>) (n))) ((<function1>) (n)))((<function1>) (((prod) (2)) (n)))}{($cykyp : FreeGroup) ↦ (($cykyq :  FreeGroup) ↦ ((_ : ($cykyp =$cykyq) :  $cykyp =$cykyq) ↦ ($cykyq =$cykyp)))}(($cykyp : FreeGroup) ↦ (Refl(FreeGroup,$cykyp)))) ((<function1>) (n) : (((mul) ((<function1>) (n))) ((<function1>) (n)) = (<function1>) (((prod) (2)) (n)))) : ((<function1>) (((prod) (2)) (n)) = ((mul) ((<function1>) (n))) ((<function1>) (n))))) (((ind{($cyhqn : FreeGroup) ↦ (($cyhqo :  FreeGroup) ↦ ($cyhqn =$cyhqo))(((mul) ((<function1>) (n))) ((<function1>) (n)))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n)))))}{($ctiow : FreeGroup) ↦ (($ctiox :  FreeGroup) ↦ ((_ : ($ctiow =$ctiox) :  $ctiow =$ctiox) ↦ (($ctiox = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($ctiow : FreeGroup) ↦ (($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) :$ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) ↦ ($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))) ((ind{($ctpfz : FreeGroup) ↦ (($ctpga :  FreeGroup) ↦ ($ctpfz =$ctpga))((<function1>) (n))(((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))}{($cpipx : FreeGroup) ↦ (($cpipy :  FreeGroup) ↦ ((_ : ($cpipx =$cpipy) :  $cpipx =$cpipy) ↦ (((mul) ($cpipx)) ((<function1>) (n)) = ((mul) ($cpipy)) ((<function1>) (n)))))}(($cpipx : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($cpipx)) ((<function1>) (n)))))) (((ind{($cnmhm : FreeGroup) ↦ (($cnmhn :  FreeGroup) ↦ ($cnmhm =$cnmhn))((<function1>) (n))((<function1>) (n))}{($cmgsz : FreeGroup) ↦ (($cmgta :  FreeGroup) ↦ ((_ : ($cmgsz =$cmgta) :  $cmgsz =$cmgta) ↦ (($cmgta = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) → ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))}(($cmgsz : FreeGroup) ↦ (($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) :$cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) ↦ ($cmhhp : ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))) ((ind{($cmkam : FreeGroup) ↦ (($cmkan :  FreeGroup) ↦ ($cmkam =$cmkan))(x)(((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))}{($ckpkx : FreeGroup) ↦ (($ckpky :  FreeGroup) ↦ ((_ : ($ckpkx =$ckpky) :  $ckpkx =$ckpky) ↦ ((<function1>) (n) = (<function1>) (n))))}(($ckpkx : FreeGroup) ↦ (Refl(FreeGroup,(<function1>) (n))))) (x ~ wy : (x = ((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s)))))) : ((<function1>) (n) = (<function1>) (n)))) ((<function1>) (n) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))) : ((<function1>) (n) = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))) : (((mul) ((<function1>) (n))) ((<function1>) (n)) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n))))))) ((ind{($cyhqq :  FreeGroup) ↦ (($cyhqr : FreeGroup) ↦ ($cyhqq = $cyhqr))((<function1>) (n))(((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))}{($cqxma :  FreeGroup) ↦ (($cqxmb : FreeGroup) ↦ ((_ : ($cqxma = $cqxmb) :$cqxma = $cqxmb) ↦ (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxma))) = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxmb))))))}(($cqxma :  FreeGroup) ↦ (Refl(FreeGroup,((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ($cqxma))))))) (((ind{($cpikk :  FreeGroup) ↦ (($cpikl : FreeGroup) ↦ ($cpikk = $cpikl))((<function1>) (n))((<function1>) (n))}{($...

scala> assert(x2nExpr.typ == (FreeGroup.power(x)(NatRing.prod(n)(nat(2))) =:= (s |+| c(n) |+| t.inverse)))


We now bound the length of the right hand side $s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

scala> val thmBound = f(n) + l(s) + l(t.inverse)

thmBound: LocalTerm = ((l) (s) + (l) ((inv) (t)) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y)))

scala> val exprBound = lemmaProof(n) + triang(s)(c(n)) + triang(s |+| c(n))(t.inverse)

exprBound: PosWitSum = PosWitSum(PosWitSum((<function1>) (n) : (Pos((((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))),((triangle-inequality) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (s) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))))),((triangle-inequality) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) ((inv) (t)) : (Pos((((prod) (-1)) ((l) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))) + (l) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (t))))))

scala> assert(exprBound.typ == leq(l(s |+| c(n) |+| t.inverse ))(thmBound))


We easily deduce the bound on $l(x^{2n})$ to complete the proof.

scala> val thmProof = x2nExpr.sym.lift (g :-> leq(l(g))(thmBound))(exprBound)

thmProof: PosWit = ((ind{($fqtdr : FreeGroup) ↦ (($fqtds :  FreeGroup) ↦ ($fqtdr =$fqtds))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))((<function1>) (((prod) (2)) (n)))}{($detqw : FreeGroup) ↦ (($detqx :  FreeGroup) ↦ ((_ : ($detqw =$detqx) :  $detqw =$detqx) ↦ ((Pos(((l) (s) + (l) ((inv) (t)) + ((prod) (-1)) ((l) ($detqw)) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (s) + (l) ((inv) (t)) + ((prod) (-1)) ((l) ($detqx)) + (l) ((inv) (s)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))}(($detqw : FreeGroup) ↦ (($ecgvs : (Pos(((l) (s) + (l) ((inv) (t)) + (l) ((inv) (s)) + ((prod) (-1)) ((l) ($detqw)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) : Pos(((l) (s) + (l) ((inv) (t)) + (l) ((inv) (s)) + ((prod) (-1)) ((l) ($detqw)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))) ↦ ($ecgvs : (Pos(((l) (s) + (l) ((inv) (t)) + (l) ((inv) (s)) + ((prod) (-1)) ((l) ($detqw)) + (l) (t) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))))))) ((ind{($fhavn : FreeGroup) ↦ (($fhavo :  FreeGroup) ↦ ($fhavn =$fhavo))((<function1>) (((prod) (2)) (n)))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))}{($dbhxy : FreeGroup) ↦ (($dbhxz :  FreeGroup) ↦ ((_ : ($dbhxy =$dbhxz) :  $dbhxy =$dbhxz) ↦ ($dbhxz =$dbhxy)))}(($dbhxy : FreeGroup) ↦ (Refl(FreeGroup,$dbhxy)))) (((ind{($dawxw : FreeGroup) ↦ (($dawxx :  FreeGroup) ↦ ($dawxw =$dawxx))((<function1>) (((prod) (2)) (n)))(((mul) ((<function1>) (n))) ((<function1>) (n)))}{($cywvb : FreeGroup) ↦ (($cywvc :  FreeGroup) ↦ ((_ : ($cywvb =$cywvc) :  $cywvb =$cywvc) ↦ (($cywvc = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($cywvb : FreeGroup) ↦ (($cyxjr : ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) :$cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) ↦ ($cyxjr : ($cywvb = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))) ((ind{($czaqz : FreeGroup) ↦ (($czara :  FreeGroup) ↦ ($czaqz =$czara))(((mul) ((<function1>) (n))) ((<function1>) (n)))((<function1>) (((prod) (2)) (n)))}{($cykyp : FreeGroup) ↦ (($cykyq :  FreeGroup) ↦ ((_ : ($cykyp =$cykyq) :  $cykyp =$cykyq) ↦ ($cykyq =$cykyp)))}(($cykyp : FreeGroup) ↦ (Refl(FreeGroup,$cykyp)))) ((<function1>) (n) : (((mul) ((<function1>) (n))) ((<function1>) (n)) = (<function1>) (((prod) (2)) (n)))) : ((<function1>) (((prod) (2)) (n)) = ((mul) ((<function1>) (n))) ((<function1>) (n))))) (((ind{($cyhqn : FreeGroup) ↦ (($cyhqo :  FreeGroup) ↦ ($cyhqn =$cyhqo))(((mul) ((<function1>) (n))) ((<function1>) (n)))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n)))))}{($ctiow : FreeGroup) ↦ (($ctiox :  FreeGroup) ↦ ((_ : ($ctiow =$ctiox) :  $ctiow =$ctiox) ↦ (($ctiox = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($ctiow : FreeGroup) ↦ (($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) :$ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) ↦ ($ctjdm : ($ctiow = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))) ((ind{($ctpfz : FreeGroup) ↦ (($ctpga :  FreeGroup) ↦ ($ctpfz =$ctpga))((<function1>) (n))(((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))))}{($cpipx : FreeGroup) ↦ (($cpipy :  FreeGroup) ↦ ((_ : ($cpipx =$cpipy) :  $cpipx =$cpipy) ↦ (((mul) ($cpipx)) ((<function1>) (n)) = ((mul) ($cpipy)) ((<function1>) (n)))))}(($cpipx : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($cpipx)) ((<function1>) (n)))))) (((ind{($cnmhm : FreeGroup) ↦ (($cnmhn :  FreeGroup) ↦ ($cnmhm =$cnmhn))((<function1>) (n))((<function1>) (n))}{($cmgsz : FreeGroup) ↦ (($cmgta :  FreeGroup) ↦ ((_ : ($cmgsz =$cmgta) :  $cmgsz =$cmgta) ↦ (($cmgta = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) → ($cmgsz = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))}(($cmgsz : FreeGroup) ↦ (($cmhhp : (\$cmgsz = ((mul) (s)) (((mul) (...

scala> val x2n = FreeGroup.power(x)(NatRing.prod(n)(nat(2)))

x2n: RepTerm[Word] = (<function1>) (((prod) (2)) (n))

scala> assert(thmProof.typ == leq(l(x2n))(thmBound ))

scala>