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[1], 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[1], 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[1], 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[1], 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[1], 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[1], x1_]->n[x1]
which follows from Substitution Lemma 18.
Critical Pair Lemma 23
The following expressions are equivalent:
t[x1, n[1]]==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[1]]==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[1]]==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[1]]]
Proof
Note that the input for the rule:
t[x1_, n[1]]->n[x1]
contains a subpattern of the form:
t[x1_, n[1]]
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[1]]]
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[1]]->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.
