PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
mem
f
dec
1
2
1
1
1
1
1.
S:
Type
2.
s:
S
3.
l:
S*
4.
n:
5.
f:
n
S
6.
g:
S
n
7.
InvFuns(
n; S; f; g)
8.
u:
S
9.
v:
S*
10.
Dec(mem_f(S;s;v))
Dec(u = s)
By:
Assert (u = s
g(u) = g(s))
Generated subgoals:
1
u = s
g(u) = g(s)
2
11.
u = s
g(u) = g(s)
Dec(u = s)
About:
u = s 
g(u) = g(s) g(u) = g(s) Dec(u = s)
n
Snn; S; f; g) Dec(u = s) g(u) = g(s)) u = s g(u) = g(s) g(u) = g(s) Dec(u = s)
