At: auto2 lemma 4 1 1 1 1 1 1 1 1 1 1 1 2 1 1
1. Alph: Type
2. R: Alph*
Alph*Prop
3. n: 
4. 
x:Alph*. R(x,x)
5. (x,y:Alph*. R(x,y) 
R(y,x))
& (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))
& (
w:(nAlph*). l:Alph*. i:n. R(l,w(i)))
6. b: Alph*
7. c: Alph*
8. n@0:
9. l:Alph*. ||l|| < n@0 (a':Alph*. ||a'|| < n
n & R((l @ b),a' @ b) & R((l @ c),a' @ c))
10. l: Alph*
11. ||l|| = n@0
12. a,b,c:Alph*. ||a||
nn (a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c))
13. ||l|| < nn
R((l @ b),l @ b)
By: Witness4 l @ b
Generated subgoals:None
About:
