PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 1 1 1

1. n:
2. m:
3. a1: nm
4. a2: nm

1of(a1)m+2of(a1) = 1of(a2)m+2of(a2) (nm) a1 = a2

By: Analyze 3

Generated subgoal:

13. a3: n
4. a4: m
5. a2: nm
1of( < a3,a4 > )m+2of( < a3,a4 > ) = 1of(a2)m+2of(a2) (nm) < a3,a4 > = a2


About:
impliesequalnatural_numbermultiplyaddproductpair