Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr66d../ec36e..
PUgTv../e84c6..
vout
Pr66d../95d3e.. 0.97 bars
PUU5U../bc442.. doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Conjecture e5f1a..A20527 : ∀ 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 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = mul_SNo 2 (add_SNo 2 x22))(∀ x22 . x22intx3 x22 = x22)x4 = 2(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo (x6 x22) (minus_SNo 2))(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = add_SNo (x9 x22) 1)(∀ x22 . x22intx11 x22 = add_SNo (mul_SNo x22 x22) (minus_SNo x22))x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 1(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = x17 x22)(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = add_SNo 1 (mul_SNo 2 (mul_SNo (add_SNo 1 2) (x20 x22))))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture eb41b..A20515 : ∀ 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 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo (add_SNo x22 (minus_SNo 1)) x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = add_SNo x22 x22)(∀ x22 . x22intx3 x22 = x22)x4 = 1(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = x6 x22)(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = add_SNo (mul_SNo x22 x22) (minus_SNo x22))x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 1(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = x17 x22)(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = add_SNo 1 (x20 x22))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 522e6..A20499 : ∀ 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 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ 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 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40intx0 x40 = add_SNo (add_SNo x40 x40) x40)(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = add_SNo x41 x41)x2 = 1(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx4 x40 x41 = x3 (x1 x40 x41) x2)(∀ x40 . x40int∀ x41 . x41intx5 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x6 = 2(∀ x40 . x40intx7 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx9 x40 = x8 x6 (x7 x40))(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x4 x40 x41) (add_SNo (x9 x40) (minus_SNo x40)))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x40 x40)) (mul_SNo x41 x41)) x40)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo (add_SNo x41 x41) x41)(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) x40)(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture 4a08b..A20494 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ 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 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50intx15 x50 = add_SNo (add_SNo x50 x50) x50)x16 = 2(∀ x50 . x50intx17 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx19 x50 = x18 x16 (x17 x50))(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (x14 x50 x51) (x19 x50))(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50int∀ x51 . x51intx31 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = x51)(∀ x50 . x50intx33 x50 = x50)x34 = 1x35 = add_SNo 1 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx36 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x31 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx37 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x32 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx38 x50 = x36 (x33 x50) x34 x35)(∀ x50 . x50intx39 x50 = mul_SNo (add_SNo (x30 x50) (minus_SNo 1)) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50)))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 335ea..A20448 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . 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 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ 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 . x48intx47 x48int)(∀ x48 . x48int∀ x49 . x49intx0 x48 x49 = mul_SNo (add_SNo 2 x49) x48)x1 = 2(∀ x48 . x48intx2 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx3 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x3 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx4 x48 = x3 x1 (x2 x48))(∀ x48 . x48int∀ x49 . x49intx5 x48 x49 = add_SNo (x4 x48) (mul_SNo (mul_SNo x49 x49) x49))(∀ x48 . x48int∀ x49 . x49intx6 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx7 x48 x49 = x49)x8 = 1x9 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx10 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x5 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx11 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x6 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx12 x48 x49 = x10 (x7 x48 x49) x8 x9)(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = add_SNo (add_SNo (x12 x48 x49) (mul_SNo 2 (add_SNo x48 x48))) x48)(∀ x48 . x48intx14 x48 = x48)x15 = 1(∀ x48 . x48int∀ x49 . x49intx16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx17 x48 = x16 (x14 x48) x15)(∀ x48 . x48intx18 x48 = x17 x48)(∀ x48 . x48int∀ x49 . x49intx19 x48 x49 = add_SNo (add_SNo (add_SNo x48 x48) x48) x49)(∀ x48 . x48int∀ x49 . x49intx20 x48 x49 = add_SNo x49 x49)(∀ x48 . x48intx21 x48 = x48)x22 = 1x23 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx24 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x19 (x24 (add_SNo x48 (minus_SNo 1)) x49 x50) (x25 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx25 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x20 (x24 (add_SNo x48 (minus_SNo 1)) x49 x50) (x25 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx26 x48 = x24 (x21 x48) x22 x23)(∀ x48 . x48intx27 x48 = mul_SNo x48 x48)x28 = 1(∀ x48 . x48intx29 x48 = add_SNo x48 x48)(∀ x48 . x48intx30 x48 = add_SNo x48 (minus_SNo 1))x31 = 2(∀ x48 . x48int∀ x49 . x49intx32 x48 x49 = If_i (SNoLe x48 0) x49 (x29 (x32 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx33 x48 = x32 (x30 x48) x31)(∀ x48 . x48intx34 x48 = x33 x48)(∀ x48 . x48int∀ x49 . x49intx35 x48 x49 = If_i (SNoLe x48 0) x49 (x27 (x35 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx36 x48 = x35 x28 (x34 x48))(∀ x48 . x48intx37 x48 = mul_SNo (x26 x48) (x36 x48))x38 = 1(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 x38 (x39 x48 x49))(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo x48 x48))) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 1(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x18 x48 = x47 x48
Conjecture 0ec49..A2042 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)x2 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo (add_SNo 1 (add_SNo 2 (add_SNo 2 2))) (x15 x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture d94bc..A204245 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 . x18int∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ 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 . x37int∀ x38 . x38intx0 x37 x38 = add_SNo (add_SNo (mul_SNo x37 x38) (minus_SNo 1)) x37)(∀ x37 . x37intx1 x37 = x37)x2 = 1(∀ x37 . x37int∀ x38 . x38intx3 x37 x38 = If_i (SNoLe x37 0) x38 (x0 (x3 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx4 x37 = x3 (x1 x37) x2)(∀ x37 . x37int∀ x38 . x38intx5 x37 x38 = mul_SNo x37 x38)(∀ x37 . x37int∀ x38 . x38intx6 x37 x38 = x38)(∀ x37 . x37intx7 x37 = x37)(∀ 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))(∀ x37 . x37int∀ x38 . x38intx10 x37 x38 = x9 x37 x38)(∀ 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 = mul_SNo (x4 x37) (x14 x37))(∀ x37 . x37int∀ x38 . x38intx16 x37 x38 = mul_SNo x37 x38)(∀ x37 . x37int∀ x38 . x38intx17 x37 x38 = x38)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 . x37int∀ x38 . x38intx20 x37 x38 = x19 (x17 x37 x38) x18)(∀ x37 . x37int∀ x38 . x38intx21 x37 x38 = mul_SNo (x20 x37 x38) x37)(∀ x37 . x37intx22 x37 = add_SNo x37 (minus_SNo 1))x23 = 1(∀ x37 . x37int∀ x38 . x38intx24 x37 x38 = If_i (SNoLe x37 0) x38 (x21 (x24 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx25 x37 = x24 (x22 x37) x23)(∀ x37 . x37int∀ x38 . x38intx26 x37 x38 = mul_SNo x37 x38)(∀ x37 . x37intx27 x37 = x37)x28 = 1(∀ x37 . x37int∀ x38 . x38intx29 x37 x38 = If_i (SNoLe x37 0) x38 (x26 (x29 (add_SNo x37 (minus_SNo 1)) x38) x37))(∀ x37 . x37intx30 x37 = x29 (x27 x37) x28)(∀ x37 . x37int∀ x38 . x38intx31 x37 x38 = add_SNo (mul_SNo x37 x38) (add_SNo x37 (minus_SNo 1)))(∀ 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 = mul_SNo (mul_SNo (x25 x37) (x30 x37)) (x35 x37))∀ x37 . x37intSNoLe 0 x37x15 x37 = x36 x37
Conjecture 1e568..A203579 : ∀ 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 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = x24)(∀ x23 . x23int∀ x24 . x24intx1 x23 x24 = mul_SNo 2 (add_SNo (add_SNo x23 x23) x24))(∀ x23 . x23intx2 x23 = x23)x3 = 1x4 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (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 = add_SNo 1 (x7 x23))(∀ x23 . x23intx9 x23 = add_SNo x23 x23)(∀ x23 . x23intx10 x23 = add_SNo x23 (minus_SNo 1))(∀ x23 . x23int∀ x24 . x24intx11 x23 x24 = add_SNo x23 x24)(∀ x23 . x23intx12 x23 = x23)(∀ x23 . x23intx13 x23 = add_SNo x23 (minus_SNo 1))x14 = 1x15 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx16 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x11 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25) (x17 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx17 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x12 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx18 x23 = x16 (x13 x23) x14 x15)(∀ x23 . x23intx19 x23 = x18 x23)(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x9 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x10 x23) (x19 x23))(∀ x23 . x23intx22 x23 = add_SNo 1 (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23
Conjecture 0050f..A20346 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45)(∀ x45 . x45intx1 x45 = x45)(∀ x45 . x45intx2 x45 = add_SNo x45 x45)(∀ x45 . x45intx3 x45 = x45)x4 = 2(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = If_i (SNoLe x45 0) x46 (x2 (x5 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx6 x45 = x5 (x3 x45) x4)(∀ x45 . x45intx7 x45 = add_SNo (x6 x45) (minus_SNo 1))(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx9 x45 = x8 (x1 x45) (x7 x45))(∀ x45 . x45intx10 x45 = x9 x45)x11 = 1(∀ x45 . x45int∀ x46 . x46intx12 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx14 x45 x46 = x13 x11 (x12 x45 x46))(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = add_SNo (x14 x45 x46) (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))))(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = x19 x45)(∀ x45 . x45intx21 x45 = add_SNo x45 x45)(∀ x45 . x45intx22 x45 = x45)x23 = 2(∀ x45 . x45int∀ x46 . x46intx24 x45 x46 = If_i (SNoLe x45 0) x46 (x21 (x24 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx25 x45 = x24 (x22 x45) x23)(∀ x45 . x45int∀ x46 . x46intx26 x45 x46 = mul_SNo x45 x46)(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = x46)(∀ x45 . x45intx28 x45 = x45)x29 = 1x30 = add_SNo 1 (add_SNo 2 2)(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx33 x45 = x31 (x28 x45) x29 x30)(∀ x45 . x45intx34 x45 = mul_SNo (add_SNo (x25 x45) (minus_SNo 1)) (x33 x45))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (x38 x45 x46) (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))))(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture b7c3a..A20343 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo (add_SNo x45 x45) x45)(∀ x45 . x45int∀ x46 . x46intx1 x45 x46 = add_SNo x46 x46)x2 = 1(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx4 x45 x46 = x3 (x1 x45 x46) x2)(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = add_SNo (x4 x45 x46) (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))))(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (add_SNo (x9 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45intx11 x45 = x45)x12 = 1(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx14 x45 = x13 (x11 x45) x12)(∀ x45 . x45intx15 x45 = x14 x45)(∀ x45 . x45int∀ x46 . x46intx16 x45 x46 = mul_SNo x45 x46)(∀ x45 . x45int∀ x46 . x46intx17 x45 x46 = x46)(∀ x45 . x45intx18 x45 = add_SNo 1 x45)x19 = 1x20 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx21 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x16 (x21 (add_SNo x45 (minus_SNo 1)) x46 x47) (x22 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx22 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x17 (x21 (add_SNo x45 (minus_SNo 1)) x46 x47) (x22 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx23 x45 = x21 (x18 x45) x19 x20)(∀ x45 . x45intx24 x45 = mul_SNo (mul_SNo x45 x45) x45)x25 = 1(∀ x45 . x45intx26 x45 = add_SNo x45 x45)(∀ x45 . x45intx27 x45 = x45)x28 = 2(∀ x45 . x45int∀ x46 . x46intx29 x45 x46 = If_i (SNoLe x45 0) x46 (x26 (x29 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx30 x45 = x29 (x27 x45) x28)(∀ x45 . x45intx31 x45 = x30 x45)(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x24 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx33 x45 = x32 x25 (x31 x45))(∀ x45 . x45intx34 x45 = add_SNo (x23 x45) (minus_SNo (x33 x45)))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (add_SNo (add_SNo (add_SNo (x38 x45 x46) x45) x45) x45) x45) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x15 x45 = x44 x45
Conjecture 82542..A20341 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40int∀ x41 . x41intx0 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x1 = 2(∀ x40 . x40intx2 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx4 x40 = x3 x1 (x2 x40))(∀ x40 . x40intx5 x40 = x4 x40)(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo (mul_SNo 2 (add_SNo x41 x41)) x41)(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 (add_SNo 2 2)(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture cda26..A203170 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ 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 . x14int∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ 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 . x48intx47 x48int)(∀ x48 . x48intx0 x48 = mul_SNo x48 x48)x1 = 2(∀ x48 . x48int∀ x49 . x49intx2 x48 x49 = add_SNo (add_SNo (add_SNo x48 (minus_SNo x49)) x48) x48)(∀ x48 . x48intx3 x48 = x48)(∀ x48 . x48intx4 x48 = x48)x5 = 1x6 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx7 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x2 (x7 (add_SNo x48 (minus_SNo 1)) x49 x50) (x8 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx8 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x3 (x7 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx9 x48 = x7 (x4 x48) x5 x6)(∀ x48 . x48intx10 x48 = x9 x48)(∀ x48 . x48int∀ x49 . x49intx11 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x11 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx12 x48 = x11 x1 (x10 x48))(∀ x48 . x48intx13 x48 = x12 x48)x14 = 1(∀ x48 . x48int∀ x49 . x49intx15 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx17 x48 x49 = x16 x14 (x15 x48 x49))(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = add_SNo (x17 x48 x49) x48)(∀ x48 . x48intx19 x48 = x48)x20 = 0(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx22 x48 = x21 (x19 x48) x20)(∀ x48 . x48intx23 x48 = x22 x48)(∀ x48 . x48intx24 x48 = mul_SNo x48 x48)x25 = 2(∀ x48 . x48int∀ x49 . x49intx26 x48 x49 = add_SNo (add_SNo (add_SNo x48 (minus_SNo x49)) x48) x48)(∀ x48 . x48intx27 x48 = x48)(∀ x48 . x48intx28 x48 = add_SNo x48 (minus_SNo 1))x29 = 1x30 = 1(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx31 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x26 (x31 (add_SNo x48 (minus_SNo 1)) x49 x50) (x32 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx32 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x27 (x31 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx33 x48 = x31 (x28 x48) x29 x30)(∀ x48 . x48intx34 x48 = x33 x48)(∀ x48 . x48int∀ x49 . x49intx35 x48 x49 = If_i (SNoLe x48 0) x49 (x24 (x35 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx36 x48 = x35 x25 (x34 x48))(∀ x48 . x48intx37 x48 = x36 x48)x38 = 1(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 x38 (x39 x48 x49))(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (x41 x48 x49) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 0(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x23 x48 = x47 x48
Conjecture 10488..A2023 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)x2 = add_SNo 1 2(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = mul_SNo 2 (x4 x17))(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo 2 (mul_SNo (add_SNo 1 2) (x15 x17)))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 70ef7..A200441 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . 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 . x23intx22 x23int)(∀ x23 . x23intx0 x23 = mul_SNo x23 x23)x1 = 2x2 = 2(∀ x23 . x23int∀ x24 . x24intx3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24)))x4 = x3 x1 x2(∀ x23 . x23int∀ x24 . x24intx5 x23 x24 = add_SNo (add_SNo (mul_SNo 2 (mul_SNo x4 x23)) (minus_SNo x24)) x23)(∀ x23 . x23intx6 x23 = x23)(∀ x23 . x23intx7 x23 = x23)x8 = 1x9 = 0(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x5 (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)))(∀ 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 (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))))) x23) (minus_SNo x24))(∀ x23 . x23intx15 x23 = x23)(∀ x23 . x23intx16 x23 = x23)x17 = 1x18 = 0(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx21 x23 = x19 (x16 x23) x17 x18)(∀ x23 . x23intx22 x23 = x21 x23)∀ x23 . x23intSNoLe 0 x23x13 x23 = x22 x23
Conjecture a2696..A20000 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40int∀ x41 . x41intx0 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x1 = 2(∀ x40 . x40intx2 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx4 x40 = x3 x1 (x2 x40))(∀ x40 . x40intx5 x40 = add_SNo (x4 x40) (minus_SNo x40))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)) x40) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo (mul_SNo 2 (add_SNo x41 x41)) x41)(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 (add_SNo 2 2)(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) x40)(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture e12ca..A19999 : ∀ 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 . 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 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = mul_SNo 2 (mul_SNo (add_SNo 2 x13) x12))(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = add_SNo 2 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 = mul_SNo 2 (x4 x12))(∀ x12 . x12int∀ x13 . x13intx6 x12 x13 = mul_SNo (mul_SNo x12 2) x13)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = 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))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = mul_SNo (mul_SNo (add_SNo 1 x12) (add_SNo 2 x12)) (x10 x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture b578d..A199761 : ∀ 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 (add_SNo (x4 x20) (minus_SNo 2)) (minus_SNo x20))(∀ x20 . x20intx6 x20 = x20)x7 = 2(∀ 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 = 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 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 3d7d5..A199760 : ∀ 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 (add_SNo (x4 x20) (minus_SNo 1)) (minus_SNo 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 (mul_SNo x20 x21) (minus_SNo 1))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = 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 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture e4a3f..A199755 : ∀ 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 = x20)x7 = add_SNo 1 (add_SNo 2 2)(∀ 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 1 (x9 x20))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = add_SNo 1 (add_SNo 2 2)x15 = 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 1 (x18 x20))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 2dfb4..A199753 : ∀ 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 = x20)x7 = 2(∀ 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 1 (mul_SNo 2 (x9 x20)))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 2x15 = 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 1 (mul_SNo 2 (x18 x20)))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20