The subtype concept is used both for checking whether the type of
the first actual parameter of a method is a subtype of the first formal 
parameter type
and for checking the specialization hierarchy property for $*$override$*$.
The above proof guarantees the desirable property of name compatibility
for Demeter subtypes.  We have proven stronger forms of compatibility, but a 
discussion of this topic is beyond the scope of this paper.
We now prove the transitivity of
the subtype relation by examining four cases.  This proof is 
needed since our subtype definition contains a disjunction (or).
The subtype transitivity theorem is not essential for object-oriented programming.
It is the Name-Signature-Theorem that is important.


\begin{theorem}
{\rm Subtype-Transitivity-Theorem:}
The subtype relation is transitive.
\end{theorem}

Proof by case analysis.

\begin{itemize}

\item
If a class C inherits from a class B and the class B inherits from A then
the class C inherits from the class A.  

\begin{enumerate}
\item
True by definition of inheritance.

\end{enumerate} 

\item
If a class C is compatible with a class B and the class B is compatible with
a class A then the class C is compatible to the class A.

\begin{enumerate}
\item
C' $\subseteq$ B' \quad   by def. of compatibility \goodbreak
B' $\subseteq$ A'  \quad  by def. of compatibility \goodbreak
C' $\subseteq$ A'  \quad  by transitivity of subset \goodbreak
C is compatible to A \quad by definition of compatibility \goodbreak
\smallskip
\end{enumerate}


For the last two cases we present class dictionary templates which demonstrate
the relationship between class dictionary structure and subtype links.

\item
If a class C inherits from a class B and a class B is compatible to a class
A then:

\begin{enumerate}

\item
This third case combines inheritance with compatibility such that there exists
a class C which inherits from a class B and the class B is compatible with a
class A.  There are three possible class dictionary templates which will 
produce this type of subtype link.
In the second we use set notation
to restrict the classes which appear on the right hand side of B to be a 
subset of the classes appearing on the right hand side of A.  This is to ensure
the compatibility relation.
\bv

            inheritance            compatibility
    C <---------------------- B <---------------------- A

   case 3a:

      A : B | ..... *common*.
      B : C | ..... *common*.

   case 3b:

      A : C | {X1 ... XN}.
      B : C | { y | y is in subset of {X1 .. XN}} *common*.
      C = ......   

   case 3c (disallowed by semantic rule 5.4): 
     for guaranteeing transitivity, not needed
     for theorem 5.1.

      A : B | ......
      B = .....
      C = *inherit* B.

\end{verbatim}



In case 3a we can prove the subtype relation in two ways.  C is both compatible
to A via the definition of compatibility and C inherits from A via the
definition of inheritance.  This occurs because B is both compatible and 
inherits from A and C is both compatible and inherits from B.

\item
In case 3b the class C is compatible to A by definition of compatibility.  
C' is a subset of A' by inspection.

\item
We disallow the case 3c with the following semantic rule.

\begin{semantic-rule}
A class which is used for inheritance with *inherit* cannot be used as an 
alternative in an alternation production without implied inheritance (i.e.
without *common*).
\end{semantic-rule}

We need this restriction since we cannot reduce the combined subtype links in
class dictionaries of this form to either compatibility or inheritance
exclusively.  Our restriction does not reduce the expressiveness of our
notation.  We can simply add implied inheritance to the alternation production
in case 3c (i.e. we use *common*).

\end{enumerate}


\item
The fourth and final case is a class hierarchy where a class C is compatible
to a class B and the class B inherits from a class A.  There are four cases
where this can occur.  We will analyze these separately.

\bv

           compatibility            inheritance
    C <---------------------- B <---------------------- A

   case 4a:

      A = ......
      B : X | Y | Z *common* *inherit* A.
      C : X | Z.

   case 4b (disallowed by semantic rule 5.3):

      A : B | ..... *common*.
      B : X | Y | Z.
      C : X | Y.

   case 4c:

      A = ......
      B = ...... *inherit* A.
      C : B.

   case 4d:

      A : B | ...... *common*.
      B = ......  
      C : B.

\end{verbatim}


\begin{enumerate}

\item
In case 4a C inherits from A since all elements in C' inherit from
A.

\item
The case 4b has been defined as illegal by a semantic rule.

\item
In cases 4c and 4d the class C inherits from class A since all elements in C'
inherit from A.


\end{enumerate}

\end{itemize}

This completes the proof of the Subtype-Transitivity-Theorem.