PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem f dec 1 2 1 1 1 1 1 2 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))
11. g(u) = g(s)

(f o g)(u) = (f o g)(s)
By:
Reduce 0
THEN
RWH (HypC -1) 0
Generated subgoals:

None

About:
equalapplyuniverselistfunctionnatural_number