\documentclass{article}

\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{amsmath}
\usepackage{fancyvrb}
\title{}
\author{}

\date{}
\begin{document}
\maketitle


\thispagestyle{empty}

The requires property of frame elements is propagated upwards, i.e.: For each frame element f1 requiring another FE f2 of the child frame we determine the corresponding frame elements f1' and f2' in the parent frame. If both exist then they also should require each other.
This rule is necessary from the logic point of view, saying that the child frame is more specific than the parent frame.
That means that the restrictions of the child frame must imply the restricions of the parent frame.
Frame elements that require each other are logically connected via "implies" whereas all other (except for extrathematic) frame elements are logically connected via "and".
So for two frame elements a and b the rule says that if we have "a implies b" in the child frame we cannot have "a and b" in the parent frame.


\[
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getAllFrames}
\left(
\mathtt{fnDB}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\mathtt{fnDB}
,
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{ident}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em frame}_{\mbox{\scriptsize\em child}}
\\
\end{array}
\right)
\\
\end{array}
\right]
,
\\
\mathtt{source}
,
\\
\mathtt{getFrameRelationsByType}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathsf{Inheritance}
\\
\end{array}
\right]
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getFrameByID}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mathtt{target}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\left[
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{filterElem}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em child}}}
,
\\
\mathtt{fst}
,
\\
\mathtt{getFEMappings}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em rel}_{\mbox{\scriptsize\em inh}}
\\
\end{array}
\right)
\\
\end{array}
\right)
\\
\end{array}
\right]
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{length}
\left(
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\right)
\mathtt{>=}
\\
\mathsf{2}
\\
\end{array}
\\
\\
\end{array}
\\
\implies 
\\
\left(
\begin{array}{@{\hspace{5pt}}l}
\exists 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{getRequires}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{fnDB}
,
\\
\mbox{\em frame}_{\mbox{\scriptsize\em parent}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{5pt}}l}
\forall 
\hspace*{5pt}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
^{
\mathsf{Keep}
}
\hspace*{5pt}
{\scriptscriptstyle \in}
\hspace*{5pt}
\mathtt{map}
\left(
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mathtt{snd}
,
\\
\mbox{\em fe}_{\mbox{\scriptsize\em mappings}_{\mbox{\scriptsize\em fe}_{\mbox{\scriptsize\em requ}}}}
\\
\end{array}
\right)
\hspace*{5pt}
\bullet 
\\
\begin{array}{@{\hspace{1pt}}l@{\hspace{1pt}}}
\mbox{\em fe}_{\mbox{\scriptsize\em parent}}
\in 
\\
\mbox{\em fe}_{\mbox{\scriptsize\em requ}_{\mbox{\scriptsize\em parent}}}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\right)
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\\
\end{array}
\]
\end{document}
