1. Alph :

2. R : Alph List Alph List

3. n :

4. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i))

5. a : Alph List

6. b : Alph List

7. c : Alph List

8. Alph:. P:Alph List . (n:. (l:Alph List. ||l|| < n P l) (l:Alph List. ||l|| = n P l)) (l:Alph List. P l)

a':Alph List. ||a'|| < n * n R (a @ b) (a' @ b) R (a @ c) (a' @ c)

With Alph (D 8) THENW Auto

1. a':Alph List. ||a'|| < n * n R (a @ b) (a' @ b) R (a @ c) (a' @ c)