  Orthogonality is a discipline of programming that in a syntactic manner
guarantees determinism of functional specifications. Essentially, orthogonality
avoids, on the one side, the inherent ambiguity of non determinism, prohibiting
the existence of different rules that specify the same function and that may
apply simultaneously (non-ambiguity), and, on the other side, it eliminates the
possibility of occurrence of repetitions of variables in the left-hand side of
these rules (left linearity). In the theory of term rewriting systems (TRSs)
determinism is captured by the well-known property of confluence, that
basically states that whenever different computations or simplifications from a
term are possible, the computed answers should coincide. Although the proofs
are technically elaborated, confluence is well-known to be a consequence of
orthogonality. Thus, orthogonality is an important mathematical discipline
intrinsic to the specification of recursive functions that is naturally applied
in functional programming and specification. Starting from a formalization of
the theory of TRSs in the proof assistant PVS, this work describes how
confluence of orthogonal TRSs has been formalized, based on axiomatizations of
properties of rules, positions and substitutions involved in parallel steps of
reduction, in this proof assistant. Proofs for some similar but restricted
properties such as the property of confluence of non-ambiguous and (left and
right) linear TRSs have been fully formalized.
