\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{GEG005$\wedge$1.p} Catalunya is not part of Paris






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\neg\,\mbox{po}@ \mbox{catalunya}@ \mbox{paris} )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG007$\wedge$1.p} Catalunya is not Paris






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\neg\,\mbox{eq}@ \mbox{catalunya}@ \mbox{paris} )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG009$\wedge$1.p} Something about Paris and Spain






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\exists z{:}\;\mbox{reg}{:}\;( \neg\,o@ z@ \mbox{paris}\mbox{ and }\neg\,\mbox{eq}@ z@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG024=1.p} Find sufficiently large and sufficiently close city (easy)






$\mbox{city}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{city\_type},\mbox{type})$

$d{:}\;( \mbox{city}\times \mbox{city} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{d\_type},\mbox{type})$

$\mbox{inh}{:}\;\mbox{city}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{inh\_type},\mbox{type})$

$\mbox{kiel}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{kiel\_type},\mbox{type})$

$\mbox{hamburg}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{hamburg\_type},\mbox{type})$

$\mbox{berlin}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{berlin\_type},\mbox{type})$

$\mbox{cologne}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{cologne\_type},\mbox{type})$

$\mbox{frankfurt}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{frankfurt\_type},\mbox{type})$

$\mbox{saarbruecken}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{saarbruecken\_type},\mbox{type})$

$\mbox{munich}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{munich\_type},\mbox{type})$

$( \forall x{:}\;\mbox{city},y{:}\;\mbox{city}{:}\;d(x,y) = d(y,x)\mbox{ and }\forall x{:}\;\mbox{city},y{:}\;\mbox{city},z{:}\;\mbox{city}{:}\;\mbox{\$lesseq}(d(x,z),\mbox{\$sum}(d(x,y),d(y,z)))\mbox{ and }\forall x{:}\;\mbox{city}{:}\;d(x,x) = 0\mbox{ and }d(\mbox{berlin},\mbox{munich}) = 510\mbox{ and }d(\mbox{berlin},\mbox{cologne}) = 480\mbox{ and }d(\mbox{berlin},\mbox{frankfurt}) = 420\mbox{ and }d(\mbox{saarbruecken},\mbox{frankfurt}) = 160\mbox{ and }d(\mbox{saarbruecken},\mbox{cologne}) = 190\mbox{ and }d(\mbox{hamburg},\mbox{cologne}) = 360\mbox{ and }d(\mbox{hamburg},\mbox{frankfurt}) = 390\mbox{ and }d(\mbox{cologne},\mbox{frankfurt}) = 150\mbox{ and }d(\mbox{hamburg},\mbox{kiel}) = 90\mbox{ and }d(\mbox{hamburg},\mbox{berlin}) = 250\mbox{ and }d(\mbox{munich},\mbox{frankfurt}) = 300\mbox{ and }d(\mbox{munich},\mbox{saarbruecken}) = 360\mbox{ and }\mbox{inh}(\mbox{berlin}) = 3442675\mbox{ and }\mbox{inh}(\mbox{hamburg}) = 1774224\mbox{ and }\mbox{inh}(\mbox{munich}) = 1330440\mbox{ and }\mbox{inh}(\mbox{cologne}) = 998105\mbox{ and }\mbox{inh}(\mbox{frankfurt}) = 671927\mbox{ and }\mbox{inh}(\mbox{saarbruecken}) = 175810\mbox{ and }\mbox{inh}(\mbox{kiel}) = 238281 ) \ \Rightarrow \ \exists x{:}\;\mbox{city}{:}\;( \mbox{\$lesseq}(d(\mbox{kiel},x),100)\mbox{ and }\mbox{\$lesseq}(1000000,\mbox{inh}(x)) )\qquad\mbox{tff}(\mbox{exists\_big\_city\_distance}_1,\mbox{conjecture})$

\medskip\textbf{GEG020$\wedge$1.p} A place that overlaps with Paris or Catalunya






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\forall z{:}\;\mbox{reg}{:}\;( ( o@ z@ \mbox{paris}\mbox{ or }o@ z@ \mbox{catalunya} ) \ \Rightarrow \ ( o@ z@ \mbox{spain}\mbox{ or }o@ z@ \mbox{france} ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG006$\wedge$1.p} Catalunya is in Spain and Paris is in France






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( o@ \mbox{catalunya}@ \mbox{spain}\mbox{ and }o@ \mbox{france}@ \mbox{paris} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG019$\wedge$1.p} If Paris and Catalunya overlap, then so do Spain and France






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\forall z{:}\;\mbox{reg}{:}\;( ( o@ z@ \mbox{paris}\mbox{ and }o@ z@ \mbox{catalunya} ) \ \Rightarrow \ ( o@ z@ \mbox{spain}\mbox{ and }o@ z@ \mbox{france} ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG022=1.p} Estimate distance between cities (two steps)






$\mbox{city}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{city\_type},\mbox{type})$

$d{:}\;( \mbox{city}\times \mbox{city} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{d\_type},\mbox{type})$

$\mbox{kiel}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{kiel\_type},\mbox{type})$

$\mbox{hamburg}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{hamburg\_type},\mbox{type})$

$\mbox{berlin}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{berlin\_type},\mbox{type})$

$\mbox{cologne}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{cologne\_type},\mbox{type})$

$\mbox{frankfurt}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{frankfurt\_type},\mbox{type})$

$\mbox{saarbruecken}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{saarbruecken\_type},\mbox{type})$

$\mbox{munich}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{munich\_type},\mbox{type})$

$( \forall x{:}\;\mbox{city},y{:}\;\mbox{city}{:}\;d(x,y) = d(y,x)\mbox{ and }\forall x{:}\;\mbox{city},y{:}\;\mbox{city},z{:}\;\mbox{city}{:}\;\mbox{\$lesseq}(d(x,z),\mbox{\$sum}(d(x,y),d(y,z)))\mbox{ and }\forall x{:}\;\mbox{city}{:}\;d(x,x) = 0\mbox{ and }d(\mbox{berlin},\mbox{munich}) = 510\mbox{ and }d(\mbox{berlin},\mbox{cologne}) = 480\mbox{ and }d(\mbox{berlin},\mbox{frankfurt}) = 420\mbox{ and }d(\mbox{saarbruecken},\mbox{frankfurt}) = 160\mbox{ and }d(\mbox{saarbruecken},\mbox{cologne}) = 190\mbox{ and }d(\mbox{hamburg},\mbox{cologne}) = 360\mbox{ and }d(\mbox{hamburg},\mbox{frankfurt}) = 390\mbox{ and }d(\mbox{cologne},\mbox{frankfurt}) = 150\mbox{ and }d(\mbox{hamburg},\mbox{kiel}) = 90\mbox{ and }d(\mbox{hamburg},\mbox{berlin}) = 250\mbox{ and }d(\mbox{munich},\mbox{frankfurt}) = 300\mbox{ and }d(\mbox{munich},\mbox{saarbruecken}) = 360 ) \ \Rightarrow \ \mbox{\$lesseq}(d(\mbox{hamburg},\mbox{munich}),700)\qquad\mbox{tff}(\mbox{city\_distance}_2,\mbox{conjecture})$

\medskip\textbf{GEG011$\wedge$1.p} Something about France, Spain, Paris, Catalunya






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\forall z{:}\;\mbox{reg}{:}\;( ( \mbox{ntpp}@ \mbox{france}@ z\mbox{ and }\mbox{ntpp}@ \mbox{spain}@ z ) \ \Rightarrow \ ( \mbox{pp}@ \mbox{paris}@ z\mbox{ and }\mbox{pp}@ \mbox{catalunya}@ z ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG025=1.p} Find sufficiently large and sufficiently close city (medium)






$\mbox{city}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{city\_type},\mbox{type})$

$d{:}\;( \mbox{city}\times \mbox{city} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{d\_type},\mbox{type})$

$\mbox{inh}{:}\;\mbox{city}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{inh\_type},\mbox{type})$

$\mbox{kiel}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{kiel\_type},\mbox{type})$

$\mbox{hamburg}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{hamburg\_type},\mbox{type})$

$\mbox{berlin}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{berlin\_type},\mbox{type})$

$\mbox{cologne}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{cologne\_type},\mbox{type})$

$\mbox{frankfurt}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{frankfurt\_type},\mbox{type})$

$\mbox{saarbruecken}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{saarbruecken\_type},\mbox{type})$

$\mbox{munich}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{munich\_type},\mbox{type})$

