Search for blocks/addresses/...

Proofgold Address

address
PUhRgd4HisU11DfEGwsWDLeS9NAG7QxoeYx
total
0
mg
-
conjpub
-
current assets
b0aa0../0b044.. bday: 25651 doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Param mul_SNomul_SNo : ιιι
Conjecture d3d27..A198960 : ∀ 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 2 (add_SNo (add_SNo x15 x15) x15))(∀ x15 . x15intx1 x15 = add_SNo x15 x15)x2 = 2(∀ 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 = x4 x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = add_SNo 1 2x10 = add_SNo 1 (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 (x13 x15) (minus_SNo 1))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture ba6bb..A198857 : ∀ 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 . 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 1 (add_SNo x17 x17))(∀ x17 . x17intx1 x17 = add_SNo 1 (add_SNo (add_SNo x17 x17) x17))x2 = add_SNo 2 2(∀ 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 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ 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 (mul_SNo 2 (mul_SNo (add_SNo 1 (add_SNo 2 2)) (x15 x17))) (minus_SNo 1))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture f1ca5..A198855 : ∀ 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 . 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 1 (add_SNo x17 x17))(∀ x17 . x17intx1 x17 = add_SNo (add_SNo x17 x17) x17)x2 = add_SNo 2 (add_SNo 2 2)(∀ 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 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ 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 (mul_SNo (add_SNo 1 (add_SNo 2 (add_SNo 2 2))) (x15 x17)) (minus_SNo 1))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 38ba3..A198854 : ∀ 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 . 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 1 (add_SNo x17 x17))(∀ x17 . x17intx1 x17 = add_SNo 1 (add_SNo (add_SNo x17 x17) x17))x2 = 2(∀ 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 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ 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 (mul_SNo 2 (mul_SNo (add_SNo 1 2) (x15 x17))) (minus_SNo 1))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture b613a..A198845 : ∀ 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 (add_SNo x15 x15) x15))(∀ x15 . x15intx1 x15 = x15)x2 = 2(∀ 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 (mul_SNo 2 (mul_SNo 2 (x4 x15))) (minus_SNo 1))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 2x10 = add_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 (mul_SNo 2 (mul_SNo 2 (x13 x15))) (minus_SNo 1))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 787f3..A198797 : ∀ 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 (add_SNo x15 x15) x15))(∀ x15 . x15intx1 x15 = x15)x2 = 2(∀ 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 (mul_SNo 2 (x4 x15)) (minus_SNo 1))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 2x10 = add_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 (mul_SNo 2 (x13 x15)) (minus_SNo 1))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 12462..A19869 : ∀ 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 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (add_SNo (x14 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx16 x50 = x50)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 (x16 x50) x17)(∀ x50 . x50intx20 x50 = x19 x50)(∀ x50 . x50intx21 x50 = add_SNo x50 x50)(∀ x50 . x50intx22 x50 = x50)x23 = 2(∀ x50 . x50int∀ x51 . x51intx24 x50 x51 = If_i (SNoLe x50 0) x51 (x21 (x24 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx25 x50 = x24 (x22 x50) x23)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = x51)(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 2 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = mul_SNo (add_SNo (x25 x50) (minus_SNo 1)) (x33 x50))x35 = 1(∀ x50 . x50int∀ x51 . x51intx36 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx38 x50 x51 = x37 x35 (x36 x50 x51))(∀ x50 . x50int∀ x51 . x51intx39 x50 x51 = add_SNo (add_SNo (x38 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx40 x50 = x50)x41 = 1(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx43 x50 = x42 (x40 x50) x41)(∀ x50 . x50intx44 x50 = x43 x50)x45 = 1(∀ x50 . x50intx46 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx48 x50 = x47 x45 (x46 x50))(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x20 x50 = x49 x50
Conjecture 77466..A198692 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ 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 . x19intx0 x18 x19 = add_SNo (mul_SNo (add_SNo 1 2) (add_SNo (add_SNo x18 x18) x19)) x18)x1 = 2(∀ x18 . x18intx2 x18 = add_SNo 1 x18)x3 = 1x4 = 1(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx5 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x0 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx6 x18 x19 x20 = If_i (SNoLe x18 0) x20 x1)(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 x4)(∀ x18 . x18intx8 x18 = x7 x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = mul_SNo x18 x19)(∀ x18 . x18int∀ x19 . x19intx10 x18 x19 = x19)(∀ x18 . x18intx11 x18 = x18)x12 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))x13 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) x12 x13)(∀ x18 . x18intx17 x18 = add_SNo (x16 x18) (minus_SNo 1))∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 3e393..A198647 : ∀ 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 (mul_SNo 2 (mul_SNo (add_SNo 1 2) (add_SNo 1 x15))) x15)(∀ x15 . x15intx1 x15 = x15)x2 = 2(∀ 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 = x4 x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = add_SNo 1 2x10 = add_SNo 1 (add_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 (x13 x15) (minus_SNo 1))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 7a008..A19854 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ 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 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40int∀ x41 . x41intx0 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x1 = 2(∀ x40 . x40intx2 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx4 x40 = x3 x1 (x2 x40))(∀ x40 . x40intx5 x40 = add_SNo (x4 x40) (minus_SNo x40))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = mul_SNo 2 (add_SNo (add_SNo x41 x41) x41))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 2 (add_SNo 2 2)(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) x40) (mul_SNo (add_SNo (mul_SNo (mul_SNo x40 2) 2) x40) 2))(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture 820e6..A19839 : ∀ 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 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45)(∀ x45 . x45intx1 x45 = x45)(∀ x45 . x45intx2 x45 = add_SNo x45 x45)(∀ x45 . x45intx3 x45 = x45)x4 = 2(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = If_i (SNoLe x45 0) x46 (x2 (x5 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx6 x45 = x5 (x3 x45) x4)(∀ x45 . x45intx7 x45 = add_SNo (x6 x45) (minus_SNo 1))(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx9 x45 = x8 (x1 x45) (x7 x45))(∀ x45 . x45intx10 x45 = x9 x45)x11 = 1(∀ x45 . x45int∀ x46 . x46intx12 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx14 x45 x46 = x13 x11 (x12 x45 x46))(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = add_SNo (x14 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = x19 x45)(∀ x45 . x45intx21 x45 = add_SNo x45 x45)(∀ x45 . x45intx22 x45 = x45)x23 = 2(∀ x45 . x45int∀ x46 . x46intx24 x45 x46 = If_i (SNoLe x45 0) x46 (x21 (x24 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx25 x45 = x24 (x22 x45) x23)(∀ x45 . x45int∀ x46 . x46intx26 x45 x46 = mul_SNo x45 x46)(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = x46)(∀ x45 . x45intx28 x45 = x45)x29 = 1x30 = add_SNo 1 (add_SNo 2 2)(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx33 x45 = x31 (x28 x45) x29 x30)(∀ x45 . x45intx34 x45 = mul_SNo (add_SNo (x25 x45) (minus_SNo 1)) (x33 x45))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture a65ac..A19793 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 . x28int∀ x29 : ι → ι → ι → ι . (∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx29 x30 x31 x32int)∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43intx0 x43 = add_SNo (add_SNo x43 x43) x43)(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)x2 = 1(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx4 x43 x44 = x3 (x1 x43 x44) x2)(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (x4 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43)))(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = x44)x7 = 1(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = If_i (SNoLe x43 0) x44 (x5 (x8 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = x8 (x6 x43 x44) x7)(∀ x43 . x43int∀ x44 . x44intx10 x43 x44 = add_SNo (add_SNo (x9 x43 x44) (mul_SNo 2 (add_SNo x43 x43))) x43)(∀ x43 . x43intx11 x43 = x43)x12 = 1(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = If_i (SNoLe x43 0) x44 (x10 (x13 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx14 x43 = x13 (x11 x43) x12)(∀ x43 . x43intx15 x43 = x14 x43)(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = add_SNo (add_SNo (add_SNo x43 x43) x43) x44)(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = add_SNo x44 x44)(∀ x43 . x43intx18 x43 = x43)x19 = 1x20 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx21 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x16 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx22 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x17 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx23 x43 = x21 (x18 x43) x19 x20)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = x44)(∀ x43 . x43intx26 x43 = x43)x27 = 1x28 = add_SNo 1 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx31 x43 = x29 (x26 x43) x27 x28)(∀ x43 . x43intx32 x43 = mul_SNo (x23 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo x43 x43))) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x15 x43 = x42 x43
Conjecture 9cf16..A197130 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ 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 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)(∀ x27 . x27int∀ x28 . x28intx0 x27 x28 = mul_SNo 2 (mul_SNo x27 x28))(∀ x27 . x27int∀ x28 . x28intx1 x27 x28 = x28)x2 = 1(∀ x27 . x27int∀ x28 . x28intx3 x27 x28 = If_i (SNoLe x27 0) x28 (x0 (x3 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx4 x27 x28 = x3 (x1 x27 x28) x2)(∀ x27 . x27int∀ x28 . x28intx5 x27 x28 = add_SNo (mul_SNo (add_SNo (x4 x27 x28) x27) (add_SNo 1 (add_SNo x28 x28))) x27)(∀ x27 . x27intx6 x27 = x27)x7 = 1(∀ x27 . x27int∀ x28 . x28intx8 x27 x28 = If_i (SNoLe x27 0) x28 (x5 (x8 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx9 x27 = x8 (x6 x27) x7)(∀ x27 . x27intx10 x27 = x9 x27)(∀ x27 . x27int∀ x28 . x28intx11 x27 x28 = mul_SNo x27 x28)(∀ x27 . x27int∀ x28 . x28intx12 x27 x28 = add_SNo x28 (minus_SNo 1))(∀ x27 . x27int∀ x28 . x28intx13 x27 x28 = x28)(∀ x27 . x27int∀ x28 . x28intx14 x27 x28 = If_i (SNoLe x27 0) x28 (x11 (x14 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx15 x27 x28 = x14 (x12 x27 x28) (x13 x27 x28))(∀ x27 . x27int∀ x28 . x28intx16 x27 x28 = add_SNo (mul_SNo (add_SNo (x15 x27 x28) x27) x28) x27)(∀ x27 . x27intx17 x27 = x27)(∀ x27 . x27intx18 x27 = add_SNo 1 x27)(∀ x27 . x27int∀ x28 . x28intx19 x27 x28 = If_i (SNoLe x27 0) x28 (x16 (x19 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx20 x27 = x19 (x17 x27) (x18 x27))(∀ x27 . x27intx21 x27 = add_SNo x27 x27)(∀ x27 . x27intx22 x27 = x27)x23 = 1(∀ x27 . x27int∀ x28 . x28intx24 x27 x28 = If_i (SNoLe x27 0) x28 (x21 (x24 (add_SNo x27 (minus_SNo 1)) x28)))(∀ x27 . x27intx25 x27 = x24 (x22 x27) x23)(∀ x27 . x27intx26 x27 = mul_SNo (x20 x27) (x25 x27))∀ x27 . x27intSNoLe 0 x27x10 x27 = x26 x27
Conjecture 9928a..A19687 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40intx0 x40 = add_SNo (add_SNo x40 x40) x40)(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = add_SNo x41 x41)x2 = 1(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx4 x40 x41 = x3 (x1 x40 x41) x2)(∀ x40 . x40int∀ x41 . x41intx5 x40 x41 = add_SNo (x4 x40 x41) (mul_SNo 2 (add_SNo x40 x40)))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x11 = 2(∀ x40 . x40intx12 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx14 x40 = x13 x11 (x12 x40))(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x9 x40 x41) (minus_SNo x40)) (x14 x40))(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (mul_SNo 2 (add_SNo x40 x40)) (mul_SNo x41 x41))(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo (add_SNo x41 x41) x41)(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) x40) (mul_SNo (add_SNo (mul_SNo (add_SNo x40 x40) 2) x40) 2))(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture 3f8cd..A19682 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)(∀ x35 . x35intx0 x35 = add_SNo (add_SNo x35 x35) x35)(∀ x35 . x35int∀ x36 . x36intx1 x35 x36 = add_SNo x36 x36)x2 = 1(∀ x35 . x35int∀ x36 . x36intx3 x35 x36 = If_i (SNoLe x35 0) x36 (x0 (x3 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35int∀ x36 . x36intx4 x35 x36 = x3 (x1 x35 x36) x2)(∀ x35 . x35int∀ x36 . x36intx5 x35 x36 = add_SNo (x4 x35 x36) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x35 x35)) x35)))(∀ x35 . x35int∀ x36 . x36intx6 x35 x36 = x36)x7 = 1(∀ x35 . x35int∀ x36 . x36intx8 x35 x36 = If_i (SNoLe x35 0) x36 (x5 (x8 (add_SNo x35 (minus_SNo 1)) x36) x35))(∀ x35 . x35int∀ x36 . x36intx9 x35 x36 = x8 (x6 x35 x36) x7)(∀ x35 . x35int∀ x36 . x36intx10 x35 x36 = add_SNo (x9 x35 x36) (mul_SNo 2 (add_SNo x35 x35)))(∀ x35 . x35intx11 x35 = x35)x12 = 1(∀ x35 . x35int∀ x36 . x36intx13 x35 x36 = If_i (SNoLe x35 0) x36 (x10 (x13 (add_SNo x35 (minus_SNo 1)) x36) x35))(∀ x35 . x35intx14 x35 = x13 (x11 x35) x12)(∀ x35 . x35intx15 x35 = x14 x35)(∀ x35 . x35int∀ x36 . x36intx16 x35 x36 = add_SNo (mul_SNo 2 (add_SNo x35 x35)) (mul_SNo x36 x36))(∀ x35 . x35int∀ x36 . x36intx17 x35 x36 = add_SNo (add_SNo x36 x36) x36)(∀ x35 . x35intx18 x35 = x35)x19 = 1x20 = add_SNo 1 2(∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx21 x35 x36 x37 = If_i (SNoLe x35 0) x36 (x16 (x21 (add_SNo x35 (minus_SNo 1)) x36 x37) (x22 (add_SNo x35 (minus_SNo 1)) x36 x37)))(∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx22 x35 x36 x37 = If_i (SNoLe x35 0) x37 (x17 (x21 (add_SNo x35 (minus_SNo 1)) x36 x37) (x22 (add_SNo x35 (minus_SNo 1)) x36 x37)))(∀ x35 . x35intx23 x35 = x21 (x18 x35) x19 x20)(∀ x35 . x35intx24 x35 = x23 x35)x25 = 1(∀ x35 . x35int∀ x36 . x36intx26 x35 x36 = x36)(∀ x35 . x35int∀ x36 . x36intx27 x35 x36 = If_i (SNoLe x35 0) x36 (x24 (x27 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35int∀ x36 . x36intx28 x35 x36 = x27 x25 (x26 x35 x36))(∀ x35 . x35int∀ x36 . x36intx29 x35 x36 = add_SNo (x28 x35 x36) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x35 x35)) x35)))(∀ x35 . x35intx30 x35 = x35)x31 = 1(∀ x35 . x35int∀ x36 . x36intx32 x35 x36 = If_i (SNoLe x35 0) x36 (x29 (x32 (add_SNo x35 (minus_SNo 1)) x36) x35))(∀ x35 . x35intx33 x35 = x32 (x30 x35) x31)(∀ x35 . x35intx34 x35 = x33 x35)∀ x35 . x35intSNoLe 0 x35x15 x35 = x34 x35
Conjecture 446a9..A196666 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ 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 : ι → ι . (∀ 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 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 2 x24)) x24)) x24) x23)x1 = 2(∀ x23 . x23intx2 x23 = x23)x3 = 1x4 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 x1)(∀ x23 . x23intx7 x23 = x5 (x2 x23) x3 x4)(∀ x23 . x23intx8 x23 = x7 x23)(∀ x23 . x23int∀ x24 . x24intx9 x23 x24 = mul_SNo x23 x24)(∀ x23 . x23int∀ x24 . x24intx10 x23 x24 = x24)(∀ x23 . x23intx11 x23 = add_SNo x23 (minus_SNo 1))(∀ x23 . x23intx12 x23 = If_i (SNoLe x23 0) 1 (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) (minus_SNo 1)))x13 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx14 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x9 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx15 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x10 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx16 x23 = x14 (x11 x23) (x12 x23) x13)(∀ x23 . x23intx17 x23 = add_SNo x23 x23)(∀ x23 . x23intx18 x23 = add_SNo x23 (minus_SNo 1))x19 = 1(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x17 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x18 x23) x19)(∀ x23 . x23intx22 x23 = mul_SNo (x16 x23) (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23
Conjecture 2f24c..A19664 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ 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 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40int∀ x41 . x41intx0 x40 x41 = mul_SNo (add_SNo (add_SNo x41 (minus_SNo 1)) x41) (mul_SNo x41 x41))(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = add_SNo x41 x41)(∀ x40 . x40int∀ x41 . x41intx2 x40 x41 = x41)x3 = 1x4 = 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx5 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x0 (x5 (add_SNo x40 (minus_SNo 1)) x41 x42) (x6 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx6 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x1 (x5 (add_SNo x40 (minus_SNo 1)) x41 x42) (x6 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41intx7 x40 x41 = x5 (x2 x40 x41) x3 x4)(∀ x40 . x40intx8 x40 = add_SNo (add_SNo x40 x40) x40)x9 = 2(∀ x40 . x40intx10 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = If_i (SNoLe x40 0) x41 (x8 (x11 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40intx12 x40 = x11 x9 (x10 x40))(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = add_SNo (x7 x40 x41) (x12 x40))(∀ x40 . x40intx14 x40 = x40)x15 = 1(∀ x40 . x40int∀ x41 . x41intx16 x40 x41 = If_i (SNoLe x40 0) x41 (x13 (x16 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx17 x40 = x16 (x14 x40) x15)(∀ x40 . x40intx18 x40 = x17 x40)(∀ x40 . x40intx19 x40 = mul_SNo (add_SNo (add_SNo x40 (minus_SNo 1)) x40) (mul_SNo x40 x40))x20 = 1(∀ x40 . x40intx21 x40 = add_SNo x40 x40)(∀ x40 . x40intx22 x40 = x40)x23 = 1(∀ x40 . x40int∀ x41 . x41intx24 x40 x41 = If_i (SNoLe x40 0) x41 (x21 (x24 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40intx25 x40 = x24 (x22 x40) x23)(∀ x40 . x40intx26 x40 = x25 x40)(∀ x40 . x40int∀ x41 . x41intx27 x40 x41 = If_i (SNoLe x40 0) x41 (x19 (x27 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40intx28 x40 = x27 x20 (x26 x40))(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) x40) (mul_SNo (mul_SNo (add_SNo x40 x40) 2) 2))(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x18 x40 = x39 x40
Conjecture ec5ed..A196558 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = add_SNo (add_SNo x20 x20) x21)x1 = 2(∀ x20 . x20int∀ x21 . x21intx2 x20 x21 = add_SNo 2 x21)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = x21)x4 = 1(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx5 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x0 (x5 (add_SNo x20 (minus_SNo 1)) x21 x22) (x6 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx6 x20 x21 x22 = If_i (SNoLe x20 0) x22 x1)(∀ x20 . x20int∀ x21 . x21intx7 x20 x21 = x5 (x2 x20 x21) (x3 x20 x21) x4)(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = x7 x20 x21)(∀ x20 . x20intx9 x20 = x20)x10 = 1(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = If_i (SNoLe x20 0) x21 (x8 (x11 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx12 x20 = x11 (x9 x20) x10)(∀ x20 . x20intx13 x20 = mul_SNo (x12 x20) 2)(∀ x20 . x20intx14 x20 = add_SNo 2 (add_SNo x20 x20))(∀ x20 . x20intx15 x20 = x20)(∀ x20 . x20intx16 x20 = mul_SNo (add_SNo 2 2) (add_SNo 1 x20))(∀ x20 . x20int∀ x21 . x21intx17 x20 x21 = If_i (SNoLe x20 0) x21 (x14 (x17 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx18 x20 = x17 (x15 x20) (x16 x20))(∀ x20 . x20intx19 x20 = mul_SNo 2 (If_i (SNoLe x20 0) 1 (x18 x20)))∀ x20 . x20intSNoLe 0 x20x13 x20 = x19 x20
Conjecture 47aa4..A196532 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ 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 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)(∀ x27 . x27int∀ x28 . x28intx0 x27 x28 = mul_SNo x27 x28)(∀ x27 . x27int∀ x28 . x28intx1 x27 x28 = add_SNo x28 (minus_SNo 1))(∀ x27 . x27int∀ x28 . x28intx2 x27 x28 = add_SNo 1 (add_SNo x28 x28))(∀ x27 . x27int∀ x28 . x28intx3 x27 x28 = If_i (SNoLe x27 0) x28 (x0 (x3 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx4 x27 x28 = x3 (x1 x27 x28) (x2 x27 x28))(∀ x27 . x27int∀ x28 . x28intx5 x27 x28 = add_SNo (add_SNo (mul_SNo x27 x28) (x4 x27 x28)) x27)(∀ x27 . x27intx6 x27 = x27)x7 = 1(∀ x27 . x27int∀ x28 . x28intx8 x27 x28 = If_i (SNoLe x27 0) x28 (x5 (x8 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx9 x27 = x8 (x6 x27) x7)(∀ x27 . x27intx10 x27 = x9 x27)(∀ x27 . x27int∀ x28 . x28intx11 x27 x28 = mul_SNo x27 x28)(∀ x27 . x27int∀ x28 . x28intx12 x27 x28 = add_SNo x28 (minus_SNo 1))x13 = 2(∀ x27 . x27int∀ x28 . x28intx14 x27 x28 = If_i (SNoLe x27 0) x28 (x11 (x14 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx15 x27 x28 = x14 (x12 x27 x28) x13)(∀ x27 . x27int∀ x28 . x28intx16 x27 x28 = add_SNo (mul_SNo x27 x28) (x15 x27 x28))(∀ x27 . x27intx17 x27 = x27)x18 = 0(∀ x27 . x27int∀ x28 . x28intx19 x27 x28 = If_i (SNoLe x27 0) x28 (x16 (x19 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx20 x27 = x19 (x17 x27) x18)(∀ x27 . x27int∀ x28 . x28intx21 x27 x28 = mul_SNo x27 x28)(∀ x27 . x27intx22 x27 = x27)x23 = 1(∀ x27 . x27int∀ x28 . x28intx24 x27 x28 = If_i (SNoLe x27 0) x28 (x21 (x24 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx25 x27 = x24 (x22 x27) x23)(∀ x27 . x27intx26 x27 = add_SNo (mul_SNo (x20 x27) (add_SNo 1 x27)) (x25 x27))∀ x27 . x27intSNoLe 0 x27x10 x27 = x26 x27
Conjecture 5c40b..A19623 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ 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 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33int∀ x34 . x34intx0 x33 x34 = mul_SNo (add_SNo 2 x34) x33)x1 = 2(∀ x33 . x33intx2 x33 = x33)(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx4 x33 = x3 x1 (x2 x33))(∀ x33 . x33int∀ x34 . x34intx5 x33 x34 = add_SNo (add_SNo (x4 x33) (minus_SNo x33)) (mul_SNo x34 x34))(∀ x33 . x33int∀ x34 . x34intx6 x33 x34 = add_SNo x34 x34)(∀ x33 . x33int∀ x34 . x34intx7 x33 x34 = x34)x8 = 1x9 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx10 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x5 (x10 (add_SNo x33 (minus_SNo 1)) x34 x35) (x11 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx11 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x6 (x10 (add_SNo x33 (minus_SNo 1)) x34 x35) (x11 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34intx12 x33 x34 = x10 (x7 x33 x34) x8 x9)(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = add_SNo (add_SNo (x12 x33 x34) (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33))) x33)(∀ x33 . x33intx14 x33 = x33)x15 = 1(∀ x33 . x33int∀ x34 . x34intx16 x33 x34 = If_i (SNoLe x33 0) x34 (x13 (x16 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx17 x33 = x16 (x14 x33) x15)(∀ x33 . x33intx18 x33 = x17 x33)(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)) (mul_SNo x34 x34)) x33)(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = add_SNo x34 x34)(∀ x33 . x33int∀ x34 . x34intx21 x33 x34 = x34)x22 = 1x23 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x19 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x20 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34intx26 x33 x34 = x24 (x21 x33 x34) x22 x23)(∀ x33 . x33int∀ x34 . x34intx27 x33 x34 = add_SNo (add_SNo (x26 x33 x34) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33))) x33)(∀ x33 . x33intx28 x33 = x33)x29 = 1(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx31 x33 = x30 (x28 x33) x29)(∀ x33 . x33intx32 x33 = x31 x33)∀ x33 . x33intSNoLe 0 x33x18 x33 = x32 x33

previous assets