2. L1 : T List
3. L2 : T List
4. L3 : T List
5. f1 :
||L1||
||L2||
6. increasing(f1;||L1||)
7.
j:||L1||. L1[j] = L2[(f1(j))]
8. f :
||L2||||L3||
9. increasing(f;||L2||)
10.
j:||L2||. L2[j] = L3[(f(j))]
11. j :
||L1||
12. L2[(f1(j))] = L3[(f(f1(j)))]
L1[j] = L3[(f(f1(j)))]
