2. f : A
AA
3. u : A
4. is_ident(A; f; u)
5. is_assoc_sep(A; f)
6. a :
7. b :
8. c : {a...b}
9. d : {c..b
}
10. e : {a..b
}A
11.
i:{a..b}. i<c 
d
i 
e(i) = u
f(u,f((Iter(f;u) i:{c..d}. e(i)),u)) = f((Iter(f;u) i:{c..d}. e(i)),u)AA
}
}A
i:{a..b}. i<c di e(i) = u
f(u,f((Iter(f;u) i:{c..d}. e(i)),u)) = f((Iter(f;u) i:{c..d}. e(i)),u)| By: |
}. e(i)] |
| 1 |
}. e(i)) = (Iter(f;u) i:{c..d}. e(i))
13. f((Iter(f;u) i:{c..d }. e(i)),u) = (Iter(f;u) i:{c..d}. e(i))
f(u,f((Iter(f;u) i:{c..d}. e(i)),u)) = f((Iter(f;u) i:{c..d}. e(i)),u) | 1 step |
About:
 |  |  |  |  |  |  |  |  |