PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 2 1 1
1. n: {1+1...}
2. E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))
3. E: nnProp
4. EquivRel x,y:n. x E y
5. x,y:n. Dec(x E y)

EquivRel x,y:(n-1). x E y
By: BackThru Thm* n:{1...}, m:n, E:(nnProp). (EquivRel x,y:n. x E y) (EquivRel x,y:m. x E y)
Generated subgoals:

None

About:
natural_numbersubtractaddallfunction
propimpliesandexistsquotient