  In this paper we present mutual coinduction as a dual of mutual induction and
also as a generalization of standard coinduction. In particular, we present a
precise formal definition of mutual induction and mutual coinduction. In the
process we present the associated mutual induction and mutual coinduction proof
principles, and we present the conditions under which these principles hold.
  In spite of some mention of mutual (co)induction in research literature, but
the formal definition of mutual (co)induction and the proof of the mutual
(co)induction proof principles we present here seem to be the first such
definition and proof. As such, it seems our work is the first to point out that
monotonicity of mutual generators seems not sufficient for guaranteeing the
existence of least and greatest simultaneous fixed points in complete lattices,
and that continuity on the other hand is sufficient for guaranteeing their
existence. [The paper has been responsively updated so as to not require the
continuity of generators but only require their monotonicity, and it now
includes a proof of the sufficiency of monotonicity. A full revision of the
paper to reflect the relaxed requirement is currently underway.]
  In the course of our presentation of mutual coinduction we also discuss some
concepts related to standard (also called direct) induction and standard
coinduction, as well as ones related to mutual (also called simultaneous or
indirect) induction. During the presentation we purposely discuss particular
standard concepts so as to help motivate the definitions of their more general
counterparts for mutual/ simultaneous/ indirect (co)induction. Greatest
simultaneous post-fixed points, in particular, will be abstractions and models
of mathematical objects (e.g., points, sets, types, predicates, etc.) that are
defined mutually-coinductively.
