\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 frozen}

\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{frozen}$}}

\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 
H1
\newline Metageneralization
\linebreak [0]\ \hskip0em plus2.0em{}over
\linebreak [0]\ \hskip0em plus2.0em{}metavariable
\linebreak [0]\ \hskip0em plus2.0em{}that
\linebreak [0]\ \hskip0em plus2.0em{}occurs
\linebreak [0]\ \hskip0em plus2.0em{}free
\linebreak [0]\ \hskip0em plus2.0em{}in
\linebreak [0]\ \hskip0em plus2.0em{}some
\linebreak [0]\ \hskip0em plus2.0em{}premise
{:}
\newline 
\forall \underline{
\mathsf {a}}
\colon 
\forall \underline{\underline{
\mathsf {a}}}
\colon 
\forall \underline{\underline{
\mathsf {b}}}
\colon 
Neg
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{\underline{
\mathsf {a}}}
\mathop {\char64} \underline{\underline{
\mathsf {b}}}
\mathop {\char64} 
\mbox{frozen}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\Rightarrow \underline{
\mathsf {a}}
{} ^ { \rhd }
{} ^ { \rhd }
; 
\forall \underline{\underline{
\mathsf {a}}}
\colon 
Repetition
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{\underline{
\mathsf {a}}}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
{} ^ { \rhd }
; 
\forall \underline{\underline{
\mathsf {a}}}
\colon 
\forall \underline{\underline{
\mathsf {b}}}
\colon 
\forall \underline{\underline{
\mathsf {c}}}
\colon 
H0b
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{\underline{
\mathsf {a}}}
\mathop {\char64} \underline{\underline{
\mathsf {b}}}
\mathop {\char64} \underline{\underline{
\mathsf {c}}}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }\underline{
\mathsf {a}}
\mathop {\char64} \underline{
\mathsf {a}}
{} ^ { \rhd }
{} ^ { \rhd }
; 
\forall \underline{\underline{
\mathsf {a}}}
\colon 
\forall \underline{\underline{
\mathsf {b}}}
\colon 
A1'
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{\underline{
\mathsf {a}}}
\mathop {\char64} \underline{\underline{
\mathsf {b}}}
\mathop {\char64} 
{\neg }
{\neg }\underline{
\mathsf {a}}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
; 
\forall \underline{\underline{
\mathsf {a}}}
\colon 
\forall \underline{\underline{
\mathsf {b}}}
\colon 
\forall \underline{\underline{
\mathsf {c}}}
\colon 
H0a
{} ^ { I }
{} ^ { \rhd }
{} ^ { \ast } 
{} ^ { \rhd }
\mathop {\char64} \underline{\underline{
\mathsf {a}}}
\mathop {\char64} \underline{\underline{
\mathsf {b}}}
\mathop {\char64} \underline{\underline{
\mathsf {c}}}
\mathop {\char64} 
{\neg }
{\neg }\underline{
\mathsf {a}}
\mathop {\char64} 
{\neg }\underline{
\mathsf {a}}
\Rightarrow 
{\neg }
{\neg }\underline{
\mathsf {a}}
\mathop {\char64} \underline{
\mathsf {a}}
{} ^ { \rhd }
{} ^ { \rhd }$

\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-26.UTC:09:52:11.033905} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{MJD-53912.TAI:09:52:44.033905} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{LGT-4658032364033905e-6}
}

\end{document}

