PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
mem
f
dec
1
2
1
1
1.
S:
Type
2.
s:
S
3.
l:
S*
4.
Fin(S)
5.
u:
S
6.
v:
S*
7.
Dec(mem_f(S;s;v))
Dec(u = s)
By:
Analyze 4
THEN
RWH (LemmaC
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B)) 5
Generated subgoal:
1
4.
n:
5.
n ~ S
6.
u:
S
7.
v:
S*
8.
Dec(mem_f(S;s;v))
Dec(u = s)
About:
n ~ S
Dec(u = s) Dec(u = s)
f:(A
B). Bij(A; B; f)) 
(A ~ B))
5n ~ S Dec(u = s)
