At: total back listify 1 1 2 1
1. Alph: Type
2. S: ActionSet(Alph)
3. sL: S.car*
4. Fin(Alph)
5. Fin(S.car)
6. n: 
7. 0 < n
8. TBL: S.car*
9. 
s:S.car. mem_f(S.car;s;TBL) 
(
w:Alph*. mem_f(S.car;(S:w
s);sL))
TBL:S.car*.
(s:S.car. mem_f(S.car;s;TBL) (w:Alph*. 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*. mem_f(S.car;(S:ws);sL)))
& (AL:S.car*.
(s:S.car. mem_f(S.car;s;AL) (w:Alph*. 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)))
By:
InstConcl [TBL]
THEN
Sel 1 (Analyze 0)
THEN
NthHyp -1
Generated subgoals:None
About:
