\documentclass [fleqn,titlepage]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}

\usepackage{latexsym}

%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}

% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}

\usepackage{makeidx}
%\usepackage{page} - fjernet 3.5.06
%\makeindex        - fjernet 3.5.06
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}

% tilfoejede pakker
\usepackage{lscape} 
\usepackage{multicol}
\usepackage{float}
\usepackage[latin1]{inputenc}
\usepackage[dvips]{graphicx} 
\usepackage{verbatim}
\usepackage[danish]{babel}
\usepackage{graphpap}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
%\hypersetup{pdftitle=}
\hypersetup{colorlinks=false}
\bibliographystyle{plain}

% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}

% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}

% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}
\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}
\afterheading}

\begin {document}

\floatplacement{figure}{h!}
\floatplacement{table}{h!}
\hyphenation{her-ud-over ek-si-stens-va-ri-ab-le an-dre dob-belt-im-pli-ka-ti-on ob-jekt-kvan-tor de-fi-ni-tions-lem-ma ens-be-tyd-en-de 
und-er-af-snit slut-ning-en inde-hol-der for-klar-ing-en si-de-be-ting-el-sen
des-uden be-vis-check-er-en}

ny----

$
[
\mathsf{x}
<<test
\mathsf{y}
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
\#1.
\newline 
{<}
{<}test
\#2.
\mbox{''}
]$ 

$
[<<testMacro(
\mathsf {t}
)
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}
{<}
{<}testMacro(
\#1.
\newline )
\mbox{''}
]$ 

 $
[
\mathsf{x}
<<test
\mathsf{y}
\stackrel{
\mathrm {macro}
}{\rightarrow}
\lambda 
\mathsf {t}
.
\lambda 
\mathsf {s}
.
\lambda 
\mathsf {c}
.<<testMacro(
\mathsf {t}
{}^h
\mathrel { : \, : }ExpandList(
\mathsf {t}
{}^t
,
\mathsf {s}
,
\mathsf {c}
)
)
]$

$
[<<testMacro(
\mathsf {t}
)
\stackrel{
\mathrm {val}
}{\rightarrow}
\tilde {{\cal Q}}(
\mathsf {t}
,
\lceil 
\mathsf{x}
\rceil 
,
\lceil 
\mathsf{x}
\rceil 
\mathrel { : \, : }
\mathsf {t}
{}^{2}
{}^{2}
{}^{2}
{}^{1}
{}^{2}
{}^{1}
{}^{2}
{}^{2}
{}^{2}
{}^{1}
{}^{1}
{}^{1}
{}^{1}
{}^{1}
{}^{1}
\mathrel { : \, : }
\mathsf {T}
)
]$

(*****)

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
+
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
+
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 1

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
+
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
+
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 2

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 3

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 4

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 5

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 6

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 7

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 8

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(\underline{(fx)}
[\underline{
\mathsf {m}}
]
* \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \overline{(crs1)}
\colon \dot{\neg}\,(
\mathsf {c}
 _{Ph} 
 = \{\{\overline{(crs1)}
,\overline{(crs1)}
\}
,\{\overline{(crs1)}
,0
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(\underline{(fx)}
[\underline{
\mathsf {m}}
]
* \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \overline{(crs1)}
\colon \dot{\neg}\,(
\mathsf {c}
 _{Ph} 
 = \{\{\overline{(crs1)}
,\overline{(crs1)}
\}
,\{\overline{(crs1)}
,0
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 8a

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(\underline{(fx)}
[\underline{
\mathsf {m}}
]
* \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \overline{(crs1)}
\colon \dot{\neg}\,(
\mathsf {c}
 _{Ph} 
 = \{\{\overline{(crs1)}
,\overline{(crs1)}
\}
,\{\overline{(crs1)}
,0
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(\underline{(fx)}
[\underline{
\mathsf {m}}
]
* \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \overline{(crs1)}
\colon \dot{\neg}\,(
\mathsf {c}
 _{Ph} 
 = \{\{\overline{(crs1)}
,\overline{(crs1)}
\}
,\{\overline{(crs1)}
,0
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 8b


$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 8

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 9

$\dot{\neg}\,(
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(\dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \dot{\neg}\,(\overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow  \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {a}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
 <= ( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {e}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
*
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u\overline{(\epsilon)}
)
)
)n
)n
)n
)n
)n
)n$ 10

$\dot{\neg}\,(
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(\dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \dot{\neg}\,(\overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow  \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {f}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(-u
\mathsf {a}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
 <= ( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,( \{ ph \mathrel{\in}  \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
\mid \dot{\neg}\,(
\forall_{obj} \underline{
\mathsf {m}}
\colon \dot{\neg}\,(
\mathsf {d}
 _{Ph} 
 = \{\{\underline{
\mathsf {m}}
,\underline{
\mathsf {m}}
\}
,\{\underline{
\mathsf {m}}
,(
\mathsf {b}
[\underline{
\mathsf {m}}
]
+
\mathsf {b}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\underline{
\mathsf {m}}
]
+
\mathsf {c}
[\underline{
\mathsf {m}}
]
)
\}
\}
)n
)n
\}
[\overline{
\mathsf {m}}
]
+(-u\overline{(\epsilon)}
)
)
)n
)n
)n
)n
)n
)n$ 11

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|(
\mathsf {a}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|(
\mathsf {a}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 12

$ \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P( \{ ph \mathrel{\in} P(P(Union(\{N
,Q
\}
)
)
)
\mid \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(
\mathsf {a}
 _{Ph} 
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\}
)
\mid \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(r1)}
\colon \overline{(r1)}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(op1)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{(op2)}
\colon \dot{\neg}\,(\dot{\neg}\,(\dot{\neg}\,(\overline{(op1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(\overline{(op2)}
 \mathrel{\in} Q
)n
)n
\Rightarrow \dot{\neg}\,(\overline{(r1)}
 = \{\{\overline{(op1)}
,\overline{(op1)}
\}
,\{\overline{(op1)}
,\overline{(op2)}
\}
\}
)n
)n
)n
)n
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(f1)}
\colon 
\forall_{obj} \overline{(f2)}
\colon 
\forall_{obj} \overline{(f3)}
\colon 
\forall_{obj} \overline{(f4)}
\colon \{\{\overline{(f1)}
,\overline{(f1)}
\}
,\{\overline{(f1)}
,\overline{(f2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \{\{\overline{(f3)}
,\overline{(f3)}
\}
,\{\overline{(f3)}
,\overline{(f4)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
\Rightarrow \overline{(f1)}
 = \overline{(f3)}
\Rightarrow \overline{(f2)}
 = \overline{(f4)}
)n
)n
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s1)}
\colon \overline{(s1)}
 \mathrel{\in} N
\Rightarrow \dot{\neg}\,(
\forall_{obj} \overline{(s2)}
\colon \dot{\neg}\,(\{\{\overline{(s1)}
,\overline{(s1)}
\}
,\{\overline{(s1)}
,\overline{(s2)}
\}
\}
 \mathrel{\in} 
\mathsf {f}
 _{Ph} 
)n
)n
)n
)n
\}
)
\mid 
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow \dot{\neg}\,(|(
\mathsf {b}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(|(
\mathsf {b}
[\overline{
\mathsf {m}}
]
+(-u
\mathsf {d}
 _{Ph} 
[\overline{
\mathsf {m}}
]
)
)
|
 = \overline{(\epsilon)}
)n
)n
)n
)n
)n
\}$ 13

$\dot{\neg}\,(
\forall_{obj} \overline{(\epsilon)}
\colon \dot{\neg}\,(\dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {n}}
\colon \dot{\neg}\,(
\forall_{obj} \overline{
\mathsf {m}}
\colon \dot{\neg}\,(\dot{\neg}\,(0
 <= \overline{(\epsilon)}
\Rightarrow \dot{\neg}\,(\dot{\neg}\,(0
 = \overline{(\epsilon)}
)n
)n
)n
\Rightarrow \dot{\neg}\,(\overline{
\mathsf {n}}
 <= \overline{
\mathsf {m}}
\Rightarrow 
\mathsf {a}
[\overline{
\mathsf {m}}
]
 <= (
\mathsf {b}
[\overline{
\mathsf {m}}
]
+(-u\overline{(\epsilon)}
)
)
)n
)n
)n
)n
)n
)n$ 14

$
\mathsf {b}$ 15





venter----


\appendix


\begin {flushleft}$
[prove
\stackrel{
\mathrm{prio}
}{\rightarrow}
\newline \mathbf {Preassociative} \newline 
[prove
] , \linebreak [0] 
[
\mbox{base}
] , \linebreak [0] 
[
\mbox{bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\mbox{big bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\ \$
\ast \$\linebreak[0]\ 
] , \linebreak [0] 
[
\mathbf{flush\ left\ }[ 
\ast 
]
] , \linebreak [0] 
[
\mathsf{x}
] , \linebreak [0] 
[
\mathsf{y}
] , \linebreak [0] 
[
\mathsf{z}
] , \linebreak [0] 
[
[
\ast 
\bowtie
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel{
\ast 
}{\rightarrow}
\ast 
]
] , \linebreak [0] 
[
\mathrm{pyk}
] , \linebreak [0] 
[
\mathrm{tex}
] , \linebreak [0] 
[
\mathrm{name}
] , \linebreak [0] 
[
\mathrm{prio}
] , \linebreak [0] 
[
\ast 
] , \linebreak [0] 
[
\mathsf {T}
] , \linebreak [0] 
[
\mathrm {if}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {
\ast 
}{\Rightarrow }
\ast 
]
] , \linebreak [0] 
[
\mathrm {val}
] , \linebreak [0] 
[
\mathrm {claim}
] , \linebreak [0] 
[
\bot 
] , \linebreak [0] 
[
f(
\ast 
)
] , \linebreak [0] 
[
(
\ast 
){}^{I} 
] , \linebreak [0] 
[
\mathsf {F}
] , \linebreak [0] 
[
\underline {0}
] , \linebreak [0] 
[
\underline {1}
] , \linebreak [0] 
[
\underline {2}
] , \linebreak [0] 
[
\underline {3}
] , \linebreak [0] 
[
\underline {4}
] , \linebreak [0] 
[
\underline {5}
] , \linebreak [0] 
[
\underline {6}
] , \linebreak [0] 
[
\underline {7}
] , \linebreak [0] 
[
\underline {8}
] , \linebreak [0] 
[
\underline {9}
] , \linebreak [0] 
[
0
] , \linebreak [0] 
[
1
] , \linebreak [0] 
[
2
] , \linebreak [0] 
[
3
] , \linebreak [0] 
[
4
] , \linebreak [0] 
[
5
] , \linebreak [0] 
[
6
] , \linebreak [0] 
[
7
] , \linebreak [0] 
[
8
] , \linebreak [0] 
[
9
] , \linebreak [0] 
[
\mathsf {a}
] , \linebreak [0] 
[
\mathsf {b}
] , \linebreak [0] 
[
\mathsf {c}
] , \linebreak [0] 
[
\mathsf {d}
] , \linebreak [0] 
[
\mathsf {e}
] , \linebreak [0] 
[
\mathsf {f}
] , \linebreak [0] 
[
\mathsf {g}
] , \linebreak [0] 
[
\mathsf {h}
] , \linebreak [0] 
[
\mathsf {i}
] , \linebreak [0] 
[
\mathsf {j}
] , \linebreak [0] 
[
\mathsf {k}
] , \linebreak [0] 
[
\mathsf {l}
] , \linebreak [0] 
[
\mathsf {m}
] , \linebreak [0] 
[
\mathsf {n}
] , \linebreak [0] 
[
\mathsf {o}
] , \linebreak [0] 
[
\mathsf {p}
] , \linebreak [0] 
[
\mathsf {q}
] , \linebreak [0] 
[
\mathsf {r}
] , \linebreak [0] 
[
\mathsf {s}
] , \linebreak [0] 
[
\mathsf {t}
] , \linebreak [0] 
[
\mathsf {u}
] , \linebreak [0] 
[
\mathsf {v}
] , \linebreak [0] 
[
\mathsf {w}
] , \linebreak [0] 
[
(
\ast 
)^M
] , \linebreak [0] 
[
\mathrm {If}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[\mathrm {array}\{
\ast 
\}
\ast 
\mathrm {end\ array}
] , \linebreak [0] 
[
l
] , \linebreak [0] 
[
c
] , \linebreak [0] 
[
r
] , \linebreak [0] 
[
\mathrm {empty}
] , \linebreak [0] 
[
\langle 
\ast 
\,{|}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
{\cal M}(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal U}}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}^M(
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}_1(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
identifier( 
\ast 
)
] , \linebreak [0] 
[
identifier_{1}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]remove( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]put( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]add( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rack
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}
] , \linebreak [0] 
[
{\cal E}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {lookup}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {abstract}(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\lceil 
\ast 
\rceil 
] , \linebreak [0] 
[
{\cal M}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathrm {macro}
] , \linebreak [0] 
[
s_0
] , \linebreak [0] 
[
\mathbf {zip}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {assoc}_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[(
\ast 
)^{\mathbf {p}}
] , \linebreak [0] 
[
\mbox{self}
] , \linebreak [0] 
[
[
\ast 
\mathrel {\ddot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\dot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\acute {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {pyk}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {tex}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {name}}{=} 
\ast 
]
] , \linebreak [0] 
[
\mathbf{Priority\ table} [ 
\ast 
]
] , \linebreak [0] 
[
\tilde {{\cal M}}_1
] , \linebreak [0] 
[
\tilde {{\cal M}}_2(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_3(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
(
\ast 
)
] , \linebreak [0] 
[
\left( 
\ast 
\right) 
] , \linebreak [0] 
[
display(
\ast 
)
] , \linebreak [0] 
[
statement(
\ast 
)
] , \linebreak [0] 
[
[
\ast 
]^{\cdot}
] , \linebreak [0] 
[
[
\ast 
]^-
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\langle 
\ast 
\rangle 
] , \linebreak [0] 
[
\mathbf {tuple}_1( 
\ast 
) 
] , \linebreak [0] 
[
\mathbf {tuple}_2( 
\ast 
) 
] , \linebreak [0] 
[
let_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
let_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {claim}{=}
\ast 
]
] , \linebreak [0] 
[
\mbox{checker}
] , \linebreak [0] 
[
\mathbf{check}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_3( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\cdot} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{-} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\circ} 
] , \linebreak [0] 
[
msg
] , \linebreak [0] 
[
[
\ast 
\stackrel {msg}{=} 
\ast 
]
] , \linebreak [0] 
[
{<}stmt{>}
] , \linebreak [0] 
[
stmt
] , \linebreak [0] 
[
[
\ast 
\stackrel {stmt}{=}
\ast 
]
] , \linebreak [0] 
[
HeadNil'
] , \linebreak [0] 
[
HeadPair'
] , \linebreak [0] 
[
Transitivity'
] , \linebreak [0] 
[
{\makebox [0mm][l]{$\bot $}\,{\bot }}
] , \linebreak [0] 
[
Contra'
] , \linebreak [0] 
[
T'_{E}
] , \linebreak [0] 
[
L_{1}
] , \linebreak [0] 
[\underline{
\ast }
] , \linebreak [0] 
[{\cal A}
] , \linebreak [0] 
[{\cal B}
] , \linebreak [0] 
[{\cal C}
] , \linebreak [0] 
[{\cal D}
] , \linebreak [0] 
[{\cal E}
] , \linebreak [0] 
[{\cal F}
] , \linebreak [0] 
[{\cal G}
] , \linebreak [0] 
[{\cal H}
] , \linebreak [0] 
[{\cal I}
] , \linebreak [0] 
[{\cal J}
] , \linebreak [0] 
[{\cal K}
] , \linebreak [0] 
[{\cal L}
] , \linebreak [0] 
[{\cal M}
] , \linebreak [0] 
[{\cal N}
] , \linebreak [0] 
[{\cal O}
] , \linebreak [0] 
[{\cal P}
] , \linebreak [0] 
[{\cal Q}
] , \linebreak [0] 
[{\cal R}
] , \linebreak [0] 
[{\cal S}
] , \linebreak [0] 
[{\cal T}
] , \linebreak [0] 
[{\cal U}
] , \linebreak [0] 
[{\cal V}
] , \linebreak [0] 
[{\cal W}
] , \linebreak [0] 
[{\cal X}
] , \linebreak [0] 
[{\cal Y}
] , \linebreak [0] 
[{\cal Z}
] , \linebreak [0] 
[
\langle 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\langle ^ { \ast } 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\emptyset 
] , \linebreak [0] 
[
Remainder
] , \linebreak [0] 
[
( 
\ast 
)^{\bf v}
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error_{2}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
proof( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
proof_{2}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{I}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\rhd}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\rhd}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{E}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{E}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{+}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{+}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{-}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{-}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\ast}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\char64}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\char64}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\vdash}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\vdash}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{i.e.}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\forall}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\forall}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{;}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{;}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{;}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal T}( 
\ast 
)
] , \linebreak [0] 
[
claims( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
claims_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{<}proof{>}
] , \linebreak [0] 
[
proof
] , \linebreak [0] 
[
[ \mathbf{Lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ \mathbf{Proof\ of\ }
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antilemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ rule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antirule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
\mbox{verifier}
] , \linebreak [0] 
[
{\cal V}_1( 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_3( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_4( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_5( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_6( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_7( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Cut( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Head_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
Tail_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
rule_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rule( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Rule\ tactic
] , \linebreak [0] 
[
Plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[ \mathbf{Theory\ } 
\ast 
]
] , \linebreak [0] 
[
theory_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_3( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_4( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
HeadNil''
] , \linebreak [0] 
[
HeadPair''
] , \linebreak [0] 
[
Transitivity''
] , \linebreak [0] 
[
Contra''
] , \linebreak [0] 
[
HeadNil
] , \linebreak [0] 
[
HeadPair
] , \linebreak [0] 
[
Transitivity
] , \linebreak [0] 
[
Contra
] , \linebreak [0] 
[
T_E
] , \linebreak [0] 
[
ragged\ right
] , \linebreak [0] 
[
ragged\ right\ expansion\ 
] , \linebreak [0] 
[
parm(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
parm^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify^*(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify_2(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[L_a
] , \linebreak [0] 
[L_b
] , \linebreak [0] 
[L_c
] , \linebreak [0] 
[L_d
] , \linebreak [0] 
[L_e
] , \linebreak [0] 
[L_f
] , \linebreak [0] 
[L_g
] , \linebreak [0] 
[L_h
] , \linebreak [0] 
[L_i
] , \linebreak [0] 
[L_j
] , \linebreak [0] 
[L_k
] , \linebreak [0] 
[L_l
] , \linebreak [0] 
[L_m
] , \linebreak [0] 
[L_n
] , \linebreak [0] 
[L_o
] , \linebreak [0] 
[L_p
] , \linebreak [0] 
[L_q
] , \linebreak [0] 
[L_r
] , \linebreak [0] 
[L_s
] , \linebreak [0] 
[L_t
] , \linebreak [0] 
[L_u
] , \linebreak [0] 
[L_v
] , \linebreak [0] 
[L_w
] , \linebreak [0] 
[L_x
] , \linebreak [0] 
[L_y
] , \linebreak [0] 
[L_z
] , \linebreak [0] 
[L_A
] , \linebreak [0] 
[L_B
] , \linebreak [0] 
[L_C
] , \linebreak [0] 
[L_D
] , \linebreak [0] 
[L_E
] , \linebreak [0] 
[L_F
] , \linebreak [0] 
[L_G
] , \linebreak [0] 
[L_H
] , \linebreak [0] 
[L_I
] , \linebreak [0] 
[L_J
] , \linebreak [0] 
[L_K
] , \linebreak [0] 
[L_L
] , \linebreak [0] 
[L_M
] , \linebreak [0] 
[L_N
] , \linebreak [0] 
[L_O
] , \linebreak [0] 
[L_P
] , \linebreak [0] 
[L_Q
] , \linebreak [0] 
[L_R
] , \linebreak [0] 
[L_S
] , \linebreak [0] 
[L_T
] , \linebreak [0] 
[L_U
] , \linebreak [0] 
[L_V
] , \linebreak [0] 
[L_W
] , \linebreak [0] 
[L_X
] , \linebreak [0] 
[L_Y
] , \linebreak [0] 
[L_Z
] , \linebreak [0] 
[L_?
] , \linebreak [0] 
[
Reflexivity
] , \linebreak [0] 
[
Reflexivity_1
] , \linebreak [0] 
[
Commutativity
] , \linebreak [0] 
[
Commutativity_1
] , \linebreak [0] 
[
{<}tactic{>}
] , \linebreak [0] 
[
tactic
] , \linebreak [0] 
[
[
\ast 
\stackrel {tactic}{=}
\ast 
]
] , \linebreak [0] 
[
{\cal P}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal P}^*( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
p_0
] , \linebreak [0] 
[
conclude_1 ( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_2 ( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_3 ( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_4 ( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mbox{check}
] , \linebreak [0] 
[
[
\ast 
\stackrel {\circ}{=}
\ast 
]
] , \linebreak [0] 
[
RootVisible(
\ast 
)
] , \linebreak [0] 
[
A
] , \linebreak [0] 
[
R
] , \linebreak [0] 
[
C
] , \linebreak [0] 
[
T
] , \linebreak [0] 
[
L
] , \linebreak [0] 
[
\{
\ast 
\}
] , \linebreak [0] 
[\overline{
\ast }
] , \linebreak [0] 
[
\mathit{a}
] , \linebreak [0] 
[
\mathit{b}
] , \linebreak [0] 
[
\mathit{c}
] , \linebreak [0] 
[
\mathit{d}
] , \linebreak [0] 
[
\mathit{e}
] , \linebreak [0] 
[
\mathit{f}
] , \linebreak [0] 
[
\mathit{g}
] , \linebreak [0] 
[
\mathit{h}
] , \linebreak [0] 
[
\mathit{i}
] , \linebreak [0] 
[
\mathit{j}
] , \linebreak [0] 
[
\mathit{k}
] , \linebreak [0] 
[
\mathit{l}
] , \linebreak [0] 
[
\mathit{m}
] , \linebreak [0] 
[
\mathit{n}
] , \linebreak [0] 
[
\mathit{o}
] , \linebreak [0] 
[
\mathit{p}
] , \linebreak [0] 
[
\mathit{q}
] , \linebreak [0] 
[
\mathit{r}
] , \linebreak [0] 
[
\mathit{s}
] , \linebreak [0] 
[
\mathit{t}
] , \linebreak [0] 
[
\mathit{u}
] , \linebreak [0] 
[
\mathit{v}
] , \linebreak [0] 
[
\mathit{w}
] , \linebreak [0] 
[
\mathit{x}
] , \linebreak [0] 
[
\mathit{y}
] , \linebreak [0] 
[
\mathit{z}
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv} 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^0 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^1 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
\langle 
\ast 
{\equiv}^* 
\ast 
| 
\ast 
{:=} 
\ast 
\rangle 
] , \linebreak [0] 
[
Ded(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_0(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_4^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_5(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_6(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_6^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_7(
\ast 
)
] , \linebreak [0] 
[
Ded_8(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Ded_8^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
S
] , \linebreak [0] 
[
Neg
] , \linebreak [0] 
[
MP
] , \linebreak [0] 
[
Gen
] , \linebreak [0] 
[
Ded
] , \linebreak [0] 
[
S1
] , \linebreak [0] 
[
S2
] , \linebreak [0] 
[
S3
] , \linebreak [0] 
[
S4
] , \linebreak [0] 
[
S5
] , \linebreak [0] 
[
S6
] , \linebreak [0] 
[
S7
] , \linebreak [0] 
[
S8
] , \linebreak [0] 
[
S9
] , \linebreak [0] 
[
Repetition
] , \linebreak [0] 
[
A1'
] , \linebreak [0] 
[
A2'
] , \linebreak [0] 
[
A4'
] , \linebreak [0] 
[
A5'
] , \linebreak [0] 
[
Prop\ 3.2a
] , \linebreak [0] 
[
Prop\ 3.2b
] , \linebreak [0] 
[
Prop\ 3.2c
] , \linebreak [0] 
[
Prop\ 3.2d
] , \linebreak [0] 
[
Prop\ 3.2e_1
] , \linebreak [0] 
[
Prop\ 3.2e_2
] , \linebreak [0] 
[
Prop\ 3.2e
] , \linebreak [0] 
[
Prop\ 3.2f_1
] , \linebreak [0] 
[
Prop\ 3.2f_2
] , \linebreak [0] 
[
Prop\ 3.2f
] , \linebreak [0] 
[
Prop\ 3.2g_1
] , \linebreak [0] 
[
Prop\ 3.2g_2
] , \linebreak [0] 
[
Prop\ 3.2g
] , \linebreak [0] 
[
Prop\ 3.2h_1
] , \linebreak [0] 
[
Prop\ 3.2h_2
] , \linebreak [0] 
[
Prop\ 3.2h
] , \linebreak [0] 
[
Block_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Block_2(
\ast 
)
] , \linebreak [0] 
[kvanti
] , \linebreak [0] 
[UniqueMember
] , \linebreak [0] 
[UniqueMember(Type)
] , \linebreak [0] 
[SameSeries
] , \linebreak [0] 
[A4
] , \linebreak [0] 
[SameMember
] , \linebreak [0] 
[Qclosed(Addition)
] , \linebreak [0] 
[Qclosed(Multiplication)
] , \linebreak [0] 
[FromCartProd(1)
] , \linebreak [0] 
[
\mbox{1rule fromCartProd(2)}
] , \linebreak [0] 
[constantRationalSeries(
\ast 
)
] , \linebreak [0] 
[cartProd(
\ast 
)
] , \linebreak [0] 
[Power(
\ast 
)
] , \linebreak [0] 
[binaryUnion(
\ast 
,
\ast 
)
] , \linebreak [0] 
[SetOfRationalSeries
] , \linebreak [0] 
[IsSubset(
\ast 
,
\ast 
)
] , \linebreak [0] 
[(p
\ast 
,
\ast 
)
] , \linebreak [0] 
[(s
\ast 
)
] , \linebreak [0] 
[(\cdots{})
] , \linebreak [0] 
[\texttt{Objekt-var}
] , \linebreak [0] 
[\texttt{Ex-var}
] , \linebreak [0] 
[\texttt{Ph-var}
] , \linebreak [0] 
[\texttt{V\ae{}rdi}
] , \linebreak [0] 
[\texttt{Variabel}
] , \linebreak [0] 
[Op(
\ast 
)
] , \linebreak [0] 
[Op(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
 \mathrel {\ddot {==}} 
\ast 
] , \linebreak [0] 
[ContainsEmpty(
\ast 
)
] , \linebreak [0] 
[Nat(
\ast 
)
] , \linebreak [0] 
[
Dedu(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_0(
\ast 
,
\ast 
)
] , \linebreak [0] 
[Dedu_{s}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_4^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_5(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_6(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_6^*(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_7(
\ast 
)
] , \linebreak [0] 
[
Dedu_8(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
Dedu_8^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[Ex_{1}
] , \linebreak [0] 
[Ex_{2}
] , \linebreak [0] 
[Ex3
] , \linebreak [0] 
[Ex_{10}
] , \linebreak [0] 
[Ex_{20}
] , \linebreak [0] 
[
\ast 
 _{Ex}
] , \linebreak [0] 
[
\ast 
 ^{Ex}
] , \linebreak [0] 
[\langle 
\ast 
{\equiv} 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ex} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^0 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ex} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^1 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ex} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^* 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ex} 
] , \linebreak [0] 
[ph_{1}
] , \linebreak [0] 
[ph_{2}
] , \linebreak [0] 
[ph_{3}
] , \linebreak [0] 
[
\ast 
 _{Ph} 
] , \linebreak [0] 
[
\ast 
 ^{Ph}
] , \linebreak [0] 
[\langle 
\ast 
{\equiv} 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ph} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^0 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ph} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^1 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ph} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^* 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Ph} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv} 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Me}
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^1 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Me} 
] , \linebreak [0] 
[\langle 
\ast 
{\equiv}^* 
\ast 
| 
\ast 
{:==} 
\ast 
\rangle_{Me} 
] , \linebreak [0] 
[\mathsf {bs}
] , \linebreak [0] 
[ \mathsf {OBS}
] , \linebreak [0] 
[{\cal BS}
] , \linebreak [0] 
[\mathrm{\O}
] , \linebreak [0] 
[SystemQ
] , \linebreak [0] 
[MP
] , \linebreak [0] 
[Gen
] , \linebreak [0] 
[Repetition
] , \linebreak [0] 
[Neg
] , \linebreak [0] 
[Ded
] , \linebreak [0] 
[ExistIntro
] , \linebreak [0] 
[Extensionality
] , \linebreak [0] 
[\O{}def
] , \linebreak [0] 
[PairDef
] , \linebreak [0] 
[UnionDef
] , \linebreak [0] 
[PowerDef
] , \linebreak [0] 
[SeparationDef
] , \linebreak [0] 
[AddDoubleNeg
] , \linebreak [0] 
[RemoveDoubleNeg
] , \linebreak [0] 
[AndCommutativity
] , \linebreak [0] 
[AutoImply
] , \linebreak [0] 
[Contrapositive
] , \linebreak [0] 
[FirstConjunct
] , \linebreak [0] 
[SecondConjunct
] , \linebreak [0] 
[FromContradiction
] , \linebreak [0] 
[FromDisjuncts
] , \linebreak [0] 
[IffCommutativity
] , \linebreak [0] 
[IffFirst
] , \linebreak [0] 
[IffSecond
] , \linebreak [0] 
[ImplyTransitivity
] , \linebreak [0] 
[JoinConjuncts
] , \linebreak [0] 
[MP2
] , \linebreak [0] 
[MP3
] , \linebreak [0] 
[MP4
] , \linebreak [0] 
[MP5
] , \linebreak [0] 
[MT
] , \linebreak [0] 
[NegativeMT
] , \linebreak [0] 
[Technicality
] , \linebreak [0] 
[Weakening
] , \linebreak [0] 
[WeakenOr1
] , \linebreak [0] 
[WeakenOr2
] , \linebreak [0] 
[Formula2Pair
] , \linebreak [0] 
[Pair2Formula
] , \linebreak [0] 
[Formula2Union
] , \linebreak [0] 
[Union2Formula
] , \linebreak [0] 
[Formula2Sep
] , \linebreak [0] 
[Sep2Formula
] , \linebreak [0] 
[Formula2Power
] , \linebreak [0] 
[SubsetInPower
] , \linebreak [0] 
[HelperPowerIsSub
] , \linebreak [0] 
[PowerIsSub
] , \linebreak [0] 
[(Switch)HelperPowerIsSub
] , \linebreak [0] 
[(Switch)PowerIsSub
] , \linebreak [0] 
[ToSetEquality
] , \linebreak [0] 
[HelperToSetEquality(t)
] , \linebreak [0] 
[ToSetEquality(t)
] , \linebreak [0] 
[HelperFromSetEquality
] , \linebreak [0] 
[FromSetEquality
] , \linebreak [0] 
[HelperReflexivity
] , \linebreak [0] 
[Reflexivity
] , \linebreak [0] 
[HelperSymmetry
] , \linebreak [0] 
[Symmetry
] , \linebreak [0] 
[HelperTransitivity
] , \linebreak [0] 
[Transitivity
] , \linebreak [0] 
[ERisReflexive
] , \linebreak [0] 
[ERisSymmetric
] , \linebreak [0] 
[ERisTransitive
] , \linebreak [0] 
[\O{}isSubset
] , \linebreak [0] 
[HelperMemberNot\O{}
] , \linebreak [0] 
[MemberNot\O{}
] , \linebreak [0] 
[HelperUnique\O{}
] , \linebreak [0] 
[Unique\O{}
] , \linebreak [0] 
[==\!{}Reflexivity
] , \linebreak [0] 
[==\!{}Symmetry
] , \linebreak [0] 
[Helper\!{}==\!{}Transitivity
] , \linebreak [0] 
[\!{}==\!{}Transitivity
] , \linebreak [0] 
[HelperTransferNotEq
] , \linebreak [0] 
[TransferNotEq
] , \linebreak [0] 
[HelperPairSubset
] , \linebreak [0] 
[Helper(2)PairSubset
] , \linebreak [0] 
[PairSubset
] , \linebreak [0] 
[SamePair
] , \linebreak [0] 
[SameSingleton
] , \linebreak [0] 
[UnionSubset
] , \linebreak [0] 
[SameUnion
] , \linebreak [0] 
[SeparationSubset
] , \linebreak [0] 
[SameSeparation
] , \linebreak [0] 
[SameBinaryUnion
] , \linebreak [0] 
[IntersectionSubset
] , \linebreak [0] 
[SameIntersection
] , \linebreak [0] 
[AutoMember
] , \linebreak [0] 
[HelperEqSysNot\O{}
] , \linebreak [0] 
[EqSysNot\O{}
] , \linebreak [0] 
[HelperEqSubset
] , \linebreak [0] 
[EqSubset
] , \linebreak [0] 
[HelperEqNecessary
] , \linebreak [0] 
[EqNecessary
] , \linebreak [0] 
[HelperNoneEqNecessary
] , \linebreak [0] 
[Helper(2)NoneEqNecessary
] , \linebreak [0] 
[NoneEqNecessary
] , \linebreak [0] 
[EqClassIsSubset
] , \linebreak [0] 
[EqClassesAreDisjoint
] , \linebreak [0] 
[AllDisjoint
] , \linebreak [0] 
[AllDisjointImply
] , \linebreak [0] 
[BSsubset
] , \linebreak [0] 
[Union(BS/R)subset
] , \linebreak [0] 
[UnionIdentity
] , \linebreak [0] 
[EqSysIsPartition
] , \linebreak [0] 
[(x1)
] , \linebreak [0] 
[(x2)
] , \linebreak [0] 
[(y1)
] , \linebreak [0] 
[(y2)
] , \linebreak [0] 
[(v1)
] , \linebreak [0] 
[(v2)
] , \linebreak [0] 
[(v3)
] , \linebreak [0] 
[(v4)
] , \linebreak [0] 
[(v2n)
] , \linebreak [0] 
[(m1)
] , \linebreak [0] 
[(m2)
] , \linebreak [0] 
[(n1)
] , \linebreak [0] 
[(n2)
] , \linebreak [0] 
[(n3)
] , \linebreak [0] 
[(\epsilon)
] , \linebreak [0] 
[(\epsilon)_{1}
] , \linebreak [0] 
[(\epsilon 2)
] , \linebreak [0] 
[(fep)
] , \linebreak [0] 
[(fx)
] , \linebreak [0] 
[(fy)
] , \linebreak [0] 
[(fz)
] , \linebreak [0] 
[(fu)
] , \linebreak [0] 
[(fv)
] , \linebreak [0] 
[(fw)
] , \linebreak [0] 
[(rx)
] , \linebreak [0] 
[(ry)
] , \linebreak [0] 
[(rz)
] , \linebreak [0] 
[(ru)
] , \linebreak [0] 
[(sx)
] , \linebreak [0] 
[(sx1)
] , \linebreak [0] 
[(sy)
] , \linebreak [0] 
[(sy1)
] , \linebreak [0] 
[(sz)
] , \linebreak [0] 
[(sz1)
] , \linebreak [0] 
[(su)
] , \linebreak [0] 
[(su1)
] , \linebreak [0] 
[(fxs)
] , \linebreak [0] 
[(fys)
] , \linebreak [0] 
[(crs1)
] , \linebreak [0] 
[(f1)
] , \linebreak [0] 
[(f2)
] , \linebreak [0] 
[(f3)
] , \linebreak [0] 
[(f4)
] , \linebreak [0] 
[(op1)
] , \linebreak [0] 
[(op2)
] , \linebreak [0] 
[(r1)
] , \linebreak [0] 
[(s1)
] , \linebreak [0] 
[(s2)
] , \linebreak [0] 
[X_{1}
] , \linebreak [0] 
[X_{2}
] , \linebreak [0] 
[Y_{1}
] , \linebreak [0] 
[Y_{2}
] , \linebreak [0] 
[V_{1}
] , \linebreak [0] 
[V_{2}
] , \linebreak [0] 
[V_{3}
] , \linebreak [0] 
[V_{4}
] , \linebreak [0] 
[V_{2n}
] , \linebreak [0] 
[M_{1}
] , \linebreak [0] 
[M_{2}
] , \linebreak [0] 
[N_{1} 
] , \linebreak [0] 
[N_{2} 
] , \linebreak [0] 
[N_{3} 
] , \linebreak [0] 
[\epsilon
] , \linebreak [0] 
[\epsilon 1
] , \linebreak [0] 
[\epsilon 2
] , \linebreak [0] 
[FX
] , \linebreak [0] 
[FY
] , \linebreak [0] 
[FZ
] , \linebreak [0] 
[FU
] , \linebreak [0] 
[FV
] , \linebreak [0] 
[FW
] , \linebreak [0] 
[FEP
] , \linebreak [0] 
[RX
] , \linebreak [0] 
[RY
] , \linebreak [0] 
[RZ
] , \linebreak [0] 
[RU
] , \linebreak [0] 
[(SX)
] , \linebreak [0] 
[(SX1)
] , \linebreak [0] 
[(SY)
] , \linebreak [0] 
[(SY1)
] , \linebreak [0] 
[(SZ)
] , \linebreak [0] 
[(SZ1)
] , \linebreak [0] 
[(SU)
] , \linebreak [0] 
[(SU1)
] , \linebreak [0] 
[FXS
] , \linebreak [0] 
[FYS
] , \linebreak [0] 
[(F1)
] , \linebreak [0] 
[(F2)
] , \linebreak [0] 
[(F3)
] , \linebreak [0] 
[(F4)
] , \linebreak [0] 
[(OP1)
] , \linebreak [0] 
[(OP2)
] , \linebreak [0] 
[(R1)
] , \linebreak [0] 
[(S1)
] , \linebreak [0] 
[(S2)
] , \linebreak [0] 
[(EPob)
] , \linebreak [0] 
[(CRS1ob)
] , \linebreak [0] 
[(F1ob)
] , \linebreak [0] 
[(F2ob)
] , \linebreak [0] 
[(F3ob)
] , \linebreak [0] 
[(F4ob)
] , \linebreak [0] 
[(N1ob)
] , \linebreak [0] 
[(N2ob)
] , \linebreak [0] 
[(OP1ob)
] , \linebreak [0] 
[(OP2ob)
] , \linebreak [0] 
[(R1ob)
] , \linebreak [0] 
[(S1ob)
] , \linebreak [0] 
[(S2ob)
] , \linebreak [0] 
[ph_{4}
] , \linebreak [0] 
[ph_{5}
] , \linebreak [0] 
[ph_{6}
] , \linebreak [0] 
[NAT
] , \linebreak [0] 
[RATIONAL_SERIES
] , \linebreak [0] 
[SERIES
] , \linebreak [0] 
[SetOfReals
] , \linebreak [0] 
[SetOfFxs
] , \linebreak [0] 
[N
] , \linebreak [0] 
[Q
] , \linebreak [0] 
[X
] , \linebreak [0] 
[xs
] , \linebreak [0] 
[xaF
] , \linebreak [0] 
[ysF
] , \linebreak [0] 
[us
] , \linebreak [0] 
[usFoelge
] , \linebreak [0] 
[0
] , \linebreak [0] 
[1
] , \linebreak [0] 
[(-1)
] , \linebreak [0] 
[2
] , \linebreak [0] 
[3
] , \linebreak [0] 
[1/2
] , \linebreak [0] 
[1/3
] , \linebreak [0] 
[2/3
] , \linebreak [0] 
[0f
] , \linebreak [0] 
[
\mbox{1f}
] , \linebreak [0] 
[00
] , \linebreak [0] 
[
\mbox{01}
] , \linebreak [0] 
[(--01)
] , \linebreak [0] 
[02
] , \linebreak [0] 
[01//02
] , \linebreak [0] 
[
\mbox{lemma plus0Left}
] , \linebreak [0] 
[
\mbox{lemma times1Left}
] , \linebreak [0] 
[
\mbox{lemma eqAdditionLeft}
] , \linebreak [0] 
[
\mbox{lemma eqMultiplicationLeft}
] , \linebreak [0] 
[PlusAssociativity(R)
] , \linebreak [0] 
[PlusAssociativity(R)XX
] , \linebreak [0] 
[Plus0(R)
] , \linebreak [0] 
[Negative(R)
] , \linebreak [0] 
[Times1(R)
] , \linebreak [0] 
[lessAddition(R)
] , \linebreak [0] 
[PlusCommutativity(R)
] , \linebreak [0] 
[LeqAntisymmetry(R)
] , \linebreak [0] 
[LeqTransitivity(R)
] , \linebreak [0] 
[leqAddition(R)
] , \linebreak [0] 
[Distribution(R)
] , \linebreak [0] 
[A4(Axiom)
] , \linebreak [0] 
[InductionAxiom
] , \linebreak [0] 
[EqualityAxiom
] , \linebreak [0] 
[EqLeqAxiom
] , \linebreak [0] 
[EqAdditionAxiom
] , \linebreak [0] 
[EqMultiplicationAxiom
] , \linebreak [0] 
[QisClosed(Reciprocal)(Imply)
] , \linebreak [0] 
[QisClosed(Reciprocal)
] , \linebreak [0] 
[QisClosed(Negative)(Imply)
] , \linebreak [0] 
[QisClosed(Negative)
] , \linebreak [0] 
[leqReflexivity
] , \linebreak [0] 
[leqAntisymmetryAxiom
] , \linebreak [0] 
[leqTransitivityAxiom
] , \linebreak [0] 
[leqTotality
] , \linebreak [0] 
[leqAdditionAxiom
] , \linebreak [0] 
[leqMultiplicationAxiom
] , \linebreak [0] 
[plusAssociativity
] , \linebreak [0] 
[plusCommutativity
] , \linebreak [0] 
[Negative
] , \linebreak [0] 
[plus0
] , \linebreak [0] 
[timesAssociativity
] , \linebreak [0] 
[timesCommutativity
] , \linebreak [0] 
[ReciprocalAxiom
] , \linebreak [0] 
[times1
] , \linebreak [0] 
[Distribution
] , \linebreak [0] 
[0not1
] , \linebreak [0] 
[
\mbox{lemma eqLeq(R)}
] , \linebreak [0] 
[TimesAssociativity(R)
] , \linebreak [0] 
[TimesCommutativity(R)
] , \linebreak [0] 
[
\mbox{lemma =f to sameF}
] , \linebreak [0] 
[
\mbox{lemma plusF(Sym)}
] , \linebreak [0] 
[
\mbox{lemma timesF(Sym)}
] , \linebreak [0] 
[Separation2formula(1)
] , \linebreak [0] 
[Separation2formula(2)
] , \linebreak [0] 
[IfThenElse(T)
] , \linebreak [0] 
[IfThenElse(F)
] , \linebreak [0] 
[Cauchy
] , \linebreak [0] 
[PlusF
] , \linebreak [0] 
[ReciprocalF
] , \linebreak [0] 
[From==
] , \linebreak [0] 
[To==
] , \linebreak [0] 
[From<<
] , \linebreak [0] 
[to<<
] , \linebreak [0] 
[FromInR
] , \linebreak [0] 
[PlusR
] , \linebreak [0] 
[PlusR(Sym)
] , \linebreak [0] 
[TimesR
] , \linebreak [0] 
[TimesR(Sym)
] , \linebreak [0] 
[ReciprocalR(Axiom)
] , \linebreak [0] 
[LessMinus1(N)
] , \linebreak [0] 
[Nonnegative(N)
] , \linebreak [0] 
[US0
] , \linebreak [0] 
[NextXS(UpperBound)
] , \linebreak [0] 
[NextXS(NoUpperBound)
] , \linebreak [0] 
[NextUS(UpperBound)
] , \linebreak [0] 
[NextUS(NoUpperBound)
] , \linebreak [0] 
[ExpZero
] , \linebreak [0] 
[ExpPositive
] , \linebreak [0] 
[ExpZero(R)
] , \linebreak [0] 
[ExpPositive(R)
] , \linebreak [0] 
[BSzero
] , \linebreak [0] 
[BSpositive
] , \linebreak [0] 
[UStelescope(Zero)
] , \linebreak [0] 
[UStelescope(Positive)
] , \linebreak [0] 
[EqAddition(R)
] , \linebreak [0] 
[Unminus(R)
] , \linebreak [0] 
[FromLimit
] , \linebreak [0] 
[ToUpperBound
] , \linebreak [0] 
[FromUpperBound
] , \linebreak [0] 
[USisUpperBound
] , \linebreak [0] 
[0not1(R)
] , \linebreak [0] 
[ExpUnbounded(R)
] , \linebreak [0] 
[FromLeq(Advanced)(N)
] , \linebreak [0] 
[FromLeastUpperBound
] , \linebreak [0] 
[ToLeastUpperBound
] , \linebreak [0] 
[XSisNotUpperBound
] , \linebreak [0] 
[ysFGreater
] , \linebreak [0] 
[ysFLess
] , \linebreak [0] 
[SmallInverse
] , \linebreak [0] 
[NatType
] , \linebreak [0] 
[RationalType
] , \linebreak [0] 
[SeriesType
] , \linebreak [0] 
[Max
] , \linebreak [0] 
[Numerical
] , \linebreak [0] 
[MemberOfSeries(Imply)
] , \linebreak [0] 
[JoinConjuncts(2conditions)
] , \linebreak [0] 
[
\mbox{prop lemma imply negation}
] , \linebreak [0] 
[TND
] , \linebreak [0] 
[FromNegatedImply
] , \linebreak [0] 
[ToNegatedImply
] , \linebreak [0] 
[FromNegated(2*Imply)
] , \linebreak [0] 
[FromNegatedAnd
] , \linebreak [0] 
[FromNegatedOr
] , \linebreak [0] 
[ToNegatedOr
] , \linebreak [0] 
[FromNegations
] , \linebreak [0] 
[From3Disjuncts
] , \linebreak [0] 
[From2*2Disjuncts
] , \linebreak [0] 
[NegateDisjunct1
] , \linebreak [0] 
[NegateDisjunct2
] , \linebreak [0] 
[ExpandDisjuncts
] , \linebreak [0] 
[SENC1
] , \linebreak [0] 
[SENC2
] , \linebreak [0] 
[LessLeq(R)
] , \linebreak [0] 
[MemberOfSeries
] , \linebreak [0] 
[memberOfSeries(Type)
] , \linebreak [0] 
[<<testMacro(
\ast 
)
] , \linebreak [0] 
[Tester1
] , \linebreak [0] 
[Tester2
] , \linebreak [0] 
[Tester3
] , \linebreak [0] 
[Tester4
] , \linebreak [0] 
[Tester5
] , \linebreak [0] 
[Tester6
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\_\{
\ast 
\}
] , \linebreak [0] 
[
\ast 
/indexintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/bothintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/nameintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast '
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\Rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
0
] , \linebreak [0] 
[
\ast 
1
] , \linebreak [0] 
[
0 \mathrm {b}
] , \linebreak [0] 
[
\ast 
\mbox {-color}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
\mbox {-color}^{\ast}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
{}^H
] , \linebreak [0] 
[
\ast 
{}^T
] , \linebreak [0] 
[
\ast 
{}^U
] , \linebreak [0] 
[
\ast 
{}^h
] , \linebreak [0] 
[
\ast 
{}^t
] , \linebreak [0] 
[
\ast 
{}^s
] , \linebreak [0] 
[
\ast 
{}^c
] , \linebreak [0] 
[
\ast 
{}^d
] , \linebreak [0] 
[
\ast 
{}^a
] , \linebreak [0] 
[
\ast 
{}^C
] , \linebreak [0] 
[
\ast 
{}^M
] , \linebreak [0] 
[
\ast 
{}^B
] , \linebreak [0] 
[
\ast 
{}^{r}
] , \linebreak [0] 
[
\ast 
{}^{i}
] , \linebreak [0] 
[
\ast 
{}^{d}
] , \linebreak [0] 
[
\ast 
{}^{R}
] , \linebreak [0] 
[
\ast 
{}^{0}
] , \linebreak [0] 
[
\ast 
{}^{1}
] , \linebreak [0] 
[
\ast 
{}^{2}
] , \linebreak [0] 
[
\ast 
{}^{3}
] , \linebreak [0] 
[
\ast 
{}^{4}
] , \linebreak [0] 
[
\ast 
{}^{5}
] , \linebreak [0] 
[
\ast 
{}^{6}
] , \linebreak [0] 
[
\ast 
{}^{7}
] , \linebreak [0] 
[
\ast 
{}^{8}
] , \linebreak [0] 
[
\ast 
{}^{9}
] , \linebreak [0] 
[
\ast 
{} ^ { E }
] , \linebreak [0] 
[
\ast 
{} ^ {\cal V}
] , \linebreak [0] 
[
\ast 
{} ^ {\cal C}
] , \linebreak [0] 
[
\ast 
{} ^ {{\cal C} ^ { \ast }}
] , \linebreak [0] 
[
\ast 
{}^{hide}
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{``}
\ast 
\mbox{''}
] , \linebreak [0] 
[
] , \linebreak [0] 
[
(
\ast 
)^{\bf t}
] , \linebreak [0] 
[
\mbox{string}(
\ast 
)+
\ast 
] , \linebreak [0] 
[\mbox{string}(
\ast 
)\mathrel{++}
\ast 
] , \linebreak [0] 
[
\newline 
\ast 
] , \linebreak [0] 
[
\linebreak [0]\ \hskip0em plus2.0em{}
\ast 
] , \linebreak [0] 
[!
\ast 
] , \linebreak [0] 
[
\mbox {\tt \char34}
\ast 
] , \linebreak [0] 
[
\#
\ast 
] , \linebreak [0] 
[
\$
\ast 
] , \linebreak [0] 
[
\%
\ast 
] , \linebreak [0] 
[
\&
\ast 
] , \linebreak [0] 
[
\mbox {'}
\ast 
] , \linebreak [0] 
[(
\ast 
] , \linebreak [0] 
[)
\ast 
] , \linebreak [0] 
[
{*}
\ast 
] , \linebreak [0] 
[
{+}
\ast 
] , \linebreak [0] 
[,
\ast 
] , \linebreak [0] 
[
\mbox{-}
\ast 
] , \linebreak [0] 
[.
\ast 
] , \linebreak [0] 
[/
\ast 
] , \linebreak [0] 
[0
\ast 
] , \linebreak [0] 
[1
\ast 
] , \linebreak [0] 
[2
\ast 
] , \linebreak [0] 
[3
\ast 
] , \linebreak [0] 
[4
\ast 
] , \linebreak [0] 
[5
\ast 
] , \linebreak [0] 
[6
\ast 
] , \linebreak [0] 
[7
\ast 
] , \linebreak [0] 
[8
\ast 
] , \linebreak [0] 
[9
\ast 
] , \linebreak [0] 
[
{:}
\ast 
] , \linebreak [0] 
[;
\ast 
] , \linebreak [0] 
[
{<}
\ast 
] , \linebreak [0] 
[
{=}
\ast 
] , \linebreak [0] 
[
{>}
\ast 
] , \linebreak [0] 
[?
\ast 
] , \linebreak [0] 
[@
\ast 
] , \linebreak [0] 
[A
\ast 
] , \linebreak [0] 
[B
\ast 
] , \linebreak [0] 
[C
\ast 
] , \linebreak [0] 
[D
\ast 
] , \linebreak [0] 
[E
\ast 
] , \linebreak [0] 
[F
\ast 
] , \linebreak [0] 
[G
\ast 
] , \linebreak [0] 
[H
\ast 
] , \linebreak [0] 
[I
\ast 
] , \linebreak [0] 
[J
\ast 
] , \linebreak [0] 
[K
\ast 
] , \linebreak [0] 
[L
\ast 
] , \linebreak [0] 
[M
\ast 
] , \linebreak [0] 
[N
\ast 
] , \linebreak [0] 
[O
\ast 
] , \linebreak [0] 
[P
\ast 
] , \linebreak [0] 
[Q
\ast 
] , \linebreak [0] 
[R
\ast 
] , \linebreak [0] 
[S
\ast 
] , \linebreak [0] 
[T
\ast 
] , \linebreak [0] 
[U
\ast 
] , \linebreak [0] 
[V
\ast 
] , \linebreak [0] 
[W
\ast 
] , \linebreak [0] 
[X
\ast 
] , \linebreak [0] 
[Y
\ast 
] , \linebreak [0] 
[Z
\ast 
] , \linebreak [0] 
[[
\ast 
] , \linebreak [0] 
[
\mbox {$\backslash $}
\ast 
] , \linebreak [0] 
[]
\ast 
] , \linebreak [0] 
[
{\char94}
\ast 
] , \linebreak [0] 
[
\_
\ast 
] , \linebreak [0] 
[
\mbox {`}
\ast 
] , \linebreak [0] 
[a
\ast 
] , \linebreak [0] 
[b
\ast 
] , \linebreak [0] 
[c
\ast 
] , \linebreak [0] 
[d
\ast 
] , \linebreak [0] 
[e
\ast 
] , \linebreak [0] 
[f
\ast 
] , \linebreak [0] 
[g
\ast 
] , \linebreak [0] 
[h
\ast 
] , \linebreak [0] 
[i
\ast 
] , \linebreak [0] 
[j
\ast 
] , \linebreak [0] 
[k
\ast 
] , \linebreak [0] 
[l
\ast 
] , \linebreak [0] 
[m
\ast 
] , \linebreak [0] 
[n
\ast 
] , \linebreak [0] 
[o
\ast 
] , \linebreak [0] 
[p
\ast 
] , \linebreak [0] 
[q
\ast 
] , \linebreak [0] 
[r
\ast 
] , \linebreak [0] 
[s
\ast 
] , \linebreak [0] 
[t
\ast 
] , \linebreak [0] 
[u
\ast 
] , \linebreak [0] 
[v
\ast 
] , \linebreak [0] 
[w
\ast 
] , \linebreak [0] 
[x
\ast 
] , \linebreak [0] 
[y
\ast 
] , \linebreak [0] 
[z
\ast 
] , \linebreak [0] 
[
\{
\ast 
] , \linebreak [0] 
[|
\ast 
] , \linebreak [0] 
[
\}
\ast 
] , \linebreak [0] 
[
\char126 
\ast 
] , \linebreak [0] 
[
\mathbf{Preassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
\mathbf{Postassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
[
\ast 
] , \linebreak [0] 
\ast 
] , \linebreak [0] 
[
\mathrm{priority} \,
\ast 
\, \mathrm{end}
] , \linebreak [0] 
[
newline\ 
\ast 
] , \linebreak [0] 
[
macro\ newline\ 
\ast 
] , \linebreak [0] 
[
MacroIndent(
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbin {\mbox {'}}
\ast 
] , \linebreak [0] 
[
\ast 
\mathbin {\mbox {`}}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[ 
\ast 
 (exp) 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
{}'
] , \linebreak [0] 
[R(
\ast 
)
] , \linebreak [0] 
[--R(
\ast 
)
] , \linebreak [0] 
[rec
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
 / 
\ast 
] , \linebreak [0] 
[
\ast 
 \cap 
\ast 
] , \linebreak [0] 
[
\ast 
[
\ast 
]
]
; 
\newline \mathbf {Preassociative} \newline 
[\cup 
\ast 
] , \linebreak [0] 
[
\ast 
 \mathrel{\cup} 
\ast 
] , \linebreak [0] 
[P(
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[\{
\ast 
\}
] , \linebreak [0] 
[StateExpand(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[extractSeries(
\ast 
)
] , \linebreak [0] 
[SetOfSeries(
\ast 
)
] , \linebreak [0] 
[--Macro(
\ast 
)
] , \linebreak [0] 
[ExpandList(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[**Macro(
\ast 
)
] , \linebreak [0] 
[++Macro(
\ast 
)
] , \linebreak [0] 
[<<Macro(
\ast 
)
] , \linebreak [0] 
[UB(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[LUB(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[BS(
\ast 
,
\ast 
)
] , \linebreak [0] 
[UStelescope(
\ast 
,
\ast 
)
] , \linebreak [0] 
[(
\ast 
)
] , \linebreak [0] 
[|r
\ast 
|
] , \linebreak [0] 
[Limit(
\ast 
,
\ast 
)
] , \linebreak [0] 
[Union(
\ast 
)
] , \linebreak [0] 
[IsOrderedPair(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[IsRelation(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[isFunction(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[IsSeries(
\ast 
,
\ast 
)
] , \linebreak [0] 
[IsNatural(
\ast 
,\ast
)
] , \linebreak [0] 
[OrderedPair(
\ast 
,
\ast 
)
] , \linebreak [0] 
[TypeNat(
\ast 
)
] , \linebreak [0] 
[TypeNat0(
\ast 
)
] , \linebreak [0] 
[TypeRational(
\ast 
)
] , \linebreak [0] 
[TypeRational0(
\ast 
)
] , \linebreak [0] 
[TypeSeries(
\ast 
,
\ast 
)
] , \linebreak [0] 
[Typeseries0(
\ast 
,
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[\{
\ast 
,
\ast 
\}
] , \linebreak [0] 
[\langle 
\ast 
,
\ast 
\rangle
] , \linebreak [0] 
[(-u
\ast 
)
] , \linebreak [0] 
[-_{f}
\ast 
] , \linebreak [0] 
[(--
\ast 
)
] , \linebreak [0] 
[1f/
\ast 
] , \linebreak [0] 
[1fny/
\ast 
] , \linebreak [0] 
[01//temp
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
 \mathrel{\in} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cdot 
\ast 
] , \linebreak [0] 
[
\ast 
\cdot_0 
\ast 
] , \linebreak [0] 
[(
\ast 
*
\ast 
)
] , \linebreak [0] 
[
\ast 
*_{f}
\ast 
] , \linebreak [0] 
[
\ast 
**
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
+ 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_1} 
\ast 
] , \linebreak [0] 
[
\ast 
- 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_1} 
\ast 
] , \linebreak [0] 
[(
\ast 
+
\ast 
)
] , \linebreak [0] 
[(
\ast 
-
\ast 
)
] , \linebreak [0] 
[
\ast 
+_{f}
\ast 
] , \linebreak [0] 
[
\ast 
-_{f}
\ast 
] , \linebreak [0] 
[
\ast 
++
\ast 
] , \linebreak [0] 
[R(
\ast 
) -- R(
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[|
\ast 
|
] , \linebreak [0] 
[if(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[Max(
\ast 
,
\ast 
)
] , \linebreak [0] 
[Max(
\ast 
,
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
 = 
\ast 
] , \linebreak [0] 
[
\ast 
 \neq 
\ast 
] , \linebreak [0] 
[
\ast 
 <= 
\ast 
] , \linebreak [0] 
[
\ast 
 < 
\ast 
] , \linebreak [0] 
[
\ast 
<_{f}
\ast 
] , \linebreak [0] 
[
\ast 
\leq_{f}
\ast 
] , \linebreak [0] 
[SF(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
 == 
\ast 
] , \linebreak [0] 
[
\ast 
 !!== 
\ast 
] , \linebreak [0] 
[
\ast 
 << 
\ast 
] , \linebreak [0] 
[
\ast 
 <<== 
\ast 
] , \linebreak [0] 
[
\ast 
<<test
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cup \{ 
\ast 
\}
] , \linebreak [0] 
[
\ast 
\cup 
\ast 
] , \linebreak [0] 
[
\ast 
\backslash \{ 
\ast 
\}
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel { \dot { . \, . } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { \dot { . \, . } } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { : \, : } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { {+} 2 \ast } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { : \, : }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { {+} 2 \ast }
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
,\linebreak [0] 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\stackrel {B}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {D}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {C}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {P}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\approx 
\ast 
] , \linebreak [0] 
[
\ast 
=
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {+}{\rightarrow }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t^*}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{r}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_t 
\ast 
] , \linebreak [0] 
[
\ast 
\subseteq_T 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{T}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{s}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in}^{\ast} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for}^{\ast} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_c 
\ast 
] , \linebreak [0] 
[
\ast 
< 
\ast 
] , \linebreak [0] 
[
\ast 
<' 
\ast 
] , \linebreak [0] 
[
\ast 
\le' 
\ast 
] , \linebreak [0] 
[
\ast 
= 
\ast 
] , \linebreak [0] 
[
\ast 
\neq 
\ast 
] , \linebreak [0] 
[
\ast 
{}^{var}
] , \linebreak [0] 
[
\ast 
\#^0
\ast 
] , \linebreak [0] 
[
\ast 
\#^1
\ast 
] , \linebreak [0] 
[
\ast 
\#^*
\ast 
] , \linebreak [0] 
[
\ast 
\!\mathrel{==}\! 
\ast 
] , \linebreak [0] 
[
\ast 
 \mathrel{\subseteq} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
{\neg }
\ast 
] , \linebreak [0] 
[\dot{\neg}\,(
\ast 
)n
] , \linebreak [0] 
[
\ast 
 \mathrel{\notin} 
\ast 
] , \linebreak [0] 
[
\ast 
 \mathrel{\neq} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\wedge 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\tilde{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\wedge_c 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\dot{\wedge}} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\vee 
\ast 
] , \linebreak [0] 
[
\ast 
\parallel 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\vee}} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
 \mathrel{\dot{\vee}} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\exists 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\forall 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\forall_{obj} 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\exists 
\ast 
\colon 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\ddot{\Rightarrow}} 
\ast 
] , \linebreak [0] 
[
\ast 
\Rightarrow 
\ast 
] , \linebreak [0] 
[
\ast 
\Leftrightarrow 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\dot{\Leftrightarrow}} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[ \{ ph \mathrel{\in} 
\ast 
\mid 
\ast 
\}
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
:
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{spy}
\ast 
] , \linebreak [0] 
[
\ast 
!
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\left\{\protect \begin {array}{l}
\ast 
\\
\ast 
\protect \end {array}\right.
]
; 
\newline \mathbf {Preassociative} \newline 
[
\lambda 
\ast 
.
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
. 
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
] , \linebreak [0] 
[
{\bf if} \ 
\ast 
\ {\bf then} \ 
\ast 
\ {\bf else} \ 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
= 
\ast 
\mathbf{\ in\ } 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
\mathrel{\ddot{=}} 
\ast 
\mathrel{\ in\ } 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\#
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
{} ^ { I }
] , \linebreak [0] 
[
\ast 
{} ^ { \rhd }
] , \linebreak [0] 
[
\ast 
{} ^ { V } 
] , \linebreak [0] 
[
\ast 
{} ^ { + } 
] , \linebreak [0] 
[
\ast 
{} ^ { - } 
] , \linebreak [0] 
[
\ast 
{} ^ { \ast } 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathop {\char64} 
\ast 
] , \linebreak [0] 
[
\ast 
\rhd 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\ast 
] , \linebreak [0] 
[
\ast 
\gg 
\ast 
] , \linebreak [0] 
[
\ast 
\unrhd 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\vdash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {i.e.} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\forall 
\ast 
\colon 
\ast 
] , \linebreak [0] 
[
\Pi 
\ast 
\colon 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel {\oplus} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
; 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\ proves\ 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbf{\ proof\ of\ } 
\ast 
: 
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: 
\ast 
\gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Last\ line \, 
\ast 
\gg 
\ast 
\,\Box
] , \linebreak [0] 
[
Line \, 
\ast 
: Premise \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: \mbox{Side-condition} \gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Arbitrary \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Local \gg 
\ast 
= 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Begin \, 
\ast 
 ; 
\ast 
 : End ; 
\ast 
] , \linebreak [0] 
[
Last\ block\ line \, 
\ast 
\gg 
\ast 
\,;
] , \linebreak [0] 
[
Arbitrary \gg 
\ast 
;
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{|} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\mathrm{,}}
\ast 
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\& 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\backslash \backslash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{linebreak[4]} 
\ast 
] , \linebreak [0] 
[
\ast 
\backslash \backslash 
\ast 
]
; 
]$
\end {flushleft}

\section{Pyk definitioner} \label{sec:pyk}

\begin{flushleft}
$
[<<testMacro(
\ast 
)
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
{<}
{<}testMacro(
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{})
\mbox{''}
]
\linebreak[4] 
[Tester1
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester1
\mbox{''}
]
\linebreak[4] 
[Tester2
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester2
\mbox{''}
]
\linebreak[4] 
[Tester3
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester3
\mbox{''}
]
\linebreak[4] 
[Tester4
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester4
\mbox{''}
]
\linebreak[4] 
[Tester5
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester5
\mbox{''}
]
\linebreak[4] 
[Tester6
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}tester6
\mbox{''}
]
\linebreak[4] 
[
\ast 
<<test
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}
{<}
{<}test
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[prove
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}prove
\mbox{''}
]
\linebreak[4] $
\end{flushleft}

\newpage

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item $
[prove
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}prove
\mbox{''}
]$ 

\item $
[Tester1
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester1
\mbox{''}
]$ 

\item $
[Tester2
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester2
\mbox{''}
]$ 

\item $
[Tester3
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester3
\mbox{''}
]$ 

\item $
[Tester4
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester4
\mbox{''}
]$ 

\item $
[Tester5
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester5
\mbox{''}
]$ 

\item $
[Tester6
\stackrel{
\mathrm{tex}
}{\rightarrow}
\mbox{``}Tester6
\mbox{''}
]$




\end{list}

\end{document}

