Level: Lib Thy Top: 1
Hypotheses:- Alph :
- S : ActionSet(Alph)
- si : S.car
- nn :
- f : nn
Alph - g : Alph nn
- Fin(S.car)
- InvFuns(nn;Alph;f;g)
- n :
Conclusion:
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: NatInd 9
Generated subgoals:1. RL:{y:{x:S.car List| 0 < ||x|| ||x|| 0 + 1} | y[(||y|| - 1)] = si}
(s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL))
(||RL|| = 0 + 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)))))2. 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)))))