%
% This example is based on:
% http://www.maths.tcd.ie/~dwilkins/LaTeXPrimer/Theorems.html
%
\documentclass[a4paper]{article}
\usepackage[english]{babel}
\usepackage[utf8x]{inputenc}
\usepackage{amsmath,amsthm}
\usepackage{ wasysym }
\usepackage{ marvosym }
\usepackage{ esint }
\usepackage{ amssymb }
\title{Data Integration, Simplified}
\author{Luc Pezet, v.1}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\begin{document}
\maketitle
\begin{definition}
Let $D$ be the set of all documents. Documents may belong to Source data or Target data.
\end{definition}
\begin{definition}
Let $T \subseteq D$ be a set of integration results, i.e. the Target set. $T$ is generally considered to be the final result of compiling multiple Source sets through successive integration steps.
\end{definition}
\begin{definition}
Let $S \subseteq D$ be a set of Source documents considered for integration into a Target set.
\end{definition}
\begin{definition}
Let $rep_i : S, T_i \mapsto \{0, 1\} $ such that for $x \in S, y \in T_i$,
\[ rep_i(x,y) =
\begin {cases}
1 & \mbox{if } x \mbox{ and } y \mbox{ represent the same document } \\
0 & \mbox{otherwise. }
\end {cases} \]
\end{definition}
\begin{definition}
Let $\aries_i$ be a function that creates a document in $T_{i+1}$ from a document of $S$.
Formally, let $\aries_i : S \mapsto T_{i+1} $ such that for $ x \in S,$
\[ \aries_i(x) = y \mid y \in T_{i+1} \land rep_{i+1}(x,y) = 1 \]
\end{definition}
\begin{definition}
Let $\gemini_i$ be a function that modfies a document from $T_i$ using a document from $S$ into $T_{i+1}$.
Formally, let $\gemini_i : S, T_i \mapsto T_{i+1} $ such that for $ x \in S, y \in T_i, rep_i(x,y) = 1$
\[ \gemini_i(x,y) = z \mid z \in T_{i+1} \land rep_{i+1}(x,z) = 1 \]
\end{definition}
\begin{definition}
Let $\capricornus_i : S \mapsto T_{i+1} $ the integration function of $x \in S$ with documents in $T_i$ into $T_{i+1}$, such that $ \forall x \in S$,
\[ \capricornus_i(x) = \begin {cases} \aries_i(x) = z & \mbox{if } \forall y \in T_i \mbox{, } rep_i(x,y) = 0. \\
\gemini_i(x,y) = y' & \mbox{if } \exists y \in T_i \mbox{, } rep_i(x,y) = 1.
\end {cases} \]
\end{definition}
\begin{lemma}
\label{pIsIdempotent}
The function $\capricornus_i$ is idempotent if and only if the subsequent integrations leads only to the $\gemini$ functions. Formally,
\[ \capricornus_i(x) \mbox{ idemptotent } \iff \capricornus_{i+1}(x) = \gemini_{i+1}(x,y) \]
\end{lemma}
\begin{proof}
If for $x \in S$ and $\forall y \in T_i, rep_i(x,y) = 0$,
\begin{align}
& \implies \capricornus_i(x) = \aries(x) = z \\
& \implies \exists z \in T_{i+1} \mid rep_{i+1}(x,z) = 1 \\
& \implies \capricornus_{i+1}(x) = \gemini_{i+1}(x,z) \qedhere
\end{align}
If for $x \in S$, $\exists y \in T_i \mid rep(x,y) = 1$,
\begin{align}
& \implies \capricornus_i(x) = \gemini_i(x,y) = y' \\
& \implies \exists y' \in T_{i+1} \mid rep_{i+1}(x,y') = 1
& \implies \capricornus_{i+1}(x) = \gemini_{i+1}(x,y) \qedhere
\end{align}
\end{proof}
\end{document}
