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.