At: back listify 1 2 1 1 1 2 1 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. n: 
5. f: n
Alph
6. 
b:Alph. 
a:n. f(a) = b
7. n1:
8. f1: n1S.car
9. b:S.car. a:n1. f1(a) = b
10. BL: S.car*
11. t: S.car
12. a: Alph
13. S.act(a,t) = s
14. a@0: n
15. f(a@0) = a
16. mem_f(S.car;((
y.S.act(f(y),t))[n])[a@0];(y.S.act(f(y),t))[n])
mem_f(S.car;s;(y.S.act(f(y),t))[n])
By:
RWH
(LemmaC
Thm* n:, f:(nT), i:n. ((f)[n])[i] = f(i))
-1
THEN
Reduce -1
THEN
RWH (HypC -2) -1
THEN
RWH (HypC 13) -1
Generated subgoals:None
About:
