Lemmas Relating the aK (single a) AIM Goals

November 2021

### 120/240 permutations of aKi_eq_aKj

A permutation of aKi_eq_aKj is an equality
aKi = aKj
where
aKi is one of the aK goals, with the variables in order (x,y,z,u),
and
aKj is one of the aK goals, with the variables in the order of some permutation of (x,y,z,u).

Each specific permutation of aKj can be labelled with a permutation of (1234), for example,

```   a(x,K(y,z),u) = a(z,x,K(u,y)) # label("aK2_eq_aK3 (3142)").
```

The equality flipped permutations of aKi_eq_aKj are the permutations of aKj_eq_aKi (after renaming variables), so we account for only one of the two sets.

There are 240 permutations of aKi_eq_aKj for the 4 single-a goals:

10 unordered (i,j) pairs of the 4 aK goals (6 with i != j, 4 with i = j)

24 possible permutations of each pair

The 240 split into two sets of 120, specifically, with 12 permutations of each of the 10 (i,j) pairs. The sets can be identified with the following two members.
a(x,K(y,z),u) = a(x,y,K(z,u)) # label("aK2_eq_aK3 (1234)").
a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
Following is a summary of the proof of all 120 members of the (1243) set. We do not yet have a proof of
a(x,K(y,z),u) = a(x,y,K(z,u)) # label("aK2_eq_aK3 (1234)").
(or anything in its set), but if we include it as an extra assumption, we get all 240 permutations.

#### Step 1

Goal:
```   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
```
Proof: (in, out, pf, xml)

#### Step 2

Assumption:
```   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
```
Goals: 11 other permutations of aK2_eq_aK3
```   a(x,K(y,z),u) = a(x,z,K(y,u)) # label("aK2_eq_aK3 (1324)").
a(x,K(y,z),u) = a(x,u,K(z,y)) # label("aK2_eq_aK3 (1432)").
a(x,K(y,z),u) = a(y,x,K(z,u)) # label("aK2_eq_aK3 (2134)").
a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").
a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").
a(x,K(y,z),u) = a(z,x,K(u,y)) # label("aK2_eq_aK3 (3142)").
a(x,K(y,z),u) = a(z,y,K(x,u)) # label("aK2_eq_aK3 (3214)").
a(x,K(y,z),u) = a(z,u,K(y,x)) # label("aK2_eq_aK3 (3421)").
a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3 (4123)").
a(x,K(y,z),u) = a(u,y,K(z,x)) # label("aK2_eq_aK3 (4231)").
a(x,K(y,z),u) = a(u,z,K(x,y)) # label("aK2_eq_aK3 (4312)").
```
Proof: (in, out, pf, xml)

#### Step 3

Assumption: 12 proved permutations of aK2_eq_aK3

Goals:

```   a(K(x,y),z,u) = a(x,y,K(z,u)) # label("aK1_eq_aK3 (1234)").
K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3 (1234)").
```
Here are proofs of the two goals.

#### Step 4

Assumptions:
```   a(K(x,y),z,u) = a(x,y,K(z,u)) # label("aK1_eq_aK3 (1234)").
K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3 (1234)").
12 proved permutations of aK2_eq_aK3
```
Goals: 120/240 permutations of aKi_eq_aKj.

Consider the implications of assuming
```   a(x,K(y,z),u) = a(x,y,K(z,u)) # label("aK2_eq_aK3 (1234)").
```

#### Step 1

Goals: 11 other permutations of aK2_eq_aK3
```   a(x,K(y,z),u) = a(x,z,K(u,y)) # label("aK2_eq_aK3 (1342)").
a(x,K(y,z),u) = a(x,u,K(y,z)) # label("aK2_eq_aK3 (1423)").
a(x,K(y,z),u) = a(y,x,K(u,z)) # label("aK2_eq_aK3 (2143)").
a(x,K(y,z),u) = a(y,z,K(x,u)) # label("aK2_eq_aK3 (2314)").
a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3 (2431)").
a(x,K(y,z),u) = a(z,x,K(y,u)) # label("aK2_eq_aK3 (3124)").
a(x,K(y,z),u) = a(z,y,K(u,x)) # label("aK2_eq_aK3 (3241)").
a(x,K(y,z),u) = a(z,u,K(x,y)) # label("aK2_eq_aK3 (3412)").
a(x,K(y,z),u) = a(u,x,K(z,y)) # label("aK2_eq_aK3 (4132)").
a(x,K(y,z),u) = a(u,y,K(x,z)) # label("aK2_eq_aK3 (4213)").
a(x,K(y,z),u) = a(u,z,K(y,x)) # label("aK2_eq_aK3 (4321)").
```
Proof: (in, out, pf, xml)

#### Step 2

Assumptions:
```   a(K(x,y),z,u) = a(x,y,K(z,u)) # label("aK1_eq_aK3 (1234)").
K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3 (1234)").
24 proved permutations of aK2_eq_aK3
```
Proof: 240 permutations of aKi_eq_aKj.