Search for blocks/addresses/...

Proofgold Address

address
PUeujSxadfXK4GysHGGi8byR2XaeXm9CwET
total
0
mg
-
conjpub
-
current assets
c3706../aaa3c.. bday: 25624 doc published by PrGxv..
Param intint : ι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Conjecture 4de6e..A350008 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ 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 (mul_SNo x33 x34) x34)(∀ x33 . x33int∀ x34 . x34intx1 x33 x34 = x34)(∀ x33 . x33int∀ x34 . x34intx2 x33 x34 = x34)x3 = 1(∀ x33 . x33int∀ x34 . x34intx4 x33 x34 = x34)(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx5 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x0 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35) (x6 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx6 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x1 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35) (x6 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34intx7 x33 x34 = x5 (x2 x33 x34) x3 (x4 x33 x34))(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = add_SNo x33 (x7 x33 x34))(∀ x33 . x33intx9 x33 = x33)x10 = 1(∀ x33 . x33int∀ x34 . x34intx11 x33 x34 = If_i (SNoLe x33 0) x34 (x8 (x11 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx12 x33 = x11 (x9 x33) x10)(∀ x33 . x33intx13 x33 = x12 x33)(∀ x33 . x33intx14 x33 = mul_SNo x33 x33)x15 = 1(∀ x33 . x33int∀ x34 . x34intx16 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx17 x33 x34 = x34)(∀ x33 . x33int∀ x34 . x34intx18 x33 x34 = add_SNo x34 (minus_SNo 1))(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = x34)(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = x34)(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx21 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x16 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx22 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x17 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34intx23 x33 x34 = x21 (x18 x33 x34) (x19 x33 x34) (x20 x33 x34))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = x23 x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = If_i (SNoLe x33 0) x34 (x14 (x25 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33int∀ x34 . x34intx26 x33 x34 = x25 x15 (x24 x33 x34))(∀ x33 . x33int∀ x34 . x34intx27 x33 x34 = add_SNo (x26 x33 x34) 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 x33x13 x33 = x32 x33
Conjecture b1410..A34976 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . 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 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo (mul_SNo x22 x23) x22))))(∀ x22 . x22intx1 x22 = x22)x2 = 1(∀ x22 . x22int∀ x23 . x23intx3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx4 x22 = x3 (x1 x22) x2)(∀ x22 . x22intx5 x22 = x4 x22)(∀ x22 . x22intx6 x22 = mul_SNo (mul_SNo x22 x22) x22)x7 = 1(∀ x22 . x22intx8 x22 = add_SNo x22 x22)(∀ x22 . x22intx9 x22 = x22)x10 = 1(∀ x22 . x22int∀ x23 . x23intx11 x22 x23 = If_i (SNoLe x22 0) x23 (x8 (x11 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx12 x22 = x11 (x9 x22) x10)(∀ x22 . x22intx13 x22 = x12 x22)(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x6 (x14 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx15 x22 = x14 x7 (x13 x22))(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx17 x22 = x22)(∀ x22 . x22intx18 x22 = add_SNo 1 x22)(∀ 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))(∀ x22 . x22intx21 x22 = mul_SNo (x15 x22) (x20 x22))∀ x22 . x22intSNoLe 0 x22x5 x22 = x21 x22
Conjecture c198e..A34975 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ 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 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = add_SNo 1 (add_SNo x20 x20))x1 = add_SNo 1 2(∀ x20 . x20int∀ x21 . x21intx2 x20 x21 = x21)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20int∀ x21 . x21intx4 x20 x21 = x3 x1 (x2 x20 x21))(∀ x20 . x20int∀ x21 . x21intx5 x20 x21 = mul_SNo (x4 x20 x21) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo (mul_SNo 2 (add_SNo 2 2)) x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) (minus_SNo 1)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture a5789..A34940 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ 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 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ 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 . 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 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι → ι → ι . (∀ x29 . x29int∀ x30 . x30int∀ x31 . x31intx28 x29 x30 x31int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)(∀ x31 . x31int∀ x32 . x32intx0 x31 x32 = add_SNo (mul_SNo 2 (mul_SNo x31 x32)) (minus_SNo x31))(∀ x31 . x31intx1 x31 = x31)x2 = 1(∀ x31 . x31int∀ x32 . x32intx3 x31 x32 = If_i (SNoLe x31 0) x32 (x0 (x3 (add_SNo x31 (minus_SNo 1)) x32) x31))(∀ x31 . x31intx4 x31 = x3 (x1 x31) x2)(∀ x31 . x31int∀ x32 . x32intx5 x31 x32 = add_SNo (mul_SNo 2 (mul_SNo x31 x32)) x31)(∀ x31 . x31int∀ x32 . x32intx6 x31 x32 = x32)(∀ x31 . x31intx7 x31 = x31)x8 = 1(∀ x31 . x31intx9 x31 = x31)(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx10 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x5 (x10 (add_SNo x31 (minus_SNo 1)) x32 x33) (x11 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx11 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x6 (x10 (add_SNo x31 (minus_SNo 1)) x32 x33) (x11 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx12 x31 = x10 (x7 x31) x8 (x9 x31))(∀ x31 . x31intx13 x31 = mul_SNo (x4 x31) (x12 x31))(∀ x31 . x31int∀ x32 . x32intx14 x31 x32 = mul_SNo x31 x32)(∀ x31 . x31int∀ x32 . x32intx15 x31 x32 = add_SNo 2 x32)(∀ x31 . x31intx16 x31 = x31)x17 = 1x18 = add_SNo 1 2(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx19 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x14 (x19 (add_SNo x31 (minus_SNo 1)) x32 x33) (x20 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx20 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x15 (x19 (add_SNo x31 (minus_SNo 1)) x32 x33) (x20 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx21 x31 = x19 (x16 x31) x17 x18)(∀ x31 . x31int∀ x32 . x32intx22 x31 x32 = mul_SNo x31 x32)(∀ x31 . x31int∀ x32 . x32intx23 x31 x32 = x32)(∀ x31 . x31intx24 x31 = add_SNo x31 (minus_SNo 1))x25 = 1(∀ x31 . x31intx26 x31 = add_SNo 1 (add_SNo x31 x31))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx27 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x22 (x27 (add_SNo x31 (minus_SNo 1)) x32 x33) (x28 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx28 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x23 (x27 (add_SNo x31 (minus_SNo 1)) x32 x33) (x28 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx29 x31 = x27 (x24 x31) x25 (x26 x31))(∀ x31 . x31intx30 x31 = mul_SNo (x21 x31) (x29 x31))∀ x31 . x31intSNoLe 0 x31x13 x31 = x30 x31
Conjecture ad8fb..A34911 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ 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 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = add_SNo 1 (mul_SNo 2 (mul_SNo x20 x21)))x1 = 2(∀ x20 . x20int∀ x21 . x21intx2 x20 x21 = x21)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20int∀ x21 . x21intx4 x20 x21 = x3 x1 (x2 x20 x21))(∀ x20 . x20int∀ x21 . x21intx5 x20 x21 = mul_SNo (x4 x20 x21) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo (mul_SNo 2 (add_SNo 2 2)) x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 88cde..A34910 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . 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 . x26intx0 x25 x26 = mul_SNo 2 (mul_SNo 2 (add_SNo (mul_SNo 2 (mul_SNo x25 x26)) x25)))(∀ x25 . x25intx1 x25 = x25)x2 = 1(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx4 x25 = x3 (x1 x25) x2)(∀ x25 . x25intx5 x25 = x4 x25)(∀ x25 . x25intx6 x25 = mul_SNo x25 x25)x7 = 1(∀ x25 . x25intx8 x25 = add_SNo x25 x25)(∀ x25 . x25intx9 x25 = x25)x10 = 1(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = If_i (SNoLe x25 0) x26 (x8 (x11 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx12 x25 = x11 (x9 x25) x10)(∀ x25 . x25intx13 x25 = x12 x25)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x6 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 x7 (x13 x25))(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = add_SNo 2 x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = add_SNo 1 2(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x5 x25 = x24 x25
Conjecture 46571..A348332 : ∀ 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 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ 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 (add_SNo x28 x29) x29)(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = mul_SNo 2 (mul_SNo x29 x29))(∀ x28 . x28intx2 x28 = x28)x3 = 1x4 = 2(∀ 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 = mul_SNo (x7 x28) 2)(∀ x28 . x28int∀ x29 . x29intx9 x28 x29 = mul_SNo (mul_SNo x28 x29) x28)(∀ x28 . x28int∀ x29 . x29intx10 x28 x29 = add_SNo x29 x29)(∀ x28 . x28intx11 x28 = add_SNo x28 (minus_SNo 1))x12 = 1x13 = 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 = add_SNo 1 (add_SNo x28 x28))(∀ x28 . x28intx18 x28 = x28)x19 = 1(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = If_i (SNoLe x28 0) x29 (x17 (x20 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx21 x28 = x20 (x18 x28) x19)(∀ x28 . x28intx22 x28 = mul_SNo x28 x28)(∀ x28 . x28intx23 x28 = x28)x24 = 2(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (mul_SNo (x16 x28) (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x8 x28 = x27 x28
Conjecture ddcda..A347478 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ 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 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = mul_SNo 2 (add_SNo 2 x22))x2 = 1(∀ x22 . x22int∀ x23 . x23intx3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx4 x22 = x3 (x1 x22) x2)x5 = 0(∀ x22 . x22intx6 x22 = x22)x7 = 1(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 x5)(∀ x22 . x22intx9 x22 = x8 (x6 x22) x7)(∀ x22 . x22intx10 x22 = add_SNo (x4 x22) (minus_SNo (x9 x22)))(∀ x22 . x22intx11 x22 = mul_SNo x22 x22)x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 2(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = mul_SNo 2 (x17 x22))(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = add_SNo (add_SNo (x20 x22) (minus_SNo 1)) (If_i (SNoLe x22 0) 0 1))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 9daa2..A346896 : ∀ 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 . 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 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17int∀ x18 . x18intx0 x17 x18 = mul_SNo (add_SNo 2 x18) x17)x1 = 2(∀ 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))(∀ x17 . x17intx4 x17 = x3 x1 (x2 x17))(∀ x17 . x17int∀ x18 . x18intx5 x17 x18 = add_SNo (mul_SNo (x4 x17) x18) (minus_SNo x17))(∀ x17 . x17intx6 x17 = x17)x7 = 1(∀ x17 . x17int∀ x18 . x18intx8 x17 x18 = If_i (SNoLe x17 0) x18 (x5 (x8 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx9 x17 = x8 (x6 x17) x7)(∀ x17 . x17intx10 x17 = x9 x17)(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = mul_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x18 x18) x18))) (minus_SNo 1)) x17)(∀ x17 . x17intx12 x17 = x17)x13 = 1(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x11 (x14 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx15 x17 = x14 (x12 x17) x13)(∀ x17 . x17intx16 x17 = x15 x17)∀ x17 . x17intSNoLe 0 x17x10 x17 = x16 x17
Conjecture 2b20f..A34673 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ 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 . x8int∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ 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 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 . x26int∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 . x42int∀ x43 . x43int∀ x44 : ι → ι → ι → ι . (∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx44 x45 x46 x47int)∀ x45 : ι → ι → ι → ι . (∀ x46 . x46int∀ x47 . x47int∀ x48 . x48intx45 x46 x47 x48int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)(∀ x48 . x48intx0 x48 = add_SNo x48 x48)(∀ x48 . x48int∀ x49 . x49intx1 x48 x49 = x49)(∀ x48 . x48intx2 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx3 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x3 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx4 x48 x49 = x3 (x1 x48 x49) (x2 x48))(∀ x48 . x48int∀ x49 . x49intx5 x48 x49 = add_SNo 1 (x4 x48 x49))(∀ x48 . x48int∀ x49 . x49intx6 x48 x49 = x49)x7 = add_SNo 1 2x8 = 1(∀ x48 . x48intx9 x48 = x48)(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx10 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x5 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx11 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x6 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx12 x48 = x10 x7 x8 (x9 x48))(∀ x48 . x48intx13 x48 = add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48)(∀ x48 . x48intx14 x48 = x48)x15 = 1(∀ x48 . x48int∀ x49 . x49intx16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx17 x48 = x16 (x14 x48) x15)(∀ x48 . x48intx18 x48 = add_SNo (add_SNo x48 x48) x48)(∀ x48 . x48intx19 x48 = x48)x20 = 1(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx22 x48 = x21 (x19 x48) x20)(∀ x48 . x48intx23 x48 = mul_SNo (mul_SNo (x12 x48) (add_SNo 1 (x17 x48))) (add_SNo 1 (x22 x48)))(∀ x48 . x48intx24 x48 = add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48)(∀ x48 . x48intx25 x48 = x48)x26 = 1(∀ x48 . x48int∀ x49 . x49intx27 x48 x49 = If_i (SNoLe x48 0) x49 (x24 (x27 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx28 x48 = x27 (x25 x48) x26)(∀ x48 . x48intx29 x48 = add_SNo x48 x48)(∀ x48 . x48intx30 x48 = x48)x31 = 1(∀ x48 . x48int∀ x49 . x49intx32 x48 x49 = If_i (SNoLe x48 0) x49 (x29 (x32 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx33 x48 = x32 (x30 x48) x31)(∀ x48 . x48intx34 x48 = add_SNo (add_SNo x48 x48) x48)(∀ x48 . x48intx35 x48 = x48)x36 = 1(∀ x48 . x48int∀ x49 . x49intx37 x48 x49 = If_i (SNoLe x48 0) x49 (x34 (x37 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx38 x48 = x37 (x35 x48) x36)(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = mul_SNo x48 x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = x49)(∀ x48 . x48intx41 x48 = x48)x42 = 1x43 = add_SNo 2 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx44 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x39 (x44 (add_SNo x48 (minus_SNo 1)) x49 x50) (x45 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx45 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x40 (x44 (add_SNo x48 (minus_SNo 1)) x49 x50) (x45 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx46 x48 = x44 (x41 x48) x42 x43)(∀ x48 . x48intx47 x48 = mul_SNo (mul_SNo (mul_SNo (add_SNo 1 (x28 x48)) (add_SNo 1 (x33 x48))) (add_SNo 1 (x38 x48))) (add_SNo 1 (x46 x48)))∀ x48 . x48intSNoLe 0 x48x23 x48 = x47 x48
Conjecture 09794..A344260 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ 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 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ 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 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ 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 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33intx0 x33 = add_SNo x33 x33)(∀ x33 . x33int∀ x34 . x34intx1 x33 x34 = x34)(∀ 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 . x33int∀ x34 . x34intx4 x33 x34 = x3 (x1 x33 x34) (x2 x33))(∀ x33 . x33int∀ x34 . x34intx5 x33 x34 = add_SNo 1 (x4 x33 x34))(∀ x33 . x33int∀ x34 . x34intx6 x33 x34 = x34)(∀ x33 . x33intx7 x33 = x33)x8 = 1(∀ x33 . x33intx9 x33 = x33)(∀ 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 . x33intx12 x33 = x10 (x7 x33) x8 (x9 x33))(∀ x33 . x33intx13 x33 = x12 x33)(∀ x33 . x33int∀ x34 . x34intx14 x33 x34 = add_SNo 1 (mul_SNo x33 x34))(∀ x33 . x33int∀ x34 . x34intx15 x33 x34 = x34)(∀ x33 . x33intx16 x33 = x33)x17 = 0(∀ x33 . x33intx18 x33 = add_SNo x33 x33)(∀ x33 . x33intx19 x33 = add_SNo x33 (minus_SNo 1))x20 = 2(∀ x33 . x33int∀ x34 . x34intx21 x33 x34 = If_i (SNoLe x33 0) x34 (x18 (x21 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx22 x33 = x21 (x19 x33) x20)(∀ x33 . x33intx23 x33 = x22 x33)(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x14 (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 (x15 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx26 x33 = x24 (x16 x33) x17 (x23 x33))(∀ x33 . x33intx27 x33 = add_SNo x33 x33)(∀ x33 . x33intx28 x33 = add_SNo x33 (minus_SNo 1))x29 = 2(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx31 x33 = x30 (x28 x33) x29)(∀ x33 . x33intx32 x33 = add_SNo (mul_SNo (x26 x33) (x31 x33)) 1)∀ x33 . x33intSNoLe 0 x33x13 x33 = x32 x33
Conjecture cd1ac..A344114 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ 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 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ 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 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33intx0 x33 = add_SNo x33 x33)(∀ x33 . x33intx1 x33 = mul_SNo (add_SNo 2 x33) x33)x2 = 2(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx4 x33 = x3 (x1 x33) x2)(∀ x33 . x33int∀ x34 . x34intx5 x33 x34 = add_SNo (mul_SNo x34 x33) x33)(∀ x33 . x33intx6 x33 = x33)x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = add_SNo (x4 x33) (minus_SNo (x9 x33)))(∀ x33 . x33int∀ x34 . x34intx11 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx12 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx13 x33 = x33)x14 = 1x15 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx16 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x11 (x16 (add_SNo x33 (minus_SNo 1)) x34 x35) (x17 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx17 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x12 (x16 (add_SNo x33 (minus_SNo 1)) x34 x35) (x17 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx18 x33 = x16 (x13 x33) x14 x15)(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx21 x33 = x33)x22 = 2x23 = add_SNo 2 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 . x33intx26 x33 = x24 (x21 x33) x22 x23)(∀ x33 . x33int∀ x34 . x34intx27 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33intx28 x33 = x33)(∀ x33 . x33intx29 x33 = add_SNo 1 x33)(∀ 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))(∀ x33 . x33intx32 x33 = add_SNo (mul_SNo (x18 x33) (x26 x33)) (minus_SNo (x31 x33)))∀ x33 . x33intSNoLe 0 x33x10 x33 = x32 x33
Conjecture a7bb5..A343539 : ∀ 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 . 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 x18 x19)(∀ x18 . x18intx1 x18 = x18)(∀ x18 . x18intx2 x18 = add_SNo x18 x18)x3 = 1x4 = 2(∀ 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 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 x4)(∀ x18 . x18intx8 x18 = mul_SNo (add_SNo 1 (add_SNo x18 x18)) (x7 x18))(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo (add_SNo (add_SNo x18 (minus_SNo x19)) x18) x18)(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = add_SNo x18 (minus_SNo 1))x12 = add_SNo 2 2x13 = 1(∀ 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)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) x12 x13)(∀ x18 . x18intx17 x18 = mul_SNo (If_i (SNoLe x18 0) 1 (x16 x18)) (add_SNo 1 (add_SNo x18 x18)))∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 0feff..A34325 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo (add_SNo 1 (add_SNo 2 2)) (add_SNo (mul_SNo x20 x21) x20))(∀ x20 . x20intx1 x20 = x20)x2 = 1(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 (x1 x20) x2)(∀ x20 . x20intx5 x20 = x4 x20)(∀ x20 . x20int∀ x21 . x21intx6 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20intx7 x20 = x20)x8 = 1(∀ x20 . x20int∀ x21 . x21intx9 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x9 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx10 x20 = x9 (x7 x20) x8)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)(∀ x20 . x20intx14 x20 = add_SNo 1 x20)x15 = add_SNo 1 (add_SNo 2 2)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) (x14 x20) x15)(∀ x20 . x20intx19 x20 = mul_SNo (x10 x20) (x18 x20))∀ x20 . x20intSNoLe 0 x20x5 x20 = x19 x20
Conjecture 16b90..A34177 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . 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 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo 2 (mul_SNo 2 (add_SNo (mul_SNo x22 x23) x22)))(∀ x22 . x22intx1 x22 = x22)x2 = 1(∀ x22 . x22int∀ x23 . x23intx3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx4 x22 = x3 (x1 x22) x2)(∀ x22 . x22intx5 x22 = x4 x22)(∀ x22 . x22intx6 x22 = mul_SNo x22 x22)x7 = 1(∀ x22 . x22intx8 x22 = add_SNo x22 x22)(∀ x22 . x22intx9 x22 = x22)x10 = 1(∀ x22 . x22int∀ x23 . x23intx11 x22 x23 = If_i (SNoLe x22 0) x23 (x8 (x11 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx12 x22 = x11 (x9 x22) x10)(∀ x22 . x22intx13 x22 = x12 x22)(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x6 (x14 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx15 x22 = x14 x7 (x13 x22))(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22intx17 x22 = x22)(∀ x22 . x22intx18 x22 = add_SNo 1 x22)(∀ 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))(∀ x22 . x22intx21 x22 = mul_SNo (x15 x22) (x20 x22))∀ x22 . x22intSNoLe 0 x22x5 x22 = x21 x22
Conjecture 1062a..A34001 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo (add_SNo 1 2) (add_SNo (mul_SNo x20 x21) x20))(∀ x20 . x20intx1 x20 = x20)x2 = 1(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 (x1 x20) x2)(∀ x20 . x20intx5 x20 = x4 x20)(∀ x20 . x20int∀ x21 . x21intx6 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20intx7 x20 = x20)x8 = 1(∀ x20 . x20int∀ x21 . x21intx9 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x9 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx10 x20 = x9 (x7 x20) x8)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)(∀ x20 . x20intx14 x20 = add_SNo 1 x20)x15 = add_SNo 1 2(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) (x14 x20) x15)(∀ x20 . x20intx19 x20 = mul_SNo (x10 x20) (x18 x20))∀ x20 . x20intSNoLe 0 x20x5 x20 = x19 x20
Conjecture 8db0a..A34000 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . x15int∀ x16 . x16intx0 x15 x16 = mul_SNo (add_SNo 2 (add_SNo (add_SNo x16 x16) x16)) 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))(∀ 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 = add_SNo 1 (add_SNo 2 x16))(∀ x15 . x15intx8 x15 = add_SNo x15 (minus_SNo 1))x9 = 1x10 = 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 x10)(∀ x15 . x15intx14 x15 = mul_SNo (x13 x15) (add_SNo (add_SNo (add_SNo (If_i (SNoLe x15 0) 1 2) x15) x15) x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 9f807..A339610 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ 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 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ 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 = x19)(∀ x18 . x18int∀ x19 . x19intx1 x18 x19 = add_SNo 2 (add_SNo x18 x19))(∀ x18 . x18intx2 x18 = x18)(∀ x18 . x18intx3 x18 = x18)x4 = 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 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) (x3 x18) x4)(∀ x18 . x18intx8 x18 = add_SNo 2 (x7 x18))(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = x18)(∀ x18 . x18intx12 x18 = add_SNo 2 x18)(∀ x18 . x18intx13 x18 = add_SNo 1 (minus_SNo x18))(∀ 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)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) (x12 x18) (x13 x18))(∀ x18 . x18intx17 x18 = x16 x18)∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture bdfac..A337 : ∀ 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 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12intx0 x12 = add_SNo (add_SNo x12 (minus_SNo 1)) x12)(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = x4 x12)(∀ x12 . x12intx6 x12 = add_SNo x12 x12)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = add_SNo x12 (minus_SNo 1))(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo 1 (x10 x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture d48b8..A33595 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ 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 . x8intx0 x7 x8 = add_SNo (add_SNo x7 (minus_SNo 2)) x8)(∀ x7 . x7intx1 x7 = mul_SNo 2 (mul_SNo x7 x7))x2 = 1(∀ x7 . x7int∀ x8 . x8intx3 x7 x8 = If_i (SNoLe x7 0) x8 (x0 (x3 (add_SNo x7 (minus_SNo 1)) x8) x7))(∀ x7 . x7intx4 x7 = x3 (x1 x7) x2)(∀ x7 . x7intx5 x7 = x4 x7)(∀ x7 . x7intx6 x7 = mul_SNo (add_SNo 1 (minus_SNo (mul_SNo 2 (mul_SNo x7 x7)))) (add_SNo 1 (minus_SNo (mul_SNo x7 x7))))∀ x7 . x7intSNoLe 0 x7x5 x7 = x6 x7

previous assets