PrintForm Definitions relation autom Sections AutomataTheory Doc

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

0 E 0
By: Analyze 2
Generated subgoal:

12. 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

About:
natural_numberfunctionpropallmemberquotientequal