PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 7 1 1 2 1 2 1 1 1 2 1
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*. L(l @ x) = L(l @ y)) (k:(nn), l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y))
16. (l:Alph*. L(l @ x) = L(l @ y)) (k:(nn), l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y))
17. t: (nn)
18. Fin({l:(Alph*)| ||l|| = t })
19. l:Alph*. ||l|| = t ||l|| = t

{l:(Alph*)| ||l|| = t } ~ {l:(Alph*)| ||l|| = t }
By: Inst Thm* P,Q:(TProp). (t:T. P(t) Q(t)) ({t:T| P(t) } ~ {t:T| Q(t) }) [Alph*;l.||l|| = t;l.||l|| = t]
Generated subgoals:

1 t@0:Alph*. (l.||l|| = t)(t@0) (l.||l|| = t )(t@0)
220. {t@0:(Alph*)| (l.||l|| = t)(t@0) } ~ {t@0:(Alph*)| (l.||l|| = t )(t@0) }
{l:(Alph*)| ||l|| = t } ~ {l:(Alph*)| ||l|| = t }

About:
setlistequalintlambdauniverse
functionpropboolallapplyimplies
andexistsnatural_numberassertmultiply