Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. sL : S.car List

  4. Fin(Alph)

  5. Fin(S.car)

Conclusion:

TBL:S.car List. s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))

Applied Tactic: Assert n: TBL:S.car List (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (||TBL|| = n (i:||TBL||. j:i. (TBL[i] = TBL[j])) (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (AL:S.car List (s:S.car. mem_f(S.car;s;AL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) (s:S.car. a:Alph. mem_f(S.car;S.act a s;TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL))))
Generated subgoals:

1. n: TBL:S.car List (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (||TBL|| = n (i:||TBL||. j:i. (TBL[i] = TBL[j])) (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (AL:S.car List (s:S.car. mem_f(S.car;s;AL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) (s:S.car. a:Alph. mem_f(S.car;S.act a s;TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL))))

2. TBL:S.car List. s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))