\documentclass{article}
\usepackage{argoclp}
\catcode`\_=\active
\def_{\_}

\def\d{{\fontencoding{T1}\selectfont\dj}}

\def\D{{\fontencoding{T1}\selectfont\DJ}}

\setlength{\textheight}{22cm} 
\newtheorem{axiom}{Aksioma}
\newtheorem{theorem}{Teorema}
\newcounter{proofstepnum} 

\begin{document}

\title{High school geometry theorems}
\author{Hilbert's axiomatic system.\\
Formalizovano od strane: Sana Stojanovic Djurdjevic \\
Dokaz generisan uz pomo\'{c}: ArgoGeoChecker.}
\date{30.03.2018.}
\maketitle

\begin{theorem}[th_14_01.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ pokazati da postoji ravan $\beta$ tako da va\v{z}i $A \in \beta$ i $B \in \beta$ i $C \in \beta$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenice $\neg col(A, B, C)$ postoji  ravan $\beta$  tako da va\v{z}i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ (aksioma $I4a$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in \beta$ i $B \in \beta$ i $C \in \beta$.} 
QED
\hrule 
\begin{theorem}[th_14_02.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ pokazati da va\v{z}i $p \in \beta$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenica $A \in r$ i $A \in r$ i $C \in r$ va\v{z}i $col(A, A, C)$ (aksioma $D1$).} 
\proofstep{0} {Va\v{z}i $A = B$ ili $A \neq B$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $col(A, A, C)$ i $A = B$ va\v{z}i $col(A, B, C)$.} 
\proofstep{6} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $col(A, B, C)$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $A \in \beta$ i $B \in \beta$ va\v{z}i $p \in \beta$ (aksioma $I6$).} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $p \in \beta$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_14_03.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ i $p \in \beta$ pokazati da va\v{z}i $q \in \beta$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenica $A \in p$ i $B \in p$ i $B \in p$ va\v{z}i $col(A, B, B)$ (aksioma $D1$).} 
\proofstep{0} {Va\v{z}i $B = C$ ili $B \neq C$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $B = C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $col(A, B, B)$ i $B = C$ va\v{z}i $col(A, B, C)$.} 
\proofstep{6} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $col(A, B, C)$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $B \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $B \neq C$ i $B \in q$ i $C \in q$ i $B \in \beta$ i $C \in \beta$ va\v{z}i $q \in \beta$ (aksioma $I6$).} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $q \in \beta$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_14_04.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ i $p \in \beta$ i $q \in \beta$ pokazati da va\v{z}i $r \in \beta$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenica $A \in p$ i $B \in p$ i $A \in p$ va\v{z}i $col(A, B, A)$ (aksioma $D1$).} 
\proofstep{0} {Va\v{z}i $A = C$ ili $A \neq C$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $col(A, B, A)$ i $A = C$ va\v{z}i $col(A, B, C)$.} 
\proofstep{6} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $col(A, B, C)$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq C$ i $A \in r$ i $C \in r$ i $A \in \beta$ i $C \in \beta$ va\v{z}i $r \in \beta$ (aksioma $I6$).} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $r \in \beta$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_14_05.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ i $p \in \beta$ i $q \in \beta$ i $r \in \beta$ pokazati da va\v{z}i $D \in \beta$ i $E \in \beta$ i $F \in \beta$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenica $p \in \beta$ i $D \in p$ va\v{z}i $D \in \beta$ (aksioma $D11$).} 
\proofstep{0} {Na osnovu \v{c}injenica $q \in \beta$ i $E \in q$ va\v{z}i $E \in \beta$ (aksioma $D11$).} 
\proofstep{0} {Na osnovu \v{c}injenica $r \in \beta$ i $F \in r$ va\v{z}i $F \in \beta$ (aksioma $D11$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $D \in \beta$ i $E \in \beta$ i $F \in \beta$.} 
QED
\hrule 
\begin{theorem}[th_14_06.]
Pod pretpostavkom da va\v{z}i $B \not \in \alpha$ i $C \not \in \alpha$ i $D \not \in \alpha$ i $\neg col(B, C, D)$ i $B \in t$ i $C \in t$ i $C \in u$ i $D \in u$ i $D \in v$ i $B \in v$ i $I \in \alpha$ i $I \in t$ i $J \in \alpha$ i $J \in u$ i $K \in \alpha$ i $K \in v$ i $B \in \gamma3$ i $C \in \gamma3$ i $D \in \gamma3$ i $t \in \gamma3$ i $u \in \gamma3$ i $v \in \gamma3$ i $I \in \gamma3$ i $J \in \gamma3$ i $K \in \gamma3$ pokazati da postoji prava $t1$ tako da va\v{z}i $t1 \in \alpha$ i $t1 \in \gamma3$.
\end{theorem}

\hrule 
\begin{theorem}[th_14_07.]
Pod pretpostavkom da va\v{z}i $B \not \in \alpha$ i $C \not \in \alpha$ i $D \not \in \alpha$ i $\neg col(B, C, D)$ i $B \in t$ i $C \in t$ i $C \in u$ i $D \in u$ i $D \in v$ i $B \in v$ i $I \in \alpha$ i $I \in t$ i $J \in \alpha$ i $J \in u$ i $K \in \alpha$ i $K \in v$ i $B \in \gamma3$ i $C \in \gamma3$ i $D \in \gamma3$ i $t \in \gamma3$ i $u \in \gamma3$ i $v \in \gamma3$ i $I \in \gamma3$ i $J \in \gamma3$ i $K \in \gamma3$ i $t1 \in \alpha$ i $t1 \in \gamma3$ pokazati da postoji ta\v{c}ka $N$  i ta\v{c}ka $P$ tako da va\v{z}i $N \neq P$ i $N \in t1$ i $P \in t1$.
\end{theorem}

\hrule 
\begin{theorem}[th_14_08.]
Pod pretpostavkom da va\v{z}i $B \not \in \alpha$ i $C \not \in \alpha$ i $D \not \in \alpha$ i $\neg col(B, C, D)$ i $B \in t$ i $C \in t$ i $C \in u$ i $D \in u$ i $D \in v$ i $B \in v$ i $I \in \alpha$ i $I \in t$ i $J \in \alpha$ i $J \in u$ i $K \in \alpha$ i $K \in v$ i $B \in \gamma3$ i $C \in \gamma3$ i $D \in \gamma3$ i $t \in \gamma3$ i $u \in \gamma3$ i $v \in \gamma3$ i $I \in \gamma3$ i $J \in \gamma3$ i $K \in \gamma3$ i $t1 \in \alpha$ i $t1 \in \gamma3$ i $N \neq P$ i $N \in t1$ i $P \in t1$ pokazati da va\v{z}i $I \in t1$ i $J \in t1$ i $K \in t1$.
\end{theorem}

\hrule 
\begin{theorem}[th_14_09.]
Pod pretpostavkom da va\v{z}i $A \not \in \alpha$ i $B \not \in \alpha$ i $C \not \in \alpha$ i $\neg col(A, B, C)$ i $A \in p$ i $B \in p$ i $B \in q$ i $C \in q$ i $C \in r$ i $A \in r$ i $D \in \alpha$ i $D \in p$ i $E \in \alpha$ i $E \in q$ i $F \in \alpha$ i $F \in r$ i $A \in \beta$ i $B \in \beta$ i $C \in \beta$ i $p \in \beta$ i $q \in \beta$ i $r \in \beta$ i $D \in \beta$ i $E \in \beta$ i $F \in \beta$ i $s \in \alpha$ i $s \in \beta$ i $G \neq I$ i $G \in s$ i $I \in s$ i $D \in s$ i $E \in s$ i $F \in s$ pokazati da va\v{z}i $col(D, E, F)$.
\end{theorem}

{\em Dokaz:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {Na osnovu \v{c}injenica $D \in s$ i $E \in s$ i $F \in s$ va\v{z}i $col(D, E, F)$ (aksioma $D1$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $col(D, E, F)$.} 
QED
\hrule 

\end{document}
