\documentclass [fleqn]{article}

\setlength {\overfullrule }{1mm}

\usepackage{latexsym}

\setlength{\parindent}{0em}

\setlength{\parskip}{1ex}

\usepackage{graphicx}

\usepackage[dvipdfm=true]{hyperref}

\hypersetup{pdfpagemode=none}

\hypersetup{pdfstartpage=1}

\hypersetup{pdfstartview=FitBH}

\hypersetup{pdfpagescrop={120 130 490 730}}

\hypersetup{pdftitle=Logiweb diagnose of pok}

\hypersetup{colorlinks=true}

\everymath{\rm}

\begin {document}\raggedright

\makebox [0mm][l]{\makebox [\linewidth ][r]{\includegraphics [0mm,18.5mm][16.5mm,19mm]{/home/disk07/grue/logiweb/20060417/html/logiweb/doc/logiweb.eps}}}%
{\bf {\Large Logiweb diagnose of $\rm 
\mbox{pok}$}}

\vspace {12.5mm}

\href {../index.html}{Up}
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/browser/diagnose/index.html}{Help}


$Error
\linebreak [0]\ \hskip0em plus2.0em{}in
\linebreak [0]\ \hskip0em plus2.0em{}proof
\linebreak [0]\ \hskip0em plus2.0em{}of
\newline 
Prop\ 3.2i
\newline Unknown
\linebreak [0]\ \hskip0em plus2.0em{}sequent
\linebreak [0]\ \hskip0em plus2.0em{}operator
{:}
\newline 
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$\underline{
\mathsf {a}}
,\linebreak [0] \underline{
\mathsf {b}}
,\linebreak [0] \underline{
\mathsf {c}}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$Begin
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
,\linebreak [0] \underline{
\mathsf {b}}
,\linebreak [0] \underline{
\mathsf {c}}
$\hfill \makebox [0mm][l]{\quad ;}}
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
Prop\ 3.2e
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\gg 
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
; Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
Prop\ 3.2h
\gg 
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
Prop\ 3.2h
\gg 
$%
\leftskip=1em%
$\underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
; Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
S1
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {a}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\gg 
$%
\leftskip=1em%
$\underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
; Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
Prop\ 3.2b
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
\gg 
$%
\leftskip=1em%
$\underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
; 
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$
Prop\ 3.2c
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
\rhd 
$%
\leftskip=1em%
$\underline{
\mathsf {b}}
+ \underline{
\mathsf {c}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
$%
\leftskip=1em%
$\underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_g \else
\if \relax \csname lgwellg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellg \fi 
$:}$Block {}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$End
$\hfill \makebox [0mm][l]{\quad ;}}Unification
\linebreak [0]\ \hskip0em plus2.0em{}failed
\newline 
Ded
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_g \else
\if \relax \csname lgwellg\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellg {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellg \fi 
\gg \underline{
\mathsf {a}}
= \underline{
\mathsf {b}}
\vdash \underline{
\mathsf {c}}
+ \underline{
\mathsf {a}}
= \underline{
\mathsf {c}}
+ \underline{
\mathsf {b}}$

\vspace{2ex}

{\em \href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/compiler/index.html}{The pyk compiler},
version 0.grue.20060417+
by
\href {http://www.diku.dk/~grue/index.html}{Klaus Grue}\\
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{GRD-2006-06-21.UTC:11:30:14.300977} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{MJD-53907.TAI:11:30:47.300977} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{LGT-4657606247300977e-6}
}

\end{document}

