Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr5pn../32029..
PUeij../1a6f5..
vout
Pr5pn../44752.. 23.98 bars
PUZQJ../141a5.. 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 30ac3..A155657 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ 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 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . 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 . x26int∀ 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 . x31intx0 x31 = add_SNo (add_SNo x31 x31) x31)x1 = 2(∀ x31 . x31intx2 x31 = x31)(∀ x31 . x31int∀ x32 . x32intx3 x31 x32 = If_i (SNoLe x31 0) x32 (x0 (x3 (add_SNo x31 (minus_SNo 1)) x32)))(∀ x31 . x31intx4 x31 = x3 x1 (x2 x31))(∀ x31 . x31int∀ x32 . x32intx5 x31 x32 = add_SNo (x4 x31) (minus_SNo x32))(∀ x31 . x31int∀ x32 . x32intx6 x31 x32 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x32 x32)) (minus_SNo x31)))(∀ x31 . x31intx7 x31 = x31)x8 = 2x9 = 1(∀ 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 . x31intx13 x31 = add_SNo (x12 x31) (minus_SNo 1))(∀ x31 . x31int∀ x32 . x32intx14 x31 x32 = mul_SNo x31 x32)(∀ x31 . x31int∀ x32 . x32intx15 x31 x32 = x32)(∀ x31 . x31intx16 x31 = x31)x17 = 1x18 = add_SNo 1 (add_SNo 2 (add_SNo 2 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 = x31)x25 = 1x26 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ 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 . x31intx30 x31 = add_SNo (add_SNo (x21 x31) (minus_SNo 1)) (x29 x31))∀ x31 . x31intSNoLe 0 x31x13 x31 = x30 x31
Conjecture d5a46..A155644 : ∀ 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 . 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 . 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 . 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 . x33intx5 x33 = add_SNo (x4 x33) (minus_SNo 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 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33)(∀ x33 . x33intx11 x33 = x33)x12 = 1(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = If_i (SNoLe x33 0) x34 (x10 (x13 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx14 x33 = x13 (x11 x33) x12)(∀ x33 . x33intx15 x33 = add_SNo 1 (add_SNo (x9 x33) (minus_SNo (x14 x33))))(∀ x33 . x33int∀ x34 . x34intx16 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx17 x33 x34 = x34)(∀ x33 . x33intx18 x33 = x33)x19 = 1x20 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ 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 . x33intx23 x33 = x21 (x18 x33) x19 x20)(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = x33)x27 = 1x28 = add_SNo 1 (add_SNo 2 2)(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = add_SNo 1 (add_SNo (x23 x33) (minus_SNo (x31 x33))))∀ x33 . x33intSNoLe 0 x33x15 x33 = x32 x33
Conjecture 9fc99..A155634 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 . x21int∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)(∀ x26 . x26int∀ x27 . x27intx0 x26 x27 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x26 x26)) x26) x27)(∀ x26 . x26int∀ x27 . x27intx1 x26 x27 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x27 x27) x27)) x27)(∀ x26 . x26intx2 x26 = x26)x3 = 2x4 = 2(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx5 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x0 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx6 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x1 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx7 x26 = x5 (x2 x26) x3 x4)(∀ x26 . x26intx8 x26 = add_SNo (x7 x26) (minus_SNo 1))(∀ x26 . x26int∀ x27 . x27intx9 x26 x27 = mul_SNo x26 x27)(∀ x26 . x26int∀ x27 . x27intx10 x26 x27 = x27)(∀ x26 . x26intx11 x26 = x26)x12 = 1x13 = add_SNo 1 (add_SNo 2 2)(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx14 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x9 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx15 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x10 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx16 x26 = x14 (x11 x26) x12 x13)(∀ x26 . x26int∀ x27 . x27intx17 x26 x27 = mul_SNo x26 x27)(∀ x26 . x26int∀ x27 . x27intx18 x26 x27 = x27)(∀ x26 . x26intx19 x26 = x26)x20 = 1x21 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx22 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x17 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx23 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x18 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28)))(∀ x26 . x26intx24 x26 = x22 (x19 x26) x20 x21)(∀ x26 . x26intx25 x26 = add_SNo (add_SNo (x16 x26) (minus_SNo 1)) (x24 x26))∀ x26 . x26intSNoLe 0 x26x8 x26 = x25 x26
Conjecture c77a5..A155631 : ∀ 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 . 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 : ι → ι . (∀ 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 . x30intx0 x30 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x30 x30)) x30))(∀ x30 . x30intx1 x30 = x30)x2 = 1(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx4 x30 = x3 (x1 x30) x2)(∀ x30 . x30intx5 x30 = add_SNo x30 x30)(∀ x30 . x30intx6 x30 = add_SNo x30 x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = add_SNo 1 (add_SNo (x4 x30) (minus_SNo (x9 x30))))(∀ x30 . x30int∀ x31 . x31intx11 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx12 x30 x31 = x31)(∀ x30 . x30intx13 x30 = x30)x14 = 1x15 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx16 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x11 (x16 (add_SNo x30 (minus_SNo 1)) x31 x32) (x17 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx17 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x12 (x16 (add_SNo x30 (minus_SNo 1)) x31 x32) (x17 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx18 x30 = x16 (x13 x30) x14 x15)(∀ x30 . x30intx19 x30 = mul_SNo x30 x30)x20 = 1(∀ x30 . x30intx21 x30 = add_SNo x30 x30)(∀ x30 . x30intx22 x30 = x30)x23 = 1(∀ x30 . x30int∀ x31 . x31intx24 x30 x31 = If_i (SNoLe x30 0) x31 (x21 (x24 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx25 x30 = x24 (x22 x30) x23)(∀ x30 . x30intx26 x30 = x25 x30)(∀ x30 . x30int∀ x31 . x31intx27 x30 x31 = If_i (SNoLe x30 0) x31 (x19 (x27 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx28 x30 = x27 x20 (x26 x30))(∀ x30 . x30intx29 x30 = add_SNo 1 (add_SNo (x18 x30) (minus_SNo (x28 x30))))∀ x30 . x30intSNoLe 0 x30x10 x30 = x29 x30
Conjecture bb94e..A155621 : ∀ 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 . 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 . 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 . x30intx0 x30 = add_SNo x30 x30)(∀ x30 . x30intx1 x30 = add_SNo x30 x30)x2 = 1(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx4 x30 = x3 (x1 x30) x2)(∀ x30 . x30intx5 x30 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x30 x30)) x30))(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = add_SNo (add_SNo (x4 x30) (minus_SNo 1)) (x9 x30))(∀ x30 . x30intx11 x30 = mul_SNo x30 x30)x12 = 1(∀ x30 . x30intx13 x30 = add_SNo x30 x30)(∀ x30 . x30intx14 x30 = x30)x15 = 1(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = If_i (SNoLe x30 0) x31 (x13 (x16 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx17 x30 = x16 (x14 x30) x15)(∀ x30 . x30intx18 x30 = x17 x30)(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x11 (x19 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx20 x30 = x19 x12 (x18 x30))(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx28 x30 = x26 (x23 x30) x24 x25)(∀ x30 . x30intx29 x30 = add_SNo (add_SNo (x20 x30) (minus_SNo 1)) (x28 x30))∀ x30 . x30intSNoLe 0 x30x10 x30 = x29 x30
Conjecture 07741..A155594 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι → ι . (∀ x19 . x19int∀ x20 . x20int∀ x21 . x21intx18 x19 x20 x21int)∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo 1 (add_SNo x25 x25))(∀ x25 . x25intx1 x25 = x25)(∀ x25 . x25intx2 x25 = add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25)(∀ x25 . x25intx3 x25 = x25)x4 = 1(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = If_i (SNoLe x25 0) x26 (x2 (x5 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx6 x25 = x5 (x3 x25) x4)(∀ x25 . x25intx7 x25 = x6 x25)(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x1 x25) (x7 x25))(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = x26)(∀ x25 . x25intx15 x25 = x25)x16 = 1x17 = add_SNo 1 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx20 x25 = x18 (x15 x25) x16 x17)(∀ x25 . x25intx21 x25 = add_SNo 1 (x20 x25))(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 (x12 x25) (x21 x25))(∀ x25 . x25intx24 x25 = add_SNo (x23 x25) (minus_SNo 1))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 9f1d0..A155477 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ 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 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ 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 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38intx0 x38 = add_SNo (mul_SNo x38 x38) x38)x1 = 2x2 = 2(∀ x38 . x38int∀ x39 . x39intx3 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x3 (add_SNo x38 (minus_SNo 1)) x39)))x4 = x3 x1 x2(∀ x38 . x38intx5 x38 = add_SNo (mul_SNo x4 x38) x38)(∀ x38 . x38intx6 x38 = add_SNo 1 (add_SNo x38 x38))x7 = 1(∀ x38 . x38int∀ x39 . x39intx8 x38 x39 = If_i (SNoLe x38 0) x39 (x5 (x8 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx9 x38 = x8 (x6 x38) x7)(∀ x38 . x38intx10 x38 = x9 x38)(∀ x38 . x38int∀ x39 . x39intx11 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx12 x38 x39 = x39)(∀ x38 . x38intx13 x38 = add_SNo 1 x38)x14 = 1(∀ x38 . x38intx15 x38 = add_SNo (mul_SNo x38 x38) x38)x16 = 2x17 = 2(∀ x38 . x38int∀ x39 . x39intx18 x38 x39 = If_i (SNoLe x38 0) x39 (x15 (x18 (add_SNo x38 (minus_SNo 1)) x39)))x19 = x18 x16 x17x20 = add_SNo 1 x19(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx21 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x11 (x21 (add_SNo x38 (minus_SNo 1)) x39 x40) (x22 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx22 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x12 (x21 (add_SNo x38 (minus_SNo 1)) x39 x40) (x22 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx23 x38 = x21 (x13 x38) x14 x20)(∀ x38 . x38int∀ x39 . x39intx24 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx25 x38 x39 = x39)(∀ x38 . x38intx26 x38 = x38)x27 = 1(∀ x38 . x38intx28 x38 = add_SNo (mul_SNo x38 x38) x38)x29 = 2x30 = 2(∀ x38 . x38int∀ x39 . x39intx31 x38 x39 = If_i (SNoLe x38 0) x39 (x28 (x31 (add_SNo x38 (minus_SNo 1)) x39)))x32 = x31 x29 x30x33 = add_SNo 1 x32(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx34 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x24 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx35 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x25 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx36 x38 = x34 (x26 x38) x27 x33)(∀ x38 . x38intx37 x38 = mul_SNo (x23 x38) (x36 x38))∀ x38 . x38intSNoLe 0 x38x10 x38 = x37 x38
Conjecture f8f04..A1553 : ∀ 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 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ 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 . x22int∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ 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 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι → ι . (∀ x42 . x42int∀ x43 . x43int∀ x44 . x44intx41 x42 x43 x44int)∀ x42 : ι → ι → ι → ι . (∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx42 x43 x44 x45int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 . x47int∀ x48 . x48int∀ x49 : ι → ι → ι → ι . (∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx49 x50 x51 x52int)∀ x50 : ι → ι → ι → ι . (∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx50 x51 x52 x53int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)(∀ x53 . x53intx0 x53 = add_SNo (add_SNo x53 x53) x53)(∀ x53 . x53intx1 x53 = x53)x2 = 1(∀ x53 . x53int∀ x54 . x54intx3 x53 x54 = If_i (SNoLe x53 0) x54 (x0 (x3 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx4 x53 = x3 (x1 x53) x2)(∀ x53 . x53intx5 x53 = add_SNo x53 x53)(∀ x53 . x53intx6 x53 = x53)x7 = 1(∀ x53 . x53int∀ x54 . x54intx8 x53 x54 = If_i (SNoLe x53 0) x54 (x5 (x8 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx9 x53 = x8 (x6 x53) x7)(∀ x53 . x53intx10 x53 = add_SNo x53 x53)(∀ x53 . x53intx11 x53 = x53)x12 = 1(∀ x53 . x53int∀ x54 . x54intx13 x53 x54 = If_i (SNoLe x53 0) x54 (x10 (x13 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx14 x53 = x13 (x11 x53) x12)(∀ x53 . x53intx15 x53 = add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53)(∀ x53 . x53intx16 x53 = x53)x17 = 1(∀ x53 . x53int∀ x54 . x54intx18 x53 x54 = If_i (SNoLe x53 0) x54 (x15 (x18 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx19 x53 = x18 (x16 x53) x17)(∀ x53 . x53intx20 x53 = add_SNo (mul_SNo (add_SNo (x4 x53) (x9 x53)) (add_SNo 1 (x14 x53))) (add_SNo 1 (x19 x53)))(∀ x53 . x53intx21 x53 = add_SNo (mul_SNo x53 x53) x53)x22 = 1(∀ x53 . x53intx23 x53 = add_SNo x53 x53)(∀ x53 . x53intx24 x53 = x53)x25 = 1(∀ x53 . x53int∀ x54 . x54intx26 x53 x54 = If_i (SNoLe x53 0) x54 (x23 (x26 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx27 x53 = x26 (x24 x53) x25)(∀ x53 . x53intx28 x53 = x27 x53)(∀ x53 . x53int∀ x54 . x54intx29 x53 x54 = If_i (SNoLe x53 0) x54 (x21 (x29 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx30 x53 = x29 x22 (x28 x53))(∀ x53 . x53int∀ x54 . x54intx31 x53 x54 = mul_SNo x53 x54)(∀ x53 . x53int∀ x54 . x54intx32 x53 x54 = x54)(∀ x53 . x53intx33 x53 = x53)(∀ x53 . x53intx34 x53 = add_SNo x53 x53)(∀ x53 . x53intx35 x53 = x53)x36 = 1(∀ x53 . x53int∀ x54 . x54intx37 x53 x54 = If_i (SNoLe x53 0) x54 (x34 (x37 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx38 x53 = x37 (x35 x53) x36)(∀ x53 . x53intx39 x53 = add_SNo 1 (x38 x53))x40 = add_SNo 1 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx41 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x31 (x41 (add_SNo x53 (minus_SNo 1)) x54 x55) (x42 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx42 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x32 (x41 (add_SNo x53 (minus_SNo 1)) x54 x55) (x42 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx43 x53 = x41 (x33 x53) (x39 x53) x40)(∀ x53 . x53int∀ x54 . x54intx44 x53 x54 = mul_SNo x53 x54)(∀ x53 . x53int∀ x54 . x54intx45 x53 x54 = x54)(∀ x53 . x53intx46 x53 = x53)x47 = 1x48 = add_SNo 1 (add_SNo 2 2)(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx49 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x44 (x49 (add_SNo x53 (minus_SNo 1)) x54 x55) (x50 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx50 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x45 (x49 (add_SNo x53 (minus_SNo 1)) x54 x55) (x50 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx51 x53 = x49 (x46 x53) x47 x48)(∀ x53 . x53intx52 x53 = add_SNo (add_SNo (add_SNo 1 (x30 x53)) (x43 x53)) (x51 x53))∀ x53 . x53intSNoLe 0 x53x20 x53 = x52 x53
Conjecture 835fe..A1545 : ∀ 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 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo 2 (add_SNo x12 x13))(∀ x12 . x12intx1 x12 = add_SNo (mul_SNo 2 (add_SNo x12 x12)) x12)x2 = 2(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx4 x12 = x3 (x1 x12) x2)(∀ x12 . x12intx5 x12 = mul_SNo 2 (x4 x12))(∀ x12 . x12intx6 x12 = add_SNo (mul_SNo x12 x12) x12)x7 = 1(∀ x12 . x12intx8 x12 = add_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x12 x12)) x12))(∀ 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 (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo (x10 x12) (minus_SNo 2))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 901e9..A15457 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 . x5int∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = x24)(∀ x23 . x23intx1 x23 = add_SNo 1 (add_SNo x23 x23))x2 = 2x3 = 2(∀ x23 . x23int∀ x24 . x24intx4 x23 x24 = If_i (SNoLe x23 0) x24 (x1 (x4 (add_SNo x23 (minus_SNo 1)) x24)))x5 = x4 x2 x3(∀ x23 . x23int∀ x24 . x24intx6 x23 x24 = add_SNo (mul_SNo x5 x24) x23)(∀ x23 . x23intx7 x23 = x23)x8 = 1x9 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x6 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx12 x23 = x10 (x7 x23) x8 x9)(∀ x23 . x23intx13 x23 = x12 x23)(∀ x23 . x23int∀ x24 . x24intx14 x23 x24 = add_SNo (mul_SNo (add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) x23) x24)(∀ x23 . x23intx15 x23 = x23)(∀ x23 . x23intx16 x23 = add_SNo x23 (minus_SNo 2))(∀ x23 . x23intx17 x23 = If_i (SNoLe (add_SNo x23 (minus_SNo 1)) 0) 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))))x18 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx21 x23 = x19 (x16 x23) (x17 x23) x18)(∀ x23 . x23intx22 x23 = x21 x23)∀ x23 . x23intSNoLe 0 x23x13 x23 = x22 x23
Conjecture e962a..A154575 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo 2 (add_SNo x12 x13))(∀ x12 . x12intx1 x12 = mul_SNo 2 (add_SNo 2 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))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = add_SNo (add_SNo (x4 x12) x12) x12)(∀ x12 . x12intx6 x12 = mul_SNo x12 x12)x7 = 1(∀ x12 . x12intx8 x12 = add_SNo 1 (add_SNo 2 x12))(∀ 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 (x8 x12))(∀ x12 . x12intx11 x12 = mul_SNo 2 (add_SNo (add_SNo (x10 x12) x12) x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 5fd3f..A15262 : ∀ 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 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 . x19int∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 . x37int∀ x38 . x38int∀ x39 : ι → ι → ι → ι . (∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx39 x40 x41 x42int)∀ x40 : ι → ι → ι → ι . (∀ x41 . x41int∀ x42 . x42int∀ x43 . x43intx40 x41 x42 x43int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)∀ x50 . x50int∀ x51 . x51int∀ x52 : ι → ι → ι → ι . (∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx52 x53 x54 x55int)∀ x53 : ι → ι → ι → ι . (∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx53 x54 x55 x56int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 : ι → ι . (∀ x56 . x56intx55 x56int)∀ x56 . x56int∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι → ι . (∀ x59 . x59int∀ x60 . x60intx58 x59 x60int)∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι → ι . (∀ x61 . x61int∀ x62 . x62intx60 x61 x62int)∀ x61 : ι → ι . (∀ x62 . x62intx61 x62int)∀ x62 . x62int∀ x63 : ι → ι → ι . (∀ x64 . x64int∀ x65 . x65intx63 x64 x65int)∀ x64 : ι → ι . (∀ x65 . x65intx64 x65int)∀ x65 : ι → ι . (∀ x66 . x66intx65 x66int)(∀ x66 . x66int∀ x67 . x67intx0 x66 x67 = mul_SNo (add_SNo 2 x67) x66)x1 = 2(∀ x66 . x66intx2 x66 = x66)(∀ x66 . x66int∀ x67 . x67intx3 x66 x67 = If_i (SNoLe x66 0) x67 (x0 (x3 (add_SNo x66 (minus_SNo 1)) x67) x66))(∀ x66 . x66intx4 x66 = x3 x1 (x2 x66))(∀ x66 . x66intx5 x66 = add_SNo (x4 x66) (minus_SNo x66))(∀ x66 . x66int∀ x67 . x67intx6 x66 x67 = x67)x7 = 1(∀ x66 . x66int∀ x67 . x67intx8 x66 x67 = If_i (SNoLe x66 0) x67 (x5 (x8 (add_SNo x66 (minus_SNo 1)) x67)))(∀ x66 . x66int∀ x67 . x67intx9 x66 x67 = x8 (x6 x66 x67) x7)(∀ x66 . x66int∀ x67 . x67intx10 x66 x67 = add_SNo (x9 x66 x67) (minus_SNo x66))(∀ x66 . x66intx11 x66 = x66)x12 = 1(∀ x66 . x66int∀ x67 . x67intx13 x66 x67 = If_i (SNoLe x66 0) x67 (x10 (x13 (add_SNo x66 (minus_SNo 1)) x67) x66))(∀ x66 . x66intx14 x66 = x13 (x11 x66) x12)(∀ x66 . x66int∀ x67 . x67intx15 x66 x67 = mul_SNo x66 x67)(∀ x66 . x66int∀ x67 . x67intx16 x66 x67 = x67)(∀ x66 . x66intx17 x66 = x66)x18 = 1x19 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx20 x66 x67 x68 = If_i (SNoLe x66 0) x67 (x15 (x20 (add_SNo x66 (minus_SNo 1)) x67 x68) (x21 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx21 x66 x67 x68 = If_i (SNoLe x66 0) x68 (x16 (x20 (add_SNo x66 (minus_SNo 1)) x67 x68) (x21 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66intx22 x66 = x20 (x17 x66) x18 x19)(∀ x66 . x66intx23 x66 = mul_SNo (x14 x66) (x22 x66))x24 = 1(∀ x66 . x66int∀ x67 . x67intx25 x66 x67 = x67)(∀ x66 . x66int∀ x67 . x67intx26 x66 x67 = If_i (SNoLe x66 0) x67 (x23 (x26 (add_SNo x66 (minus_SNo 1)) x67)))(∀ x66 . x66int∀ x67 . x67intx27 x66 x67 = x26 x24 (x25 x66 x67))(∀ x66 . x66int∀ x67 . x67intx28 x66 x67 = add_SNo (x27 x66 x67) x66)(∀ x66 . x66intx29 x66 = x66)x30 = 1(∀ x66 . x66int∀ x67 . x67intx31 x66 x67 = If_i (SNoLe x66 0) x67 (x28 (x31 (add_SNo x66 (minus_SNo 1)) x67) x66))(∀ x66 . x66intx32 x66 = x31 (x29 x66) x30)(∀ x66 . x66intx33 x66 = x32 x66)(∀ x66 . x66int∀ x67 . x67intx34 x66 x67 = mul_SNo x66 x67)(∀ x66 . x66int∀ x67 . x67intx35 x66 x67 = x67)(∀ x66 . x66int∀ x67 . x67intx36 x66 x67 = x67)x37 = 1x38 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx39 x66 x67 x68 = If_i (SNoLe x66 0) x67 (x34 (x39 (add_SNo x66 (minus_SNo 1)) x67 x68) (x40 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx40 x66 x67 x68 = If_i (SNoLe x66 0) x68 (x35 (x39 (add_SNo x66 (minus_SNo 1)) x67 x68) (x40 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66int∀ x67 . x67intx41 x66 x67 = x39 (x36 x66 x67) x37 x38)(∀ x66 . x66int∀ x67 . x67intx42 x66 x67 = add_SNo (x41 x66 x67) (minus_SNo x66))(∀ x66 . x66intx43 x66 = x66)x44 = 1(∀ x66 . x66int∀ x67 . x67intx45 x66 x67 = If_i (SNoLe x66 0) x67 (x42 (x45 (add_SNo x66 (minus_SNo 1)) x67) x66))(∀ x66 . x66intx46 x66 = x45 (x43 x66) x44)(∀ x66 . x66int∀ x67 . x67intx47 x66 x67 = mul_SNo x66 x67)(∀ x66 . x66int∀ x67 . x67intx48 x66 x67 = x67)(∀ x66 . x66intx49 x66 = x66)x50 = 1x51 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx52 x66 x67 x68 = If_i (SNoLe x66 0) x67 (x47 (x52 (add_SNo x66 (minus_SNo 1)) x67 x68) (x53 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66int∀ x67 . x67int∀ x68 . x68intx53 x66 x67 x68 = If_i (SNoLe x66 0) x68 (x48 (x52 (add_SNo x66 (minus_SNo 1)) x67 x68) (x53 (add_SNo x66 (minus_SNo 1)) x67 x68)))(∀ x66 . x66intx54 x66 = x52 (x49 x66) x50 x51)(∀ x66 . x66intx55 x66 = mul_SNo (x46 x66) (x54 x66))x56 = 1(∀ x66 . x66int∀ x67 . x67intx57 x66 x67 = x67)(∀ x66 . x66int∀ x67 . x67intx58 x66 x67 = If_i (SNoLe x66 0) x67 (x55 (x58 (add_SNo x66 (minus_SNo 1)) x67)))(∀ x66 . x66int∀ x67 . x67intx59 x66 x67 = x58 x56 (x57 x66 x67))(∀ x66 . x66int∀ x67 . x67intx60 x66 x67 = add_SNo (x59 x66 x67) x66)(∀ x66 . x66intx61 x66 = x66)x62 = 1(∀ x66 . x66int∀ x67 . x67intx63 x66 x67 = If_i (SNoLe x66 0) x67 (x60 (x63 (add_SNo x66 (minus_SNo 1)) x67) x66))(∀ x66 . x66intx64 x66 = x63 (x61 x66) x62)(∀ x66 . x66intx65 x66 = x64 x66)∀ x66 . x66intSNoLe 0 x66x33 x66 = x65 x66
Conjecture 330d1..A15261 : ∀ 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 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 . x14int∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 . x41int∀ x42 : ι → ι → ι → ι . (∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx42 x43 x44 x45int)∀ x43 : ι → ι → ι → ι . (∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx43 x44 x45 x46int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 . x52int∀ x53 : ι → ι → ι . (∀ x54 . x54int∀ x55 . x55intx53 x54 x55int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 : ι → ι . (∀ x56 . x56intx55 x56int)(∀ x56 . x56intx0 x56 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x56 x56)) x56))(∀ x56 . x56int∀ x57 . x57intx1 x56 x57 = x57)x2 = 1(∀ x56 . x56int∀ x57 . x57intx3 x56 x57 = If_i (SNoLe x56 0) x57 (x0 (x3 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56int∀ x57 . x57intx4 x56 x57 = x3 (x1 x56 x57) x2)(∀ x56 . x56int∀ x57 . x57intx5 x56 x57 = add_SNo (x4 x56 x57) (minus_SNo x56))(∀ x56 . x56intx6 x56 = x56)x7 = 1(∀ x56 . x56int∀ x57 . x57intx8 x56 x57 = If_i (SNoLe x56 0) x57 (x5 (x8 (add_SNo x56 (minus_SNo 1)) x57) x56))(∀ x56 . x56intx9 x56 = x8 (x6 x56) x7)(∀ x56 . x56int∀ x57 . x57intx10 x56 x57 = mul_SNo x56 x57)(∀ x56 . x56int∀ x57 . x57intx11 x56 x57 = x57)(∀ x56 . x56intx12 x56 = x56)x13 = 1x14 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx15 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x10 (x15 (add_SNo x56 (minus_SNo 1)) x57 x58) (x16 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx16 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x11 (x15 (add_SNo x56 (minus_SNo 1)) x57 x58) (x16 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx17 x56 = x15 (x12 x56) x13 x14)(∀ x56 . x56intx18 x56 = mul_SNo (x9 x56) (x17 x56))x19 = 1(∀ x56 . x56int∀ x57 . x57intx20 x56 x57 = x57)(∀ x56 . x56int∀ x57 . x57intx21 x56 x57 = If_i (SNoLe x56 0) x57 (x18 (x21 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56int∀ x57 . x57intx22 x56 x57 = x21 x19 (x20 x56 x57))(∀ x56 . x56int∀ x57 . x57intx23 x56 x57 = add_SNo (x22 x56 x57) x56)(∀ x56 . x56intx24 x56 = x56)x25 = 1(∀ x56 . x56int∀ x57 . x57intx26 x56 x57 = If_i (SNoLe x56 0) x57 (x23 (x26 (add_SNo x56 (minus_SNo 1)) x57) x56))(∀ x56 . x56intx27 x56 = x26 (x24 x56) x25)(∀ x56 . x56intx28 x56 = x27 x56)(∀ x56 . x56int∀ x57 . x57intx29 x56 x57 = add_SNo x57 (minus_SNo x56))(∀ x56 . x56int∀ x57 . x57intx30 x56 x57 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x57 x57)) x57))(∀ x56 . x56intx31 x56 = x56)x32 = 1x33 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx34 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x29 (x34 (add_SNo x56 (minus_SNo 1)) x57 x58) (x35 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx35 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x30 (x34 (add_SNo x56 (minus_SNo 1)) x57 x58) (x35 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx36 x56 = x34 (x31 x56) x32 x33)(∀ x56 . x56int∀ x57 . x57intx37 x56 x57 = mul_SNo x56 x57)(∀ x56 . x56int∀ x57 . x57intx38 x56 x57 = x57)(∀ x56 . x56intx39 x56 = x56)x40 = 1x41 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx42 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x37 (x42 (add_SNo x56 (minus_SNo 1)) x57 x58) (x43 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx43 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x38 (x42 (add_SNo x56 (minus_SNo 1)) x57 x58) (x43 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx44 x56 = x42 (x39 x56) x40 x41)(∀ x56 . x56intx45 x56 = mul_SNo (x36 x56) (x44 x56))x46 = 1(∀ x56 . x56int∀ x57 . x57intx47 x56 x57 = x57)(∀ x56 . x56int∀ x57 . x57intx48 x56 x57 = If_i (SNoLe x56 0) x57 (x45 (x48 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56int∀ x57 . x57intx49 x56 x57 = x48 x46 (x47 x56 x57))(∀ x56 . x56int∀ x57 . x57intx50 x56 x57 = add_SNo (x49 x56 x57) x56)(∀ x56 . x56intx51 x56 = x56)x52 = 1(∀ x56 . x56int∀ x57 . x57intx53 x56 x57 = If_i (SNoLe x56 0) x57 (x50 (x53 (add_SNo x56 (minus_SNo 1)) x57) x56))(∀ x56 . x56intx54 x56 = x53 (x51 x56) x52)(∀ x56 . x56intx55 x56 = x54 x56)∀ x56 . x56intSNoLe 0 x56x28 x56 = x55 x56
Conjecture acb81..A15259 : ∀ 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 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 . x12int∀ x13 : ι → ι → ι → ι . (∀ x14 . x14int∀ x15 . x15int∀ x16 . x16intx13 x14 x15 x16int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ 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 . 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 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 . x31int∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι → ι → ι . (∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx33 x34 x35 x36int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 . x52int∀ x53 : ι → ι → ι . (∀ x54 . x54int∀ x55 . x55intx53 x54 x55int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 : ι → ι . (∀ x56 . x56intx55 x56int)(∀ x56 . x56int∀ x57 . x57intx0 x56 x57 = add_SNo (mul_SNo (mul_SNo x57 x57) x57) (minus_SNo x56))(∀ x56 . x56int∀ x57 . x57intx1 x56 x57 = add_SNo x57 x57)(∀ x56 . x56intx2 x56 = x56)x3 = 1x4 = 2(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx5 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x0 (x5 (add_SNo x56 (minus_SNo 1)) x57 x58) (x6 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx6 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x1 (x5 (add_SNo x56 (minus_SNo 1)) x57 x58) (x6 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx7 x56 = x5 (x2 x56) x3 x4)(∀ x56 . x56int∀ x57 . x57intx8 x56 x57 = mul_SNo x56 x57)(∀ x56 . x56int∀ x57 . x57intx9 x56 x57 = x57)(∀ x56 . x56intx10 x56 = x56)x11 = 1x12 = mul_SNo 2 (add_SNo 2 2)(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx13 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x8 (x13 (add_SNo x56 (minus_SNo 1)) x57 x58) (x14 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx14 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x9 (x13 (add_SNo x56 (minus_SNo 1)) x57 x58) (x14 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx15 x56 = x13 (x10 x56) x11 x12)(∀ x56 . x56intx16 x56 = mul_SNo (x7 x56) (x15 x56))x17 = 1(∀ x56 . x56int∀ x57 . x57intx18 x56 x57 = x57)(∀ x56 . x56int∀ x57 . x57intx19 x56 x57 = If_i (SNoLe x56 0) x57 (x16 (x19 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56int∀ x57 . x57intx20 x56 x57 = x19 x17 (x18 x56 x57))(∀ x56 . x56int∀ x57 . x57intx21 x56 x57 = add_SNo (x20 x56 x57) x56)(∀ x56 . x56intx22 x56 = x56)x23 = 1(∀ x56 . x56int∀ x57 . x57intx24 x56 x57 = If_i (SNoLe x56 0) x57 (x21 (x24 (add_SNo x56 (minus_SNo 1)) x57) x56))(∀ x56 . x56intx25 x56 = x24 (x22 x56) x23)(∀ x56 . x56intx26 x56 = x25 x56)(∀ x56 . x56int∀ x57 . x57intx27 x56 x57 = add_SNo (mul_SNo (mul_SNo x57 x57) x57) (minus_SNo x56))(∀ x56 . x56int∀ x57 . x57intx28 x56 x57 = add_SNo x57 x57)(∀ x56 . x56intx29 x56 = x56)x30 = 1x31 = 2(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx32 x56 x57 x58 = If_i (SNoLe x56 0) x57 (x27 (x32 (add_SNo x56 (minus_SNo 1)) x57 x58) (x33 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56int∀ x57 . x57int∀ x58 . x58intx33 x56 x57 x58 = If_i (SNoLe x56 0) x58 (x28 (x32 (add_SNo x56 (minus_SNo 1)) x57 x58) (x33 (add_SNo x56 (minus_SNo 1)) x57 x58)))(∀ x56 . x56intx34 x56 = x32 (x29 x56) x30 x31)(∀ x56 . x56intx35 x56 = mul_SNo (mul_SNo x56 x56) x56)x36 = 1(∀ x56 . x56intx37 x56 = add_SNo x56 x56)(∀ x56 . x56intx38 x56 = x56)x39 = 1(∀ x56 . x56int∀ x57 . x57intx40 x56 x57 = If_i (SNoLe x56 0) x57 (x37 (x40 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56intx41 x56 = x40 (x38 x56) x39)(∀ x56 . x56intx42 x56 = x41 x56)(∀ x56 . x56int∀ x57 . x57intx43 x56 x57 = If_i (SNoLe x56 0) x57 (x35 (x43 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56intx44 x56 = x43 x36 (x42 x56))(∀ x56 . x56intx45 x56 = mul_SNo (x34 x56) (x44 x56))x46 = 1(∀ x56 . x56int∀ x57 . x57intx47 x56 x57 = x57)(∀ x56 . x56int∀ x57 . x57intx48 x56 x57 = If_i (SNoLe x56 0) x57 (x45 (x48 (add_SNo x56 (minus_SNo 1)) x57)))(∀ x56 . x56int∀ x57 . x57intx49 x56 x57 = x48 x46 (x47 x56 x57))(∀ x56 . x56int∀ x57 . x57intx50 x56 x57 = add_SNo (x49 x56 x57) x56)(∀ x56 . x56intx51 x56 = x56)x52 = 1(∀ x56 . x56int∀ x57 . x57intx53 x56 x57 = If_i (SNoLe x56 0) x57 (x50 (x53 (add_SNo x56 (minus_SNo 1)) x57) x56))(∀ x56 . x56intx54 x56 = x53 (x51 x56) x52)(∀ x56 . x56intx55 x56 = x54 x56)∀ x56 . x56intSNoLe 0 x56x26 x56 = x55 x56
Conjecture 15163..A15013 : ∀ 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 . 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 (minus_SNo (add_SNo x20 x20)))(∀ x20 . x20int∀ x21 . x21intx1 x20 x21 = x21)x2 = 1(∀ 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 x20 x21) x2)(∀ 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 1 (minus_SNo (add_SNo x21 x21)))(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 0 (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 1b62e..A15000 : ∀ 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 . 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 = mul_SNo (add_SNo 2 x21) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ 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 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo 1 (minus_SNo (add_SNo (x4 x20) 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 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (minus_SNo (mul_SNo x20 x21)))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = 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 37f08..A14994 : ∀ 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 . 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 = mul_SNo (add_SNo 2 x21) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ 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 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo 1 (minus_SNo (x4 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 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (minus_SNo (mul_SNo x20 x21)))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = 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 ba35e..A14993 : ∀ 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 . 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 = mul_SNo (add_SNo 2 x21) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ 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 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo 1 (add_SNo x20 (minus_SNo (x4 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 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (mul_SNo x20 x21))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (minus_SNo (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 11705..A14992 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo 1 (minus_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15))))(∀ x15 . x15intx1 x15 = x15)x2 = 1(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = x4 x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = add_SNo 1 (minus_SNo (mul_SNo x15 x16)))(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 1x10 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) x9 x10)(∀ x15 . x15intx14 x15 = x13 x15)∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture cee99..A14991 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . 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 (add_SNo x20 x20) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx4 x20 = x3 x1 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo 1 (minus_SNo (x4 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 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (minus_SNo (mul_SNo x20 x21)))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (mul_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