Search for blocks/addresses/...

Proofgold Asset

asset id
0d91ba94c217e9d676e7f7f79914c5a9f9f1a3ede59b4b551ae9c79bbb9da7ed
asset hash
4e40c1a9d1ecda2e63ccdb2635d15357ceb4780c99edd6df8faa65ac82322b30
bday / block
25657
tx
9fd53..
preasset
doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Param mul_SNomul_SNo : ιιι
Conjecture 6b84f..A2446 : ∀ 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 = 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 = add_SNo (x4 x17) (minus_SNo 2))(∀ 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 = add_SNo (mul_SNo 2 (x15 x17)) (minus_SNo 2))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 64401..A24444 : ∀ 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 1 (add_SNo (x4 x40) (minus_SNo x40)))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 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 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo (add_SNo x41 x41) x41)) x41))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = mul_SNo 2 (add_SNo 2 2)(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (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 e876e..A24439 : ∀ 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 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x40 x40))))(∀ x40 . x40int∀ x41 . x41intx1 x40 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 (add_SNo (x4 x40 x41) (minus_SNo x40)) (x9 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 (add_SNo x40 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 x40 x40))) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo (add_SNo x41 x41) x41)) x41))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = mul_SNo 2 (add_SNo 2 2)(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (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 0270a..A24434 : ∀ 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 1 (add_SNo (x4 x40) (minus_SNo x40)))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo (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 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x41 x41) x41)))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (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 6a36f..A24346 : ∀ 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 . x6intx5 x6int)∀ 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 . 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 . 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 1 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45int∀ x46 . x46intx1 x45 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 . x45intx5 x45 = add_SNo (add_SNo x45 x45) x45)x6 = 2(∀ x45 . x45intx7 x45 = x45)(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx9 x45 = x8 x6 (x7 x45))(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (x4 x45 x46) (x9 x45))(∀ x45 . x45int∀ x46 . x46intx11 x45 x46 = x46)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 . x45int∀ x46 . x46intx14 x45 x46 = x13 (x11 x45 x46) x12)(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = mul_SNo (add_SNo 2 x46) x45)x16 = 2(∀ x45 . x45intx17 x45 = x45)(∀ 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 (x17 x45))(∀ x45 . x45int∀ x46 . x46intx20 x45 x46 = add_SNo (add_SNo (x14 x45 x46) (minus_SNo x45)) (x19 x45))(∀ x45 . x45intx21 x45 = x45)x22 = 1(∀ x45 . x45int∀ x46 . x46intx23 x45 x46 = If_i (SNoLe x45 0) x46 (x20 (x23 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx24 x45 = x23 (x21 x45) x22)(∀ x45 . x45intx25 x45 = x24 x45)(∀ x45 . x45int∀ x46 . x46intx26 x45 x46 = add_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))) x45) x46)(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x46 x46) x46)))(∀ x45 . x45intx28 x45 = x45)x29 = 1x30 = add_SNo 1 (add_SNo 2 (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 = 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 (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 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 x45x25 x45 = x44 x45
Conjecture 86d70..A24170 : ∀ 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 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40intx0 x40 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)))(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = x41)x2 = 1(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx4 x40 x41 = x3 (x1 x40 x41) x2)(∀ x40 . x40int∀ x41 . x41intx5 x40 x41 = add_SNo (x4 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40intx10 x40 = add_SNo (add_SNo x40 x40) x40)x11 = 2(∀ x40 . x40intx12 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40intx14 x40 = x13 x11 (x12 x40))(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (x9 x40 x41) (x14 x40))(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)) x41)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x41 x41) x41)))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (mul_SNo 2 (add_SNo 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 ca41e..A24167 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)(∀ x27 . x27int∀ x28 . x28intx0 x27 x28 = add_SNo 0 (minus_SNo (mul_SNo x27 x28)))(∀ x27 . x27int∀ x28 . x28intx1 x27 x28 = x28)x2 = 1(∀ x27 . x27int∀ x28 . x28intx3 x27 x28 = If_i (SNoLe x27 0) x28 (x0 (x3 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx4 x27 x28 = x3 (x1 x27 x28) x2)(∀ x27 . x27int∀ x28 . x28intx5 x27 x28 = add_SNo (add_SNo (mul_SNo x27 x28) (x4 x27 x28)) x27)(∀ x27 . x27intx6 x27 = x27)x7 = 1(∀ x27 . x27int∀ x28 . x28intx8 x27 x28 = If_i (SNoLe x27 0) x28 (x5 (x8 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx9 x27 = x8 (x6 x27) x7)(∀ x27 . x27intx10 x27 = x9 x27)(∀ x27 . x27int∀ x28 . x28intx11 x27 x28 = mul_SNo x27 x28)(∀ x27 . x27int∀ x28 . x28intx12 x27 x28 = x28)x13 = 1(∀ x27 . x27int∀ x28 . x28intx14 x27 x28 = If_i (SNoLe x27 0) x28 (x11 (x14 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx15 x27 x28 = x14 (x12 x27 x28) x13)(∀ x27 . x27int∀ x28 . x28intx16 x27 x28 = add_SNo (x15 x27 x28) (minus_SNo (mul_SNo (add_SNo 1 x28) x27)))(∀ x27 . x27intx17 x27 = x27)x18 = 1(∀ x27 . x27int∀ x28 . x28intx19 x27 x28 = If_i (SNoLe x27 0) x28 (x16 (x19 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx20 x27 = x19 (x17 x27) x18)(∀ x27 . x27intx21 x27 = add_SNo 0 (minus_SNo x27))(∀ x27 . x27intx22 x27 = x27)x23 = 1(∀ x27 . x27int∀ x28 . x28intx24 x27 x28 = If_i (SNoLe x27 0) x28 (x21 (x24 (add_SNo x27 (minus_SNo 1)) x28)))(∀ x27 . x27intx25 x27 = x24 (x22 x27) x23)(∀ x27 . x27intx26 x27 = mul_SNo (x20 x27) (x25 x27))∀ x27 . x27intSNoLe 0 x27x10 x27 = x26 x27
Conjecture 67d0f..A24148 : ∀ 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 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30int∀ x31 . x31intx0 x30 x31 = mul_SNo (add_SNo 2 x31) x30)x1 = 2(∀ x30 . x30intx2 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx4 x30 = x3 x1 (x2 x30))(∀ x30 . x30intx5 x30 = x4 x30)(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = mul_SNo x30 x30)x11 = 2(∀ x30 . x30intx12 x30 = mul_SNo x30 x30)(∀ x30 . x30int∀ x31 . x31intx13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx14 x30 = x13 x11 (x12 x30))(∀ x30 . x30intx15 x30 = add_SNo (x9 x30) (minus_SNo (x14 x30)))(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx17 x30 x31 = x31)(∀ x30 . x30intx18 x30 = x30)x19 = 1x20 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx23 x30 = x21 (x18 x30) x19 x20)(∀ x30 . x30intx24 x30 = mul_SNo x30 x30)x25 = 2(∀ x30 . x30intx26 x30 = mul_SNo x30 x30)(∀ x30 . x30int∀ x31 . x31intx27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx28 x30 = x27 x25 (x26 x30))(∀ x30 . x30intx29 x30 = add_SNo (x23 x30) (minus_SNo (x28 x30)))∀ x30 . x30intSNoLe 0 x30x15 x30 = x29 x30
Conjecture a26c3..A24141 : ∀ 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 = x4 x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = add_SNo (x9 x20) (minus_SNo x20))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = add_SNo (x18 x20) (minus_SNo x20))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 068bd..A24139 : ∀ 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 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30int∀ x31 . x31intx0 x30 x31 = mul_SNo (add_SNo 2 x31) x30)x1 = 2(∀ x30 . x30intx2 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx4 x30 = x3 x1 (x2 x30))(∀ x30 . x30intx5 x30 = add_SNo (x4 x30) (minus_SNo x30))(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = mul_SNo x30 x30)x11 = 2(∀ x30 . x30intx12 x30 = mul_SNo (mul_SNo x30 x30) x30)(∀ x30 . x30int∀ x31 . x31intx13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx14 x30 = x13 x11 (x12 x30))(∀ x30 . x30intx15 x30 = add_SNo (x9 x30) (minus_SNo (x14 x30)))(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx17 x30 x31 = x31)(∀ x30 . x30intx18 x30 = x30)x19 = 1x20 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx23 x30 = x21 (x18 x30) x19 x20)(∀ x30 . x30intx24 x30 = mul_SNo x30 x30)x25 = 2(∀ x30 . x30intx26 x30 = mul_SNo (mul_SNo x30 x30) x30)(∀ x30 . x30int∀ x31 . x31intx27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx28 x30 = x27 x25 (x26 x30))(∀ x30 . x30intx29 x30 = add_SNo (x23 x30) (minus_SNo (x28 x30)))∀ x30 . x30intSNoLe 0 x30x15 x30 = x29 x30
Conjecture b3ba9..A24134 : ∀ 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 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ 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 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33int∀ x34 . x34intx0 x33 x34 = mul_SNo (add_SNo 2 x34) x33)x1 = 2(∀ x33 . x33intx2 x33 = x33)(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx4 x33 = x3 x1 (x2 x33))(∀ x33 . x33intx5 x33 = add_SNo (x4 x33) (minus_SNo x33))(∀ x33 . x33intx6 x33 = x33)x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33int∀ x34 . x34intx10 x33 x34 = mul_SNo (mul_SNo x33 x33) x34)(∀ x33 . x33intx11 x33 = x33)x12 = 2(∀ x33 . x33intx13 x33 = x33)(∀ x33 . x33intx14 x33 = x33)(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx15 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x10 (x15 (add_SNo x33 (minus_SNo 1)) x34 x35) (x16 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx16 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x11 (x15 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx17 x33 = x15 x12 (x13 x33) (x14 x33))(∀ x33 . x33intx18 x33 = add_SNo (x9 x33) (minus_SNo (x17 x33)))(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = x34)(∀ x33 . x33intx21 x33 = x33)x22 = 1x23 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x19 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x20 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx26 x33 = x24 (x21 x33) x22 x23)(∀ x33 . x33intx27 x33 = mul_SNo (mul_SNo x33 x33) x33)x28 = 1(∀ x33 . x33intx29 x33 = mul_SNo x33 x33)(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx31 x33 = x30 x28 (x29 x33))(∀ x33 . x33intx32 x33 = add_SNo (x26 x33) (minus_SNo (mul_SNo (x31 x33) x33)))∀ x33 . x33intSNoLe 0 x33x18 x33 = x32 x33
Conjecture ffe94..A24133 : ∀ 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 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30int∀ x31 . x31intx0 x30 x31 = mul_SNo (add_SNo 2 x31) x30)x1 = 2(∀ x30 . x30intx2 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx4 x30 = x3 x1 (x2 x30))(∀ x30 . x30intx5 x30 = add_SNo (x4 x30) (minus_SNo x30))(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = mul_SNo x30 x30)x11 = 2(∀ x30 . x30intx12 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx14 x30 = x13 x11 (x12 x30))(∀ x30 . x30intx15 x30 = add_SNo (x9 x30) (minus_SNo (mul_SNo (mul_SNo (x14 x30) x30) x30)))(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx17 x30 x31 = x31)(∀ x30 . x30intx18 x30 = x30)x19 = 1x20 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx23 x30 = x21 (x18 x30) x19 x20)(∀ x30 . x30intx24 x30 = mul_SNo (mul_SNo x30 x30) x30)x25 = 1(∀ x30 . x30intx26 x30 = mul_SNo x30 x30)(∀ x30 . x30int∀ x31 . x31intx27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx28 x30 = x27 x25 (x26 x30))(∀ x30 . x30intx29 x30 = add_SNo (x23 x30) (minus_SNo (x28 x30)))∀ x30 . x30intSNoLe 0 x30x15 x30 = x29 x30
Conjecture ae856..A24118 : ∀ 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 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x20 x20)) 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 . x20intx4 x20 = x3 (x1 x20) x2)(∀ x20 . x20intx5 x20 = mul_SNo x20 x20)x6 = 2(∀ x20 . x20intx7 x20 = x20)(∀ 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 (x7 x20))(∀ x20 . x20intx10 x20 = add_SNo (x4 x20) (minus_SNo (x9 x20)))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = 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 (mul_SNo (mul_SNo (mul_SNo x20 x20) x20) x20)))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 592a1..A24116 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x15 x15)) x15))(∀ x15 . x15intx1 x15 = x15)x2 = 1(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = add_SNo (x4 x15) (minus_SNo (mul_SNo x15 x15)))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 1x10 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) x9 x10)(∀ x15 . x15intx14 x15 = add_SNo (x13 x15) (minus_SNo (mul_SNo x15 x15)))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 26eb2..A241031 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 . x8int∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38intx0 x38 = add_SNo x38 x38)(∀ x38 . x38int∀ x39 . x39intx1 x38 x39 = x39)(∀ x38 . x38intx2 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx3 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x3 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx4 x38 x39 = x3 (x1 x38 x39) (x2 x38))(∀ x38 . x38int∀ x39 . x39intx5 x38 x39 = add_SNo 1 (x4 x38 x39))(∀ x38 . x38int∀ x39 . x39intx6 x38 x39 = x39)x7 = 2x8 = 1(∀ x38 . x38intx9 x38 = x38)(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx10 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x5 (x10 (add_SNo x38 (minus_SNo 1)) x39 x40) (x11 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx11 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x6 (x10 (add_SNo x38 (minus_SNo 1)) x39 x40) (x11 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx12 x38 = x10 x7 x8 (x9 x38))(∀ x38 . x38intx13 x38 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x38 x38) x38)) x38)(∀ x38 . x38intx14 x38 = x38)x15 = 1(∀ x38 . x38int∀ x39 . x39intx16 x38 x39 = If_i (SNoLe x38 0) x39 (x13 (x16 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx17 x38 = x16 (x14 x38) x15)(∀ x38 . x38intx18 x38 = mul_SNo (x12 x38) (add_SNo 1 (x17 x38)))(∀ x38 . x38intx19 x38 = add_SNo (mul_SNo x38 x38) x38)x20 = 1(∀ x38 . x38intx21 x38 = add_SNo x38 x38)(∀ x38 . x38intx22 x38 = x38)x23 = 1(∀ x38 . x38int∀ x39 . x39intx24 x38 x39 = If_i (SNoLe x38 0) x39 (x21 (x24 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx25 x38 = x24 (x22 x38) x23)(∀ x38 . x38intx26 x38 = x25 x38)(∀ x38 . x38int∀ x39 . x39intx27 x38 x39 = If_i (SNoLe x38 0) x39 (x19 (x27 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx28 x38 = x27 x20 (x26 x38))(∀ x38 . x38int∀ x39 . x39intx29 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = x39)(∀ x38 . x38intx31 x38 = x38)x32 = 1x33 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx34 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x29 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx35 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x30 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx36 x38 = x34 (x31 x38) x32 x33)(∀ x38 . x38intx37 x38 = mul_SNo (add_SNo 1 (x28 x38)) (add_SNo 1 (x36 x38)))∀ x38 . x38intSNoLe 0 x38x18 x38 = x37 x38
Conjecture a1b36..A24102 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15intx0 x15 = add_SNo (add_SNo x15 x15) x15)(∀ x15 . x15intx1 x15 = add_SNo x15 x15)x2 = 1(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = add_SNo (x4 x15) (minus_SNo x15))(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = mul_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = x16)(∀ x15 . x15intx8 x15 = x15)x9 = 1x10 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) x9 x10)(∀ x15 . x15intx14 x15 = add_SNo (x13 x15) (minus_SNo x15))∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 315e2..A241029 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 . x6int∀ 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 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30intx0 x30 = add_SNo x30 x30)(∀ x30 . x30intx1 x30 = x30)x2 = 1(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx4 x30 = x3 (x1 x30) x2)(∀ x30 . x30int∀ x31 . x31intx5 x30 x31 = mul_SNo (add_SNo 2 x31) x30)x6 = 2(∀ x30 . x30intx7 x30 = x30)(∀ 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 (x7 x30))(∀ x30 . x30intx10 x30 = add_SNo (x9 x30) (minus_SNo x30))(∀ x30 . x30intx11 x30 = x30)x12 = 1(∀ x30 . x30int∀ x31 . x31intx13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx14 x30 = x13 (x11 x30) x12)(∀ x30 . x30intx15 x30 = mul_SNo (add_SNo 1 (x4 x30)) (add_SNo 1 (x14 x30)))(∀ x30 . x30intx16 x30 = add_SNo x30 x30)(∀ x30 . x30intx17 x30 = x30)x18 = 1(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x16 (x19 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx20 x30 = x19 (x17 x30) x18)(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx28 x30 = x26 (x23 x30) x24 x25)(∀ x30 . x30intx29 x30 = mul_SNo (add_SNo 1 (x20 x30)) (add_SNo 1 (x28 x30)))∀ x30 . x30intSNoLe 0 x30x15 x30 = x29 x30
Conjecture 6e435..A24091 : ∀ 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 (add_SNo x17 x17) x17)x2 = 1(∀ 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 = add_SNo (x4 x17) (minus_SNo (mul_SNo (mul_SNo x17 x17) x17)))(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = add_SNo (x15 x17) (minus_SNo (mul_SNo (mul_SNo x17 x17) x17)))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 1ceae..A24088 : ∀ 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 (add_SNo x17 x17) x17)x2 = 1(∀ 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 = add_SNo (x4 x17) (minus_SNo 1))(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = add_SNo (x15 x17) (minus_SNo 1))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture e986f..A24086 : ∀ 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 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25)) x25)(∀ x25 . x25intx1 x25 = x25)x2 = 1(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx4 x25 = x3 (x1 x25) x2)(∀ x25 . x25intx5 x25 = mul_SNo (mul_SNo x25 x25) x25)x6 = 2(∀ x25 . x25intx7 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 x6 (x7 x25))(∀ x25 . x25intx10 x25 = add_SNo (x4 x25) (minus_SNo (mul_SNo (mul_SNo (x9 x25) x25) x25)))(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1x15 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ 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 . x25intx19 x25 = mul_SNo (mul_SNo x25 x25) x25)x20 = 1(∀ x25 . x25intx21 x25 = mul_SNo (mul_SNo x25 x25) x25)(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 x20 (x21 x25))(∀ x25 . x25intx24 x25 = add_SNo (x18 x25) (minus_SNo (mul_SNo (mul_SNo (x23 x25) x25) x25)))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25