PrintForm Definitions relation autom Sections AutomataTheory Doc

At: rest equi rel 1
1. n: {1...}
2. m: n
3. E: nnProp
4. EquivRel x,y:n. x E y

Refl(m;x,y.x E y) & Sym x,y:m. x E y & Trans x,y:m. x E y
By:
Unfold `equiv_rel` 4
THEN
ExRepD
Generated subgoal:

14. Refl(n;x,y.x E y)
5. Sym x,y:n. x E y
6. Trans x,y:n. x E y
Refl(m;x,y.x E y) & Sym x,y:m. x E y & Trans x,y:m. x E y

About:
andnatural_numberfunctionprop