Rank | Theorem | Name |
2 | ![]() ![]() ![]() ![]() ![]() Thm* is_ident(A; f; u) Thm* ![]() ![]() Thm* is_assoc_sep(A; f) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (a ![]() Thm* ( ![]() ![]() Thm* (c ![]() Thm* ( ![]() ![]() Thm* ((Iter(f;u) i:{a..b ![]() Thm* (= Thm* (f((Iter(f;u) i:{a..c ![]() ![]() | [iter_via_intseg_split_mid] |
cites the following: | ||
0 | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* b ![]() ![]() ![]() ![]() | [iter_via_intseg_null] |
1 | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* a<b Thm* ![]() ![]() Thm* (Iter(f;u) i:{a..b ![]() ![]() | [iter_via_intseg_split_last] |