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 [ ]: