Nuprl - Pf auto2_lemma

PrintForm Definitions exponent Sections AutomataTheory Doc

1. Alph: Type
2. R: Alph*Alph*Prop
3. n:
4. L: Alph*
5. m:
6. x:Alph*. R(x,x)
7. x,y:Alph*. R(x,y) R(y,x)
8. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
9. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
10. w:(nAlph*). l:Alph*. i:n. R(l,w(i))
11. v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))
12. Fin(Alph)
13. x: Alph*
14. y: Alph*
15. l: Alph*
16. L(l @ x) = L(l @ y)
17. a,b,c:Alph*. a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c)

k:(nn), l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y)

By: Witness17 l THEN Witness17 x THEN Witness17 y THEN Analyze 17 THEN Analyze 18 THEN Analyze 19

Generated subgoal:

1 17. a': Alph*
18. ||a'|| < nn
19. R((l @ x),a' @ x)
20. R((l @ y),a' @ y)
k:(nn), l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y)

About: