is mentioned by
![]() ![]() ![]() ![]() ![]() 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 ![]() ![]() | [iter_via_intseg_split_pluck] |
![]() ![]() ![]() ![]() ![]() Thm* is_ident(A; f; u) Thm* ![]() ![]() Thm* is_assoc_sep(A; f) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() Thm* (( ![]() ![]() ![]() ![]() ![]() ![]() Thm* ( ![]() ![]() Thm* ((Iter(f;u) i:{a..b ![]() ![]() | [iter_via_intseg_amputate_units] |
![]() ![]() ![]() ![]() ![]() 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] |
![]() ![]() ![]() ![]() ![]() Thm* is_commutative_sep(A; f) Thm* ![]() ![]() Thm* is_ident(A; f; u) Thm* ![]() ![]() Thm* is_assoc_sep(A; f) Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (f((Iter(f;u) i:{a..b ![]() ![]() Thm* (= Thm* ((Iter(f;u) i:{a..b ![]() Thm* ( ![]() | [iter_via_intseg_comp_binop] |
![]() ![]() | [is_assoc_intadd] |
![]() ![]() ![]() | [is_assoc_intmul] |
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html