Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr53g../b42b4..
PUL3p../da182..
vout
Pr53g../f6242.. 0.94 bars
PUMwx../5bee5.. 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 19030..A334991 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . 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 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)(∀ x35 . x35intx0 x35 = add_SNo (add_SNo x35 x35) x35)x1 = 2(∀ x35 . x35intx2 x35 = x35)(∀ x35 . x35int∀ x36 . x36intx3 x35 x36 = If_i (SNoLe x35 0) x36 (x0 (x3 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35intx4 x35 = x3 x1 (x2 x35))(∀ x35 . x35intx5 x35 = mul_SNo 2 (x4 x35))(∀ x35 . x35intx6 x35 = x35)x7 = add_SNo 1 2(∀ x35 . x35int∀ x36 . x36intx8 x35 x36 = If_i (SNoLe x35 0) x36 (x5 (x8 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35intx9 x35 = x8 (x6 x35) x7)(∀ x35 . x35intx10 x35 = add_SNo x35 x35)(∀ x35 . x35intx11 x35 = add_SNo x35 x35)x12 = 1(∀ x35 . x35int∀ x36 . x36intx13 x35 x36 = If_i (SNoLe x35 0) x36 (x10 (x13 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35intx14 x35 = x13 (x11 x35) x12)(∀ x35 . x35intx15 x35 = add_SNo (x9 x35) (x14 x35))(∀ x35 . x35intx16 x35 = add_SNo x35 x35)(∀ x35 . x35intx17 x35 = x35)x18 = 1(∀ x35 . x35int∀ x36 . x36intx19 x35 x36 = If_i (SNoLe x35 0) x36 (x16 (x19 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35intx20 x35 = x19 (x17 x35) x18)(∀ x35 . x35int∀ x36 . x36intx21 x35 x36 = mul_SNo x35 x36)(∀ x35 . x35int∀ x36 . x36intx22 x35 x36 = x36)(∀ x35 . x35intx23 x35 = x35)x24 = add_SNo 1 2x25 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx26 x35 x36 x37 = If_i (SNoLe x35 0) x36 (x21 (x26 (add_SNo x35 (minus_SNo 1)) x36 x37) (x27 (add_SNo x35 (minus_SNo 1)) x36 x37)))(∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx27 x35 x36 x37 = If_i (SNoLe x35 0) x37 (x22 (x26 (add_SNo x35 (minus_SNo 1)) x36 x37) (x27 (add_SNo x35 (minus_SNo 1)) x36 x37)))(∀ x35 . x35intx28 x35 = x26 (x23 x35) x24 x25)(∀ x35 . x35intx29 x35 = add_SNo x35 x35)(∀ x35 . x35intx30 x35 = x35)x31 = 1(∀ x35 . x35int∀ x36 . x36intx32 x35 x36 = If_i (SNoLe x35 0) x36 (x29 (x32 (add_SNo x35 (minus_SNo 1)) x36)))(∀ x35 . x35intx33 x35 = x32 (x30 x35) x31)(∀ x35 . x35intx34 x35 = mul_SNo (add_SNo (x20 x35) (x28 x35)) (x33 x35))∀ x35 . x35intSNoLe 0 x35x15 x35 = x34 x35
Conjecture 91c46..A333385 : ∀ 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 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 . x9int∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 . x28int∀ x29 : ι → ι → ι → ι . (∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx29 x30 x31 x32int)∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33intx0 x33 = add_SNo (add_SNo x33 x33) x33)(∀ x33 . x33intx1 x33 = x33)x2 = 1(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx4 x33 = x3 (x1 x33) x2)(∀ x33 . x33intx5 x33 = mul_SNo x33 x33)x6 = 2x7 = 2(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34)))x9 = x8 x6 x7(∀ x33 . x33intx10 x33 = add_SNo (mul_SNo x9 x33) x33)(∀ x33 . x33intx11 x33 = x33)x12 = 2(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = If_i (SNoLe x33 0) x34 (x10 (x13 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx14 x33 = x13 (x11 x33) x12)(∀ x33 . x33intx15 x33 = add_SNo (x4 x33) (x14 x33))(∀ x33 . x33int∀ x34 . x34intx16 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx17 x33 x34 = x34)(∀ x33 . x33intx18 x33 = x33)x19 = 1x20 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx21 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x16 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx22 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x17 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx23 x33 = x21 (x18 x33) x19 x20)(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = x33)x27 = 1x28 = add_SNo 1 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = add_SNo (mul_SNo 2 (x23 x33)) (x31 x33))∀ x33 . x33intSNoLe 0 x33x15 x33 = x32 x33
Conjecture 612e0..A332186 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 . x26int∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι → ι → ι . (∀ x29 . x29int∀ x30 . x30int∀ x31 . x31intx28 x29 x30 x31int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)(∀ x31 . x31intx0 x31 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x31 x31)) x31)) (minus_SNo 1))(∀ x31 . x31intx1 x31 = add_SNo 1 (add_SNo x31 x31))x2 = 1(∀ x31 . x31int∀ x32 . x32intx3 x31 x32 = If_i (SNoLe x31 0) x32 (x0 (x3 (add_SNo x31 (minus_SNo 1)) x32)))(∀ x31 . x31intx4 x31 = x3 (x1 x31) x2)(∀ x31 . x31int∀ x32 . x32intx5 x31 x32 = mul_SNo x31 x32)(∀ x31 . x31int∀ x32 . x32intx6 x31 x32 = x32)(∀ x31 . x31intx7 x31 = x31)x8 = 2x9 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx10 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x5 (x10 (add_SNo x31 (minus_SNo 1)) x32 x33) (x11 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx11 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x6 (x10 (add_SNo x31 (minus_SNo 1)) x32 x33) (x11 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx12 x31 = x10 (x7 x31) x8 x9)(∀ x31 . x31intx13 x31 = add_SNo (add_SNo (x4 x31) (minus_SNo 1)) (minus_SNo (x12 x31)))(∀ x31 . x31int∀ x32 . x32intx14 x31 x32 = mul_SNo x31 x32)(∀ x31 . x31int∀ x32 . x32intx15 x31 x32 = x32)(∀ x31 . x31intx16 x31 = x31)x17 = 2x18 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx19 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x14 (x19 (add_SNo x31 (minus_SNo 1)) x32 x33) (x20 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx20 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x15 (x19 (add_SNo x31 (minus_SNo 1)) x32 x33) (x20 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx21 x31 = x19 (x16 x31) x17 x18)(∀ x31 . x31int∀ x32 . x32intx22 x31 x32 = add_SNo 1 (mul_SNo x31 x32))(∀ x31 . x31int∀ x32 . x32intx23 x31 x32 = x32)(∀ x31 . x31intx24 x31 = x31)x25 = 1x26 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx27 x31 x32 x33 = If_i (SNoLe x31 0) x32 (x22 (x27 (add_SNo x31 (minus_SNo 1)) x32 x33) (x28 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx28 x31 x32 x33 = If_i (SNoLe x31 0) x33 (x23 (x27 (add_SNo x31 (minus_SNo 1)) x32 x33) (x28 (add_SNo x31 (minus_SNo 1)) x32 x33)))(∀ x31 . x31intx29 x31 = x27 (x24 x31) x25 x26)(∀ x31 . x31intx30 x31 = add_SNo (mul_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (x21 x31))) (minus_SNo 1)) (x29 x31)) (minus_SNo 1))∀ x31 . x31intSNoLe 0 x31x13 x31 = x30 x31
Conjecture e38db..A332185 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 . x14int∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 . x31int∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι → ι → ι . (∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx33 x34 x35 x36int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 . x39int∀ x40 : ι → ι → ι → ι . (∀ x41 . x41int∀ x42 . x42int∀ x43 . x43intx40 x41 x42 x43int)∀ x41 : ι → ι → ι → ι . (∀ x42 . x42int∀ x43 . x43int∀ x44 . x44intx41 x42 x43 x44int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)(∀ x44 . x44intx0 x44 = add_SNo 2 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x44 x44)) x44)))(∀ x44 . x44intx1 x44 = add_SNo x44 x44)x2 = 2(∀ x44 . x44int∀ x45 . x45intx3 x44 x45 = If_i (SNoLe x44 0) x45 (x0 (x3 (add_SNo x44 (minus_SNo 1)) x45)))(∀ x44 . x44intx4 x44 = x3 (x1 x44) x2)(∀ x44 . x44intx5 x44 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x44 x44)) x44))(∀ x44 . x44intx6 x44 = x44)x7 = 1(∀ x44 . x44int∀ x45 . x45intx8 x44 x45 = If_i (SNoLe x44 0) x45 (x5 (x8 (add_SNo x44 (minus_SNo 1)) x45)))(∀ x44 . x44intx9 x44 = x8 (x6 x44) x7)(∀ x44 . x44int∀ x45 . x45intx10 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx11 x44 x45 = x45)(∀ x44 . x44intx12 x44 = x44)x13 = 1x14 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx15 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x10 (x15 (add_SNo x44 (minus_SNo 1)) x45 x46) (x16 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx16 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x11 (x15 (add_SNo x44 (minus_SNo 1)) x45 x46) (x16 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx17 x44 = x15 (x12 x44) x13 x14)(∀ x44 . x44intx18 x44 = add_SNo (mul_SNo (mul_SNo (add_SNo (x4 x44) (minus_SNo (x9 x44))) 2) 2) (x17 x44))(∀ x44 . x44int∀ x45 . x45intx19 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx20 x44 x45 = x45)(∀ x44 . x44intx21 x44 = x44)x22 = 2x23 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx24 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x19 (x24 (add_SNo x44 (minus_SNo 1)) x45 x46) (x25 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx25 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x20 (x24 (add_SNo x44 (minus_SNo 1)) x45 x46) (x25 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx26 x44 = x24 (x21 x44) x22 x23)(∀ x44 . x44int∀ x45 . x45intx27 x44 x45 = add_SNo 1 (mul_SNo x44 x45))(∀ x44 . x44int∀ x45 . x45intx28 x44 x45 = x45)(∀ x44 . x44intx29 x44 = x44)x30 = 1x31 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx32 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x27 (x32 (add_SNo x44 (minus_SNo 1)) x45 x46) (x33 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx33 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x28 (x32 (add_SNo x44 (minus_SNo 1)) x45 x46) (x33 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx34 x44 = x32 (x29 x44) x30 x31)(∀ x44 . x44int∀ x45 . x45intx35 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx36 x44 x45 = x45)(∀ x44 . x44intx37 x44 = x44)x38 = 1x39 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx40 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x35 (x40 (add_SNo x44 (minus_SNo 1)) x45 x46) (x41 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx41 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x36 (x40 (add_SNo x44 (minus_SNo 1)) x45 x46) (x41 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx42 x44 = x40 (x37 x44) x38 x39)(∀ x44 . x44intx43 x44 = add_SNo (add_SNo (mul_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (x26 x44))) (minus_SNo 1)) (x34 x44)) (minus_SNo 1)) (minus_SNo (x42 x44)))∀ x44 . x44intSNoLe 0 x44x18 x44 = x43 x44
Conjecture 50486..A332136 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . 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 . x28intx0 x28 = add_SNo 1 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x28 x28)) x28)))(∀ x28 . x28intx1 x28 = add_SNo x28 x28)x2 = 1(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx4 x28 = x3 (x1 x28) x2)(∀ x28 . x28intx5 x28 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x28 x28)) x28))(∀ x28 . x28intx6 x28 = x28)x7 = 1(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = If_i (SNoLe x28 0) x29 (x5 (x8 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx9 x28 = x8 (x6 x28) x7)(∀ x28 . x28intx10 x28 = mul_SNo (add_SNo (x4 x28) (x9 x28)) (add_SNo 1 2))(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = x29)(∀ x28 . x28intx13 x28 = x28)x14 = add_SNo 1 2x15 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx18 x28 = x16 (x13 x28) x14 x15)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo 1 (mul_SNo x28 x29))(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = x29)(∀ x28 . x28intx21 x28 = x28)x22 = 1x23 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (add_SNo 1 (add_SNo 2 (x18 x28))) (x26 x28))∀ x28 . x28intSNoLe 0 x28x10 x28 = x27 x28
Conjecture 657c1..A332115 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 . x31int∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι → ι → ι . (∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx33 x34 x35 x36int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)(∀ x36 . x36intx0 x36 = add_SNo 1 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x36 x36)) x36)))(∀ x36 . x36intx1 x36 = add_SNo x36 x36)x2 = 1(∀ x36 . x36int∀ x37 . x37intx3 x36 x37 = If_i (SNoLe x36 0) x37 (x0 (x3 (add_SNo x36 (minus_SNo 1)) x37)))(∀ x36 . x36intx4 x36 = x3 (x1 x36) x2)(∀ x36 . x36intx5 x36 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x36 x36)) x36))(∀ x36 . x36intx6 x36 = x36)x7 = 2(∀ x36 . x36int∀ x37 . x37intx8 x36 x37 = If_i (SNoLe x36 0) x37 (x5 (x8 (add_SNo x36 (minus_SNo 1)) x37)))(∀ x36 . x36intx9 x36 = x8 (x6 x36) x7)(∀ x36 . x36intx10 x36 = add_SNo (x4 x36) (mul_SNo 2 (x9 x36)))(∀ x36 . x36int∀ x37 . x37intx11 x36 x37 = add_SNo 1 (mul_SNo x36 x37))(∀ x36 . x36int∀ x37 . x37intx12 x36 x37 = x37)(∀ x36 . x36intx13 x36 = x36)x14 = 1x15 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx16 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x11 (x16 (add_SNo x36 (minus_SNo 1)) x37 x38) (x17 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx17 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x12 (x16 (add_SNo x36 (minus_SNo 1)) x37 x38) (x17 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36intx18 x36 = x16 (x13 x36) x14 x15)(∀ x36 . x36int∀ x37 . x37intx19 x36 x37 = mul_SNo x36 x37)(∀ x36 . x36int∀ x37 . x37intx20 x36 x37 = x37)(∀ x36 . x36intx21 x36 = x36)x22 = 1x23 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx24 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x19 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38) (x25 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx25 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x20 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38) (x25 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36intx26 x36 = x24 (x21 x36) x22 x23)(∀ x36 . x36int∀ x37 . x37intx27 x36 x37 = mul_SNo x36 x37)(∀ x36 . x36int∀ x37 . x37intx28 x36 x37 = x37)(∀ x36 . x36intx29 x36 = x36)x30 = 2x31 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx32 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x27 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38) (x33 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx33 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x28 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38) (x33 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36intx34 x36 = x32 (x29 x36) x30 x31)(∀ x36 . x36intx35 x36 = add_SNo (add_SNo (mul_SNo (add_SNo 1 (x18 x36)) (add_SNo 1 (x26 x36))) (minus_SNo 1)) (x34 x36))∀ x36 . x36intSNoLe 0 x36x10 x36 = x35 x36
Conjecture 4e5ad..A330135 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = mul_SNo x25 x25)x1 = 2x2 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = add_SNo 1 (mul_SNo x4 x25))(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = add_SNo 1 (mul_SNo x25 x26))(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = mul_SNo x25 x25)x16 = 2x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x25 . x25int∀ x26 . x26intx18 x25 x26 = If_i (SNoLe x25 0) x26 (x15 (x18 (add_SNo x25 (minus_SNo 1)) x26)))x19 = x18 x16 x17x20 = x19(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x13 x25) x14 x20)(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture b298c..A327926 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = add_SNo 1 (mul_SNo (add_SNo 2 x28) x28))x1 = 2x2 = 2(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28intx5 x28 = add_SNo (mul_SNo x4 x28) (minus_SNo x28))(∀ x28 . x28intx6 x28 = x28)x7 = 1(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = If_i (SNoLe x28 0) x29 (x5 (x8 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx9 x28 = x8 (x6 x28) x7)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = x29)(∀ x28 . x28intx13 x28 = x28)x14 = 1x15 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx18 x28 = x16 (x13 x28) x14 x15)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = x29)(∀ x28 . x28intx21 x28 = x28)x22 = 1x23 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (x18 x28) (x26 x28))∀ x28 . x28intSNoLe 0 x28x10 x28 = x27 x28
Conjecture 2b51b..A3266 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ 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 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = x29)x3 = 0(∀ x28 . x28intx4 x28 = x28)(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx5 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x0 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30) (x6 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx6 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x1 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29intx7 x28 x29 = x5 (x2 x28 x29) x3 (x4 x28))(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = x7 x28 x29)(∀ x28 . x28intx9 x28 = x28)x10 = 1(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x8 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x9 x28) x10)(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx16 x28 x29 = add_SNo x29 (minus_SNo 1))x17 = 2x18 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29intx21 x28 x29 = x19 (x16 x28 x29) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 (x21 x28 x29))(∀ x28 . x28intx23 x28 = add_SNo x28 (minus_SNo 2))x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = x26 x28)∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture 3799a..A3261 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12intx0 x12 = add_SNo 1 (add_SNo x12 x12))(∀ x12 . x12intx1 x12 = add_SNo 1 x12)(∀ x12 . x12intx2 x12 = x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = x4 x12)(∀ x12 . x12intx6 x12 = add_SNo x12 x12)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = add_SNo 1 x12)(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo (mul_SNo 2 (x10 x12)) (minus_SNo 1))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 2597a..A325958 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo x12 x13)(∀ x12 . x12intx1 x12 = mul_SNo 2 (add_SNo 2 (add_SNo x12 x12)))x2 = 2(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx4 x12 = x3 (x1 x12) x2)(∀ x12 . x12intx5 x12 = mul_SNo 2 (x4 x12))(∀ x12 . x12intx6 x12 = add_SNo (mul_SNo x12 x12) x12)x7 = 1(∀ x12 . x12intx8 x12 = mul_SNo 2 (add_SNo 2 (add_SNo x12 x12)))(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 x7 (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo 2 (add_SNo 2 (x10 x12)))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 67455..A324269 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι → ι . (∀ x19 . x19int∀ x20 . x20int∀ x21 . x21intx18 x19 x20 x21int)∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25int∀ x26 . x26intx0 x25 x26 = add_SNo (mul_SNo x25 x26) x25)x1 = add_SNo 2 2(∀ x25 . x25intx2 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx4 x25 = x3 x1 (x2 x25))(∀ x25 . x25intx5 x25 = add_SNo (x4 x25) x25)(∀ x25 . x25intx6 x25 = x25)x7 = add_SNo 1 2(∀ 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 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = mul_SNo (add_SNo (add_SNo x25 x25) x25) x25)x12 = 1(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = x26)(∀ x25 . x25intx15 x25 = x25)x16 = 1x17 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx20 x25 = x18 (x15 x25) x16 x17)(∀ x25 . x25intx21 x25 = x20 x25)(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 x12 (x21 x25))(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture e168e..A324265 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 . x12int∀ x13 : ι → ι → ι → ι . (∀ x14 . x14int∀ x15 . x15int∀ x16 . x16intx13 x14 x15 x16int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x20 x20) x20)) x20)(∀ x20 . x20intx1 x20 = add_SNo (add_SNo x20 x20) x20)x2 = add_SNo 1 (add_SNo 2 2)(∀ 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 = x4 x20)(∀ x20 . x20intx6 x20 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo x20 x20)) x20) (mul_SNo x20 x20))x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx9 x20 x21 = x21)(∀ x20 . x20intx10 x20 = x20)x11 = 1x12 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx15 x20 = x13 (x10 x20) x11 x12)(∀ x20 . x20intx16 x20 = x15 x20)(∀ x20 . x20int∀ x21 . x21intx17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx18 x20 = x17 x7 (x16 x20))(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x5 x20 = x19 x20
Conjecture eab3e..A3222 : ∀ 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 = 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 (mul_SNo 2 (add_SNo (mul_SNo 2 (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 = mul_SNo (add_SNo (add_SNo (x15 x17) (minus_SNo (mul_SNo 2 (mul_SNo x17 x17)))) (minus_SNo x17)) 2)∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 819fb..A321003 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι → ι . (∀ x19 . x19int∀ x20 . x20int∀ x21 . x21intx18 x19 x20 x21int)∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo x25 x25)(∀ x25 . x25intx1 x25 = x25)(∀ x25 . x25intx2 x25 = add_SNo (mul_SNo 2 (add_SNo 2 x25)) x25)(∀ x25 . x25intx3 x25 = x25)x4 = 2(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = If_i (SNoLe x25 0) x26 (x2 (x5 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx6 x25 = x5 (x3 x25) x4)(∀ x25 . x25intx7 x25 = add_SNo 1 (x6 x25))(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x1 x25) (x7 x25))(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = x26)(∀ x25 . x25intx15 x25 = x25)x16 = 2x17 = add_SNo 1 2(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx20 x25 = x18 (x15 x25) x16 x17)(∀ x25 . x25intx21 x25 = add_SNo (mul_SNo 2 (x20 x25)) (minus_SNo 1))(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 (x12 x25) (x21 x25))(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 72f12..A320468 : ∀ 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 2 (add_SNo 2 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 (mul_SNo x4 x24) x23)(∀ x23 . x23intx6 x23 = x23)(∀ x23 . x23intx7 x23 = x23)x8 = 1x9 = 2(∀ 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 2 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x24 x24)) x24))) x23)(∀ x23 . x23intx15 x23 = x23)(∀ x23 . x23intx16 x23 = x23)x17 = 1x18 = 2(∀ 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 8c8c0..A307172 : ∀ 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 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 . x13int∀ x14 . x14int∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ 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 . x28intx0 x28 = mul_SNo x28 x28)x1 = 2x2 = 2(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28int∀ x29 . x29intx5 x28 x29 = add_SNo (mul_SNo x4 x28) (minus_SNo x29))(∀ x28 . x28intx6 x28 = x28)(∀ x28 . x28intx7 x28 = x28)x8 = add_SNo 2 2(∀ x28 . x28intx9 x28 = add_SNo 1 (add_SNo x28 x28))x10 = 2x11 = 2(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = If_i (SNoLe x28 0) x29 (x9 (x12 (add_SNo x28 (minus_SNo 1)) x29)))x13 = x12 x10 x11x14 = x13(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx15 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x5 (x15 (add_SNo x28 (minus_SNo 1)) x29 x30) (x16 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x6 (x15 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx17 x28 = x15 (x7 x28) x8 x14)(∀ x28 . x28intx18 x28 = x17 x28)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo (mul_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) x28) (minus_SNo x29))(∀ x28 . x28intx20 x28 = x28)(∀ x28 . x28intx21 x28 = x28)x22 = add_SNo 2 2x23 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = x26 x28)∀ x28 . x28intSNoLe 0 x28x18 x28 = x27 x28
Conjecture 5f8ee..A307169 : ∀ 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 (mul_SNo x4 x23) x24)(∀ x23 . x23intx6 x23 = add_SNo 0 (minus_SNo x23))(∀ x23 . x23intx7 x23 = x23)x8 = add_SNo 2 2x9 = 1(∀ 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 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) x23) (minus_SNo x24))(∀ x23 . x23intx15 x23 = x23)(∀ x23 . x23intx16 x23 = x23)x17 = add_SNo 2 2x18 = add_SNo 0 (minus_SNo 1)(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx21 x23 = x19 (x16 x23) x17 x18)(∀ x23 . x23intx22 x23 = x21 x23)∀ x23 . x23intSNoLe 0 x23x13 x23 = x22 x23
Conjecture a47e1..A307168 : ∀ 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 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 . x13int∀ x14 . x14int∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ 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 . x28intx0 x28 = mul_SNo x28 x28)x1 = 2x2 = 2(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28int∀ x29 . x29intx5 x28 x29 = add_SNo (mul_SNo x4 x28) (minus_SNo x29))(∀ x28 . x28intx6 x28 = x28)(∀ x28 . x28intx7 x28 = x28)(∀ x28 . x28intx8 x28 = add_SNo 1 (add_SNo x28 x28))x9 = 2x10 = 2(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x8 (x11 (add_SNo x28 (minus_SNo 1)) x29)))x12 = x11 x9 x10x13 = x12x14 = add_SNo 2 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx15 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x5 (x15 (add_SNo x28 (minus_SNo 1)) x29 x30) (x16 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x6 (x15 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx17 x28 = x15 (x7 x28) x13 x14)(∀ x28 . x28intx18 x28 = x17 x28)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo (mul_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) x28) (minus_SNo x29))(∀ x28 . x28intx20 x28 = x28)(∀ x28 . x28intx21 x28 = x28)x22 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))x23 = add_SNo 2 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = x26 x28)∀ x28 . x28intSNoLe 0 x28x18 x28 = x27 x28
Conjecture 99cfa..A306948 : ∀ 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 . 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 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ 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 . x32intx31 x32int)(∀ x32 . x32int∀ x33 . x33intx0 x32 x33 = add_SNo 1 (minus_SNo (mul_SNo x32 x33)))(∀ x32 . x32int∀ x33 . x33intx1 x32 x33 = add_SNo x33 (minus_SNo 2))x2 = 1(∀ x32 . x32int∀ x33 . x33intx3 x32 x33 = If_i (SNoLe x32 0) x33 (x0 (x3 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32int∀ x33 . x33intx4 x32 x33 = x3 (x1 x32 x33) x2)(∀ x32 . x32int∀ x33 . x33intx5 x32 x33 = add_SNo (x4 x32 x33) x32)(∀ x32 . x32int∀ x33 . x33intx6 x32 x33 = x33)(∀ x32 . x32intx7 x32 = x32)(∀ x32 . x32int∀ x33 . x33intx8 x32 x33 = If_i (SNoLe x32 0) x33 (x5 (x8 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32int∀ x33 . x33intx9 x32 x33 = x8 (x6 x32 x33) (x7 x32))(∀ x32 . x32int∀ x33 . x33intx10 x32 x33 = x9 x32 x33)(∀ x32 . x32intx11 x32 = x32)x12 = 0(∀ x32 . x32int∀ x33 . x33intx13 x32 x33 = If_i (SNoLe x32 0) x33 (x10 (x13 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32intx14 x32 = x13 (x11 x32) x12)(∀ x32 . x32intx15 x32 = x14 x32)(∀ x32 . x32int∀ x33 . x33intx16 x32 x33 = add_SNo 1 (minus_SNo (mul_SNo x32 x33)))(∀ x32 . x32int∀ x33 . x33intx17 x32 x33 = add_SNo x33 (minus_SNo 1))x18 = 1(∀ x32 . x32int∀ x33 . x33intx19 x32 x33 = If_i (SNoLe x32 0) x33 (x16 (x19 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32int∀ x33 . x33intx20 x32 x33 = x19 (x17 x32 x33) x18)(∀ x32 . x32int∀ x33 . x33intx21 x32 x33 = add_SNo (x20 x32 x33) x32)(∀ x32 . x32int∀ x33 . x33intx22 x32 x33 = add_SNo x33 (minus_SNo 1))x23 = 1(∀ x32 . x32int∀ x33 . x33intx24 x32 x33 = If_i (SNoLe x32 0) x33 (x21 (x24 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32int∀ x33 . x33intx25 x32 x33 = x24 (x22 x32 x33) x23)(∀ x32 . x32int∀ x33 . x33intx26 x32 x33 = add_SNo (x25 x32 x33) x32)(∀ x32 . x32intx27 x32 = x32)x28 = 0(∀ x32 . x32int∀ x33 . x33intx29 x32 x33 = If_i (SNoLe x32 0) x33 (x26 (x29 (add_SNo x32 (minus_SNo 1)) x33) x32))(∀ x32 . x32intx30 x32 = x29 (x27 x32) x28)(∀ x32 . x32intx31 x32 = x30 x32)∀ x32 . x32intSNoLe 0 x32x15 x32 = x31 x32