PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem f dec 1 2 1 1 1 1 1

1. S: Type
2. s: S
3. l: S*
4. n:
5. f: nS
6. g: Sn
7. InvFuns(n; S; f; g)
8. u: S
9. v: S*
10. Dec(mem_f(S;s;v))

u = s g(u) = g(s)

By: GenRepD

Generated subgoals:

111. u = s
g(u) = g(s)
211. g(u) = g(s)
u = s


About:
equalnatural_numberapplyuniverselistfunction