At: back listify 1 2 1 1 1 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. n: 
5. f:
n
Alph
6. Bij(
n; Alph; f)
7. n1: 
8. f1:
n1
S.car
9. Bij(
n1; S.car; f1)
10. BL: S.car*
11. t: S.car
12. i:
||(
x. < f1(x),(
y.S.act(f(y),f1(x)))[
n] > )[
n1]||
13. f1(i) = t
14. mem_f(S.car;s;(
y.S.act(f(y),f1(i)))[
n])
15. i1:
||(
y.S.act(f(y),f1(i)))[
n]||
16. S.act(f(i1),f1(i)) = s
a:Alph. S.act(a,t) = s
By:
InstConcl [f(i1)]
THEN
RWH (HypC 13) -1
Generated subgoals:None
About: