Search for blocks/addresses/...

Proofgold Asset

asset id
dfa18bb54f301ecd1cff93714b4c4fe38886594a0285287aefd7c6b0a9436084
asset hash
7cd4fa262e3007b36fb94886b1e48382dd95e11c68c9c2adf96247ccc6d9675f
bday / block
25627
tx
f1bf4..
preasset
doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param minus_SNominus_SNo : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Conjecture c0a4c..A53464 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15)(∀ x15 . x15intx1 x15 = add_SNo x15 (minus_SNo 1))(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) (x2 x15))(∀ x15 . x15intx5 x15 = x4 x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = add_SNo x15 (minus_SNo 1))(∀ x15 . x15intx9 x15 = x15)x10 = add_SNo 1 (add_SNo 2 2)(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = x13 x15)∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture a3d52..A53422 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo 1 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15)))(∀ x15 . x15intx1 x15 = x15)x2 = 0(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = mul_SNo (x4 x15) x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = add_SNo 1 (mul_SNo x15 x16))(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = add_SNo x15 (minus_SNo 1))x9 = 1x10 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) x9 x10)(∀ x15 . x15intx14 x15 = mul_SNo x15 (x13 x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture f60f5..A533 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15))(∀ x15 . x15intx1 x15 = x15)x2 = 1(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = add_SNo 1 (If_i (SNoLe x15 0) 0 (x4 x15)))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 1x10 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) x9 x10)(∀ x15 . x15intx14 x15 = add_SNo 1 (If_i (SNoLe x15 0) 0 (x13 x15)))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture b96c4..A53220 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15int∀ x16 . x16intx0 x15 x16 = add_SNo (add_SNo x15 x15) x16)x1 = 0(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15intx3 x15 = add_SNo 1 x15)(∀ x15 . x15intx4 x15 = x15)(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx5 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x0 (x5 (add_SNo x15 (minus_SNo 1)) x16 x17) (x6 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx6 x15 x16 x17 = If_i (SNoLe x15 0) x17 x1)(∀ x15 . x15intx7 x15 = x5 (x2 x15) (x3 x15) (x4 x15))(∀ x15 . x15intx8 x15 = x7 x15)(∀ x15 . x15intx9 x15 = add_SNo x15 x15)(∀ x15 . x15intx10 x15 = add_SNo x15 (minus_SNo 1))(∀ x15 . x15intx11 x15 = add_SNo 2 (add_SNo (add_SNo x15 x15) x15))(∀ x15 . x15int∀ x16 . x16intx12 x15 x16 = If_i (SNoLe x15 0) x16 (x9 (x12 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx13 x15 = x12 (x10 x15) (x11 x15))(∀ x15 . x15intx14 x15 = If_i (SNoLe x15 0) 1 (x13 x15))∀ x15 . x15intSNoLe 0 x15x8 x15 = x14 x15
Conjecture b6ae7..A52951 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15int∀ x16 . x16intx0 x15 x16 = add_SNo (add_SNo x15 x15) x16)x1 = 1(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15intx3 x15 = x15)x4 = 2(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx5 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x0 (x5 (add_SNo x15 (minus_SNo 1)) x16 x17) (x6 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx6 x15 x16 x17 = If_i (SNoLe x15 0) x17 x1)(∀ x15 . x15intx7 x15 = x5 (x2 x15) (x3 x15) x4)(∀ x15 . x15intx8 x15 = add_SNo 1 (x7 x15))(∀ x15 . x15intx9 x15 = add_SNo x15 x15)(∀ x15 . x15intx10 x15 = add_SNo x15 (minus_SNo 1))(∀ x15 . x15intx11 x15 = add_SNo 1 (add_SNo 2 (add_SNo x15 x15)))(∀ x15 . x15int∀ x16 . x16intx12 x15 x16 = If_i (SNoLe x15 0) x16 (x9 (x12 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx13 x15 = x12 (x10 x15) (x11 x15))(∀ x15 . x15intx14 x15 = If_i (SNoLe x15 0) 1 (x13 x15))∀ x15 . x15intSNoLe 0 x15x8 x15 = x14 x15
Conjecture 88f65..A52850 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx1 x22 = add_SNo x22 (minus_SNo 1))(∀ x22 . x22intx2 x22 = add_SNo x22 x22)(∀ x22 . x22intx3 x22 = x22)x4 = 1(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo (add_SNo (x6 x22) (minus_SNo 1)) x22)(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = add_SNo x22 x22)(∀ x22 . x22intx12 x22 = x22)x13 = 1(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x14 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx15 x22 = x14 (x12 x22) x13)(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx17 x22 = add_SNo x22 (minus_SNo 1))x18 = 1(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x16 (x19 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx20 x22 = x19 (x17 x22) x18)(∀ x22 . x22intx21 x22 = mul_SNo (add_SNo (add_SNo (x15 x22) (minus_SNo 1)) x22) (x20 x22))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture bc5e6..A52832 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = add_SNo x28 (minus_SNo 1))(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = add_SNo x28 (minus_SNo 1))x5 = 1x6 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = add_SNo (x9 x28) (minus_SNo 1))(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28intx16 x28 = add_SNo x28 (minus_SNo 1))x17 = 1x18 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = add_SNo x28 (minus_SNo 1))x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (add_SNo (x21 x28) (minus_SNo 1)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture bfa1d..A52677 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo (mul_SNo 2 (add_SNo x28 x28)) (minus_SNo x29))(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = x28)x5 = 1x6 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo (mul_SNo 2 (add_SNo x28 x28)) (minus_SNo x29))(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28intx16 x28 = add_SNo x28 (minus_SNo 1))x17 = add_SNo 1 2x18 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (If_i (SNoLe x28 0) 1 (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture dd497..A52661 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx4 x28 = x28)x5 = 1x6 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = add_SNo 1 (x9 x28))(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx15 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx16 x28 = x28)x17 = 1x18 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (add_SNo 1 (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture 8de98..A52635 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = add_SNo (add_SNo (add_SNo x28 x29) x29) x29)(∀ x28 . x28intx4 x28 = x28)x5 = 1x6 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo (add_SNo (add_SNo x28 x28) x28) x29)(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28intx16 x28 = add_SNo x28 (minus_SNo 1))x17 = 0x18 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (If_i (SNoLe x28 0) 1 (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture ee7c0..A52606 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo (mul_SNo 2 (add_SNo x28 x28)) (minus_SNo x29))(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = add_SNo x28 (minus_SNo 1))(∀ x28 . x28intx5 x28 = If_i (SNoLe x28 0) 1 2)x6 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) (x5 x28) x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo (mul_SNo 2 (add_SNo x28 x28)) (minus_SNo x29))(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28intx16 x28 = add_SNo x28 (minus_SNo 1))x17 = 2x18 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (If_i (SNoLe x28 0) 1 (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture e2ad3..A52584 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = add_SNo x22 x22)(∀ x22 . x22intx3 x22 = add_SNo x22 (minus_SNo 1))x4 = 1(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo 1 (x6 x22))(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = add_SNo x22 x22)(∀ x22 . x22intx12 x22 = add_SNo x22 (minus_SNo 1))x13 = 1(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x14 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx15 x22 = x14 (x12 x22) x13)(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx17 x22 = x22)x18 = 1(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x16 (x19 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx20 x22 = x19 (x17 x22) x18)(∀ x22 . x22intx21 x22 = mul_SNo (add_SNo 1 (x15 x22)) (x20 x22))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 30d4f..A52482 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx2 x17 x18 = add_SNo x17 x18)(∀ x17 . x17intx3 x17 = add_SNo 2 x17)x4 = 0(∀ x17 . x17int∀ x18 . x18intx5 x17 x18 = If_i (SNoLe x17 0) x18 (x2 (x5 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx6 x17 = x5 (x3 x17) x4)(∀ x17 . x17intx7 x17 = x6 x17)(∀ x17 . x17int∀ x18 . x18intx8 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x8 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx9 x17 = x8 (x1 x17) (x7 x17))(∀ x17 . x17intx10 x17 = x9 x17)(∀ x17 . x17intx11 x17 = add_SNo x17 x17)(∀ x17 . x17intx12 x17 = add_SNo x17 (minus_SNo 1))(∀ x17 . x17intx13 x17 = add_SNo 2 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x11 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 (x12 x17) (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo (add_SNo 1 (add_SNo 2 x17)) (If_i (SNoLe x17 0) 1 (x15 x17)))∀ x17 . x17intSNoLe 0 x17x10 x17 = x16 x17
Conjecture fa3b4..A50915 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)(∀ x17 . x17intx2 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) (x2 x17))(∀ x17 . x17intx5 x17 = add_SNo 1 (x4 x17))(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = add_SNo x17 (minus_SNo 1))x10 = 2(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = add_SNo 1 (mul_SNo (x15 x17) x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 31702..A5062 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 . x21int∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)(∀ x26 . x26int∀ x27 . x27intx0 x26 x27 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x26 x26)) x26) x27)(∀ x26 . x26int∀ x27 . x27intx1 x26 x27 = mul_SNo 2 (add_SNo (add_SNo x27 x27) x27))(∀ x26 . x26intx2 x26 = x26)x3 = 0x4 = 1(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx5 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x0 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx6 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x1 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx7 x26 = x5 (x2 x26) x3 x4)(∀ x26 . x26intx8 x26 = x7 x26)(∀ x26 . x26int∀ x27 . x27intx9 x26 x27 = mul_SNo x26 x27)(∀ x26 . x26int∀ x27 . x27intx10 x26 x27 = x27)(∀ x26 . x26intx11 x26 = x26)x12 = 1x13 = add_SNo 2 (add_SNo 2 2)(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx14 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x9 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx15 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x10 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx16 x26 = x14 (x11 x26) x12 x13)(∀ x26 . x26int∀ x27 . x27intx17 x26 x27 = mul_SNo x26 x27)(∀ x26 . x26int∀ x27 . x27intx18 x26 x27 = x27)(∀ x26 . x26intx19 x26 = x26)x20 = 1x21 = add_SNo 1 (add_SNo 2 2)(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx22 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x17 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx23 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x18 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx24 x26 = x22 (x19 x26) x20 x21)(∀ x26 . x26intx25 x26 = add_SNo (x16 x26) (minus_SNo (x24 x26)))∀ x26 . x26intSNoLe 0 x26x8 x26 = x25 x26
Conjecture 19951..A50621 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι → ι . (∀ x19 . x19int∀ x20 . x20int∀ x21 . x21intx18 x19 x20 x21int)∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo x25 x25)(∀ x25 . x25intx1 x25 = x25)(∀ x25 . x25intx2 x25 = add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25)(∀ x25 . x25intx3 x25 = x25)x4 = 1(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = If_i (SNoLe x25 0) x26 (x2 (x5 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx6 x25 = x5 (x3 x25) x4)(∀ x25 . x25intx7 x25 = add_SNo 1 (x6 x25))(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x1 x25) (x7 x25))(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = x26)(∀ x25 . x25intx15 x25 = x25)x16 = 1x17 = add_SNo 1 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx20 x25 = x18 (x15 x25) x16 x17)(∀ x25 . x25intx21 x25 = add_SNo 1 (x20 x25))(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 (x12 x25) (x21 x25))(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture b53ef..A5060 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 . x21int∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x28 x28)) (mul_SNo x29 x29)) x28)(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = add_SNo x29 x29)(∀ x28 . x28intx2 x28 = x28)x3 = 0x4 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx5 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x0 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30) (x6 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx6 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x1 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30) (x6 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx7 x28 = x5 (x2 x28) x3 x4)(∀ x28 . x28intx8 x28 = x7 x28)(∀ x28 . x28int∀ x29 . x29intx9 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx10 x28 x29 = x29)(∀ x28 . x28intx11 x28 = x28)x12 = 1x13 = add_SNo 1 (add_SNo 2 2)(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx14 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x9 (x14 (add_SNo x28 (minus_SNo 1)) x29 x30) (x15 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx15 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x10 (x14 (add_SNo x28 (minus_SNo 1)) x29 x30) (x15 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx16 x28 = x14 (x11 x28) x12 x13)(∀ x28 . x28intx17 x28 = mul_SNo x28 x28)x18 = 1(∀ x28 . x28intx19 x28 = add_SNo x28 x28)(∀ x28 . x28intx20 x28 = x28)x21 = 1(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = If_i (SNoLe x28 0) x29 (x19 (x22 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx23 x28 = x22 (x20 x28) x21)(∀ x28 . x28intx24 x28 = x23 x28)(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x17 (x25 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx26 x28 = x25 x18 (x24 x28))(∀ x28 . x28intx27 x28 = add_SNo (x16 x28) (minus_SNo (x26 x28)))∀ x28 . x28intSNoLe 0 x28x8 x28 = x27 x28
Conjecture 74df6..A49678 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 . x21int∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)(∀ x26 . x26int∀ x27 . x27intx0 x26 x27 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x26 x26) x26)) (minus_SNo x27)) x26)(∀ x26 . x26intx1 x26 = x26)(∀ x26 . x26intx2 x26 = add_SNo x26 x26)x3 = 1x4 = 0(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx5 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x0 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx6 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x1 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx7 x26 = x5 (x2 x26) x3 x4)(∀ x26 . x26intx8 x26 = x7 x26)(∀ x26 . x26int∀ x27 . x27intx9 x26 x27 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x26 x26) x26)) (minus_SNo x27)) x26)(∀ x26 . x26intx10 x26 = x26)(∀ x26 . x26intx11 x26 = add_SNo x26 (minus_SNo 1))(∀ x26 . x26intx12 x26 = If_i (SNoLe x26 0) 1 (add_SNo 2 (add_SNo 2 2)))x13 = 1(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx14 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x9 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx15 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x10 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx16 x26 = x14 (x11 x26) (x12 x26) x13)(∀ x26 . x26int∀ x27 . x27intx17 x26 x27 = add_SNo x26 x27)(∀ x26 . x26intx18 x26 = x26)(∀ x26 . x26intx19 x26 = mul_SNo 2 (add_SNo x26 x26))x20 = 1x21 = 1(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx22 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x17 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx23 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x18 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx24 x26 = x22 (x19 x26) x20 x21)(∀ x26 . x26intx25 x26 = mul_SNo (x16 x26) (x24 x26))∀ x26 . x26intSNoLe 0 x26x8 x26 = x25 x26
Conjecture c2d1c..A49670 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 . x16int∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = add_SNo 2 (mul_SNo x28 x28))x1 = 2x2 = add_SNo 1 2(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28int∀ x29 . x29intx5 x28 x29 = add_SNo (mul_SNo x4 x28) (minus_SNo x29))(∀ x28 . x28intx6 x28 = x28)(∀ x28 . x28intx7 x28 = x28)x8 = 0x9 = add_SNo 1 (minus_SNo 2)(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx10 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x5 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30) (x11 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx11 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x6 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx12 x28 = x10 (x7 x28) x8 x9)(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28intx14 x28 = mul_SNo (mul_SNo x28 x28) x28)x15 = 1x16 = add_SNo 1 (add_SNo 2 2)(∀ x28 . x28int∀ x29 . x29intx17 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x17 (add_SNo x28 (minus_SNo 1)) x29)))x18 = x17 x15 x16(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo (mul_SNo (add_SNo x18 (minus_SNo 2)) x28) (minus_SNo x29))(∀ x28 . x28intx20 x28 = x28)(∀ x28 . x28intx21 x28 = add_SNo x28 (minus_SNo 1))(∀ x28 . x28intx22 x28 = If_i (SNoLe x28 0) 0 1)x23 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) (x22 x28) x23)(∀ x28 . x28intx27 x28 = x26 x28)∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture 5e293..A49668 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 . x5int∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = x24)(∀ x23 . x23intx1 x23 = add_SNo 1 (add_SNo x23 x23))x2 = add_SNo 2 2x3 = 2(∀ x23 . x23int∀ x24 . x24intx4 x23 x24 = If_i (SNoLe x23 0) x24 (x1 (x4 (add_SNo x23 (minus_SNo 1)) x24)))x5 = x4 x2 x3(∀ x23 . x23int∀ x24 . x24intx6 x23 x24 = add_SNo (mul_SNo x5 x24) (minus_SNo x23))(∀ x23 . x23intx7 x23 = x23)x8 = 0x9 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x6 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx12 x23 = x10 (x7 x23) x8 x9)(∀ x23 . x23intx13 x23 = x12 x23)(∀ x23 . x23int∀ x24 . x24intx14 x23 x24 = add_SNo (mul_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))))) (minus_SNo 1)) x23) (minus_SNo x24))(∀ x23 . x23intx15 x23 = x23)(∀ x23 . x23intx16 x23 = add_SNo x23 (minus_SNo 1))(∀ x23 . x23intx17 x23 = If_i (SNoLe x23 0) 0 1)x18 = 0(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx21 x23 = x19 (x16 x23) (x17 x23) x18)(∀ x23 . x23intx22 x23 = x21 x23)∀ x23 . x23intSNoLe 0 x23x13 x23 = x22 x23