PrintForm Definitions relation autom Sections AutomataTheory Doc

At: rest equi rel 1 1 2 1

1. n: {1...}
2. m: n
3. E: nnProp
4. Refl(n;x,y.x E y)
5. Sym x,y:n. x E y
6. Trans x,y:n. x E y

Sym x,y:m. x E y

By: BackThru Thm* n:{1...}, m:n, E:(nnProp). Sym x,y:n. x E y Sym x,y:m. x E y

Generated subgoals:

None


About:
natural_numberfunctionprop