210. [x; y][j] = s[(f1(j))]
[(f(x)); (f(y))][j] = f([x; y][j])
T'
2||s||
j:2. [x; y][j] = s[(f1(j))]
j:2. [(f(x)); (f(y))][j] = map(f;s)[(f1(j))]
f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])
0))
THEN
(RevHypSubst -1 0))
THENA
(Auto THEN (Reduce 0))
| 1 | 9. j: 2 10. [x; y][j] = s[(f1(j))] [(f(x)); (f(y))][j] = f([x; y][j]) | 1 step |
About:
 |  |  |  |  |  |  |  |  |