2. T': Type
3. f: T
T'4. x: T
5. y: T
6. s: T List
7. f1:
2||s||8.
j:2. [x; y][j] = s[(f1(j))]
j:2. [(f(x)); (f(y))][j] = map(f;s)[(f1(j))]
T,T':Type, f:(TT'), x,y:T, s:T List. x before y 
s 
f(x) before f(y) map(f;s)
| 1 | 1. T: Type 2. T': Type 3. f: T T'4. x: T 5. y: T 6. s: T List 7. f1: 2||s||8. j:2. [x; y][j] = s[(f1(j))] j:2. [(f(x)); (f(y))][j] = map(f;s)[(f1(j))] | 2 steps |
About:
 |  |  |  |  |  |  |  |  |  |