PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 3 1 1 1 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)
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*
9. l:Alph*. i:n. R(l,w(i))
10. a: Alph*
11. b: Alph*
12. c: Alph*
13. ||a||nn
14. f: Alph*n
15. x:Alph*. R(x,w(f(x)))
16. f1: nn(nn)
17. Bij(nn; (nn); f1)
18. n1nn

1nn
By: RWH (RevLemmaC Thm* i:. i = i1) 18
Generated subgoals:

None

About:
natural_numbermultiplyuniversefunctionlistprop
allapplyimpliesandexistsproduct