Advertisement

Auxiliary Lemmas, Proofs, and Models

Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2262)

Abstract

\( \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T \) is reflexive and transitive by definition. It remains to show antisymmetry: \( S\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T T \wedge T \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T S \Rightarrow S = T \) This proof runs by case distinction on the forms of S and T. \( \begin{gathered} Case 1:S = grndT(S') \hfill \\ S\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T T \wedge T\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T S \wedge S = grndT(S') \hfill \\ \Rightarrow [Axionatization of \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _T ] \hfill \\ T = grndT(T') \wedge S = grndT(S') \wedge S'\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _M T' \wedge T'\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _M S' for some T' \hfill \\ \Rightarrow [Antisymmetry of \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \prec } _M (Axiom subM1) \hfill \\ T = grndT(T') \wedge S = grndT(S') \wedge S' = T' \hfill \\ \Rightarrow \hfill \\ S = T \hfill \\ \end{gathered} \) The cases for rep, readonly, and primitive types are analogous or trivial. □ For a more convenient handling of universes, we introduce an auxiliary function h that yields the depth of a universe in the universe hierarchy: h : UniverseNath(stdU) =0 h(typeU (T,U)) = 1 + h(U) h(objU (OID, C, U)) = 1+h(U) The following two auxiliary lemmas about h are used in the proof of Lemma 3.1.3. Basically, both lemmas express that the natural number N used in the universe order \( \underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{ \triangleleft } _N \) is the difference between the depths of the two compared universes.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Personalised recommendations