# (-a) × (-a) = a × a

We all know that $$\(-a) \times (-a) = a \times a\$$ (hopefully), but can you prove it?

Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of rules that two binary operations on a set have to follow. The two operation are addition, $$\+\$$, and multiplication, $$\\times\$$. For this challenge here are the ring axioms where $$\+\$$ and $$\\times\$$ are closed binary operations on some set $$\S\$$, $$\-\$$ is a closed unary operation on $$\S\$$, and $$\a\$$, $$\b\$$, $$\c\$$ are members of $$\S\$$:

1. $$\a + (b + c) = (a + b) + c\$$

2. $$\a + 0 = a\$$

3. $$\a + (-a) = 0\$$

4. $$\a + b = b + a\$$*

5. $$\a \times (b \times c) = (a \times b) \times c\$$

6. $$\a \times 1 = a\$$

7. $$\1 × a = a\$$

8. $$\a \times (b + c) = (a \times b) + (a × c)\$$

9. $$\(b + c) \times a = (b \times a) + (c \times a)\$$

Your proof should be a string of equalities each being the application of one axiom.

You may apply the axioms to either the entire expression or to some sub-expression. For example if we have $$\(a + c) + (b + c)\$$ we can apply Axiom 4 to just the $$\(b + c)\$$ term, the $$\(a + c)\$$ term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to $$\((a \times c) + b) + ((-a) + 1)\$$ to get $$\((-a) + 1) + ((a \times c) + b)\$$. In each step of the proof you can only apply one axiom to one expression. All axioms are bidirectional, meaning substitution can go in either direction. Things like the following are not allowed

(a + b) + (c + d) = (a + (b + c)) + d Ax. 1


This should be done in two steps:

(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
= (a + (b + c)) + d Ax. 1


Facts you might normally take for granted but are not listed on the axioms list cannot be assumed, for example $$\(-a) = (-1) \times a\$$ is true but requires multiple steps to preform.

User Anthony has kindly provided a online proof validator that can be used as a replacement for TIO.

## Example proof

Here is an example proof that $$\-(-a) = a\$$ with the axioms used labeled on the right of each step.

 -(-a) = (-(-a)) + 0          Ax. 2
= 0 + (-(-a))          Ax. 4
= (a + (-a)) + (-(-a)) Ax. 3
= a + ((-a) + (-(-a))) Ax. 1
= a + 0                Ax. 3
= a                    Ax. 2


Try it online!

You will be tasked to prove $$\(-a) \times (-a) = a \times a\$$ using successive substitution like that shown above.

## Scoring

This is so your answers will be scored in number of steps taken to get from $$\(-a) \times (-a)\$$ to $$\a \times a\$$, with a lower score being better.

### Lemmas

Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion. For the uninitiated, lemmas are proofs of facts that you use later in the proof. In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader. In this challenge using lemmas should not have an direct effect on your score. (Although proof organization may make it easier or harder to golf)

If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it. For example the here is the score breakdown of a proof using lemmas.

Lemma:
a × 0 = 0

Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
= (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
= ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
= (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
= (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
= (a × b) + (-(a × b))               Ax. 2 (1)
= 0                                  Ax. 3 (1)

Theorem:
(a × 0) + (b × 0) = 0

Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
= (b × 0) + 0  Ax. 4 (1)
= b × 0        Ax. 2 (1)
= 0            Lemma (7)


*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.

†: Since $$\1\$$ does not appear in the desired equality any proof that uses these axioms is not minimal. That is these axioms cannot help with proving the desired fact. They have been included just for the sake of completeness.

• Is a program we write supposed to solve this, or just print the answer? – Tahg Sep 26 '17 at 22:42
• @Tahg You're supposed to prove it and submit your proof as an answer. This is different from most (if not all) problems you will see here. – hyper-neutrino Sep 26 '17 at 22:44
• I got frustratingly close before I realized that a*0=0 isn't in the list of axioms. – Sparr Sep 26 '17 at 22:48
• Erm... I might be wrong but isn't this way off-topic? Shouldn't answers contain code? – totallyhuman Sep 27 '17 at 1:25
• @icrieverytim if it helps, think of the axiom list as a programming language with nine built-in parameter substitution functions, and this is a code golf for a function that turns a specific input into a specific output. – Sparr Sep 27 '17 at 1:33

## 18 Steps

(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
= ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
= (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
= (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
= ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
= ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
= ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
= ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
= ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
= (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
= ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
= (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
= (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
= (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
= (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
= (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
= (a*a)+0                                                   Axiom 3
= a*a                                                       Axiom 2


I wrote a program to check my solution. So if you find an error in this, then my program is wrong too.

• @Etoplay Just out of curiosity, did you write your program in Prolog? – Jalil Compaoré Sep 27 '17 at 23:49
• It would be great if you could include your program. It could certainly help verify other solutions. – Wheat Wizard Sep 28 '17 at 4:20
• How did you get from the first line to the second just by applying one axiom one time? – SztupY Sep 28 '17 at 8:15
• @SztupY Axiom 3 is v + (-v) = 0 let v = ((a*a)+(a*(-a)) and you get there in 1 step. – MT0 Sep 28 '17 at 11:42
• validated – Antony Oct 18 '17 at 10:43

## 18 steps

Different from the already posted 18-step solution.

a*a = a*a + 0                                                 A2
= a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
= (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
= (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
= a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
= a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
= a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
= a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
= a*(-a) + (-(a*(-a) + a*(-a)))                           A2
= (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
= (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
= ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
= ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
= ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
= ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
= (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
= (-a)*(-a) + 0                                           A3
= (-a)*(-a)                                               A2

• Interesting to see someone do it backwards. All the steps are reversible so this is a fine proof. – Wheat Wizard Sep 29 '17 at 13:22
• That it goes upside down is mostly accidental. The proof is actually fairly symmetric: I use two similar sequences of steps to get from either end to the middle term a*(-a) + stuff. – Emil Jeřábek Sep 29 '17 at 13:27
• validated – Antony Oct 18 '17 at 18:57

# 29 26 Steps

No lemmas!

Comment if you see anything wrong. (It's very easy to make a mistake)

(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
= ((-a) + (a + (-a))) × (-a)                                         Ax. 3
= ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
= (a + ((-a) + (-a))) × (-a)                                         Ax. 1
= (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
= (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
= (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
= (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
= (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
= ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
= (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
= (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
= (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
= (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
= (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
= (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
= (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
= (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
= (a × a) + (0 × (-a))                                               Ax. 3
= (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
= (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
= (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
= (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
= (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
= (a × a) + 0                                                        Ax. 3
= (a × a)                                                            Ax. 2


Credit goes to Maltysen for 0 × (-a) = 0

• validated – Antony Oct 18 '17 at 10:45

# 18 steps

Not the first 18-step proof, but it’s simpler than the others.

(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]


Validate

# 23 steps

(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
= ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
= (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
= (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
= (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
= ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
= (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
= ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
= (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
= ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
= ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
= 0 + -((-a) * a)                                   ✔ axiom 3
= (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
= ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
= ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
= ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
= ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
= (0 * a ) + -((-a) * a)                            ✔ axiom 2
= ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
= ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
= (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
= (a * a) + 0                                       ✔ axiom 3
= a * a                                             ✔ axiom 2


Try it online!

Yes you read that right, I've written a proof-checker for this puzzle (naturally there's a possibility that the checker itself is wrong)

• Here’s a modest reward for the proof checker. – Emil Jeřábek May 23 '20 at 12:24
• @EmilJeřábek wow, thank you! Yeah, interesting trick with parse trees that, and not too painful to implement. I have enjoyed playing a little with a fully general prover (Metamath) since. – Antony May 30 '20 at 16:35
A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)

Lemma: 0 = 0 x a

A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)


27 26 steps Thank you Funky Computer Man for noticing a duplicate line.

• Welcome to the site! I'm not sure why you create a lemma only to use it once but I suppose its not against the rules. – Wheat Wizard Sep 27 '17 at 4:30
• @FunkyComputerMan Thank you! You're right; I'm not sure what I was thinking when I wrote that lemma ^^. And thank you for your edit and your remark. – Jalil Compaoré Sep 27 '17 at 5:11
• @JalilCompaoré I think you might be able to save that last A3 by starting by applying A2 to the second (-a) rather than the first. I'm not sure though, as I don't have the time to work through it right now. – H.PWiz Sep 27 '17 at 7:38

# 6 + 7 + 7 + 6 + 3 = 29 steps

Lemma 1. a*0=0 (6 steps)

0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2

Lemma 2. a*(-b) = -(a*b) (7 steps)

a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2

Lemma 3. (-a)*b = -(a*b) (7 steps)
same as above

Lemma 4. -(-(a)) = a (6 steps)

-(-a) = (-(-a)) + 0    axiom 2
= 0 + (-(-a))          axiom 4
= (a + (-a)) + (-(-a)) axiom 3
= a + ((-a) + (-(-a))) axiom 1
= a + 0                axiom 3
= a                    axiom 2

Theorem. -a*-a=0 (3 steps)

-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4

Q.E.D.

• I don't think you can make lemmas though – hyper-neutrino Sep 26 '17 at 23:37
• "Theorem. -a*-a=0" should be =a*a ? – Sparr Sep 27 '17 at 0:39
• @H.PWiz I don't have a problem with people using lemmas, but they cost as many steps as they are long each time they are used. I would recommend against using them because they can get in the way of optimizations, but as far as I'm concerned this post is fine. – Wheat Wizard Sep 27 '17 at 2:14
• going from "0 + -(a*b)" to "-(a*b)" in a single application of axiom 2 is not right. you need to use axiom 4 to swap the sides of the + first. – Sparr Sep 27 '17 at 6:20
• The way I read it is lemma 2/3 are 6 steps plus an instance of lemma 1 for 12 steps, lemma 4 is 6 steps, for a total of 30 steps. Am I missing something here? – Tahg Sep 29 '17 at 13:27

# 304 steps

Community wiki because this proof is generated by Mathematica's FindEquationalProof function.

The proof is rather long. Mathematica doesn't know how to golf it.

This is the Mathematica code that generates the proof (requires Mathematica 11.3), where p, t, n means +, ×, - respectively:

ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
ForAll[a, p[a, 0] == a],
ForAll[a, p[a, n[a]] == 0],
ForAll[{a, b}, p[a, b] == p[b, a]],
ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};

proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];

proof["ProofNotebook"]


It is not easy to count the steps directly, so I calculate it by the number of paths from the axioms to the conclusion in the "proof graph".

graph = proof["ProofGraph"];
score = Sum[
Length[FindPath[graph, axiom, "Conclusion 1", Infinity,
All]], {axiom,
Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]


Try it online!

This is the proof generated by the code:

Axiom 1

We are given that:

x1==p[x1, 0]

Axiom 2

We are given that:

x1==t[x1, 1]

Axiom 3

We are given that:

x1==t[1, x1]

Axiom 4

We are given that:

p[x1, x2]==p[x2, x1]

Axiom 5

We are given that:

p[x1, p[x2, x3]]==p[p[x1, x2], x3]

Axiom 6

We are given that:

p[x1, n[x1]]==0

Axiom 7

We are given that:

p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]

Axiom 8

We are given that:

p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]

Axiom 9

We are given that:

t[x1, t[x2, x3]]==t[t[x1, x2], x3]

Hypothesis 1

We would like to show that:

t[n[a], n[a]]==t[a, a]

Critical Pair Lemma 1

The following expressions are equivalent:

p[0, x1]==x1

Proof

Note that the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Axiom 4 and Axiom 1 respectively.

Critical Pair Lemma 2

The following expressions are equivalent:

p[x1, p[n[x1], x2]]==p[0, x2]

Proof

Note that the input for the rule:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Axiom 5 and Axiom 6 respectively.

Critical Pair Lemma 3

The following expressions are equivalent:

t[p[1, x1], x2]==p[x2, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[1, x1_]->x1

where these rules follow from Axiom 7 and Axiom 3 respectively.

Critical Pair Lemma 4

The following expressions are equivalent:

t[x1, p[1, x2]]==p[x1, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 1]->x1

where these rules follow from Axiom 8 and Axiom 2 respectively.

Critical Pair Lemma 5

The following expressions are equivalent:

t[p[1, x1], 0]==t[x1, 0]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

p[x1_, t[x2_, x1_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 6

The following expressions are equivalent:

t[0, 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.

Substitution Lemma 1

It can be shown that:

t[0, 0]==0

Proof

We start by taking Critical Pair Lemma 6, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 7

The following expressions are equivalent:

t[x1, 0]==t[p[x1, 1], 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.

Critical Pair Lemma 8

The following expressions are equivalent:

t[0, p[1, x1]]==t[0, x1]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

p[x1_, t[x1_, x2_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 9

The following expressions are equivalent:

t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[p[x1_, 1], 0]->t[x1, 0]

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.

Substitution Lemma 2

It can be shown that:

t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Critical Pair Lemma 9, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 3

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Substitution Lemma 2, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Substitution Lemma 4

It can be shown that:

p[x1, 1]==p[x1, p[1, t[x1, 0]]]

Proof

We start by taking Substitution Lemma 3, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Critical Pair Lemma 10

The following expressions are equivalent:

t[0, x1]==t[0, p[x1, 1]]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.

Critical Pair Lemma 11

The following expressions are equivalent:

t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

t[x2_, x1_]

which can be unified with the input for the rule:

t[0, p[x1_, 1]]->t[0, x1]

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.

Substitution Lemma 5

It can be shown that:

t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Critical Pair Lemma 11, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 6

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Substitution Lemma 5, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Substitution Lemma 7

It can be shown that:

p[x1, 1]==p[x1, p[1, t[0, x1]]]

Proof

We start by taking Substitution Lemma 6, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Substitution Lemma 8

It can be shown that:

p[x1, p[n[x1], x2]]==x2

Proof

We start by taking Critical Pair Lemma 2, and apply the substitution:

p[0, x1_]->x1

which follows from Critical Pair Lemma 1.

Critical Pair Lemma 12

The following expressions are equivalent:

n[n[x1]]==p[x1, 0]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

p[n[x1_], x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.

Substitution Lemma 9

It can be shown that:

n[n[x1]]==x1

Proof

We start by taking Critical Pair Lemma 12, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 13

The following expressions are equivalent:

x1==p[n[x2], p[x2, x1]]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

n[x1_]

which can be unified with the input for the rule:

n[n[x1_]]->x1

where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.

Critical Pair Lemma 14

The following expressions are equivalent:

t[x1, x2]==p[n[x2], t[p[1, x1], x2]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.

Critical Pair Lemma 15

The following expressions are equivalent:

t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.

Critical Pair Lemma 16

The following expressions are equivalent:

p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.

Substitution Lemma 10

It can be shown that:

p[1, t[x1, 0]]==1

Proof

We start by taking Critical Pair Lemma 16, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 17

The following expressions are equivalent:

t[t[x1, 0], 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[x1_, 0]]->1

where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.

Substitution Lemma 11

It can be shown that:

t[x1, t[0, 0]]==t[1, 0]

Proof

We start by taking Critical Pair Lemma 17, and apply the substitution:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

which follows from Axiom 9.

Substitution Lemma 12

It can be shown that:

t[x1, 0]==t[1, 0]

Proof

We start by taking Substitution Lemma 11, and apply the substitution:

t[0, 0]->0

which follows from Substitution Lemma 1.

Substitution Lemma 13

It can be shown that:

t[x1, 0]==0

Proof

We start by taking Substitution Lemma 12, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 18

The following expressions are equivalent:

t[x1, t[0, x2]]==t[0, x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 0]->0

where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.

Critical Pair Lemma 19

The following expressions are equivalent:

p[1, t[0, x1]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[0, x1_]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.

Substitution Lemma 14

It can be shown that:

p[1, t[0, x1]]==1

Proof

We start by taking Critical Pair Lemma 19, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 20

The following expressions are equivalent:

t[0, t[0, x1]]==t[0, 1]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[0, x1_]]->1

where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.

Substitution Lemma 15

It can be shown that:

t[0, x1]==t[0, 1]

Proof

We start by taking Critical Pair Lemma 20, and apply the substitution:

t[x1_, t[0, x2_]]->t[0, x2]

which follows from Critical Pair Lemma 18.

Substitution Lemma 16

It can be shown that:

t[0, x1]==0

Proof

We start by taking Substitution Lemma 15, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Critical Pair Lemma 21

The following expressions are equivalent:

t[n, x1]==p[n[x1], t[0, x1]]

Proof

Note that the input for the rule:

p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.

Substitution Lemma 17

It can be shown that:

t[n, x1]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 21, and apply the substitution:

t[0, x1_]->0

which follows from Substitution Lemma 16.

Substitution Lemma 18

It can be shown that:

t[n, x1]==n[x1]

Proof

We start by taking Substitution Lemma 17, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 22

The following expressions are equivalent:

t[n, t[x1, x2]]==t[n[x1], x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[n, x1_]->n[x1]

where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.

Substitution Lemma 19

It can be shown that:

n[t[x1, x2]]==t[n[x1], x2]

Proof

We start by taking Critical Pair Lemma 22, and apply the substitution:

t[n, x1_]->n[x1]

which follows from Substitution Lemma 18.

Critical Pair Lemma 23

The following expressions are equivalent:

t[x1, n]==p[n[x1], t[x1, 0]]

Proof

Note that the input for the rule:

p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.

Substitution Lemma 20

It can be shown that:

t[x1, n]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 23, and apply the substitution:

t[x1_, 0]->0

which follows from Substitution Lemma 13.

Substitution Lemma 21

It can be shown that:

t[x1, n]==n[x1]

Proof

We start by taking Substitution Lemma 20, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 24

The following expressions are equivalent:

n[t[x1, x2]]==t[x1, t[x2, n]]

Proof

Note that the input for the rule:

t[x1_, n]->n[x1]

contains a subpattern of the form:

t[x1_, n]

which can be unified with the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.

Substitution Lemma 22

It can be shown that:

t[n[x1], x2]==t[x1, t[x2, n]]

Proof

We start by taking Critical Pair Lemma 24, and apply the substitution:

n[t[x1_, x2_]]->t[n[x1], x2]

which follows from Substitution Lemma 19.

Substitution Lemma 23

It can be shown that:

t[n[x1], x2]==t[x1, n[x2]]

Proof

We start by taking Substitution Lemma 22, and apply the substitution:

t[x1_, n]->n[x1]

which follows from Substitution Lemma 21.

Substitution Lemma 24

It can be shown that:

t[a, n[n[a]]]==t[a, a]

Proof

We start by taking Hypothesis 1, and apply the substitution:

t[n[x1_], x2_]->t[x1, n[x2]]

which follows from Substitution Lemma 23.

Conclusion 1

We obtain the conclusion:

True

Proof

Take Substitution Lemma 24, and apply the substitution:

n[n[x1_]]->x1

which follows from Substitution Lemma 9.


# 34 steps

Lemma 1: 0=0*a (8 steps)
0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0

Theorem: -a*-a = a*a (49 steps)

-a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a

• I'm noticing a lack of parens after a while. Because association costs steps, I think it would make it easier to verify your proof if you included the parens. – Wheat Wizard Sep 27 '17 at 1:04
• Am still improving and updating. Will try to include all the parens when I'm done. – Sparr Sep 27 '17 at 1:13

# 25 steps

Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly.

Lemma Z [6 steps]: 0*a = 0:

0 = (0*a) + (-(0*a))       | Ax. 3
= ((0+0)*a) + (-(0*a))   | Ax. 2
= (0*a + 0*a) + (-(0*a)) | Ax. 9
= 0*a + (0*a + (-(0*a))) | Ax. 1
= 0*a + (0)              | Ax. 3
= 0*a                    | Ax. 2


Lemma M [12 steps]: (-a)*b = -(a*b)

(-a)*b = (-a)*b + 0                | Ax. 2
= (-a)*b + (a*b + (-(a*b))) | Ax. 3
= ((-a)*b + a*b) + (-(a*b)) | Ax. 5
= ((-a)+a)*b + (-(a*b))     | Ax. 9
= 0*b + (-(a*b))            | Ax. 3
= 0 + (-(a*b))              | Lem. Z 
= -(a*b)                    | Ax. 2


Theorem [25 steps]: (-a)*(-a) = a*a

(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
= 0 + (-a)*(-a)                | Ax. 4
= (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
= a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
= a*a + ((-a)*a + (-a)*(-a))   | Lem. M 
= a*a + ((-a)*(a + (-a)))      | Ax. 8
= a*a + ((-a)*0)               | Ax. 3
= a*a + 0                      | Lem. Z 
= a*a                          | Ax. 2


I feel like there's room for improvement here; for example, I use the commutative property of addition, though it feels like that should be unnecessary, since (-a)*(-a) = a*a is true in algebraic structures where addition is non-commutative. On the other hand, in those structures, the additive identity is commutative, and that's all I needed for the proof. I dunno. More generally, the proof's structure seems rather directionless; I just sort of threw stuff at the problem until it worked, so I bet there's some optimization to be done.

This was fun--thanks for the interesting and creative question OP! I haven't seen challenges like these before; hopefully becomes a thing!

• I see how the approach used in Lemma Z could make an equivalent proof for 0=(-a)*0 in 6 steps. Technically it deserves its own Lemma though, doesn't it? – vo1stv Jul 4 '19 at 1:52

## 22 23 Steps

• The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string.
• Multiplication is not assumed to be commutative.
• We are given a unit 1, but it plays no role whatsoever in the puzzle because it is involved exclusively in the rules that define it.

Now for the proof (notice I define n = (-a) to simplify reading):

(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]

• @H.PWiz why can't you go from n to 0 + n in one step? Isn't that just A2? The rules do say The variables can also stand in for arbitrarily complex expressions – jq170727 Sep 28 '17 at 0:17
• @jq170727 Axiom 2 only states that a + 0 = a not that 0 + a = a. You need one extra commutative step to get from n to 0 + n. – Wheat Wizard Sep 28 '17 at 4:29
• @H.PWiz can't you read the axiom in reverse? – jq170727 Sep 28 '17 at 4:35
• @jq170727 No you have to use commutativity for that. – Jalil Compaoré Oct 1 '17 at 23:15