PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 lem 1

Alph:Type, R:(Alph*Alph*Prop). Fin(Alph) (EquivRel x,y:Alph*. x R y) Fin(x,y:Alph*//(x R y)) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
By: RepD
Generated subgoal:

11. Alph: Type
2. R: Alph*Alph*Prop
3. Fin(Alph)
4. EquivRel x,y:Alph*. x R y
5. Fin(x,y:Alph*//(x R y))
6. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))
7. g: (x,y:Alph*//(x R y))
8. x: x,y:Alph*//(x R y)
9. y: x,y:Alph*//(x R y)
Dec(x Rg y)

About:
alluniversefunctionlistpropimpliesquotientbool