x,y. mentions_trace(x) 
y;false;v) 
(
i:
. i < ||v|| & mentions_trace(v[i]))6. reduce(
x,y. mentions_trace(x) y;false;v)7. i:
8. i < ||v||
9. mentions_trace(v[i])
mentions_trace([u / v][(i+1)])x,y. mentions_trace(x) y;false;v) 
(i:. i < ||v|| & mentions_trace(v[i]))x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i])) reduce(x,y. mentions_trace(x) y;false;v) i:. i < ||v||+1 & mentions_trace([u / v][i])| 1 | 5. reduce(x,y. mentions_trace(x) y;false;v) (i:. i < ||v|| & mentions_trace(v[i])) 6. reduce( x,y. mentions_trace(x) y;false;v)7. i: 8. i < ||v|| 9. mentions_trace(v[i]) mentions_trace([u / v][(i+1)]) |
About:
 |  |  |  |  |  |  |  |  |  |  |