PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lquo rel tran 1 1
1. A: Type
2. R: A*A*Prop
3. EquivRel x,y:A*. x R y
4. x,y,z:A*. (x R y) ((z @ x) R (z @ y))
5. g: (x,y:A*//(x R y))

a,b,c:x,y:A*//(x R y). (z:A*. g(z@a) g(z@b)) (z:A*. g(z@b) g(z@c)) (z:A*. g(z@a) g(z@c))
By: Auto
Generated subgoals:

16. a: x,y:A*//(x R y)
7. b: x,y:A*//(x R y)
8. c: x,y:A*//(x R y)
9. z:A*. g(z@a) g(z@b)
10. z:A*. g(z@b) g(z@c)
11. z: A*
12. g(z@a)
g(z@c)
26. a: x,y:A*//(x R y)
7. b: x,y:A*//(x R y)
8. c: x,y:A*//(x R y)
9. z:A*. g(z@a) g(z@b)
10. z:A*. g(z@b) g(z@c)
11. z: A*
12. g(z@c)
g(z@a)

About:
allquotientlistimpliesassert
applyuniversefunctionpropbool