$( \forall x{:}\;\mbox{city},y{:}\;\mbox{city}{:}\;d(x,y) = d(y,x)\mbox{ and }\forall x{:}\;\mbox{city},y{:}\;\mbox{city},z{:}\;\mbox{city}{:}\;\mbox{\$lesseq}(d(x,z),\mbox{\$sum}(d(x,y),d(y,z)))\mbox{ and }\forall x{:}\;\mbox{city}{:}\;d(x,x) = 0\mbox{ and }d(\mbox{berlin},\mbox{munich}) = 510\mbox{ and }d(\mbox{berlin},\mbox{cologne}) = 480\mbox{ and }d(\mbox{berlin},\mbox{frankfurt}) = 420\mbox{ and }d(\mbox{saarbruecken},\mbox{frankfurt}) = 160\mbox{ and }d(\mbox{saarbruecken},\mbox{cologne}) = 190\mbox{ and }d(\mbox{hamburg},\mbox{cologne}) = 360\mbox{ and }d(\mbox{hamburg},\mbox{frankfurt}) = 390\mbox{ and }d(\mbox{cologne},\mbox{frankfurt}) = 150\mbox{ and }d(\mbox{hamburg},\mbox{kiel}) = 90\mbox{ and }d(\mbox{hamburg},\mbox{berlin}) = 250\mbox{ and }d(\mbox{munich},\mbox{frankfurt}) = 300\mbox{ and }d(\mbox{munich},\mbox{saarbruecken}) = 360\mbox{ and }\mbox{inh}(\mbox{berlin}) = 3442675\mbox{ and }\mbox{inh}(\mbox{hamburg}) = 1774224\mbox{ and }\mbox{inh}(\mbox{munich}) = 1330440\mbox{ and }\mbox{inh}(\mbox{cologne}) = 998105\mbox{ and }\mbox{inh}(\mbox{frankfurt}) = 671927\mbox{ and }\mbox{inh}(\mbox{saarbruecken}) = 175810\mbox{ and }\mbox{inh}(\mbox{kiel}) = 238281 ) \ \Rightarrow \ \exists x{:}\;\mbox{city}{:}\;( \mbox{\$lesseq}(d(\mbox{saarbruecken},x),600)\mbox{ and }\mbox{\$lesseq}(3000000,\mbox{inh}(x)) )\qquad\mbox{tff}(\mbox{exists\_big\_city\_distance}_2,\mbox{conjecture})$

\medskip\textbf{GEG013$\wedge$1.p} Unequal regions






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\exists z{:}\;\mbox{reg},y{:}\;\mbox{reg}{:}\;\neg\,\mbox{eq}@ z@ y )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG016$\wedge$1.p} Places in Spain and France do not overlap






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;\forall z{:}\;\mbox{reg},y{:}\;\mbox{reg}{:}\;( ( p@ z@ \mbox{spain}\mbox{ and }p@ y@ \mbox{france} ) \ \Rightarrow \ \neg\,o@ z@ y ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG012$\wedge$1.p} Something about France, Spain, Paris, Catalunya






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\forall x{:}\;\mbox{reg}{:}\;( ( \mbox{ntpp}@ \mbox{france}@ x\mbox{ and }\mbox{ntpp}@ \mbox{spain}@ x ) \ \Rightarrow \ ( \mbox{ntpp}@ \mbox{paris}@ x\mbox{ and }\mbox{ntpp}@ \mbox{catalunya}@ x ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG015$\wedge$1.p} Two unequal regions in France






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\exists z{:}\;\mbox{reg},y{:}\;\mbox{reg}{:}\;( \neg\,\mbox{eq}@ z@ y\mbox{ and }p@ z@ \mbox{france}\mbox{ and }p@ y@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG018$\wedge$1.p} Some places are non-tangential proper parts






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;\neg\,\exists z{:}\;\mbox{reg}{:}\;\forall y{:}\;\mbox{reg}{:}\;( \mbox{ntpp}@ z@ y ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG004$\wedge$1.p} Is it commonly known that places are disconnected?

We here express that some spatial relations about Catalunya, 
 France, Spain, and Paris are commonly known (modality box\_fool), 
 while others are known only to person Bob (modality box\_bob). We 
 ask whether it is commonly known that Catalunya and Paris and 
 Spain and Paris are disconnected. (This is not the case).




$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{dc}@ \mbox{catalunya}@ \mbox{paris}\mbox{ and }\mbox{dc}@ \mbox{spain}@ \mbox{paris} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG010$\wedge$1.p} Catalunya and Paris are not in the same place






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\forall z{:}\;\mbox{reg}{:}\;( ( p@ z@ \mbox{catalunya} ) \ \Rightarrow \ \neg\,p@ z@ \mbox{paris} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG003$\wedge$1.p} Bob knows Catalunya and Paris and Spain and Paris are disconnected

We here express that some spatial relations about Catalunya, 
 France, Spain, and Paris are commonly known (modality box\_fool), 
 while others are known only to person Bob (modality box\_bob). We 
 prove that Bob knows that Catalunya and Paris and Spain and Paris 
 are disconnected.




$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{dc}@ \mbox{catalunya}@ \mbox{paris}\mbox{ and }\mbox{dc}@ \mbox{spain}@ \mbox{paris} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG023=1.p} Estimate distance between cities (three steps)






$\mbox{city}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{city\_type},\mbox{type})$

$d{:}\;( \mbox{city}\times \mbox{city} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{d\_type},\mbox{type})$

$\mbox{kiel}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{kiel\_type},\mbox{type})$

$\mbox{hamburg}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{hamburg\_type},\mbox{type})$

$\mbox{berlin}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{berlin\_type},\mbox{type})$

$\mbox{cologne}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{cologne\_type},\mbox{type})$

$\mbox{frankfurt}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{frankfurt\_type},\mbox{type})$

$\mbox{saarbruecken}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{saarbruecken\_type},\mbox{type})$

$\mbox{munich}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{munich\_type},\mbox{type})$

$( \forall x{:}\;\mbox{city},y{:}\;\mbox{city}{:}\;d(x,y) = d(y,x)\mbox{ and }\forall x{:}\;\mbox{city},y{:}\;\mbox{city},z{:}\;\mbox{city}{:}\;\mbox{\$lesseq}(d(x,z),\mbox{\$sum}(d(x,y),d(y,z)))\mbox{ and }\forall x{:}\;\mbox{city}{:}\;d(x,x) = 0\mbox{ and }d(\mbox{berlin},\mbox{munich}) = 510\mbox{ and }d(\mbox{berlin},\mbox{cologne}) = 480\mbox{ and }d(\mbox{berlin},\mbox{frankfurt}) = 420\mbox{ and }d(\mbox{saarbruecken},\mbox{frankfurt}) = 160\mbox{ and }d(\mbox{saarbruecken},\mbox{cologne}) = 190\mbox{ and }d(\mbox{hamburg},\mbox{cologne}) = 360\mbox{ and }d(\mbox{hamburg},\mbox{frankfurt}) = 390\mbox{ and }d(\mbox{cologne},\mbox{frankfurt}) = 150\mbox{ and }d(\mbox{hamburg},\mbox{kiel}) = 90\mbox{ and }d(\mbox{hamburg},\mbox{berlin}) = 250\mbox{ and }d(\mbox{munich},\mbox{frankfurt}) = 300\mbox{ and }d(\mbox{munich},\mbox{saarbruecken}) = 360 ) \ \Rightarrow \ \mbox{\$lesseq}(d(\mbox{kiel},\mbox{saarbruecken}),640)\qquad\mbox{tff}(\mbox{city\_distance}_3,\mbox{conjecture})$

\medskip\textbf{GEG014$\wedge$1.p} Two unequal regions in France






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;\exists z{:}\;\mbox{reg},y{:}\;\mbox{reg}{:}\;( \neg\,\mbox{eq}@ z@ y\mbox{ and }o@ z@ \mbox{france}\mbox{ and }o@ z@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG021=1.p} Estimate distance between cities (one step)






$\mbox{city}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{city\_type},\mbox{type})$

$d{:}\;( \mbox{city}\times \mbox{city} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{d\_type},\mbox{type})$

$\mbox{kiel}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{kiel\_type},\mbox{type})$

$\mbox{hamburg}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{hamburg\_type},\mbox{type})$

$\mbox{berlin}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{berlin\_type},\mbox{type})$

$\mbox{cologne}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{cologne\_type},\mbox{type})$

$\mbox{frankfurt}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{frankfurt\_type},\mbox{type})$

$\mbox{saarbruecken}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{saarbruecken\_type},\mbox{type})$

$\mbox{munich}{:}\;\mbox{city}\qquad\mbox{tff}(\mbox{munich\_type},\mbox{type})$

