Rename pair to unorderedPair

lisa-front/src/main/scala/lisa/front/theory/SetTheory.scala

@@ -21,7 +21,7 @@ object SetTheory {
   val sameCardinality: ConstantPredicateLabel[2] = fromKernel(AxiomaticSetTheory.in).asInstanceOf[ConstantPredicateLabel[2]]
 
   val emptySet: ConstantFunctionLabel[0] = fromKernel(AxiomaticSetTheory.emptySet).asInstanceOf[ConstantFunctionLabel[0]]
-  val unorderedPairSet: ConstantFunctionLabel[2] = fromKernel(AxiomaticSetTheory.pair).asInstanceOf[ConstantFunctionLabel[2]]
+  val unorderedPairSet: ConstantFunctionLabel[2] = fromKernel(AxiomaticSetTheory.unorderedPair).asInstanceOf[ConstantFunctionLabel[2]]
   // val singletonSet: ConstantFunctionLabel[1] = fromKernel(AxiomaticSetTheory.singleton).asInstanceOf[ConstantFunctionLabel[1]]
   val powerSet: ConstantFunctionLabel[1] = fromKernel(AxiomaticSetTheory.powerSet).asInstanceOf[ConstantFunctionLabel[1]]
   val unionSet: ConstantFunctionLabel[1] = fromKernel(AxiomaticSetTheory.union).asInstanceOf[ConstantFunctionLabel[1]]

lisa-theories/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala

@@ -42,7 +42,7 @@ private[settheory] trait SetTheoryDefinitions {
   /**
    * The symbol for the unordered pair function.
    */
-  final val pair = ConstantFunctionLabel("unordered_pair", 2)
+  final val unorderedPair = ConstantFunctionLabel("unordered_pair", 2)
 
   /**
    * The symbol for the powerset function.
@@ -62,7 +62,7 @@ private[settheory] trait SetTheoryDefinitions {
   /**
    * Set Theory basic functions.
    */
-  final val functions = Set(emptySet, pair, powerSet, union, universe)
+  final val functions = Set(emptySet, unorderedPair, powerSet, union, universe)
 
   /**
    * The kernel theory loaded with Set Theory symbols and axioms.

lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala

@@ -16,7 +16,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
   final val emptySetAxiom: Formula = forall(x, !in(x, emptySet()))
   final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
   final val subsetAxiom: Formula = forall(x, forall(y, subset(x, y) <=> forall(z, in(z, x) ==> in(z, y))))
-  final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
+  final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, unorderedPair(x, y)) <=> (x === z) \/ (y === z))))
   final val unionAxiom: Formula = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
   final val powerAxiom: Formula = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
   final val foundationAxiom: Formula = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))

src/main/scala/lisa/proven/mathematics/SetTheory.scala

@@ -42,10 +42,10 @@ object SetTheory extends lisa.Main {
             Seq(-1)
           )
           val pr2 = RightSubstIff(
-            Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))),
+            Sequent(pr1.bot.right, Set(in(z, unorderedPair(x, y)) <=> in(z, unorderedPair(y, x)))),
             0,
-            List(((x === z) \/ (y === z), in(z, pair(y, x)))),
-            LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h)
+            List(((x === z) \/ (y === z), in(z, unorderedPair(y, x)))),
+            LambdaFormulaFormula(Seq(h), in(z, unorderedPair(x, y)) <=> h)
           )
           val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
           val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
@@ -55,8 +55,8 @@ object SetTheory extends lisa.Main {
       )
       val pairExt = SCSubproof(
         {
-          val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", pair(x, y))
-          instantiateForall(pairExt1, pairExt1.conclusion.right.head, pair(y, x))
+          val pairExt1 = instantiateForall(Proof(steps(), imports(ax"extensionalityAxiom")), ax"extensionalityAxiom", unorderedPair(x, y))
+          instantiateForall(pairExt1, pairExt1.conclusion.right.head, unorderedPair(y, x))
         },
         Seq(-1)
       )
@@ -80,8 +80,8 @@ object SetTheory extends lisa.Main {
       val z = VariableLabel("z")
       val g = VariableLabel("g")
       val h = VariableFormulaLabel("h")
-      val pxy = pair(x, y)
-      val pxy1 = pair(x1, y1)
+      val pxy = unorderedPair(x, y)
+      val pxy1 = unorderedPair(x1, y1)
       val p0 = SCSubproof(
         {
           val p0 = SCSubproof(