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.

Proof: 120/240 permutations of aKi_eq_aKj.

Combined

Combining the previous steps results in a complete proof of the 120/240 permutations of aKi_eq_aKj in a single run.

Proof: (in, out, pf, xml) (The output/proof files are large!)

Here are the remaining (not yet proved) 120/240 permutations of aKi_eq_aKj.

Additional result

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.