PrintForm Definitions relation autom Sections AutomataTheory Doc

At: rest symm rel 1 1 1

1. n: {1...}
2. m: n
3. E: nnProp
4. a,b:n. (a E b) (b E a)
5. a: m
6. b: m

(a E b) (b E a)

By:
Analyze 0
THEN
InstHyp [a;b] 4


Generated subgoals:

None


About:
impliesnatural_numberfunctionpropall