$( \forall x{:}\;\mbox{city},y{:}\;\mbox{city}{:}\;d(x,y) = d(y,x)\mbox{ and }\forall x{:}\;\mbox{city},y{:}\;\mbox{city},z{:}\;\mbox{city}{:}\;\mbox{\$lesseq}(d(x,z),\mbox{\$sum}(d(x,y),d(y,z)))\mbox{ and }\forall x{:}\;\mbox{city}{:}\;d(x,x) = 0\mbox{ and }d(\mbox{berlin},\mbox{munich}) = 510\mbox{ and }d(\mbox{berlin},\mbox{cologne}) = 480\mbox{ and }d(\mbox{berlin},\mbox{frankfurt}) = 420\mbox{ and }d(\mbox{saarbruecken},\mbox{frankfurt}) = 160\mbox{ and }d(\mbox{saarbruecken},\mbox{cologne}) = 190\mbox{ and }d(\mbox{hamburg},\mbox{cologne}) = 360\mbox{ and }d(\mbox{hamburg},\mbox{frankfurt}) = 390\mbox{ and }d(\mbox{cologne},\mbox{frankfurt}) = 150\mbox{ and }d(\mbox{hamburg},\mbox{kiel}) = 90\mbox{ and }d(\mbox{hamburg},\mbox{berlin}) = 250\mbox{ and }d(\mbox{munich},\mbox{frankfurt}) = 300\mbox{ and }d(\mbox{munich},\mbox{saarbruecken}) = 360 ) \ \Rightarrow \ \mbox{\$lesseq}(d(\mbox{cologne},\mbox{berlin}),500)\qquad\mbox{tff}(\mbox{city\_distance}_1,\mbox{conjecture})$

\medskip\textbf{GEG002$\wedge$1.p} Catalunya and Paris, and Spain and Paris, are disconnected

The assumptions express that Catalunya is a border region of 
 Spain, Spain and France are two different countries sharing a 
 common border, and Paris is a proper part of France. The 
 conjecture is that Catalunya and Paris are disconnected as well 
 as Spain and Paris.




$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$\mbox{tpp}@ \mbox{catalunya}@ \mbox{spain}\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{ec}@ \mbox{spain}@ \mbox{france}\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{ntpp}@ \mbox{paris}@ \mbox{france}\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{dc}@ \mbox{catalunya}@ \mbox{paris}\mbox{ and }\mbox{dc}@ \mbox{spain}@ \mbox{paris}\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip\textbf{GEG008$\wedge$1.p} If Catalunya is Paris then France is Spain






$\mbox{include}(\mbox{'Axioms/LCL013\string^0.ax'})$

$\mbox{include}(\mbox{'Axioms/LCL014\string^0.ax'})$

$\mbox{catalunya}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{catalunya},\mbox{type})$

$\mbox{france}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{france},\mbox{type})$

$\mbox{spain}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{spain},\mbox{type})$

$\mbox{paris}{:}\;\mbox{reg}\qquad\mbox{thf}(\mbox{paris},\mbox{type})$

$a{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(a,\mbox{type})$

$\mbox{fool}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{fool},\mbox{type})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ a ) )\qquad\mbox{thf}(\mbox{t\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda a{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ a )@ ( \mbox{mbox}@ \mbox{fool}@ ( \mbox{mbox}@ \mbox{fool}@ a ) ) ) )\qquad\mbox{thf}(\mbox{k\_axiom\_for\_fool},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mforall\_prop}@ \lambda \mbox{phi}{:}\;\mbox{\$i}\to \mbox{\$o}{:}\;( \mbox{mimplies}@ ( \mbox{mbox}@ \mbox{fool}@ \mbox{phi} )@ ( \mbox{mbox}@ a@ \mbox{phi} ) ) )\qquad\mbox{thf}(\mbox{i\_axiom\_for\_fool\_a},\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{tpp}@ \mbox{catalunya}@ \mbox{spain} ) )\qquad\mbox{thf}(\mbox{ax}_1,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ \mbox{fool}@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ec}@ \mbox{spain}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_2,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( \mbox{ntpp}@ \mbox{paris}@ \mbox{france} ) )\qquad\mbox{thf}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{mvalid}@ ( \mbox{mbox}@ a@ \lambda x{:}\;\mbox{\$i}{:}\;( ( \mbox{eq}@ \mbox{catalunya}@ \mbox{paris} ) \ \Rightarrow \ ( o@ \mbox{france}@ \mbox{spain} ) ) )\qquad\mbox{thf}(\mbox{con},\mbox{conjecture})$

\medskip
\end{document}