PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux4 quo 1 1 1 1 1
1. n: {1...}
2. E: nnProp
3. EquivRel i,j:n. i E j
4. x1: n
5. x2: n
6. x1 E x2
7. x1 = n-1 i,j:n//(i E j)
8. EquivRel x,y:(n-1). x E y

x1 = n-1 n
By:
Analyze 0
THEN
FwdThru Thm* E:(TTProp). (EquivRel x,y:T. x E y) (x,y:T. x = y x = y u,v:T//(u E v)) [3;-1]
Generated subgoals:

None

About:
equalnatural_numbersubtractfunctionpropquotient