Pursuing consequences of aK2 ...

We have proofs of the following instances of aK1 and aK3.

   a(K(x,u),x,y) = 1   # label("aK1{x/z}").
   a(K(z,x),x,y) = 1   # label("aK1{x/u}").
   a(K(y,u),x,y) = 1   # label("aK1{y/z}").
   a(K(z,y),x,y) = 1   # label("aK1{y/u}").
   a(K(z,z),x,y) = 1   # label("aK1{z/u}").

   a(x,y,K(x,u)) = 1   # label("aK3{x/z}").
   a(x,y,K(z,x)) = 1   # label("aK3{x/u}").
   a(x,y,K(y,u)) = 1   # label("aK3{y/z}").
   a(x,y,K(z,y)) = 1   # label("aK3{y/u}").
   a(x,y,K(z,z)) = 1   # label("aK3{z/u}").

We do *not* yet have proofs of the following instances.

   *** Update June 2016:  We now have proofs for these. ***

   a(K(z,u),x,x) = 1   # label("aK1{x/y}").
   a(x,x,K(z,u)) = 1   # label("aK3{x/y}").

We have proofs of {aK2,Greer} => aK1 (aK3 and Ka follow)

   T(x,y) * (T(z,y) * T(x,y)) = T(x * (z * x),y)           # label("Greer 1").
   L(x,y,z) * (L(u,y,z) * L(x,y,z)) = L(x * (u * x),y,z)   # label("Greer 2").
   R(x,y,z) * (R(u,y,z) * R(x,y,z)) = R(x * (u * x),y,z)   # label("Greer 3").

      Note:  The Greer lemmas are consequences of the RIF case.