PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 Rl equal Rg 1 3 2
1. Alph: Type
2. L: Alph*Prop
3. R: Alph*Alph*Prop
4. EquivRel x,y:Alph*. x R y
5. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))
6. g: (x,y:Alph*//(x R y))
7. l:Alph*. L(l) g(l)

EquivRel u,v:x,y:Alph*//(x R y). u Rg v
By: BackThru Thm* R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). EquivRel u,v:x,y:A*//(x R y). u Rg v)
Generated subgoals:

1 EquivRel x,y:Alph*. x R y
2 x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))

About:
quotientlistuniversefunctionprop
allimpliesboolapplyassert