Nuprl - Pf auto2_lemma_4 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 2 1 1 1 2

PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 4 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 2 1 1 1 2

1. Alph: Type
2. R: Alph*Alph*Prop
3. n:
4. (x:Alph*. R(x,x)) & (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)))
5. b: Alph*
6. c: Alph*
7. n@0:
8. l: Alph*
9. ||l|| = n@0
10. ||l|| < nn
11. a': Alph*
12. ||a'|| < ||l|| & R((l @ b),a' @ b) & R((l @ c),a' @ c)
13. a'@0: Alph*
14. ||a'@0|| < nn
15. R((a' @ b),a'@0 @ b) & R((a' @ c),a'@0 @ c)

R((l @ b),a'@0 @ b) & R((l @ c),a'@0 @ c)

By: Analyze 4 THEN Analyze 5 THEN Analyze 6 THEN Analyze 7 THEN Analyze 16 THEN Analyze 17 THEN Analyze 21 THEN Analyze 0

Generated subgoals:

1 4. x:Alph*. R(x,x)
5. x,y:Alph*. R(x,y) R(y,x)
6. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
7. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
8. w:(nAlph*). l:Alph*. i:n. R(l,w(i))
9. b: Alph*
10. c: Alph*
11. n@0:
12. l: Alph*
13. ||l|| = n@0
14. ||l|| < nn
15. a': Alph*
16. ||a'|| < ||l||
17. R((l @ b),a' @ b)
18. R((l @ c),a' @ c)
19. a'@0: Alph*
20. ||a'@0|| < nn
21. R((a' @ b),a'@0 @ b)
22. R((a' @ c),a'@0 @ c)
R((l @ b),a'@0 @ b)

2 4. x:Alph*. R(x,x)
5. x,y:Alph*. R(x,y) R(y,x)
6. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
7. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
8. w:(nAlph*). l:Alph*. i:n. R(l,w(i))
9. b: Alph*
10. c: Alph*
11. n@0:
12. l: Alph*
13. ||l|| = n@0
14. ||l|| < nn
15. a': Alph*
16. ||a'|| < ||l||
17. R((l @ b),a' @ b)
18. R((l @ c),a' @ c)
19. a'@0: Alph*
20. ||a'@0|| < nn
21. R((a' @ b),a'@0 @ b)
22. R((a' @ c),a'@0 @ c)
R((l @ c),a'@0 @ c)

About: