PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 3

Alph:Type, R:(Alph*Alph*Prop), n:. (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))) (a,b,c:Alph*. ||a||nn (a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)))
By:
GenUnivCD
THEN
Analyze 4
THEN
Analyze 5
THEN
Analyze 6
THEN
Analyze 7
THEN
Analyze 8
Generated subgoal:

11. 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
a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)

About:
alluniversefunctionlistpropimplies
andapplyexistsnatural_numbermultiplyless_than