PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 1 1 1 1 2 1 2 1 1 1 1 1
1. E: 11Prop
2. Refl(1;x,y.x E y)
3. Sym x,y:1. x E y & Trans x,y:1. x E y
4. x,y:1. Dec(x E y)
5. 0 i,j:1//(i E j)
6. x1: 1
7. x2: 1
8. x1 E x2
9. x2 = 0 1

0 E 0
By: Unfold `refl` 2
Generated subgoal:

12. a:1. a E a
3. Sym x,y:1. x E y & Trans x,y:1. x E y
4. x,y:1. Dec(x E y)
5. 0 i,j:1//(i E j)
6. x1: 1
7. x2: 1
8. x1 E x2
9. x2 = 0 1
0 E 0

About:
natural_numberfunctionpropandallmemberquotientequal