At:
mul via intseg split pluck
By: |
Thm* ![]() ![]() ![]() ![]() ![]() Thm* is_ident(A; f; u) Thm* ![]() ![]() Thm* is_assoc_sep(A; f) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (a ![]() Thm* ( ![]() ![]() Thm* (c<b Thm* ( ![]() ![]() Thm* ((Iter(f;u) i:{a..b ![]() Thm* (= Thm* (f((Iter(f;u) i:{a..c ![]() ![]() Using:[ ![]() ![]() ![]() THEN OnAllClauses Reduce |
1 |
![]() ![]() ![]() ![]() ![]() | 2 steps |
2 |
![]() ![]() ![]() ![]() ![]() | 2 steps |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() |