PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 2 1

1. n:
2. m:

b:(nm). a:(nm). (z.1of(z)m+2of(z))(a) = b

By: Analyze 0

Generated subgoal:

13. b: (nm)
a:(nm). (z.1of(z)m+2of(z))(a) = b


About:
allnatural_numbermultiplyexistsproduct
equalapplylambdaadd