\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{REL001+1.ax} Dedkind and two modular laws






$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 )\vee ( x_0\wedge x_2;x_1^\smallsmile );( x_1\wedge x_0^\smallsmile;x_2 ) = ( x_0\wedge x_2;x_1^\smallsmile );( x_1\wedge x_0^\smallsmile;x_2 )\qquad\mbox{fof}(\mbox{dedekind\_law},\mbox{axiom})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 )\vee ( x_0;( x_1\wedge x_0^\smallsmile;x_2 )\wedge x_2 ) = x_0;( x_1\wedge x_0^\smallsmile;x_2 )\wedge x_2\qquad\mbox{fof}(\mbox{modular\_law}_1,\mbox{axiom})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 )\vee ( ( x_0\wedge x_2;x_1^\smallsmile );x_1\wedge x_2 ) = ( x_0\wedge x_2;x_1^\smallsmile );x_1\wedge x_2\qquad\mbox{fof}(\mbox{modular\_law}_2,\mbox{axiom})$

\medskip\textbf{REL001-1.ax} Dedkind and two modular laws






$( a;b\wedge c )\vee ( a\wedge c;b^\smallsmile );( b\wedge a^\smallsmile;c ) = ( a\wedge c;b^\smallsmile );( b\wedge a^\smallsmile;c )\qquad\mbox{cnf}(\mbox{dedekind\_law}_{14},\mbox{axiom})$

$( a;b\wedge c )\vee ( a;( b\wedge a^\smallsmile;c )\wedge c ) = a;( b\wedge a^\smallsmile;c )\wedge c\qquad\mbox{cnf}(\mbox{modular\_law\_1}_{15},\mbox{axiom})$

$( a;b\wedge c )\vee ( ( a\wedge c;b^\smallsmile );b\wedge c ) = ( a\wedge c;b^\smallsmile );b\wedge c\qquad\mbox{cnf}(\mbox{modular\_law\_2}_{16},\mbox{axiom})$

\medskip\textbf{REL001-0.ax} Relation algebra






$a\vee b = b\vee a\qquad\mbox{cnf}(\mbox{maddux1\_join\_commutativity}_1,\mbox{axiom})$

$a\vee ( b\vee c ) = ( a\vee b )\vee c\qquad\mbox{cnf}(\mbox{maddux2\_join\_associativity}_2,\mbox{axiom})$

$a = ( a'\vee b' )'\vee ( a'\vee b )'\qquad\mbox{cnf}(\mbox{maddux3\_a\_kind\_of\_de\_Morgan}_3,\mbox{axiom})$

$a\wedge b = ( a'\vee b' )'\qquad\mbox{cnf}(\mbox{maddux4\_definiton\_of\_meet}_4,\mbox{axiom})$

$a;( b;c ) = ( a;b );c\qquad\mbox{cnf}(\mbox{composition\_associativity}_5,\mbox{axiom})$

$a;1 = a\qquad\mbox{cnf}(\mbox{composition\_identity}_6,\mbox{axiom})$

$( a\vee b );c = a;c\vee b;c\qquad\mbox{cnf}(\mbox{composition\_distributivity}_7,\mbox{axiom})$

$( a^\smallsmile )^\smallsmile = a\qquad\mbox{cnf}(\mbox{converse\_idempotence}_8,\mbox{axiom})$

$( a\vee b )^\smallsmile = a^\smallsmile\vee b^\smallsmile\qquad\mbox{cnf}(\mbox{converse\_additivity}_9,\mbox{axiom})$

$( a;b )^\smallsmile = b^\smallsmile;a^\smallsmile\qquad\mbox{cnf}(\mbox{converse\_multiplicativity}_{10},\mbox{axiom})$

$a^\smallsmile;( a;b )'\vee b' = b'\qquad\mbox{cnf}(\mbox{converse\_cancellativity}_{11},\mbox{axiom})$

$\top  = a\vee a'\qquad\mbox{cnf}(\mbox{def\_top}_{12},\mbox{axiom})$

$0 = a\wedge a'\qquad\mbox{cnf}(\mbox{def\_zero}_{13},\mbox{axiom})$

\medskip\textbf{REL001+0.ax} Relation Algebra






$\forall x_0,x_1{:}\;x_0\vee x_1 = x_1\vee x_0\qquad\mbox{fof}(\mbox{maddux1\_join\_commutativity},\mbox{axiom})$

$\forall x_0,x_1,x_2{:}\;x_0\vee ( x_1\vee x_2 ) = ( x_0\vee x_1 )\vee x_2\qquad\mbox{fof}(\mbox{maddux2\_join\_associativity},\mbox{axiom})$

$\forall x_0,x_1{:}\;x_0 = ( x_0'\vee x_1' )'\vee ( x_0'\vee x_1 )'\qquad\mbox{fof}(\mbox{maddux3\_a\_kind\_of\_de\_Morgan},\mbox{axiom})$

$\forall x_0,x_1{:}\;x_0\wedge x_1 = ( x_0'\vee x_1' )'\qquad\mbox{fof}(\mbox{maddux4\_definiton\_of\_meet},\mbox{axiom})$

$\forall x_0,x_1,x_2{:}\;x_0;( x_1;x_2 ) = ( x_0;x_1 );x_2\qquad\mbox{fof}(\mbox{composition\_associativity},\mbox{axiom})$

$\forall x_0{:}\;x_0;1 = x_0\qquad\mbox{fof}(\mbox{composition\_identity},\mbox{axiom})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee x_1 );x_2 = x_0;x_2\vee x_1;x_2\qquad\mbox{fof}(\mbox{composition\_distributivity},\mbox{axiom})$

$\forall x_0{:}\;( x_0^\smallsmile )^\smallsmile = x_0\qquad\mbox{fof}(\mbox{converse\_idempotence},\mbox{axiom})$

$\forall x_0,x_1{:}\;( x_0\vee x_1 )^\smallsmile = x_0^\smallsmile\vee x_1^\smallsmile\qquad\mbox{fof}(\mbox{converse\_additivity},\mbox{axiom})$

$\forall x_0,x_1{:}\;( x_0;x_1 )^\smallsmile = x_1^\smallsmile;x_0^\smallsmile\qquad\mbox{fof}(\mbox{converse\_multiplicativity},\mbox{axiom})$

$\forall x_0,x_1{:}\;x_0^\smallsmile;( x_0;x_1 )'\vee x_1' = x_1'\qquad\mbox{fof}(\mbox{converse\_cancellativity},\mbox{axiom})$

$\forall x_0{:}\;\top  = x_0\vee x_0'\qquad\mbox{fof}(\mbox{def\_top},\mbox{axiom})$

$\forall x_0{:}\;0 = x_0\wedge x_0'\qquad\mbox{fof}(\mbox{def\_zero},\mbox{axiom})$

\medskip\textbf{REL029-1.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL040+2.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ ( x_0;( x_1\wedge x_2 )\vee ( x_0;x_1\wedge x_0;x_2 ) = x_0;x_1\wedge x_0;x_2\mbox{ and }( x_0;x_1\wedge x_0;x_2 )\vee x_0;( x_1\wedge x_2 ) = x_0;( x_1\wedge x_2 ) ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL026-3.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\top \wedge \mbox{sk}_2\ne \mbox{sk}_1;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL042+1.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( \forall x_1{:}\;x_0;x_1\wedge x_0;x_1' = 0 \ \Rightarrow \ x_0^\smallsmile;x_0\vee 1 = 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL030-4.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' ) = \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3' )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3'\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL010-2.p} Schroeder equivalence (first implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3 = 0\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3\ne 0\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL021+1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge 1 );x_1\vee ( x_0\wedge x_1 ) = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL019+1.p} Vectors are closed under meet

If x and y are vectors then x meet y is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( ( x_0;\top  = x_0\mbox{ and }x_1;\top  = x_1 ) \ \Rightarrow \ ( x_0\wedge x_1 );\top  = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL029-2.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\vee ( \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 ) = \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL017-3.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3\ne ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL016+1.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;x_1\wedge ( x_0;x_2 )' = x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL011-1.p} Schroeder equivalence (second implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile;\mbox{sk}_3 = 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2;\mbox{sk}_1\wedge \mbox{sk}_3\ne 0\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL016-2.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' ) = \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' \ \Rightarrow \ ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\ne \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL021-2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 )\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL028-2.p} For subidentities meet and composition coincide






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{19},\mbox{negated\_conjecture})$

\medskip\textbf{REL053+1.p} Relation Algebra






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

\medskip\textbf{REL009-2.p} Sequential composition is isotone in both arguments






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_3\vee \mbox{sk}_2;\mbox{sk}_3 = \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ \mbox{sk}_3;\mbox{sk}_1\vee \mbox{sk}_3;\mbox{sk}_2\ne \mbox{sk}_3;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL008-3.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL050+1.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0;\top  )' = ( x_0;\top  )';\top \qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL030+4.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( x_0;x_1\wedge x_2' )\vee ( x_0;x_1\wedge ( x_0;x_2 )' ) = x_0;x_1\wedge ( x_0;x_2 )'\mbox{ and }( x_0;x_1\wedge ( x_0;x_2 )' )\vee ( x_0;x_1\wedge x_2' ) = x_0;x_1\wedge x_2' ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL002+1.p} There is a (unique) greatest element, namely x + x'






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;x_0\vee \top  = \top \qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL014+1.p} One is neutral element






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0;1 = x_0\mbox{ and }1;x_0 = x_0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL011-2.p} Schroeder equivalence (second implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile;\mbox{sk}_3 = 0\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2;\mbox{sk}_1\wedge \mbox{sk}_3\ne 0\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL037+2.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL010+2.p} Schroeder equivalence (first implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 = 0 \ \Rightarrow \ x_1\wedge x_0^\smallsmile;x_2 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL033+4.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( ( x_0\wedge x_1 );x_2\vee ( x_0\wedge x_1;x_2 ) = x_0\wedge x_1;x_2\mbox{ and }( x_0\wedge x_1;x_2 )\vee ( x_0\wedge x_1 );x_2 = ( x_0\wedge x_1 );x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL012+2.p} Cancelativity of converse






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0;x_1 )';x_1^\smallsmile\vee x_0' = x_0'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL027-4.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1'\wedge 1 )\vee ( ( \mbox{sk}_1;\top  )'\wedge 1 ) = ( \mbox{sk}_1;\top  )'\wedge 1 \ \Rightarrow \ ( ( \mbox{sk}_1;\top  )'\wedge 1 )\vee ( \mbox{sk}_1'\wedge 1 )\ne \mbox{sk}_1'\wedge 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL047-1.p} Meet splitting

Meet can be split into 2 inequations iff the meet is on the
 right hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee \mbox{sk}_3 = \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee ( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_2\wedge \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL026+2.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( x_0;\top \wedge x_1 )\vee x_0;x_1 = x_0;x_1\mbox{ and }x_0;x_1\vee ( x_0;\top \wedge x_1 ) = x_0;\top \wedge x_1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL023+2.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile );( x_1\wedge x_2 )\vee x_0;( x_1\wedge x_2 ) = x_0;( x_1\wedge x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL007-1.p} For empty meet the converse slides over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile = 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2\ne 0\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL032-1.p} Subdistributivity

Sequential composition subdistributes over meet, i.e.
 x;(y meet z) $\leq$ x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL008+4.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0;( x_1\vee x_2 )\vee x_0;x_1 )\vee x_0;x_2 = x_0;x_1\vee x_0;x_2\mbox{ and }( x_0;x_1\vee x_0;x_2 )\vee x_0;( x_1\vee x_2 ) = x_0;( x_1\vee x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL004+2.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;x_0'^\smallsmile = ( x_0^\smallsmile )'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL016-3.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL042-1.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;a\wedge \mbox{sk}_1;a' = 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1\ne 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL050+2.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( ( x_0;\top  )'\vee ( x_0;\top  )';\top  = ( x_0;\top  )';\top \mbox{ and }( x_0;\top  )';\top \vee ( x_0;\top  )' = ( x_0;\top  )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL033+3.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over
 meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge x_1 );x_2 = x_0\wedge x_1;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL026-2.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\vee ( \mbox{sk}_1;\top \wedge \mbox{sk}_2 ) = \mbox{sk}_1;\top \wedge \mbox{sk}_2 \ \Rightarrow \ ( \mbox{sk}_1;\top \wedge \mbox{sk}_2 )\vee \mbox{sk}_1;\mbox{sk}_2\ne \mbox{sk}_1;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL033-3.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over
 meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL008-1.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL031-1.p} Partial functions are closed under composition

If x and y are partial functions then x;y is also a partial
 functions.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2^\smallsmile;\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\mbox{sk}_2 )^\smallsmile;( \mbox{sk}_1;\mbox{sk}_2 )\vee 1\ne 1\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL027+4.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( ( x_0;\top  )'\wedge 1 )\vee ( x_0'\wedge 1 ) = x_0'\wedge 1\mbox{ and }( x_0'\wedge 1 )\vee ( ( x_0;\top  )'\wedge 1 ) = ( x_0;\top  )'\wedge 1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL015-1.p} TOP is idempotent w.r.t. composition






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\top ;\top \ne \top \qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL024-1.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL008+2.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0;( x_1\vee x_2 )\vee x_0;x_1 )\vee x_0;x_2 = x_0;x_1\vee x_0;x_2\mbox{ and }( x_0;x_1\vee x_0;x_2 )\vee x_0;( x_1\vee x_2 ) = x_0;( x_1\vee x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL020-2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL027-3.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\top  )'\wedge 1\ne \mbox{sk}_1'\wedge 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL050-3.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\top  )'\ne ( \mbox{sk}_1;\top  )';\top \qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL025+1.p} For subidentities converse is redundant

If x is a subidentity then the converse of x equals x.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ x_0^\smallsmile = x_0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL005+2.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( ( x_0\wedge x_1 )^\smallsmile\vee ( x_0^\smallsmile\wedge x_1^\smallsmile ) = x_0^\smallsmile\wedge x_1^\smallsmile\mbox{ and }( x_0^\smallsmile\wedge x_1^\smallsmile )\vee ( x_0\wedge x_1 )^\smallsmile = ( x_0\wedge x_1 )^\smallsmile )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL002-1.p} There is a (unique) greatest element, namely x + x'






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee \top \ne \top \qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL015+1.p} TOP is idempotent w.r.t. composition






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\top ;\top  = \top \qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL008+1.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;( x_1\vee x_2 ) = x_0;x_1\vee x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL036-1.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );\mbox{sk}_3\vee ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL050-2.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\top  )'\vee ( \mbox{sk}_1;\top  )';\top  = ( \mbox{sk}_1;\top  )';\top  \ \Rightarrow \ ( \mbox{sk}_1;\top  )';\top \vee ( \mbox{sk}_1;\top  )'\ne ( \mbox{sk}_1;\top  )'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL027+1.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( x_0;\top  )'\wedge 1 = x_0'\wedge 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL026+4.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( x_0;\top \wedge x_1 )\vee x_0;x_1 = x_0;x_1\mbox{ and }x_0;x_1\vee ( x_0;\top \wedge x_1 ) = x_0;\top \wedge x_1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL019-1.p} Vectors are closed under meet

If x and y are vectors then x meet y is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2;\top  = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\top \ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL030+3.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ x_0;x_1\wedge x_2' = x_0;x_1\wedge ( x_0;x_2 )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL013+1.p} Zero is annihilator






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0;0 = 0\mbox{ and }0;x_0 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL036-2.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );\mbox{sk}_3\vee ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL007+1.p} For empty meet the converse slides over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0\wedge x_1^\smallsmile = 0 \ \Rightarrow \ x_0^\smallsmile\wedge x_1 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL008-2.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 ) = \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 ) \ \Rightarrow \ ( \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 )\vee \mbox{sk}_1;\mbox{sk}_2 )\vee \mbox{sk}_1;\mbox{sk}_3\ne \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL050+4.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( ( x_0;\top  )'\vee ( x_0;\top  )';\top  = ( x_0;\top  )';\top \mbox{ and }( x_0;\top  )';\top \vee ( x_0;\top  )' = ( x_0;\top  )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL026-4.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\vee ( \mbox{sk}_1;\top \wedge \mbox{sk}_2 ) = \mbox{sk}_1;\top \wedge \mbox{sk}_2 \ \Rightarrow \ ( \mbox{sk}_1;\top \wedge \mbox{sk}_2 )\vee \mbox{sk}_1;\mbox{sk}_2\ne \mbox{sk}_1;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL021+2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge 1 );x_1\vee ( x_0\wedge x_1 ) = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL041+1.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ \forall x_1{:}\;x_0;x_1\wedge x_0;x_1' = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL012-1.p} Cancelativity of converse






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2 )';\mbox{sk}_2^\smallsmile\vee \mbox{sk}_1'\ne \mbox{sk}_1'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL005+3.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0\wedge x_1 )^\smallsmile = x_0^\smallsmile\wedge x_1^\smallsmile\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL027-2.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1'\wedge 1 )\vee ( ( \mbox{sk}_1;\top  )'\wedge 1 ) = ( \mbox{sk}_1;\top  )'\wedge 1 \ \Rightarrow \ ( ( \mbox{sk}_1;\top  )'\wedge 1 )\vee ( \mbox{sk}_1'\wedge 1 )\ne \mbox{sk}_1'\wedge 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL024+2.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile );( x_1\wedge x_2 )\vee ( x_0\wedge x_1^\smallsmile );x_2 = ( x_0\wedge x_1^\smallsmile );x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL030-3.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3'\ne \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL020+1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge 1 );x_1 = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL032+1.p} Subdistributivity

Sequential composition subdistributes over meet, i.e.
 x;(y meet z) $\leq$ x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;( x_1\wedge x_2 )\vee ( x_0;x_1\wedge x_0;x_2 ) = x_0;x_1\wedge x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL040-4.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 ) = \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL029+2.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ ( ( x_0;x_2\wedge x_1;x_2 )\vee ( x_0\wedge x_1 );x_2 = ( x_0\wedge x_1 );x_2\mbox{ and }( x_0\wedge x_1 );x_2\vee ( x_0;x_2\wedge x_1;x_2 ) = x_0;x_2\wedge x_1;x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL029-3.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{19},\mbox{negated\_conjecture})$

\medskip\textbf{REL013-1.p} Zero is annihilator






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;0 = 0 \ \Rightarrow \ 0;\mbox{sk}_1\ne 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL030-1.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3'\ne \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL016+2.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0;x_1\wedge ( x_0;x_2 )' )\vee ( x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )' ) = x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )'\mbox{ and }( x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )' )\vee ( x_0;x_1\wedge ( x_0;x_2 )' ) = x_0;x_1\wedge ( x_0;x_2 )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL027-1.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\top  )'\wedge 1\ne \mbox{sk}_1'\wedge 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL043-2.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\mbox{sk}_2^\smallsmile\vee \mbox{sk}_3 = \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_3';\mbox{sk}_2\vee \mbox{sk}_1'\ne \mbox{sk}_1'\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL033-2.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\vee ( \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 ) = \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL026+1.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ x_0;\top \wedge x_1 = x_0;x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL045+1.p} An unfold law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;x_0\vee ( x_0;x_0^\smallsmile );x_0 = ( x_0;x_0^\smallsmile );x_0\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL040-2.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 ) = \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL017+4.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( ( ( x_0;x_1 )'\vee x_0;x_2 )\vee ( x_0;( x_1\wedge x_2' ) )' )\vee x_0;x_2 = ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2\mbox{ and }( ( ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2 )\vee ( x_0;x_1 )' )\vee x_0;x_2 = ( x_0;x_1 )'\vee x_0;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL035-1.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne \mbox{sk}_2;( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL053-1.p} Relation Algebra






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

\medskip\textbf{REL037-2.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL006-1.p} For empty meet the converse slides over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2 = 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile\ne 0\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL048-1.p} Join splitting

Join can be split into 2 inequations iff the join is on the
 left hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1\vee \mbox{sk}_2 )\vee \mbox{sk}_3 = \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee \mbox{sk}_3 = \mbox{sk}_3 \ \Rightarrow \ \mbox{sk}_2\vee \mbox{sk}_3\ne \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL003+1.p} Isotonicity of converse

x is less or equal than y iff the converse of x is less or equal
 than converse of y.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( ( x_0\vee x_1 = x_1 \ \Rightarrow \ x_0^\smallsmile\vee x_1^\smallsmile = x_1^\smallsmile )\mbox{ and }( x_0^\smallsmile\vee x_1^\smallsmile = x_1^\smallsmile \ \Rightarrow \ x_0\vee x_1 = x_1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL031-2.p} Partial functions are closed under composition

If x and y are partial functions then x;y is also a partial
 functions.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2^\smallsmile;\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\mbox{sk}_2 )^\smallsmile;( \mbox{sk}_1;\mbox{sk}_2 )\vee 1\ne 1\qquad\mbox{cnf}(\mbox{goals}_{19},\mbox{negated\_conjecture})$

\medskip\textbf{REL037+1.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL044-2.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1';\mbox{sk}_2\vee \mbox{sk}_3' = \mbox{sk}_3'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_3;\mbox{sk}_2^\smallsmile\vee \mbox{sk}_1\ne \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL027+3.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( x_0;\top  )'\wedge 1 = x_0'\wedge 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL039-1.p} Dedekind law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_3;\mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3 )\ne ( \mbox{sk}_1\wedge \mbox{sk}_3;\mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL025-1.p} For subidentities converse is redundant

If x is a subidentity then the converse of x equals x.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1^\smallsmile\ne \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL038+1.p} Modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 )\vee ( x_0;( x_1\wedge x_0^\smallsmile;x_2 )\wedge x_2 ) = x_0;( x_1\wedge x_0^\smallsmile;x_2 )\wedge x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL043+1.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1^\smallsmile\vee x_2 = x_2 \ \Rightarrow \ x_2';x_1\vee x_0' = x_0' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL014-1.p} One is neutral element






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

\medskip\textbf{REL050-1.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\top  )'\ne ( \mbox{sk}_1;\top  )';\top \qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL004-2.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1'^\smallsmile\ne ( \mbox{sk}_1^\smallsmile )'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL040-1.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL028+1.p} For subidentities meet and composition coincide






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ x_0;x_1 = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL045-2.p} An unfold law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee ( \mbox{sk}_1;\mbox{sk}_1^\smallsmile );\mbox{sk}_1\ne ( \mbox{sk}_1;\mbox{sk}_1^\smallsmile );\mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL026-1.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\top \wedge \mbox{sk}_2\ne \mbox{sk}_1;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL011+1.p} Schroeder equivalence (second implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile;x_2 = 0 \ \Rightarrow \ x_1;x_0\wedge x_2 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL025+2.p} For subidentities converse is redundant

If x is a subidentity then the converse of x equals x.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( ( x_0\vee 1 = 1 \ \Rightarrow \ x_0^\smallsmile\vee x_0 = x_0 )\mbox{ and }( x_0\vee 1 = 1 \ \Rightarrow \ x_0\vee x_0^\smallsmile = x_0^\smallsmile ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL044-1.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1';\mbox{sk}_2\vee \mbox{sk}_3' = \mbox{sk}_3'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_3;\mbox{sk}_2^\smallsmile\vee \mbox{sk}_1\ne \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL016+3.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;x_1\wedge ( x_0;x_2 )' = x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL036+1.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );x_2\vee ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL041+2.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ \forall x_1{:}\;x_0;x_1\wedge x_0;x_1' = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL044+1.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0';x_1\vee x_2' = x_2' \ \Rightarrow \ x_2;x_1^\smallsmile\vee x_0 = x_0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL034+1.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ x_1;( x_0\wedge x_2 )\vee ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL017+3.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1 )'\vee x_0;x_2 = ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL009+1.p} Sequential composition is isotone in both arguments






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee x_1 = x_1 \ \Rightarrow \ ( x_0;x_2\vee x_1;x_2 = x_1;x_2\mbox{ and }x_2;x_0\vee x_2;x_1 = x_2;x_1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL012-2.p} Cancelativity of converse






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2 )';\mbox{sk}_2^\smallsmile\vee \mbox{sk}_1'\ne \mbox{sk}_1'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL035+2.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = x_1;( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL016-1.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL029+1.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ x_0;x_2\wedge x_1;x_2 = ( x_0\wedge x_1 );x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL037-1.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL034+2.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ x_1;( x_0\wedge x_2 )\vee ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL016+4.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0;x_1\wedge ( x_0;x_2 )' )\vee ( x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )' ) = x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )'\mbox{ and }( x_0;( x_1\wedge x_2' )\wedge ( x_0;x_2 )' )\vee ( x_0;x_1\wedge ( x_0;x_2 )' ) = x_0;x_1\wedge ( x_0;x_2 )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL034-2.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2;( \mbox{sk}_1\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL031+1.p} Partial functions are closed under composition

If x and y are partial functions then x;y is also a partial
 functions.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( ( x_0^\smallsmile;x_0\vee 1 = 1\mbox{ and }x_1^\smallsmile;x_1\vee 1 = 1 ) \ \Rightarrow \ ( x_0;x_1 )^\smallsmile;( x_0;x_1 )\vee 1 = 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL040+4.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ ( x_0;( x_1\wedge x_2 )\vee ( x_0;x_1\wedge x_0;x_2 ) = x_0;x_1\wedge x_0;x_2\mbox{ and }( x_0;x_1\wedge x_0;x_2 )\vee x_0;( x_1\wedge x_2 ) = x_0;( x_1\wedge x_2 ) ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL023-1.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL039+1.p} Dedekind law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 )\vee ( x_0\wedge x_2;x_1^\smallsmile );( x_1\wedge x_0^\smallsmile;x_2 ) = ( x_0\wedge x_2;x_1^\smallsmile );( x_1\wedge x_0^\smallsmile;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL035+1.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = x_1;( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL043-1.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\mbox{sk}_2^\smallsmile\vee \mbox{sk}_3 = \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_3';\mbox{sk}_2\vee \mbox{sk}_1'\ne \mbox{sk}_1'\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL040-3.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL042-2.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;a\wedge \mbox{sk}_1;a' = 0\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1\ne 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL001-1.p} There is a (unique) least element, namely 0






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$0\vee \mbox{sk}_1\ne \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL041-1.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_2'\ne 0\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL033+1.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over
 meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge x_1 );x_2 = x_0\wedge x_1;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL046+1.p} Meet splitting

Meet can be split into 2 inequations iff the meet is on the
 right hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee ( x_1\wedge x_2 ) = x_1\wedge x_2 \ \Rightarrow \ ( x_0\vee x_1 = x_1\mbox{ and }x_0\vee x_2 = x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL026+3.p} Splitting rule for x;y if x is a subidentity

If x is a subidentity then the composition of x and y can be
 split into a meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ x_0;\top \wedge x_1 = x_0;x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL029+3.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ x_0;x_2\wedge x_1;x_2 = ( x_0\wedge x_1 );x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL045-1.p} An unfold law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee ( \mbox{sk}_1;\mbox{sk}_1^\smallsmile );\mbox{sk}_1\ne ( \mbox{sk}_1;\mbox{sk}_1^\smallsmile );\mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL001+1.p} There is a (unique) least element, namely 0






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;0\vee x_0 = x_0\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL005+4.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( ( x_0\wedge x_1 )^\smallsmile\vee ( x_0^\smallsmile\wedge x_1^\smallsmile ) = x_0^\smallsmile\wedge x_1^\smallsmile\mbox{ and }( x_0^\smallsmile\wedge x_1^\smallsmile )\vee ( x_0\wedge x_1 )^\smallsmile = ( x_0\wedge x_1 )^\smallsmile )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL040+3.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ x_0;( x_1\wedge x_2 ) = x_0;x_1\wedge x_0;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL022-1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )\vee ( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\ne ( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL019-2.p} Vectors are closed under meet

If x and y are vectors then x meet y is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2;\top  = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\top \ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{19},\mbox{negated\_conjecture})$

\medskip\textbf{REL034-1.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2;( \mbox{sk}_1\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne ( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL004+3.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;x_0'^\smallsmile = ( x_0^\smallsmile )'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL043+2.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1^\smallsmile\vee x_2 = x_2 \ \Rightarrow \ x_2';x_1\vee x_0' = x_0' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL022-2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )\vee ( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\ne ( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL004-1.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1'^\smallsmile\ne ( \mbox{sk}_1^\smallsmile )'\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL021-1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 )\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL004-3.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1'^\smallsmile\ne ( \mbox{sk}_1^\smallsmile )'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL005-2.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\vee ( \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile ) = \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile \ \Rightarrow \ ( \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL033+2.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( ( x_0\wedge x_1 );x_2\vee ( x_0\wedge x_1;x_2 ) = x_0\wedge x_1;x_2\mbox{ and }( x_0\wedge x_1;x_2 )\vee ( x_0\wedge x_1 );x_2 = ( x_0\wedge x_1 );x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL010+1.p} Schroeder equivalence (first implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1\wedge x_2 = 0 \ \Rightarrow \ x_1\wedge x_0^\smallsmile;x_2 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL020-1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge 1 );\mbox{sk}_2\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL045+2.p} An unfold law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;x_0\vee ( x_0;x_0^\smallsmile );x_0 = ( x_0;x_0^\smallsmile );x_0\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL050-4.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\top  )'\vee ( \mbox{sk}_1;\top  )';\top  = ( \mbox{sk}_1;\top  )';\top  \ \Rightarrow \ ( \mbox{sk}_1;\top  )';\top \vee ( \mbox{sk}_1;\top  )'\ne ( \mbox{sk}_1;\top  )'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL030-2.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' ) = \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3' )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3'\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL032-2.p} Subdistributivity

Sequential composition subdistributes over meet, i.e.
 x;(y meet z) $\leq$ x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3 )\ne \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL049+1.p} Join splitting

Join can be split into 2 inequations iff the join is on the
 left hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee x_1 = x_1\mbox{ and }x_2\vee x_1 = x_1 ) \ \Rightarrow \ ( x_0\vee x_2 )\vee x_1 = x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL011+2.p} Schroeder equivalence (second implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile;x_2 = 0 \ \Rightarrow \ x_1;x_0\wedge x_2 = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL051+1.p} Dense linear ordering






$\forall a{:}\;o(a,a)\qquad\mbox{fof}(f_{01},\mbox{axiom})$

$\forall a,b{:}\;( ( a\ne b\mbox{ and }o(a,b) ) \ \Rightarrow \ \neg\,o(b,a) )\qquad\mbox{fof}(f_{02},\mbox{axiom})$

$\forall a,b,c{:}\;( ( o(a,b)\mbox{ and }o(b,c) ) \ \Rightarrow \ o(a,c) )\qquad\mbox{fof}(f_{03},\mbox{axiom})$

$\forall a,b{:}\;( ( a\ne b\mbox{ and }o(a,b) ) \ \Rightarrow \ ( o(a,f(a,b))\mbox{ and }o(f(a,b),b) ) )\qquad\mbox{fof}(f_{04},\mbox{axiom})$

$\forall a,b{:}\;( f(a,b)\ne a\mbox{ and }f(a,b)\ne b )\qquad\mbox{fof}(f_{05},\mbox{axiom})$

$\forall a,b{:}\;( o(a,b)\mbox{ or }o(b,a) )\qquad\mbox{fof}(f_{06},\mbox{axiom})$

\medskip\textbf{REL024-2.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL005-3.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\ne \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL042+2.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( \forall x_1{:}\;x_0;x_1\wedge x_0;x_1' = 0 \ \Rightarrow \ x_0^\smallsmile;x_0\vee 1 = 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL035-2.p} Propagation of vectors

Pre-assertion x to z can be propagated as post-assertion x$\wedge$ to
 the left cofactor y.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile );( \mbox{sk}_1\wedge \mbox{sk}_3 )\ne \mbox{sk}_2;( \mbox{sk}_1\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL006+1.p} For empty meet the converse slides over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0^\smallsmile\wedge x_1 = 0 \ \Rightarrow \ x_0\wedge x_1^\smallsmile = 0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL032+2.p} Subdistributivity

Sequential composition subdistributes over meet, i.e.
 x;(y meet z) $\leq$ x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;( x_1\wedge x_2 )\vee ( x_0;x_1\wedge x_0;x_2 ) = x_0;x_1\wedge x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL049-1.p} Join splitting

Join can be split into 2 inequations iff the join is on the
 left hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_3\vee \mbox{sk}_2 = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\vee \mbox{sk}_3 )\vee \mbox{sk}_2\ne \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL009-1.p} Sequential composition is isotone in both arguments






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_3\vee \mbox{sk}_2;\mbox{sk}_3 = \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ \mbox{sk}_3;\mbox{sk}_1\vee \mbox{sk}_3;\mbox{sk}_2\ne \mbox{sk}_3;\mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL005+1.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0\wedge x_1 )^\smallsmile = x_0^\smallsmile\wedge x_1^\smallsmile\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL033-4.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\vee ( \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 ) = \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL020+2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge 1 );x_1 = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL003-1.p} Isotonicity of converse

x is less or equal than y iff the converse of x is less or equal
 than converse of y.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2\mbox{ or }\mbox{sk}_1^\smallsmile\vee \mbox{sk}_2^\smallsmile = \mbox{sk}_2^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2 \ \Rightarrow \ \mbox{sk}_1^\smallsmile\vee \mbox{sk}_2^\smallsmile\ne \mbox{sk}_2^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL017-4.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( ( ( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3 )\vee ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )' )\vee \mbox{sk}_1;\mbox{sk}_3 = ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3 \ \Rightarrow \ ( ( ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2 )' )\vee \mbox{sk}_1;\mbox{sk}_3\ne ( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL033-1.p} Sequential composition distributes in each argument of meet

If x is a vector then sequential composition distributes over
 meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne \mbox{sk}_1\wedge \mbox{sk}_2;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL029-4.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\vee ( \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 ) = \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 \ \Rightarrow \ ( \mbox{sk}_1;\mbox{sk}_3\wedge \mbox{sk}_2;\mbox{sk}_3 )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 );\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{19},\mbox{negated\_conjecture})$

\medskip\textbf{REL030+2.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( x_0;x_1\wedge x_2' )\vee ( x_0;x_1\wedge ( x_0;x_2 )' ) = x_0;x_1\wedge ( x_0;x_2 )'\mbox{ and }( x_0;x_1\wedge ( x_0;x_2 )' )\vee ( x_0;x_1\wedge x_2' ) = x_0;x_1\wedge x_2' ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL040+1.p} Partial functions distribute over meet under sequential comp'n

If x is partial function then x;(y meet z) = x;y meet x;z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0^\smallsmile;x_0\vee 1 = 1 \ \Rightarrow \ x_0;( x_1\wedge x_2 ) = x_0;x_1\wedge x_0;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL008-4.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 ) = \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 ) \ \Rightarrow \ ( \mbox{sk}_1;( \mbox{sk}_2\vee \mbox{sk}_3 )\vee \mbox{sk}_1;\mbox{sk}_2 )\vee \mbox{sk}_1;\mbox{sk}_3\ne \mbox{sk}_1;\mbox{sk}_2\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL038-1.p} Modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3 )\vee ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3 )\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3 )\wedge \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL004+1.p} Converse negation are interconvertible






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;x_0'^\smallsmile = ( x_0^\smallsmile )'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL031+2.p} Partial functions are closed under composition

If x and y are partial functions then x;y is also a partial
 functions.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( ( x_0^\smallsmile;x_0\vee 1 = 1\mbox{ and }x_1^\smallsmile;x_1\vee 1 = 1 ) \ \Rightarrow \ ( x_0;x_1 )^\smallsmile;( x_0;x_1 )\vee 1 = 1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL009+2.p} Sequential composition is isotone in both arguments






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee x_1 = x_1 \ \Rightarrow \ ( x_0;x_2\vee x_1;x_2 = x_1;x_2\mbox{ and }x_2;x_0\vee x_2;x_1 = x_2;x_1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL017+1.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;x_1 )'\vee x_0;x_2 = ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL048+1.p} Join splitting

Join can be split into 2 inequations iff the join is on the
 left hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee x_1 )\vee x_2 = x_2 \ \Rightarrow \ ( x_0\vee x_2 = x_2\mbox{ and }x_1\vee x_2 = x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL022+2.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge x_1 )\vee ( x_0\wedge 1 );x_1 = ( x_0\wedge 1 );x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL017-1.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3\ne ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL005-1.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\ne \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL027+2.p} Complements of vectors and subidentities

The relative complement of subidentity x w.r.t. 1 can also be
 obtained by projecting the complement of the corresponding vector
 x;TOP to a subidentity.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ ( ( ( x_0;\top  )'\wedge 1 )\vee ( x_0'\wedge 1 ) = x_0'\wedge 1\mbox{ and }( x_0'\wedge 1 )\vee ( ( x_0;\top  )'\wedge 1 ) = ( x_0;\top  )'\wedge 1 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL046-1.p} Meet splitting

Meet can be split into 2 inequations iff the meet is on the
 right hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee ( \mbox{sk}_2\wedge \mbox{sk}_3 ) = \mbox{sk}_2\wedge \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee \mbox{sk}_2 = \mbox{sk}_2 \ \Rightarrow \ \mbox{sk}_1\vee \mbox{sk}_3\ne \mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL050+3.p} The complement of x;TOP is left ideal






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0{:}\;( x_0;\top  )' = ( x_0;\top  )';\top \qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL008+3.p} Sequential composition distributes over addition






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;x_0;( x_1\vee x_2 ) = x_0;x_1\vee x_0;x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL018-1.p} Vectors are closed under complementation

If x is a vector then overline{x} is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\top  = \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1';\top \ne \mbox{sk}_1'\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL024+1.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile );( x_1\wedge x_2 )\vee ( x_0\wedge x_1^\smallsmile );x_2 = ( x_0\wedge x_1^\smallsmile );x_2\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL016-4.p} A modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' ) = \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' \ \Rightarrow \ ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' )\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\vee ( \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )' )\ne \mbox{sk}_1;\mbox{sk}_2\wedge ( \mbox{sk}_1;\mbox{sk}_3 )'\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL044+2.p} Shunting rule






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0';x_1\vee x_2' = x_2' \ \Rightarrow \ x_2;x_1^\smallsmile\vee x_0 = x_0 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL028-1.p} For subidentities meet and composition coincide






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\ne \mbox{sk}_1\wedge \mbox{sk}_2\qquad\mbox{cnf}(\mbox{goals}_{16},\mbox{negated\_conjecture})$

\medskip\textbf{REL010-1.p} Schroeder equivalence (first implication)

Describes the interplay between composition, converse and
 complement, w.r.t. containment.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_3 = 0\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_2\wedge \mbox{sk}_1^\smallsmile;\mbox{sk}_3\ne 0\qquad\mbox{cnf}(\mbox{goals}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{REL023-2.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2^\smallsmile );( \mbox{sk}_2\wedge \mbox{sk}_3 )\vee \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\ne \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3 )\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL012+1.p} Cancelativity of converse






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0;x_1 )';x_1^\smallsmile\vee x_0' = x_0'\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL028+2.p} For subidentities meet and composition coincide






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ x_0;x_1 = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL036+2.p} Propagation of vectors

Post-assertion x$\wedge$ to y can be propagated as pre-assertion x to
 the right cofactor z.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_1\wedge x_0^\smallsmile );x_2\vee ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) = ( x_1\wedge x_0^\smallsmile );( x_0\wedge x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL030+1.p} Propagation of subidentities






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\vee 1 = 1 \ \Rightarrow \ x_0;x_1\wedge x_2' = x_0;x_1\wedge ( x_0;x_2 )' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL047+1.p} Meet splitting

Meet can be split into 2 inequations iff the meet is on the
 right hand side of an inequation.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee x_1 = x_1\mbox{ and }x_0\vee x_2 = x_2 ) \ \Rightarrow \ x_0\vee ( x_1\wedge x_2 ) = x_1\wedge x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL023+1.p} A simple consequence of isotonicity






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( x_0\wedge x_1^\smallsmile );( x_1\wedge x_2 )\vee x_0;( x_1\wedge x_2 ) = x_0;( x_1\wedge x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL019+2.p} Vectors are closed under meet

If x and y are vectors then x meet y is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1{:}\;( ( x_0;\top  = x_0\mbox{ and }x_1;\top  = x_1 ) \ \Rightarrow \ ( x_0\wedge x_1 );\top  = x_0\wedge x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL052+1.p} Non-discrete dense ordering






$\forall a{:}\;o(a,a)\qquad\mbox{fof}(f_{01},\mbox{axiom})$

$\forall a,b{:}\;( ( a\ne b\mbox{ and }o(a,b) ) \ \Rightarrow \ \neg\,o(b,a) )\qquad\mbox{fof}(f_{02},\mbox{axiom})$

$\forall a,b,c{:}\;( ( o(a,b)\mbox{ and }o(b,c) ) \ \Rightarrow \ o(a,c) )\qquad\mbox{fof}(f_{03},\mbox{axiom})$

$\forall a,b{:}\;( ( a\ne b\mbox{ and }o(a,b) ) \ \Rightarrow \ ( o(a,f(a,b))\mbox{ and }o(f(a,b),b) ) )\qquad\mbox{fof}(f_{04},\mbox{axiom})$

$\forall a,b{:}\;( f(a,b)\ne a\mbox{ and }f(a,b)\ne b )\qquad\mbox{fof}(f_{05},\mbox{axiom})$

$\exists a,b{:}\;( o(a,b)\mbox{ and }a\ne b )\qquad\mbox{fof}(f_{06},\mbox{axiom})$

\medskip\textbf{REL022+1.p} Restriction of subidentities

For vectors restriction of subidientities equals intersection
 with vectors.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1{:}\;( x_0;\top  = x_0 \ \Rightarrow \ ( x_0\wedge x_1 )\vee ( x_0\wedge 1 );x_1 = ( x_0\wedge 1 );x_1 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL029+4.p} Distributivity of subidentities

For subidentities, sequential composition distributes over meet.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001+1.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( x_0\vee 1 = 1\mbox{ and }x_1\vee 1 = 1 ) \ \Rightarrow \ ( ( x_0;x_2\wedge x_1;x_2 )\vee ( x_0\wedge x_1 );x_2 = ( x_0\wedge x_1 );x_2\mbox{ and }( x_0\wedge x_1 );x_2\vee ( x_0;x_2\wedge x_1;x_2 ) = x_0;x_2\wedge x_1;x_2 ) )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL017+2.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0,x_1,x_2{:}\;( ( ( ( x_0;x_1 )'\vee x_0;x_2 )\vee ( x_0;( x_1\wedge x_2' ) )' )\vee x_0;x_2 = ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2\mbox{ and }( ( ( x_0;( x_1\wedge x_2' ) )'\vee x_0;x_2 )\vee ( x_0;x_1 )' )\vee x_0;x_2 = ( x_0;x_1 )'\vee x_0;x_2 )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip\textbf{REL041-2.p} Equivalence of different definitions of partial functions

x is a partial function if x$\wedge$;x is a subidentity ([SS93]). x is
 a partial function if for all y x;y meet x;overline{y} = 0.
 These definitions are equivalent.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$\mbox{sk}_1^\smallsmile;\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

$\mbox{sk}_1;\mbox{sk}_2\wedge \mbox{sk}_1;\mbox{sk}_2'\ne 0\qquad\mbox{cnf}(\mbox{goals}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{REL017-2.p} Another modular law






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$( ( ( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3 )\vee ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )' )\vee \mbox{sk}_1;\mbox{sk}_3 = ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3 \ \Rightarrow \ ( ( ( \mbox{sk}_1;( \mbox{sk}_2\wedge \mbox{sk}_3' ) )'\vee \mbox{sk}_1;\mbox{sk}_3 )\vee ( \mbox{sk}_1;\mbox{sk}_2 )' )\vee \mbox{sk}_1;\mbox{sk}_3\ne ( \mbox{sk}_1;\mbox{sk}_2 )'\vee \mbox{sk}_1;\mbox{sk}_3\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

\medskip\textbf{REL025-2.p} For subidentities converse is redundant

If x is a subidentity then the converse of x equals x.




$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{sk}_1\vee 1 = 1\qquad\mbox{cnf}(\mbox{goals}_{14},\mbox{negated\_conjecture})$

$\mbox{sk}_1\vee \mbox{sk}_1^\smallsmile = \mbox{sk}_1^\smallsmile \ \Rightarrow \ \mbox{sk}_1^\smallsmile\vee \mbox{sk}_1\ne \mbox{sk}_1\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL005-4.p} Converse distributes over meet






$\mbox{include}(\mbox{'Axioms/REL001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/REL001-1.ax'})$

$( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\vee ( \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile ) = \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile \ \Rightarrow \ ( \mbox{sk}_1^\smallsmile\wedge \mbox{sk}_2^\smallsmile )\vee ( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\ne ( \mbox{sk}_1\wedge \mbox{sk}_2 )^\smallsmile\qquad\mbox{cnf}(\mbox{goals}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{REL018+1.p} Vectors are closed under complementation

If x is a vector then overline{x} is a vector too.




$\mbox{include}(\mbox{'Axioms/REL001+0.ax'})$

$\forall x_0{:}\;( x_0;\top  = x_0 \ \Rightarrow \ x_0';\top  = x_0' )\qquad\mbox{fof}(\mbox{goals},\mbox{conjecture})$

\medskip
\end{document}