tg1: TermGenParams = TermGenParams(
0.1,
0.1,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.3,
0.7,
0.5,
0.0,
0.0,
0.0
)
import library._, MonoidSimple._
ts: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(e_l, 0.047619047619047616),
Weighted(e_r, 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(e_l)(a))(a)}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
Weighted(eqM, 0.2857142857142857),
Weighted(mul, 0.2857142857142857)
)
),
FiniteDistribution(
Vector(
Weighted(M, 0.047619047619047616),
Weighted(M, 0.047619047619047616),
Weighted((M → (M → M)), 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.047619047619047616),
Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
Weighted(
∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
0.047619047619047616
),
Weighted(
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
0.047619047619047616
),
Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.2857142857142857),
Weighted((M → (M → M)), 0.2857142857142857)
...
lp1: LocalProver = LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(e_l, 0.047619047619047616),
Weighted(e_r, 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(e_l)(a))(a)}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
Weighted(eqM, 0.2857142857142857),
Weighted(mul, 0.2857142857142857)
)
),
FiniteDistribution(
Vector(
Weighted(M, 0.047619047619047616),
Weighted(M, 0.047619047619047616),
Weighted((M → (M → M)), 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.047619047619047616),
Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
Weighted(
∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
0.047619047619047616
),
Weighted(
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
0.047619047619047616
),
Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.2857142857142857),
...