PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 4 1 1 1
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. a: Alph*
6. b: Alph*
7. c: Alph*
8. P:(Alph*Prop). (n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l))) (l:Alph*. P(l))

a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c)
By: Witness8 a.a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c)
Generated subgoal:

18. (n@0:. (l:Alph*. ||l|| < n@0 (a.a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c))(l)) (l:Alph*. ||l|| = n@0 (a.a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c))(l))) (l:Alph*. (a.a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c))(l))
a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c)

About:
existslistandless_thanmultiplyapplylambdauniverse
functionpropallimpliesnatural_numberequalint