Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. S:ActionSet(Alph). si:S.car. nn:
. f:nn 
Alph. g:Alph nn.
Fin(S.car)
InvFuns(nn;Alph;f;g)
(n:
RL:{y:{x:S.car List| 0 < ||x|| 
||x|| 
n + 1} | y[(||y|| - 1)] = si}
(s:S.car. (w:Alph List. (S:w
si) = s) 
mem_f(S.car;s;RL))
(||RL|| = n + 1
(i:||RL||. j:i. 
(RL[i] = RL[j]))
(s:S.car. mem_f(S.car;s;RL) (w:Alph List. (S:wsi) = s))
(k:
k nn
(RLa:S.car List
(i:{1..||RL||
}. a:Alph.
mem_f(S.car;S.act a RL[i];RL) mem_f(S.car;S.act a RL[i];RLa))
(a:Alph
g a < k
mem_f(S.car;S.act a hd(RL);RL) mem_f(S.car;S.act a hd(RL);RLa))
(s:S.car. mem_f(S.car;s;RLa) (w:Alph List. (S:wsi) = s))))))
Applied Tactic: (RepD ...a)
Generated subgoals:1. RL:{y:{x:S.car List| 0 < ||x|| ||x|| n + 1} | y[(||y|| - 1)] = si}
(s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL))
(||RL|| = n + 1
(i:||RL||. j:i. (RL[i] = RL[j]))
(s:S.car. mem_f(S.car;s;RL) (w:Alph List. (S:wsi) = s))
(k:
k nn
(RLa:S.car List
(i:{1..||RL||}. a:Alph.
mem_f(S.car;S.act a RL[i];RL) mem_f(S.car;S.act a RL[i];RLa))
(a:Alph
g a < k mem_f(S.car;S.act a hd(RL);RL) mem_f(S.car;S.act a hd(RL);RLa))
(s:S.car. mem_f(S.car;s;RLa) (w:Alph List. (S:wsi) = s)))))