At: back listify 1 1 2 1 1 2 2 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. Fin(Alph)
5. Fin(S.car)
6. LL: (S.car
S.car*)*
7. u1: S.car
8. u2: S.car*
9. v: (S.carS.car*)*
10. BL: S.car*
11. 
t:S.car. mem_f(S.car;t;BL) 
(
i:
||v||. 1of(v[i]) = t & mem_f(S.car;s;2of(v[i])))
12. mem_f(S.car;s;u2)
13. t: S.car
14. i: (||v||+1)
15. 
i = 0
16. 0 < i
17. 1of(v[(i-1)]) = t
18. mem_f(S.car;s;2of(v[(i-1)]))
i:||v||. 1of(v[i]) = t & mem_f(S.car;s;2of(v[i]))
By: InstConcl [i-1]
Generated subgoals:None
About:
