A proof by identifying Lemmas

Credits: This is work of Achal Kumar.

Let ⋆ be a binary operation on a nonempty set $M$. That is, every pair $(a,b) \in M$ is assigned an element $a$ ⋆$ b$ in $M$. Suppose that ⋆ has the additional property that $(a $ ⋆ $b) $ ⋆$ b= a$ and $a$ ⋆ $(a$ ⋆$ b)= b$ for all $a,b \in M$. Show that $a$ ⋆ $b = b$ ⋆ $a$ for all $a,b \in M$.

Here we try to solve the given problem by identifying the lemmas generated by the LocalProver. We can not add all the axioms in one single distribution because it would not be possible for the LocaProver to generate any relevant lemmas due to combinatorial explosion.

Thus we divide the whole set of axioms ,relevant with the proof into different parts, use the LocalProver on them to get a significant set of lemmas then create distribution which consist of the derrived lemmas and repeat the process until we get the desired result.

In the proof we would be generating following results :

  1. $ (m*n)*n= m $
  2. $ (m*n)*((m*n)*n) = n $
  3. $ ((m*n)*m) = (m*n)*((m*n)*n) $
  4. $ ((m*n)*m))*m = m*n $
  5. $ (m*n)*m = n $
  6. $ ((m*n)*m)*m = n*m $

These are the intermediate results that the prover proves and then using them finally proves the desired result

$ m*n = n*m $


In [1]:
import $cp.bin.`provingground-core-jvm-c30de0f4e0.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}


Out[1]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 

In [2]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._


Out[2]:
import provingground._ , interface._, HoTT._

import learning._

import library._, MonoidSimple._

Here we add the different distributions with each distrtibution focusing attention on differtent thing then these are used in succession to generate lemmas


In [3]:
val M = "M" :: Type

  val eqM = "eqM" :: M ->: M ->: Type

  // val sym = IdentityTyp.symm(M)
  //
  // val trans = IdentityTyp.trans(M)

  val a = "a" :: M
  val b = "b" :: M
  val c = "c" :: M



  val m = "m" :: M

  val n = "n" :: M

  val op = "mul" :: M ->: M ->: M
  val pl = "plus" :: M ->: M ->: M

  import FineDeducer.unif


Out[3]:
M: Typ[Term] = M
eqM: Func[Term, Func[Term, Typ[Term]]] = eqM
a: Term = a
b: Term = b
c: Term = c
m: Term = m
n: Term = n
op: Func[Term, Func[Term, Term]] = mul
pl: Func[Term, Func[Term, Term]] = plus
import FineDeducer.unif

 

In [4]:
val putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
    eqM(a)(a),
    eqM(a)(b) ->: eqM(b)(a),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term) * 0.125) ++ (FiniteDistribution.unif(op : Term ) * 0.375)


Out[4]:
putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.041666666666666664),
    Weighted(b, 0.041666666666666664),
    Weighted(c, 0.041666666666666664),
    Weighted(m, 0.041666666666666664),
    Weighted(n, 0.041666666666666664),
    Weighted(mul, 0.041666666666666664),
    Weighted(eqM, 0.041666666666666664),
    Weighted(axiom_{eqM(a)(a)}, 0.041666666666666664),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.041666666666666664),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.041666666666666664
    ),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.041666666666666664),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.041666666666666664),
    Weighted(eqM, 0.125),
    Weighted(mul, 0.375)
  )
)

In [5]:
val tputn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
    eqM(a)(a),
    eqM(a)(b) ->: eqM(b)(a),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
    eqM(op(op(m)(n))(n))(m),
    eqM(op(m)(op(m)(n)))(n)
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)


Out[5]:
tputn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.03571428571428571),
    Weighted(b, 0.03571428571428571),
    Weighted(c, 0.03571428571428571),
    Weighted(m, 0.03571428571428571),
    Weighted(n, 0.03571428571428571),
    Weighted(mul, 0.03571428571428571),
    Weighted(eqM, 0.03571428571428571),
    Weighted(axiom_{eqM(a)(a)}, 0.03571428571428571),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.03571428571428571),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.03571428571428571
    ),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.03571428571428571),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.03571428571428571),
    Weighted(axiom_{eqM(mul(mul(m)(n))(n))(m)}, 0.03571428571428571),
    Weighted(axiom_{eqM(mul(m)(mul(m)(n)))(n)}, 0.03571428571428571),
    Weighted(eqM, 0.25),
    Weighted(mul, 0.25)
  )
)

In [6]:
val t2putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
    eqM(a)(a),
    eqM(a)(b) ->: eqM(b)(a),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)


Out[6]:
t2putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(m, 0.045454545454545456),
    Weighted(n, 0.045454545454545456),
    Weighted(mul, 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(axiom_{eqM(a)(a)}, 0.045454545454545456),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.045454545454545456),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.045454545454545456),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.045454545454545456),
    Weighted(eqM, 0.25),
    Weighted(mul, 0.25)
  )
)

In [7]:
val t3putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op,op(m)(n), eqM)(
    eqM(a)(b) ->: eqM(b)(a),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)


Out[7]:
t3putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(m, 0.045454545454545456),
    Weighted(n, 0.045454545454545456),
    Weighted(mul, 0.045454545454545456),
    Weighted(mul(m)(n), 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.045454545454545456),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.045454545454545456),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.045454545454545456),
    Weighted(eqM, 0.25),
    Weighted(mul, 0.25)
  )
)

In [8]:
val t0putn: FiniteDistribution[Term] = unif(a,b,c)(m,n,op, eqM)(
    eqM(a)(a),
    eqM(a)(b) ->: eqM(b)(a),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
    eqM(b)(c) ->: eqM(op(a)(b))(op(a)(c))
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)


Out[8]:
t0putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.045454545454545456),
    Weighted(b, 0.045454545454545456),
    Weighted(c, 0.045454545454545456),
    Weighted(m, 0.045454545454545456),
    Weighted(n, 0.045454545454545456),
    Weighted(mul, 0.045454545454545456),
    Weighted(eqM, 0.045454545454545456),
    Weighted(axiom_{eqM(a)(a)}, 0.045454545454545456),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.045454545454545456),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.045454545454545456
    ),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
      0.045454545454545456
    ),
    Weighted(eqM, 0.25),
    Weighted(mul, 0.25)
  )
)

In [9]:
val t0putn1 = t0putn.filter((t) => !Set(a, b, c).contains(t)).normalized()

  val putn1 = putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
  val tputn1 = tputn.filter((t) => !Set(a, b, c).contains(t)).normalized()
  val t2putn1 = t2putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
  val t3putn1 = t3putn.filter((t) => !Set(a, b, c).contains(t)).normalized()


Out[9]:
t0putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.05263157894736841),
    Weighted(n, 0.05263157894736841),
    Weighted(mul, 0.05263157894736841),
    Weighted(eqM, 0.05263157894736841),
    Weighted(axiom_{eqM(a)(a)}, 0.05263157894736841),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05263157894736841
    ),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
      0.05263157894736841
    ),
    Weighted(eqM, 0.28947368421052627),
    Weighted(mul, 0.28947368421052627)
  )
)
putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.047619047619047616),
    Weighted(n, 0.047619047619047616),
    Weighted(mul, 0.047619047619047616),
    Weighted(eqM, 0.047619047619047616),
    Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.047619047619047616
    ),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.047619047619047616),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.047619047619047616),
    Weighted(eqM, 0.14285714285714285),
    Weighted(mul, 0.42857142857142855)
  )
)
tputn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.04),
    Weighted(n, 0.04),
    Weighted(mul, 0.04),
    Weighted(eqM, 0.04),
    Weighted(axiom_{eqM(a)(a)}, 0.04),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.04),
    Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.04),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.04),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.04),
    Weighted(axiom_{eqM(mul(mul(m)(n))(n))(m)}, 0.04),
    Weighted(axiom_{eqM(mul(m)(mul(m)(n)))(n)}, 0.04),
    Weighted(eqM, 0.28),
    Weighted(mul, 0.28)
  )
)
t2putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.05263157894736841),
    Weighted(n, 0.05263157894736841),
    Weighted(mul, 0.05263157894736841),
    Weighted(eqM, 0.05263157894736841),
    Weighted(axiom_{eqM(a)(a)}, 0.05263157894736841),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
    Weighted(eqM, 0.28947368421052627),
    Weighted(mul, 0.28947368421052627)
  )
)
t3putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.05263157894736841),
    Weighted(n, 0.05263157894736841),
    Weighted(mul, 0.05263157894736841),
    Weighted(mul(m)(n), 0.05263157894736841),
    Weighted(eqM, 0.05263157894736841),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
    Weighted(eqM, 0.28947368421052627),
    Weighted(mul, 0.28947368421052627)
  )
)

Here we use the distribution which focuses attention on terms $m$ , $n$ and $m*n$ to generate lemmas where $m$ , $n$ are the terms we would use to prove the result


In [10]:
import monix.execution.Scheduler.Implicits.global
val ts = TermState(t3putn1,t3putn1.map(_.typ))
val lp = LocalProver(ts, cutoff = 0.000005).noIsles
val lem = lp.lemmas.runSyncUnsafe()


Out[10]:
import monix.execution.Scheduler.Implicits.global

ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.05263157894736841),
      Weighted(n, 0.05263157894736841),
      Weighted(mul, 0.05263157894736841),
      Weighted(mul(m)(n), 0.05263157894736841),
      Weighted(eqM, 0.05263157894736841),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
      Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
      Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
      Weighted(eqM, 0.28947368421052627),
      Weighted(mul, 0.28947368421052627)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.05263157894736841),
      Weighted(M, 0.05263157894736841),
      Weighted((M → (M → M)), 0.05263157894736841),
      Weighted(M, 0.05263157894736841),
      Weighted((M → (M → 𝒰 )), 0.05263157894736841),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.05263157894736841
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
        0.05263157894736841
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
        0.05263157894736841
      ),
      Weighted((M → (M → 𝒰 )), 0.28947368421052627),
      Weighted((M → (M → M)), 0.28947368421052627)
    )
  ),
  Vector(),
...
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.05263157894736841),
        Weighted(n, 0.05263157894736841),
        Weighted(mul, 0.05263157894736841),
        Weighted(mul(m)(n), 0.05263157894736841),
        Weighted(eqM, 0.05263157894736841),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
        Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
        Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
        Weighted(eqM, 0.28947368421052627),
        Weighted(mul, 0.28947368421052627)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05263157894736841),
        Weighted(M, 0.05263157894736841),
        Weighted((M → (M → M)), 0.05263157894736841),
        Weighted(M, 0.05263157894736841),
        Weighted((M → (M → 𝒰 )), 0.05263157894736841),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.05263157894736841
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
          0.05263157894736841
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
          0.05263157894736841
        ),
        Weighted((M → (M → 𝒰 )), 0.28947368421052627),
        Weighted((M → (M → M)), 0.28947368421052627)
      )
    ),
...
lem: Vector[(Typ[Term], Double)] = Vector(
  (eqM(n)(mul(m)(mul(m)(n))), 3.150279366819256E-4),
  (eqM(m)(mul(mul(m)(n))(n)), 2.7034870284010703E-4),
  (eqM(mul(mul(m)(n))(n))(m), 3.062988293669645E-5),
  (eqM(mul(m)(mul(m)(n)))(n), 3.062988293669645E-5),
  (eqM(mul(m)(n))(mul(n)(mul(n)(mul(m)(n)))), 1.2164940347298408E-5),
  (eqM(mul(m)(n))(mul(m)(mul(m)(mul(m)(n)))), 1.2164940347298408E-5),
  (
    eqM(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
    1.2164940347298408E-5
  ),
  (eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0614151718697937E-5),
  (eqM(n)(mul(n)(mul(n)(n))), 1.0614151718697937E-5),
  (eqM(m)(mul(n)(mul(n)(m))), 1.0614151718697937E-5),
  (eqM(m)(mul(m)(mul(m)(m))), 1.0614151718697937E-5),
  (eqM(m)(mul(mul(m)(n))(mul(mul(m)(n))(m))), 1.0614151718697937E-5)
)

In [11]:
import provingground.{FiniteDistribution => FD}
val x = "lemma1" :: lem(1)._1
val y = "lemma2" :: lem(7)._1
val tputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
    eqM(b)(c) ->: eqM(op(a)(b))(op(a)(c))
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x ,op(m)(n)) * 0.5)
val tputin1 = tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts1 = TermState(tputin1,tputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))( op(op(m)(n))(op(op(m)(n))(n)))))
val lp1 = LocalProver(ts1, cutoff = 0.000002).noIsles
val lem2 = lp1.lemmas.runSyncUnsafe()


Out[11]:
import provingground.{FiniteDistribution => FD}

x: Term = lemma1
y: Term = lemma2
tputin: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(m, 0.0625),
    Weighted(n, 0.0625),
    Weighted(mul, 0.0625),
    Weighted(eqM, 0.0625),
    Weighted(axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))}, 0.0625),
    Weighted(eqM, 0.16666666666666666),
    Weighted(lemma1, 0.16666666666666666),
    Weighted(mul(m)(n), 0.16666666666666666)
  )
)
tputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.07692307692307693),
    Weighted(n, 0.07692307692307693),
    Weighted(mul, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
      0.07692307692307693
    ),
    Weighted(eqM, 0.20512820512820512),
    Weighted(lemma1, 0.20512820512820512),
    Weighted(mul(m)(n), 0.20512820512820512)
  )
)
ts1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.07692307692307693),
      Weighted(n, 0.07692307692307693),
      Weighted(mul, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(
        axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
        0.07692307692307693
      ),
      Weighted(eqM, 0.20512820512820512),
      Weighted(lemma1, 0.20512820512820512),
      Weighted(mul(m)(n), 0.20512820512820512)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.07692307692307693),
      Weighted(M, 0.07692307692307693),
      Weighted((M → (M → M)), 0.07692307692307693),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(a)(b))(mul(a)(c))) } } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.20512820512820512),
      Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.20512820512820512),
      Weighted(M, 0.20512820512820512)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0)
    )
  ),
...
lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.07692307692307693),
        Weighted(n, 0.07692307692307693),
        Weighted(mul, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(
          axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
          0.07692307692307693
        ),
        Weighted(eqM, 0.20512820512820512),
        Weighted(lemma1, 0.20512820512820512),
        Weighted(mul(m)(n), 0.20512820512820512)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.07692307692307693),
        Weighted(M, 0.07692307692307693),
        Weighted((M → (M → M)), 0.07692307692307693),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(a)(b))(mul(a)(c))) } } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.20512820512820512),
        Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.20512820512820512),
        Weighted(M, 0.20512820512820512)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0)
      )
...
lem2: Vector[(Typ[Term], Double)] = Vector(
  (
    eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
    0.9079462369542685
  ),
  (eqM(mul(n)(m))(mul(n)(mul(mul(m)(n))(n))), 1.0252535689104723E-5),
  (eqM(mul(m)(m))(mul(m)(mul(mul(m)(n))(n))), 1.0252535689104723E-5)
)

In [12]:
val z = "lemma3" :: lem2(0)._1


Out[12]:
z: Term = lemma3

In [13]:
val tt2putn =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(op(op(a)(b))(b))(a),
 eqM(op(a)(op(a)(b)))(b)
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op(m)(n)) * 0.5)
val tt2putn1 = tt2putn.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts2 = TermState(tt2putn1,tt2putn1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(m)(n))))
val lp2 = LocalProver(ts2, cutoff = 0.00001).noIsles

val lem3 = lp2.lemmas.runSyncUnsafe()


Out[13]:
tt2putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(m, 0.05555555555555555),
    Weighted(n, 0.05555555555555555),
    Weighted(mul, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05555555555555555),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05555555555555555),
    Weighted(eqM, 0.25),
    Weighted(mul(m)(n), 0.25)
  )
)
tt2putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666667),
    Weighted(n, 0.06666666666666667),
    Weighted(mul, 0.06666666666666667),
    Weighted(eqM, 0.06666666666666667),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
    Weighted(eqM, 0.3),
    Weighted(mul(m)(n), 0.3)
  )
)
ts2: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666667),
      Weighted(n, 0.06666666666666667),
      Weighted(mul, 0.06666666666666667),
      Weighted(eqM, 0.06666666666666667),
      Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
      Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
      Weighted(eqM, 0.3),
      Weighted(mul(m)(n), 0.3)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666667),
      Weighted(M, 0.06666666666666667),
      Weighted((M → (M → M)), 0.06666666666666667),
      Weighted((M → (M → 𝒰 )), 0.06666666666666667),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
        0.06666666666666667
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
        0.06666666666666667
      ),
      Weighted((M → (M → 𝒰 )), 0.3),
      Weighted(M, 0.3)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 1.0))
  ),
  Empty
)
lp2: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666667),
        Weighted(n, 0.06666666666666667),
        Weighted(mul, 0.06666666666666667),
        Weighted(eqM, 0.06666666666666667),
        Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
        Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
        Weighted(eqM, 0.3),
        Weighted(mul(m)(n), 0.3)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666667),
        Weighted(M, 0.06666666666666667),
        Weighted((M → (M → M)), 0.06666666666666667),
        Weighted((M → (M → 𝒰 )), 0.06666666666666667),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
          0.06666666666666667
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
          0.06666666666666667
        ),
        Weighted((M → (M → 𝒰 )), 0.3),
        Weighted(M, 0.3)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 1.0))
    ),
    Empty
  ),
...
lem3: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.9036614962977492),
  (eqM(mul(mul(m)(n))(n))(m), 1.0248486491665673E-5)
)

In [14]:
val w = "lemma4" :: lem3(0)._1


Out[14]:
w: Term = lemma4

In [15]:
val stputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(a)(b) ->: eqM(b)(a),
 eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x, y,z) * 0.5)
val stputin1 = stputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts4 = TermState(stputin1,stputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))(n)) )
val lp4 = LocalProver(ts4, cutoff = 0.00001).noIsles

val lemI = lp4.lemmas.runSyncUnsafe()


Out[15]:
stputin: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(m, 0.05555555555555555),
    Weighted(n, 0.05555555555555555),
    Weighted(mul, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.125),
    Weighted(lemma1, 0.125),
    Weighted(lemma2, 0.125),
    Weighted(lemma3, 0.125)
  )
)
stputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666667),
    Weighted(n, 0.06666666666666667),
    Weighted(mul, 0.06666666666666667),
    Weighted(eqM, 0.06666666666666667),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.06666666666666667
    ),
    Weighted(eqM, 0.15),
    Weighted(lemma1, 0.15),
    Weighted(lemma2, 0.15),
    Weighted(lemma3, 0.15)
  )
)
ts4: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666667),
      Weighted(n, 0.06666666666666667),
      Weighted(mul, 0.06666666666666667),
      Weighted(eqM, 0.06666666666666667),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.06666666666666667
      ),
      Weighted(eqM, 0.15),
      Weighted(lemma1, 0.15),
      Weighted(lemma2, 0.15),
      Weighted(lemma3, 0.15)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666667),
      Weighted(M, 0.06666666666666667),
      Weighted((M → (M → M)), 0.06666666666666667),
      Weighted((M → (M → 𝒰 )), 0.06666666666666667),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.06666666666666667
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.06666666666666667
      ),
      Weighted((M → (M → 𝒰 )), 0.15),
      Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.15),
      Weighted(eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15),
      Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15)
    )
  ),
...
lp4: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666667),
        Weighted(n, 0.06666666666666667),
        Weighted(mul, 0.06666666666666667),
        Weighted(eqM, 0.06666666666666667),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.06666666666666667
        ),
        Weighted(eqM, 0.15),
        Weighted(lemma1, 0.15),
        Weighted(lemma2, 0.15),
        Weighted(lemma3, 0.15)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666667),
        Weighted(M, 0.06666666666666667),
        Weighted((M → (M → M)), 0.06666666666666667),
        Weighted((M → (M → 𝒰 )), 0.06666666666666667),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.06666666666666667
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.06666666666666667
        ),
        Weighted((M → (M → 𝒰 )), 0.15),
        Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.15),
        Weighted(eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15),
        Weighted(
          eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
...
lemI: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(m)(n))(m))(n), 0.9085367798328954),
  (eqM(m)(m), 0.0057629510380071665),
  (eqM(n)(n), 0.0057629510380071665)
)

In [16]:
val lI = "lemma5" :: lemI(0)._1


Out[16]:
lI: Term = lemma5

In [17]:
val s2tputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(b)(c) ->: eqM(op(b)(a))(op(c)(a))
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, lI) * 0.5)
val s2tputin1 = s2tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts5 = TermState(s2tputin1,s2tputin1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles
val lemI1 = lp5.lemmas.runSyncUnsafe()


Out[17]:
s2tputin: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.0625),
    Weighted(b, 0.0625),
    Weighted(c, 0.0625),
    Weighted(m, 0.0625),
    Weighted(n, 0.0625),
    Weighted(mul, 0.0625),
    Weighted(eqM, 0.0625),
    Weighted(axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))}, 0.0625),
    Weighted(eqM, 0.25),
    Weighted(lemma5, 0.25)
  )
)
s2tputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.07692307692307693),
    Weighted(n, 0.07692307692307693),
    Weighted(mul, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
      0.07692307692307693
    ),
    Weighted(eqM, 0.3076923076923077),
    Weighted(lemma5, 0.3076923076923077)
  )
)
ts5: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.07692307692307693),
      Weighted(n, 0.07692307692307693),
      Weighted(mul, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(
        axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
        0.07692307692307693
      ),
      Weighted(eqM, 0.3076923076923077),
      Weighted(lemma5, 0.3076923076923077)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.07692307692307693),
      Weighted(M, 0.07692307692307693),
      Weighted((M → (M → M)), 0.07692307692307693),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(b)(a))(mul(c)(a))) } } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.3076923076923077),
      Weighted(eqM(mul(mul(m)(n))(m))(n), 0.3076923076923077)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 1.0))
  ),
  Empty
)
lp5: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.07692307692307693),
        Weighted(n, 0.07692307692307693),
        Weighted(mul, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(
          axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
          0.07692307692307693
        ),
        Weighted(eqM, 0.3076923076923077),
        Weighted(lemma5, 0.3076923076923077)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.07692307692307693),
        Weighted(M, 0.07692307692307693),
        Weighted((M → (M → M)), 0.07692307692307693),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(b)(a))(mul(c)(a))) } } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.3076923076923077),
        Weighted(eqM(mul(mul(m)(n))(m))(n), 0.3076923076923077)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 1.0))
    ),
    Empty
  ),
  TermGenParams(
...
lemI1: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.9002505096459986)
)

In [18]:
val lI1 = "lemma6" :: lemI1(0)._1


Out[18]:
lI1: Term = lemma6

In [19]:
val finalstputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(a)(b) ->: eqM(b)(a),
 eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, w, lI1) * 0.5)
val finalstputin1 = finalstputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts5 = TermState(finalstputin1,finalstputin1.map(_.typ), goals = FD.unif(eqM(op(m)(n))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles
lp5.lemmas.runSyncUnsafe()


Out[19]:
finalstputin: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(m, 0.05555555555555555),
    Weighted(n, 0.05555555555555555),
    Weighted(mul, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.16666666666666666),
    Weighted(lemma4, 0.16666666666666666),
    Weighted(lemma6, 0.16666666666666666)
  )
)
finalstputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666668),
    Weighted(n, 0.06666666666666668),
    Weighted(mul, 0.06666666666666668),
    Weighted(eqM, 0.06666666666666668),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.06666666666666668
    ),
    Weighted(eqM, 0.2),
    Weighted(lemma4, 0.2),
    Weighted(lemma6, 0.2)
  )
)
ts5: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666668),
      Weighted(n, 0.06666666666666668),
      Weighted(mul, 0.06666666666666668),
      Weighted(eqM, 0.06666666666666668),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.06666666666666668
      ),
      Weighted(eqM, 0.2),
      Weighted(lemma4, 0.2),
      Weighted(lemma6, 0.2)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666668),
      Weighted(M, 0.06666666666666668),
      Weighted((M → (M → M)), 0.06666666666666668),
      Weighted((M → (M → 𝒰 )), 0.06666666666666668),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.06666666666666668
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.06666666666666668
      ),
      Weighted((M → (M → 𝒰 )), 0.2),
      Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.2),
      Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.2)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...
lp5: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666668),
        Weighted(n, 0.06666666666666668),
        Weighted(mul, 0.06666666666666668),
        Weighted(eqM, 0.06666666666666668),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.06666666666666668
        ),
        Weighted(eqM, 0.2),
        Weighted(lemma4, 0.2),
        Weighted(lemma6, 0.2)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666668),
        Weighted(M, 0.06666666666666668),
        Weighted((M → (M → M)), 0.06666666666666668),
        Weighted((M → (M → 𝒰 )), 0.06666666666666668),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.06666666666666668
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.06666666666666668
        ),
        Weighted((M → (M → 𝒰 )), 0.2),
        Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.2),
        Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.2)
      )
    ),
    Vector(),
...
res18_4: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(m)(n))(mul(n)(m)), 0.9118516347852311)
)

$ m*n = n*m $ is generated as a lemma in the last LocalProver.


In [ ]: