By: |
THEN RWW Thm* a,b:T, l1,l2:T List. [a / l1] [b / l2] a = b & l1 l2 0 |
1 |
9. 9. ||[u / v]||||v1|| & (i:. i<||[u / v]|| [u / v][i] = v1[i]) 10. [u / v] v1 (||[u / v]||||v1|| 10. & (i:. i<||[u / v]|| [u / v][i] = v1[i])) 11. ||v||+1||v1||+1 12. i:. i<||v||+1 [u / v][i] = [u1 / v1][i] u = u1 | 1 step |
2 |
9. 9. ||[u / v]||||v1|| & (i:. i<||[u / v]|| [u / v][i] = v1[i]) 10. [u / v] v1 (||[u / v]||||v1|| 10. & (i:. i<||[u / v]|| [u / v][i] = v1[i])) 11. ||v||+1||v1||+1 12. i:. i<||v||+1 [u / v][i] = [u1 / v1][i] v v1 | 2 steps |
About: