Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNRc../16e9c..
PUf9i../0482c..
vout
PrNRc../0e189.. 23.99 bars
PUfac../c2dfe.. doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Param ordsuccordsucc : ιι
Conjecture 83a8a..A133073 : ∀ 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 . x8intx0 x7 x8 = add_SNo (add_SNo x7 x8) x8)(∀ x7 . x7intx1 x7 = mul_SNo x7 x7)(∀ x7 . x7intx2 x7 = x7)(∀ 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))(∀ x7 . x7intx5 x7 = mul_SNo (x4 x7) x7)(∀ x7 . x7intx6 x7 = mul_SNo (add_SNo 1 (add_SNo (mul_SNo (mul_SNo x7 x7) x7) x7)) (mul_SNo x7 x7))∀ x7 . x7intSNoLe 0 x7x5 x7 = x6 x7
Conjecture e854b..A132911 : ∀ 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 : ι → ι . (∀ x9 . x9intx8 x9int)∀ 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 . 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 (mul_SNo (add_SNo 1 (add_SNo x21 x21)) (mul_SNo x20 x21)) (minus_SNo 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)(∀ x20 . x20intx8 x20 = add_SNo 1 x20)(∀ 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))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo 2 x21)(∀ x20 . x20intx13 x20 = add_SNo x20 (minus_SNo 1))x14 = 1x15 = 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 x15)(∀ x20 . x20intx19 x20 = mul_SNo (x10 x20) (x18 x20))∀ x20 . x20intSNoLe 0 x20x5 x20 = x19 x20
Conjecture 64261..A132371 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ 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 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25int∀ x26 . x26intx0 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx1 x25 x26 = x26)(∀ x25 . x25int∀ x26 . x26intx2 x25 x26 = add_SNo x26 (minus_SNo 1))(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25int∀ x26 . x26intx4 x25 x26 = x3 (x1 x25 x26) (x2 x25 x26))(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = add_SNo (x4 x25 x26) x25)(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo (add_SNo x25 (minus_SNo 1)) x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = add_SNo x26 (minus_SNo 1))(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = x25)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx16 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx17 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx18 x25 = x16 (x13 x25) x14 (x15 x25))(∀ x25 . x25int∀ x26 . x26intx19 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25intx20 x25 = x25)(∀ x25 . x25intx21 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx23 x25 = x22 (x20 x25) (x21 x25))(∀ x25 . x25intx24 x25 = add_SNo (x18 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture a7319..A1308 : ∀ 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 . x23int∀ x24 . x24intx0 x23 x24 = mul_SNo (add_SNo (mul_SNo 2 (mul_SNo x23 x24)) (minus_SNo x23)) (mul_SNo (mul_SNo (add_SNo 1 x24) x24) x24))(∀ x23 . x23int∀ x24 . x24intx1 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx2 x23 = x23)x3 = 1x4 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx7 x23 = x5 (x2 x23) x3 x4)(∀ x23 . x23intx8 x23 = x7 x23)(∀ x23 . x23int∀ x24 . x24intx9 x23 x24 = mul_SNo (mul_SNo (add_SNo (mul_SNo (mul_SNo x24 x24) x24) (minus_SNo x24)) x24) x23)(∀ x23 . x23int∀ x24 . x24intx10 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx11 x23 = x23)x12 = 1x13 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx14 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x9 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx15 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x10 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx16 x23 = x14 (x11 x23) x12 x13)(∀ x23 . x23intx17 x23 = add_SNo 1 (add_SNo x23 x23))(∀ x23 . x23intx18 x23 = x23)x19 = 1(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x17 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x18 x23) x19)(∀ x23 . x23intx22 x23 = mul_SNo (x16 x23) (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23
Conjecture a9794..A130652 : ∀ 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 (x4 x20) (minus_SNo x20))(∀ x20 . x20intx6 x20 = add_SNo 1 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 = add_SNo (x9 x20) (minus_SNo 2))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = add_SNo 1 x20)x14 = 1x15 = add_SNo 1 (add_SNo 2 (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 = add_SNo (x18 x20) (minus_SNo 2))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 7d032..A129890 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ 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 . x30int∀ x31 . x31intx0 x30 x31 = mul_SNo 2 (mul_SNo x30 x31))(∀ x30 . x30int∀ x31 . x31intx1 x30 x31 = x31)x2 = 1(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30int∀ x31 . x31intx4 x30 x31 = x3 (x1 x30 x31) x2)(∀ x30 . x30int∀ x31 . x31intx5 x30 x31 = add_SNo (add_SNo (mul_SNo 2 (mul_SNo x30 x31)) (x4 x30 x31)) 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))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = x9 x30)(∀ x30 . x30intx11 x30 = add_SNo x30 x30)(∀ x30 . x30intx12 x30 = x30)x13 = 2(∀ x30 . x30int∀ x31 . x31intx14 x30 x31 = If_i (SNoLe x30 0) x31 (x11 (x14 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx15 x30 = x14 (x12 x30) x13)(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30intx17 x30 = x30)(∀ x30 . x30intx18 x30 = add_SNo 1 x30)(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x16 (x19 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx20 x30 = x19 (x17 x30) (x18 x30))(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = add_SNo 2 x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = add_SNo 1 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 (mul_SNo (x15 x30) (x20 x30)) (minus_SNo (x28 x30)))∀ x30 . x30intSNoLe 0 x30x10 x30 = x29 x30
Conjecture c2cb1..A128965 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x15 x15) x15)) x15)(∀ x15 . x15intx1 x15 = add_SNo x15 1)(∀ x15 . x15intx2 x15 = add_SNo 2 x15)(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) (x2 x15))(∀ x15 . x15intx5 x15 = mul_SNo (mul_SNo (add_SNo 1 x15) (x4 x15)) x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = add_SNo 1 x15)(∀ x15 . x15intx9 x15 = add_SNo 1 x15)x10 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = mul_SNo (mul_SNo (x13 x15) (add_SNo 2 x15)) x15)∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 2277e..A128803 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo (add_SNo x15 x15) x15)(∀ x15 . x15intx1 x15 = add_SNo x15 x15)(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) (x2 x15))(∀ x15 . x15intx5 x15 = mul_SNo (add_SNo x15 (minus_SNo 1)) (x4 x15))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)(∀ x15 . x15intx9 x15 = x15)x10 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = mul_SNo (add_SNo x15 (minus_SNo 1)) (x13 x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 06f13..A128802 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo (add_SNo x17 x17) x17)(∀ x17 . x17intx2 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) (x2 x17))(∀ x17 . x17intx5 x17 = mul_SNo (add_SNo x17 (minus_SNo 1)) (x4 x17))(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = add_SNo x17 (minus_SNo 1))x10 = 2(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo (add_SNo (mul_SNo x17 x17) (minus_SNo x17)) (x15 x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 47e8b..A128800 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = mul_SNo 2 (add_SNo (add_SNo x15 x15) x15))(∀ x15 . x15intx1 x15 = x15)(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) (x2 x15))(∀ x15 . x15intx5 x15 = mul_SNo (add_SNo x15 (minus_SNo 1)) (x4 x15))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)(∀ x15 . x15intx9 x15 = x15)x10 = add_SNo 2 (add_SNo 2 2)(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = mul_SNo (add_SNo x15 (minus_SNo 1)) (x13 x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 6414d..A128791 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15)(∀ x15 . x15intx1 x15 = x15)(∀ x15 . x15intx2 x15 = x15)(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) (x2 x15))(∀ x15 . x15intx5 x15 = mul_SNo (mul_SNo (x4 x15) x15) x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)(∀ x15 . x15intx9 x15 = x15)x10 = add_SNo 1 (add_SNo 2 2)(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = mul_SNo (mul_SNo x15 x15) (x13 x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 1e182..A128790 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)(∀ x17 . x17intx2 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) (x2 x17))(∀ x17 . x17intx5 x17 = mul_SNo (mul_SNo (x4 x17) x17) x17)(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)(∀ x17 . x17intx10 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) (x10 x17))(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo (x15 x17) x17)∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 67d6d..A127859 : ∀ 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 = add_SNo (mul_SNo (add_SNo 2 x21) x20) (minus_SNo 1))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 = x4 x20)(∀ x20 . x20intx6 x20 = add_SNo 1 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 2 (mul_SNo x20 x21))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 2x15 = 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 = add_SNo (mul_SNo (add_SNo 1 2) (x18 x20)) 1)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 9f2c8..A127858 : ∀ 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 = add_SNo 2 (minus_SNo (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 = x4 x20)(∀ x20 . x20intx6 x20 = add_SNo 1 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 (mul_SNo x20 x21) (minus_SNo 2))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 2x15 = 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 = mul_SNo (x18 x20) (add_SNo 1 2))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 41629..A1277 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)(∀ x37 . x37intx0 x37 = add_SNo 0 (minus_SNo x37))(∀ x37 . x37int∀ x38 . x38intx1 x37 x38 = x38)x2 = 1(∀ x37 . x37int∀ x38 . x38intx3 x37 x38 = If_i (SNoLe x37 0) x38 (x0 (x3 (add_SNo x37 (minus_SNo 1)) x38)))(∀ x37 . x37int∀ x38 . x38intx4 x37 x38 = x3 (x1 x37 x38) x2)(∀ x37 . x37int∀ x38 . x38intx5 x37 x38 = add_SNo (mul_SNo (add_SNo 2 x38) x37) (x4 x37 x38))(∀ x37 . x37int∀ x38 . x38intx6 x37 x38 = x38)x7 = 1(∀ x37 . x37int∀ x38 . x38intx8 x37 x38 = If_i (SNoLe x37 0) x38 (x5 (x8 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37int∀ x38 . x38intx9 x37 x38 = x8 (x6 x37 x38) x7)(∀ x37 . x37int∀ x38 . x38intx10 x37 x38 = add_SNo (x9 x37 x38) x37)(∀ x37 . x37intx11 x37 = x37)x12 = 1(∀ x37 . x37int∀ x38 . x38intx13 x37 x38 = If_i (SNoLe x37 0) x38 (x10 (x13 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx14 x37 = x13 (x11 x37) x12)(∀ x37 . x37intx15 x37 = x14 x37)(∀ x37 . x37int∀ x38 . x38intx16 x37 x38 = add_SNo 1 (minus_SNo (mul_SNo x37 x38)))(∀ x37 . x37intx17 x37 = add_SNo 2 x37)x18 = 1(∀ x37 . x37int∀ x38 . x38intx19 x37 x38 = If_i (SNoLe x37 0) x38 (x16 (x19 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx20 x37 = x19 (x17 x37) x18)(∀ x37 . x37intx21 x37 = add_SNo 0 (minus_SNo x37))(∀ x37 . x37intx22 x37 = x37)x23 = 1(∀ x37 . x37int∀ x38 . x38intx24 x37 x38 = If_i (SNoLe x37 0) x38 (x21 (x24 (add_SNo x37 (minus_SNo 1)) x38)))(∀ x37 . x37intx25 x37 = x24 (x22 x37) x23)(∀ x37 . x37intx26 x37 = mul_SNo (x20 x37) (x25 x37))x27 = 1(∀ x37 . x37int∀ x38 . x38intx28 x37 x38 = x38)(∀ x37 . x37int∀ x38 . x38intx29 x37 x38 = If_i (SNoLe x37 0) x38 (x26 (x29 (add_SNo x37 (minus_SNo 1)) x38)))(∀ x37 . x37int∀ x38 . x38intx30 x37 x38 = x29 x27 (x28 x37 x38))(∀ x37 . x37int∀ x38 . x38intx31 x37 x38 = add_SNo (x30 x37 x38) x37)(∀ x37 . x37intx32 x37 = x37)x33 = 1(∀ x37 . x37int∀ x38 . x38intx34 x37 x38 = If_i (SNoLe x37 0) x38 (x31 (x34 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx35 x37 = x34 (x32 x37) x33)(∀ x37 . x37intx36 x37 = x35 x37)∀ x37 . x37intSNoLe 0 x37x15 x37 = x36 x37
Conjecture 7a36c..A127595 : ∀ 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 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ 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 : ι → ι → ι . (∀ 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 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 . x29int∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)(∀ x34 . x34int∀ x35 . x35intx0 x34 x35 = add_SNo x34 x35)(∀ x34 . x34intx1 x34 = x34)(∀ x34 . x34intx2 x34 = mul_SNo 2 (add_SNo x34 x34))x3 = 0x4 = 1(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx5 x34 x35 x36 = If_i (SNoLe x34 0) x35 (x0 (x5 (add_SNo x34 (minus_SNo 1)) x35 x36) (x6 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx6 x34 x35 x36 = If_i (SNoLe x34 0) x36 (x1 (x5 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34intx7 x34 = x5 (x2 x34) x3 x4)(∀ x34 . x34int∀ x35 . x35intx8 x34 x35 = add_SNo x34 x35)(∀ x34 . x34intx9 x34 = x34)(∀ x34 . x34intx10 x34 = add_SNo x34 x34)x11 = 0x12 = 2(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx13 x34 x35 x36 = If_i (SNoLe x34 0) x35 (x8 (x13 (add_SNo x34 (minus_SNo 1)) x35 x36) (x14 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx14 x34 x35 x36 = If_i (SNoLe x34 0) x36 (x9 (x13 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34intx15 x34 = x13 (x10 x34) x11 x12)(∀ x34 . x34intx16 x34 = add_SNo (x7 x34) (minus_SNo (x15 x34)))(∀ x34 . x34int∀ x35 . x35intx17 x34 x35 = add_SNo (add_SNo x34 x34) x35)(∀ x34 . x34int∀ x35 . x35intx18 x34 x35 = add_SNo x34 x35)(∀ x34 . x34intx19 x34 = add_SNo x34 (minus_SNo 1))x20 = add_SNo 1 2x21 = 1(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx22 x34 x35 x36 = If_i (SNoLe x34 0) x35 (x17 (x22 (add_SNo x34 (minus_SNo 1)) x35 x36) (x23 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx23 x34 x35 x36 = If_i (SNoLe x34 0) x36 (x18 (x22 (add_SNo x34 (minus_SNo 1)) x35 x36) (x23 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34intx24 x34 = x22 (x19 x34) x20 x21)(∀ x34 . x34int∀ x35 . x35intx25 x34 x35 = add_SNo x34 x35)(∀ x34 . x34intx26 x34 = x34)(∀ x34 . x34intx27 x34 = add_SNo x34 x34)x28 = 0x29 = 1(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx30 x34 x35 x36 = If_i (SNoLe x34 0) x35 (x25 (x30 (add_SNo x34 (minus_SNo 1)) x35 x36) (x31 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx31 x34 x35 x36 = If_i (SNoLe x34 0) x36 (x26 (x30 (add_SNo x34 (minus_SNo 1)) x35 x36)))(∀ x34 . x34intx32 x34 = x30 (x27 x34) x28 x29)(∀ x34 . x34intx33 x34 = mul_SNo (add_SNo (x24 x34) (minus_SNo 2)) (x32 x34))∀ x34 . x34intSNoLe 0 x34x16 x34 = x33 x34
Conjecture 414ea..A127429 : ∀ 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 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ 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 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33int∀ x34 . x34intx0 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx1 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx2 x33 = x33)x3 = 1x4 = 1(∀ 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 . x33intx7 x33 = x5 (x2 x33) x3 x4)(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = mul_SNo 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 = add_SNo (x7 x33) (minus_SNo (x12 x33)))(∀ x33 . x33intx14 x33 = add_SNo x33 x33)(∀ x33 . x33intx15 x33 = add_SNo x33 (minus_SNo 1))x16 = 1(∀ x33 . x33int∀ x34 . x34intx17 x33 x34 = If_i (SNoLe x33 0) x34 (x14 (x17 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx18 x33 = x17 (x15 x33) x16)(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx21 x33 = add_SNo x33 (minus_SNo 2))x22 = 1x23 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x19 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x20 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx26 x33 = x24 (x21 x33) x22 x23)(∀ x33 . x33int∀ x34 . x34intx27 x33 x34 = mul_SNo x33 x34)(∀ 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 = add_SNo (mul_SNo (x18 x33) (x26 x33)) (minus_SNo (x31 x33)))∀ x33 . x33intSNoLe 0 x33x13 x33 = x32 x33
Conjecture 48e32..A127212 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . 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 (mul_SNo 2 (add_SNo x31 x31)) x31)(∀ x31 . x31intx1 x31 = add_SNo 1 x31)(∀ x31 . x31int∀ x32 . x32intx2 x31 x32 = add_SNo x31 x32)(∀ x31 . x31intx3 x31 = x31)(∀ x31 . x31intx4 x31 = x31)x5 = 1x6 = 2(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx7 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x2 (x7 (add_SNo x31 (minus_SNo 1)) x32 x33) (x8 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx8 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x3 (x7 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx9 x31 = x7 (x4 x31) x5 x6)(∀ x31 . x31intx10 x31 = x9 x31)(∀ x31 . x31int∀ x32 . x32intx11 x31 x32 = If_i (SNoLe x31 0) x32 (x0 (x11 (add_SNo x31 (minus_SNo 1)) x32)))(∀ x31 . x31intx12 x31 = x11 (x1 x31) (x10 x31))(∀ x31 . x31intx13 x31 = x12 x31)(∀ x31 . x31int∀ x32 . x32intx14 x31 x32 = add_SNo x31 x32)(∀ x31 . x31intx15 x31 = x31)(∀ x31 . x31intx16 x31 = x31)x17 = 1x18 = 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)))(∀ 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 = add_SNo 1 (add_SNo 2 2)x26 = add_SNo 1 (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 = mul_SNo (x21 x31) (x29 x31))∀ x31 . x31intSNoLe 0 x31x13 x31 = x30 x31
Conjecture 38a0a..A124657 : ∀ 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 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = mul_SNo (add_SNo 2 x13) x12)(∀ x12 . x12intx1 x12 = add_SNo 2 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 = x4 x12)(∀ x12 . x12int∀ x13 . x13intx6 x12 x13 = mul_SNo x12 x13)(∀ x12 . x12intx7 x12 = add_SNo 2 (add_SNo 2 x12))x8 = 1(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx10 x12 = x9 (x7 x12) x8)(∀ x12 . x12intx11 x12 = x10 x12)∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 77a11..A1240 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ 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 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = add_SNo (add_SNo x28 x28) x28)(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = add_SNo 1 x29)x2 = 1(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28int∀ x29 . x29intx4 x28 x29 = x3 (x1 x28 x29) x2)(∀ x28 . x28int∀ x29 . x29intx5 x28 x29 = add_SNo (add_SNo (x4 x28 x29) x28) x28)(∀ x28 . x28int∀ x29 . x29intx6 x28 x29 = x29)(∀ x28 . x28intx7 x28 = x28)x8 = 1(∀ x28 . x28intx9 x28 = x28)(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx10 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x5 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30) (x11 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx11 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x6 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30) (x11 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx12 x28 = x10 (x7 x28) x8 (x9 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx15 x28 x29 = x29)(∀ x28 . x28intx16 x28 = x28)x17 = add_SNo 1 2x18 = add_SNo 1 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28intx22 x28 = add_SNo x28 x28)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = add_SNo (mul_SNo (add_SNo 1 (x21 x28)) (add_SNo (x26 x28) (minus_SNo 1))) 1)∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28