Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr999../48887..
PUfxu../ba2d1..
vout
Pr999../8e0ef.. 23.98 bars
PUh7w../f832b.. doc published by PrGxv..
Param intint : ι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Conjecture 0d73a..A13801 : ∀ 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 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 . x21int∀ x22 . x22int∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ 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 = mul_SNo x38 x38)x1 = 2x2 = 2(∀ x38 . x38int∀ x39 . x39intx3 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x3 (add_SNo x38 (minus_SNo 1)) x39)))x4 = x3 x1 x2(∀ x38 . x38intx5 x38 = mul_SNo (add_SNo x4 (minus_SNo 2)) x38)(∀ x38 . x38intx6 x38 = add_SNo 1 (add_SNo x38 x38))x7 = 2(∀ x38 . x38intx8 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx9 x38 x39 = If_i (SNoLe x38 0) x39 (x6 (x9 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx10 x38 = x9 x7 (x8 x38))(∀ x38 . x38intx11 x38 = x10 x38)x12 = 1(∀ x38 . x38int∀ x39 . x39intx13 x38 x39 = If_i (SNoLe x38 0) x39 (x5 (x13 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx14 x38 = x13 (x11 x38) x12)(∀ x38 . x38intx15 x38 = x14 x38)(∀ x38 . x38intx16 x38 = mul_SNo x38 x38)x17 = 1(∀ x38 . x38int∀ x39 . x39intx18 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx19 x38 x39 = x39)(∀ x38 . x38intx20 x38 = add_SNo 1 x38)x21 = 1x22 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx23 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x18 (x23 (add_SNo x38 (minus_SNo 1)) x39 x40) (x24 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx24 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x19 (x23 (add_SNo x38 (minus_SNo 1)) x39 x40) (x24 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx25 x38 = x23 (x20 x38) x21 x22)(∀ x38 . x38intx26 x38 = x25 x38)(∀ x38 . x38int∀ x39 . x39intx27 x38 x39 = If_i (SNoLe x38 0) x39 (x16 (x27 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx28 x38 = x27 x17 (x26 x38))(∀ x38 . x38int∀ x39 . x39intx29 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = x39)(∀ x38 . x38intx31 x38 = add_SNo 1 (add_SNo x38 x38))x32 = 1x33 = add_SNo 2 (mul_SNo 2 (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 (x28 x38) (x36 x38))∀ x38 . x38intSNoLe 0 x38x15 x38 = x37 x38
Conjecture 6889c..A13800 : ∀ 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 . 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 . 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 = mul_SNo x33 x33)x1 = 2x2 = 2(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34)))x4 = x3 x1 x2(∀ x33 . x33intx5 x33 = mul_SNo (add_SNo x4 (minus_SNo 2)) x33)(∀ x33 . x33intx6 x33 = add_SNo 1 (mul_SNo 2 (add_SNo x33 x33)))x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = x9 x33)(∀ x33 . x33intx11 x33 = mul_SNo x33 x33)x12 = 1(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx14 x33 x34 = x34)(∀ x33 . x33intx15 x33 = x33)x16 = 1x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx18 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x13 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx19 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x14 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx20 x33 = x18 (x15 x33) x16 x17)(∀ x33 . x33intx21 x33 = x20 x33)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = If_i (SNoLe x33 0) x34 (x11 (x22 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx23 x33 = x22 x12 (x21 x33))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = add_SNo 1 (add_SNo x33 x33))x27 = 1x28 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = mul_SNo (x23 x33) (x31 x33))∀ x33 . x33intSNoLe 0 x33x10 x33 = x32 x33
Conjecture d6199..A13797 : ∀ 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 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 . x21int∀ x22 . x22int∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ 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 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = mul_SNo (add_SNo 2 x44) x43)x1 = 2(∀ x43 . x43intx2 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx4 x43 = x3 x1 (x2 x43))(∀ x43 . x43intx5 x43 = x4 x43)(∀ x43 . x43intx6 x43 = add_SNo 1 (add_SNo x43 x43))x7 = 2(∀ x43 . x43intx8 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = If_i (SNoLe x43 0) x44 (x6 (x9 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx10 x43 = x9 x7 (x8 x43))(∀ x43 . x43intx11 x43 = x10 x43)x12 = 1(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = If_i (SNoLe x43 0) x44 (x5 (x13 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx14 x43 = x13 (x11 x43) x12)(∀ x43 . x43intx15 x43 = x14 x43)(∀ x43 . x43intx16 x43 = mul_SNo x43 x43)x17 = 1(∀ x43 . x43int∀ x44 . x44intx18 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx19 x43 x44 = x44)(∀ x43 . x43intx20 x43 = x43)x21 = 1x22 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx23 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x18 (x23 (add_SNo x43 (minus_SNo 1)) x44 x45) (x24 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx24 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x19 (x23 (add_SNo x43 (minus_SNo 1)) x44 x45) (x24 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx25 x43 = x23 (x20 x43) x21 x22)(∀ x43 . x43intx26 x43 = x25 x43)(∀ x43 . x43int∀ x44 . x44intx27 x43 x44 = If_i (SNoLe x43 0) x44 (x16 (x27 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx28 x43 = x27 x17 (x26 x43))(∀ x43 . x43intx29 x43 = mul_SNo x43 x43)x30 = 1(∀ x43 . x43int∀ x44 . x44intx31 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx32 x43 x44 = x44)(∀ x43 . x43intx33 x43 = add_SNo 1 x43)x34 = 1x35 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx36 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x31 (x36 (add_SNo x43 (minus_SNo 1)) x44 x45) (x37 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx37 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x32 (x36 (add_SNo x43 (minus_SNo 1)) x44 x45) (x37 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx38 x43 = x36 (x33 x43) x34 x35)(∀ x43 . x43intx39 x43 = x38 x43)(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x29 (x40 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx41 x43 = x40 x30 (x39 x43))(∀ x43 . x43intx42 x43 = mul_SNo (mul_SNo (x28 x43) (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))) (x41 x43))∀ x43 . x43intSNoLe 0 x43x15 x43 = x42 x43
Conjecture 55898..A13796 : ∀ 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 : ι → ι → ι . (∀ 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 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38int∀ x39 . x39intx0 x38 x39 = mul_SNo (add_SNo 2 x39) x38)x1 = 2(∀ 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))(∀ x38 . x38intx4 x38 = x3 x1 (x2 x38))(∀ x38 . x38intx5 x38 = x4 x38)(∀ x38 . x38intx6 x38 = add_SNo 1 (mul_SNo 2 (add_SNo x38 x38)))x7 = 1(∀ x38 . x38int∀ x39 . x39intx8 x38 x39 = If_i (SNoLe x38 0) x39 (x5 (x8 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx9 x38 = x8 (x6 x38) x7)(∀ x38 . x38intx10 x38 = x9 x38)(∀ x38 . x38intx11 x38 = mul_SNo x38 x38)x12 = 1(∀ x38 . x38int∀ x39 . x39intx13 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx14 x38 x39 = x39)(∀ x38 . x38intx15 x38 = x38)x16 = 1x17 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx18 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x13 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx19 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x14 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx20 x38 = x18 (x15 x38) x16 x17)(∀ x38 . x38intx21 x38 = x20 x38)(∀ x38 . x38int∀ x39 . x39intx22 x38 x39 = If_i (SNoLe x38 0) x39 (x11 (x22 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx23 x38 = x22 x12 (x21 x38))(∀ x38 . x38intx24 x38 = mul_SNo x38 x38)x25 = 1(∀ x38 . x38int∀ x39 . x39intx26 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx27 x38 x39 = x39)(∀ x38 . x38intx28 x38 = x38)x29 = 1x30 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx31 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x26 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx32 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x27 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx33 x38 = x31 (x28 x38) x29 x30)(∀ x38 . x38intx34 x38 = x33 x38)(∀ x38 . x38int∀ x39 . x39intx35 x38 x39 = If_i (SNoLe x38 0) x39 (x24 (x35 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx36 x38 = x35 x25 (x34 x38))(∀ x38 . x38intx37 x38 = mul_SNo (mul_SNo (x23 x38) (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))) (x36 x38))∀ x38 . x38intSNoLe 0 x38x10 x38 = x37 x38
Conjecture 9a82b..A13793 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 : ι → ι → ι . (∀ 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 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38intx0 x38 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x38 x38)) x38))(∀ x38 . x38intx1 x38 = add_SNo 1 (add_SNo x38 x38))x2 = 2(∀ x38 . x38intx3 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx4 x38 x39 = If_i (SNoLe x38 0) x39 (x1 (x4 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx5 x38 = x4 x2 (x3 x38))(∀ x38 . x38intx6 x38 = x5 x38)x7 = 1(∀ x38 . x38int∀ x39 . x39intx8 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x8 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx9 x38 = x8 (x6 x38) x7)(∀ x38 . x38intx10 x38 = x9 x38)(∀ x38 . x38intx11 x38 = mul_SNo x38 x38)x12 = 1(∀ x38 . x38int∀ x39 . x39intx13 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx14 x38 x39 = x39)(∀ x38 . x38intx15 x38 = x38)x16 = 1x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx18 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x13 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx19 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x14 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx20 x38 = x18 (x15 x38) x16 x17)(∀ x38 . x38intx21 x38 = x20 x38)(∀ x38 . x38int∀ x39 . x39intx22 x38 x39 = If_i (SNoLe x38 0) x39 (x11 (x22 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx23 x38 = x22 x12 (x21 x38))(∀ x38 . x38intx24 x38 = mul_SNo x38 x38)x25 = 1(∀ x38 . x38int∀ x39 . x39intx26 x38 x39 = mul_SNo x38 x39)(∀ x38 . x38int∀ x39 . x39intx27 x38 x39 = x39)(∀ x38 . x38intx28 x38 = add_SNo 1 x38)x29 = 1x30 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx31 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x26 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx32 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x27 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx33 x38 = x31 (x28 x38) x29 x30)(∀ x38 . x38intx34 x38 = x33 x38)(∀ x38 . x38int∀ x39 . x39intx35 x38 x39 = If_i (SNoLe x38 0) x39 (x24 (x35 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx36 x38 = x35 x25 (x34 x38))(∀ x38 . x38intx37 x38 = mul_SNo (mul_SNo (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) (x23 x38)) (x36 x38))∀ x38 . x38intSNoLe 0 x38x10 x38 = x37 x38
Conjecture f2600..A13792 : ∀ 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 . x20int∀ 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 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33intx0 x33 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33))(∀ x33 . x33intx1 x33 = add_SNo 1 (mul_SNo 2 (add_SNo 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 = x4 x33)(∀ x33 . x33intx6 x33 = mul_SNo x33 x33)x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx9 x33 x34 = x34)(∀ x33 . x33intx10 x33 = x33)x11 = 1x12 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx13 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x8 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx14 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x9 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx15 x33 = x13 (x10 x33) x11 x12)(∀ x33 . x33intx16 x33 = x15 x33)(∀ x33 . x33int∀ x34 . x34intx17 x33 x34 = If_i (SNoLe x33 0) x34 (x6 (x17 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx18 x33 = x17 x7 (x16 x33))(∀ x33 . x33intx19 x33 = mul_SNo x33 x33)x20 = 1(∀ x33 . x33int∀ x34 . x34intx21 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = x34)(∀ x33 . x33intx23 x33 = x33)x24 = 1x25 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx26 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x21 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx27 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x22 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx28 x33 = x26 (x23 x33) x24 x25)(∀ x33 . x33intx29 x33 = x28 x33)(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x19 (x30 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx31 x33 = x30 x20 (x29 x33))(∀ x33 . x33intx32 x33 = mul_SNo (mul_SNo (x18 x33) (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) (x31 x33))∀ x33 . x33intSNoLe 0 x33x5 x33 = x32 x33
Conjecture 6031f..A13787 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . 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 (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)) x33)(∀ x33 . x33intx1 x33 = add_SNo 1 (add_SNo x33 x33))x2 = 2(∀ x33 . x33intx3 x33 = x33)(∀ x33 . x33int∀ x34 . x34intx4 x33 x34 = If_i (SNoLe x33 0) x34 (x1 (x4 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx5 x33 = x4 x2 (x3 x33))(∀ x33 . x33intx6 x33 = x5 x33)x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x8 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = x9 x33)(∀ x33 . x33intx11 x33 = mul_SNo x33 x33)x12 = 1(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx14 x33 x34 = x34)(∀ x33 . x33intx15 x33 = add_SNo 1 x33)x16 = 1x17 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx18 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x13 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx19 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x14 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx20 x33 = x18 (x15 x33) x16 x17)(∀ x33 . x33intx21 x33 = x20 x33)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = If_i (SNoLe x33 0) x34 (x11 (x22 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx23 x33 = x22 x12 (x21 x33))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = add_SNo 1 (add_SNo x33 x33))x27 = 1x28 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = mul_SNo (x23 x33) (x31 x33))∀ x33 . x33intSNoLe 0 x33x10 x33 = x32 x33
Conjecture f4d98..A13786 : ∀ 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 . 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 (mul_SNo 2 (add_SNo (add_SNo x28 x28) x28)) x28)(∀ x28 . x28intx1 x28 = add_SNo 1 (mul_SNo 2 (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 = x4 x28)(∀ x28 . x28intx6 x28 = mul_SNo x28 x28)x7 = 1(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx9 x28 x29 = x29)(∀ x28 . x28intx10 x28 = x28)x11 = 1x12 = add_SNo 1 (add_SNo 2 (add_SNo 2 2))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx13 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x8 (x13 (add_SNo x28 (minus_SNo 1)) x29 x30) (x14 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx14 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x9 (x13 (add_SNo x28 (minus_SNo 1)) x29 x30) (x14 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx15 x28 = x13 (x10 x28) x11 x12)(∀ x28 . x28intx16 x28 = x15 x28)(∀ x28 . x28int∀ x29 . x29intx17 x28 x29 = If_i (SNoLe x28 0) x29 (x6 (x17 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx18 x28 = x17 x7 (x16 x28))(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = x29)(∀ x28 . x28intx21 x28 = add_SNo 1 (add_SNo x28 x28))x22 = 1x23 = add_SNo 1 (add_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 x28x5 x28 = x27 x28
Conjecture f86f5..A13785 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x25intx0 x25 = mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))(∀ x25 . x25intx1 x25 = add_SNo 1 (add_SNo x25 x25))x2 = 2(∀ x25 . x25intx3 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx4 x25 x26 = If_i (SNoLe x25 0) x26 (x1 (x4 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx5 x25 = x4 x2 (x3 x25))(∀ x25 . x25intx6 x25 = x5 x25)x7 = 1(∀ 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 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = mul_SNo (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25)) x25)x12 = 2(∀ 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 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 4bd62..A13784 : ∀ 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 = mul_SNo 2 (add_SNo (add_SNo x20 x20) x20))(∀ x20 . x20intx1 x20 = add_SNo 1 (mul_SNo 2 (add_SNo 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 = x4 x20)(∀ x20 . x20intx6 x20 = mul_SNo (mul_SNo (mul_SNo x20 x20) (add_SNo 2 (add_SNo 2 2))) (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 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 787bd..A13783 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x25intx0 x25 = add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25)(∀ x25 . x25intx1 x25 = add_SNo 1 (add_SNo x25 x25))x2 = 2(∀ x25 . x25intx3 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx4 x25 x26 = If_i (SNoLe x25 0) x26 (x1 (x4 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx5 x25 = x4 x2 (x3 x25))(∀ x25 . x25intx6 x25 = x5 x25)x7 = 1(∀ 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 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25) x25)x12 = 2(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = x26)(∀ x25 . x25intx15 x25 = x25)x16 = 1x17 = add_SNo 1 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx20 x25 = x18 (x15 x25) x16 x17)(∀ x25 . x25intx21 x25 = 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 e6520..A13782 : ∀ 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 x20 x20)) x20)(∀ x20 . x20intx1 x20 = add_SNo 1 (mul_SNo 2 (add_SNo 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 = x4 x20)(∀ x20 . x20intx6 x20 = mul_SNo (mul_SNo x20 x20) (mul_SNo (add_SNo 1 (add_SNo 2 2)) (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 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 693a8..A13781 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)(∀ x32 . x32intx0 x32 = add_SNo x32 x32)(∀ x32 . x32intx1 x32 = add_SNo 1 (add_SNo x32 x32))x2 = 2(∀ x32 . x32intx3 x32 = x32)(∀ x32 . x32int∀ x33 . x33intx4 x32 x33 = If_i (SNoLe x32 0) x33 (x1 (x4 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx5 x32 = x4 x2 (x3 x32))(∀ x32 . x32intx6 x32 = mul_SNo 2 (x5 x32))x7 = 1(∀ x32 . x32int∀ x33 . x33intx8 x32 x33 = If_i (SNoLe x32 0) x33 (x0 (x8 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx9 x32 = x8 (x6 x32) x7)(∀ x32 . x32intx10 x32 = x9 x32)(∀ x32 . x32intx11 x32 = mul_SNo x32 x32)x12 = 2(∀ x32 . x32intx13 x32 = add_SNo x32 x32)(∀ x32 . x32intx14 x32 = x32)x15 = 1(∀ x32 . x32int∀ x33 . x33intx16 x32 x33 = If_i (SNoLe x32 0) x33 (x13 (x16 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx17 x32 = x16 (x14 x32) x15)(∀ x32 . x32intx18 x32 = x17 x32)(∀ x32 . x32int∀ x33 . x33intx19 x32 x33 = If_i (SNoLe x32 0) x33 (x11 (x19 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx20 x32 = x19 x12 (x18 x32))(∀ x32 . x32intx21 x32 = mul_SNo x32 x32)x22 = 2(∀ x32 . x32intx23 x32 = add_SNo x32 x32)(∀ x32 . x32intx24 x32 = x32)x25 = 2(∀ x32 . x32int∀ x33 . x33intx26 x32 x33 = If_i (SNoLe x32 0) x33 (x23 (x26 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx27 x32 = x26 (x24 x32) x25)(∀ x32 . x32intx28 x32 = x27 x32)(∀ x32 . x32int∀ x33 . x33intx29 x32 x33 = If_i (SNoLe x32 0) x33 (x21 (x29 (add_SNo x32 (minus_SNo 1)) x33)))(∀ x32 . x32intx30 x32 = x29 x22 (x28 x32))(∀ x32 . x32intx31 x32 = mul_SNo (mul_SNo 2 (mul_SNo 2 (x20 x32))) (x30 x32))∀ x32 . x32intSNoLe 0 x32x10 x32 = x31 x32
Conjecture 61dfd..A13779 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x25intx0 x25 = add_SNo (add_SNo x25 x25) x25)(∀ x25 . x25intx1 x25 = add_SNo 1 (add_SNo x25 x25))x2 = 2(∀ x25 . x25intx3 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx4 x25 x26 = If_i (SNoLe x25 0) x26 (x1 (x4 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx5 x25 = x4 x2 (x3 x25))(∀ x25 . x25intx6 x25 = x5 x25)x7 = 1(∀ 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 (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 = add_SNo 1 2x17 = add_SNo 1 (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 1cb49..A13778 : ∀ 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 (add_SNo x20 x20) x20)(∀ x20 . x20intx1 x20 = add_SNo 1 (mul_SNo 2 (add_SNo 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 = x4 x20)(∀ x20 . x20intx6 x20 = mul_SNo (add_SNo (add_SNo x20 x20) x20) (mul_SNo (mul_SNo x20 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 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 34312..A13777 : ∀ 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 2 (mul_SNo 2 (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 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 2(∀ 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 (mul_SNo 2 (add_SNo 2 2)) (x15 x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 7188e..A13776 : ∀ 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 = mul_SNo 2 (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 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 2(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo 2 (x15 x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 20258..A13769 : ∀ 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 . 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 . 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 = mul_SNo 2 (add_SNo 2 x33))x1 = 2x2 = 2(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34)))x4 = x3 x1 x2(∀ x33 . x33intx5 x33 = add_SNo (mul_SNo x4 x33) x33)(∀ x33 . x33intx6 x33 = add_SNo 2 (add_SNo (add_SNo x33 x33) x33))x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = x9 x33)(∀ x33 . x33intx11 x33 = mul_SNo x33 x33)x12 = 1(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx14 x33 x34 = x34)(∀ x33 . x33intx15 x33 = x33)x16 = 1x17 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx18 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x13 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx19 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x14 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx20 x33 = x18 (x15 x33) x16 x17)(∀ x33 . x33intx21 x33 = x20 x33)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = If_i (SNoLe x33 0) x34 (x11 (x22 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx23 x33 = x22 x12 (x21 x33))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = add_SNo 2 x33)x27 = 1x28 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = mul_SNo (x23 x33) (x31 x33))∀ x33 . x33intSNoLe 0 x33x10 x33 = x32 x33
Conjecture fb648..A13768 : ∀ 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 . 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 . 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 = mul_SNo 2 (add_SNo 2 x33))x1 = 2x2 = 2(∀ x33 . x33int∀ x34 . x34intx3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34)))x4 = x3 x1 x2(∀ x33 . x33intx5 x33 = add_SNo (mul_SNo x4 x33) x33)(∀ x33 . x33intx6 x33 = add_SNo 1 (add_SNo (add_SNo x33 x33) x33))x7 = 1(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx9 x33 = x8 (x6 x33) x7)(∀ x33 . x33intx10 x33 = x9 x33)(∀ x33 . x33intx11 x33 = mul_SNo x33 x33)x12 = 1(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx14 x33 x34 = x34)(∀ x33 . x33intx15 x33 = x33)x16 = 1x17 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx18 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x13 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx19 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x14 (x18 (add_SNo x33 (minus_SNo 1)) x34 x35) (x19 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx20 x33 = x18 (x15 x33) x16 x17)(∀ x33 . x33intx21 x33 = x20 x33)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = If_i (SNoLe x33 0) x34 (x11 (x22 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx23 x33 = x22 x12 (x21 x33))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo x33 x34)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = x34)(∀ x33 . x33intx26 x33 = add_SNo 1 x33)x27 = 1x28 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx31 x33 = x29 (x26 x33) x27 x28)(∀ x33 . x33intx32 x33 = mul_SNo (x23 x33) (x31 x33))∀ x33 . x33intSNoLe 0 x33x10 x33 = x32 x33
Conjecture 6a754..A13767 : ∀ 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 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43intx0 x43 = mul_SNo 2 (add_SNo 2 x43))x1 = 2x2 = 2(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44)))x4 = x3 x1 x2(∀ x43 . x43intx5 x43 = mul_SNo x4 x43)(∀ x43 . x43intx6 x43 = add_SNo 2 (add_SNo (add_SNo x43 x43) x43))x7 = 1(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = If_i (SNoLe x43 0) x44 (x5 (x8 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx9 x43 = x8 (x6 x43) x7)(∀ x43 . x43intx10 x43 = x9 x43)(∀ x43 . x43int∀ x44 . x44intx11 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x44)(∀ x43 . x43intx13 x43 = add_SNo 2 x43)x14 = 1x15 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx16 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x11 (x16 (add_SNo x43 (minus_SNo 1)) x44 x45) (x17 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx17 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x12 (x16 (add_SNo x43 (minus_SNo 1)) x44 x45) (x17 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx18 x43 = x16 (x13 x43) x14 x15)(∀ x43 . x43intx19 x43 = mul_SNo (mul_SNo x43 x43) x43)x20 = 1(∀ x43 . x43intx21 x43 = add_SNo x43 x43)(∀ x43 . x43intx22 x43 = x43)x23 = 1(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = If_i (SNoLe x43 0) x44 (x21 (x24 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx25 x43 = x24 (x22 x43) x23)(∀ x43 . x43intx26 x43 = x25 x43)(∀ x43 . x43int∀ x44 . x44intx27 x43 x44 = If_i (SNoLe x43 0) x44 (x19 (x27 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx28 x43 = x27 x20 (x26 x43))(∀ x43 . x43intx29 x43 = mul_SNo x43 x43)x30 = 1(∀ x43 . x43int∀ x44 . x44intx31 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx32 x43 x44 = x44)(∀ x43 . x43intx33 x43 = x43)x34 = 2x35 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx36 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x31 (x36 (add_SNo x43 (minus_SNo 1)) x44 x45) (x37 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx37 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x32 (x36 (add_SNo x43 (minus_SNo 1)) x44 x45) (x37 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx38 x43 = x36 (x33 x43) x34 x35)(∀ x43 . x43intx39 x43 = x38 x43)(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x29 (x40 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx41 x43 = x40 x30 (x39 x43))(∀ x43 . x43intx42 x43 = mul_SNo (mul_SNo (x18 x43) (x28 x43)) (x41 x43))∀ x43 . x43intSNoLe 0 x43x10 x43 = x42 x43