summaryrefslogtreecommitdiff
path: root/Source/Provers/TPTP/TypeDeclCollector.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/TPTP/TypeDeclCollector.cs')
-rw-r--r--Source/Provers/TPTP/TypeDeclCollector.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs
index 0d0eb19a..beecf660 100644
--- a/Source/Provers/TPTP/TypeDeclCollector.cs
+++ b/Source/Provers/TPTP/TypeDeclCollector.cs
@@ -113,10 +113,10 @@ void ObjectInvariant()
}
string ax1 = "fof(selectEq" + id + ", axiom, ! [M,V," + xS + "] : (" +
- string.Format("{0}({1}(M,{2},V),{2}) = V", sel, name, xS) + ")).";
+ string.Format("{0}({1}(M,{2},V),{2}) {3} V", sel, name, xS, eq) + ")).";
string ax2 = "fof(selectNeq" + id + ", axiom, ! [M,V," + xS + "," + yS + "] : (" +
string.Format("( {0} ) => ", dist) +
- string.Format("{0}({1}(M,{2},V),{3}) = {0}(M,{3})", sel, name, xS, yS) + ")).";
+ string.Format("{0}({1}(M,{2},V),{3}) {4} {0}(M,{3})", sel, name, xS, yS, eq) + ")).";
AddDeclaration(ax1);
AddDeclaration(ax2);