Search for blocks/addresses/...

Proofgold Asset

asset id
433346a54a30b3dcd18c69b7850d0addbf82cabfb53ed1ac3b4144e05cee5175
asset hash
ef6deb0709278ce576192f9e5585b21aa527909d3c9a61a64e0c32cc851cd066
bday / block
25650
tx
b4c68..
preasset
doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param minus_SNominus_SNo : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Conjecture 97664..A20871 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo (mul_SNo 2 (add_SNo x18 x18)) (minus_SNo x19))(∀ x18 . x18intx1 x18 = x18)(∀ x18 . x18intx2 x18 = x18)x3 = 1x4 = 2(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx5 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x0 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx6 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x1 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 x4)(∀ x18 . x18intx8 x18 = add_SNo (mul_SNo x18 (x7 x18)) x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo (mul_SNo 2 (add_SNo x18 x18)) (minus_SNo x19))(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = add_SNo x18 (minus_SNo 1))x12 = 2x13 = 1(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) x12 x13)(∀ x18 . x18intx17 x18 = add_SNo (mul_SNo x18 (x16 x18)) x18)∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 155ce..A20766 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 . x16int∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = mul_SNo (add_SNo 2 x51) x50)x16 = 2(∀ x50 . x50intx17 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 x16 (x17 x50))(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (x14 x50 x51) (add_SNo (x19 x50) (minus_SNo x50)))(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50int∀ x51 . x51intx31 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = x51)(∀ x50 . x50intx33 x50 = x50)x34 = 1x35 = add_SNo 2 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx36 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x31 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx37 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x32 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx38 x50 = x36 (x33 x50) x34 x35)(∀ x50 . x50intx39 x50 = mul_SNo (add_SNo (x30 x50) (minus_SNo 1)) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 19b53..A20758 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (x14 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)))(∀ x50 . x50intx16 x50 = x50)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 (x16 x50) x17)(∀ x50 . x50intx20 x50 = x19 x50)(∀ x50 . x50intx21 x50 = add_SNo x50 x50)(∀ x50 . x50intx22 x50 = x50)x23 = 2(∀ x50 . x50int∀ x51 . x51intx24 x50 x51 = If_i (SNoLe x50 0) x51 (x21 (x24 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx25 x50 = x24 (x22 x50) x23)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = x51)(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 1 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = mul_SNo (add_SNo (x25 x50) (minus_SNo 1)) (x33 x50))x35 = 1(∀ x50 . x50int∀ x51 . x51intx36 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx38 x50 x51 = x37 x35 (x36 x50 x51))(∀ x50 . x50int∀ x51 . x51intx39 x50 x51 = add_SNo (add_SNo (x38 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx40 x50 = x50)x41 = 1(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx43 x50 = x42 (x40 x50) x41)(∀ x50 . x50intx44 x50 = add_SNo x50 x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = mul_SNo (x43 x50) (x48 x50))∀ x50 . x50intSNoLe 0 x50x20 x50 = x49 x50
Conjecture efa92..A20726 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45int∀ x46 . x46intx0 x45 x46 = mul_SNo (add_SNo 2 x46) x45)x1 = 2(∀ x45 . x45intx2 x45 = x45)(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx4 x45 = x3 x1 (x2 x45))(∀ x45 . x45intx5 x45 = add_SNo (x4 x45) (minus_SNo x45))(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (x9 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45int∀ x46 . x46intx11 x45 x46 = x46)x12 = 1(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx14 x45 x46 = x13 (x11 x45 x46) x12)(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = add_SNo (x14 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45)))(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = x19 x45)(∀ x45 . x45int∀ x46 . x46intx21 x45 x46 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45) x46)(∀ x45 . x45int∀ x46 . x46intx22 x45 x46 = add_SNo (add_SNo x46 x46) x46)(∀ x45 . x45intx23 x45 = x45)x24 = 1x25 = add_SNo 1 2(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx26 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x21 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx27 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x22 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx28 x45 = x26 (x23 x45) x24 x25)(∀ x45 . x45intx29 x45 = add_SNo x45 x45)(∀ x45 . x45intx30 x45 = x45)x31 = 1(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx33 x45 = x32 (x30 x45) x31)(∀ x45 . x45intx34 x45 = mul_SNo (x28 x45) (x33 x45))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45))) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture 32a47..A2066 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)x2 = add_SNo 1 (add_SNo 2 2)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = mul_SNo 2 (x4 x17))(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = mul_SNo 2 (mul_SNo (add_SNo 1 (add_SNo 2 2)) (x15 x17)))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture c9987..A20606 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . 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 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)(∀ x48 . x48intx0 x48 = add_SNo (add_SNo x48 x48) x48)(∀ x48 . x48int∀ x49 . x49intx1 x48 x49 = add_SNo x49 x49)x2 = 1(∀ x48 . x48int∀ x49 . x49intx3 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x3 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx4 x48 x49 = x3 (x1 x48 x49) x2)(∀ x48 . x48int∀ x49 . x49intx5 x48 x49 = mul_SNo (add_SNo 2 x49) x48)x6 = 2(∀ x48 . x48intx7 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx8 x48 x49 = If_i (SNoLe x48 0) x49 (x5 (x8 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx9 x48 = x8 x6 (x7 x48))(∀ x48 . x48int∀ x49 . x49intx10 x48 x49 = add_SNo (x4 x48 x49) (add_SNo (x9 x48) (minus_SNo x48)))(∀ x48 . x48int∀ x49 . x49intx11 x48 x49 = x49)x12 = 1(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = If_i (SNoLe x48 0) x49 (x10 (x13 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48int∀ x49 . x49intx14 x48 x49 = x13 (x11 x48 x49) x12)(∀ x48 . x48int∀ x49 . x49intx15 x48 x49 = add_SNo (x14 x48 x49) (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48)))(∀ x48 . x48intx16 x48 = x48)x17 = 1(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = If_i (SNoLe x48 0) x49 (x15 (x18 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx19 x48 = x18 (x16 x48) x17)(∀ x48 . x48intx20 x48 = x19 x48)(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = add_SNo (add_SNo (add_SNo x48 x48) x48) x49)(∀ x48 . x48int∀ x49 . x49intx22 x48 x49 = add_SNo x49 x49)(∀ x48 . x48intx23 x48 = x48)x24 = 1x25 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx26 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x21 (x26 (add_SNo x48 (minus_SNo 1)) x49 x50) (x27 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx27 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x22 (x26 (add_SNo x48 (minus_SNo 1)) x49 x50) (x27 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx28 x48 = x26 (x23 x48) x24 x25)(∀ x48 . x48int∀ x49 . x49intx29 x48 x49 = mul_SNo x48 x49)(∀ x48 . x48int∀ x49 . x49intx30 x48 x49 = x49)(∀ x48 . x48intx31 x48 = x48)x32 = 1x33 = add_SNo 1 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx34 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x29 (x34 (add_SNo x48 (minus_SNo 1)) x49 x50) (x35 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx35 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x30 (x34 (add_SNo x48 (minus_SNo 1)) x49 x50) (x35 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx36 x48 = x34 (x31 x48) x32 x33)(∀ x48 . x48intx37 x48 = mul_SNo (x28 x48) (x36 x48))x38 = 1(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 x38 (x39 x48 x49))(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48))) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 1(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x20 x48 = x47 x48
Conjecture 04070..A20595 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . 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 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43intx0 x43 = add_SNo (add_SNo x43 x43) x43)(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)x2 = 1(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx4 x43 x44 = x3 (x1 x43 x44) x2)(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (x4 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43)))(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = x44)x7 = 1(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = If_i (SNoLe x43 0) x44 (x5 (x8 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = x8 (x6 x43 x44) x7)(∀ x43 . x43int∀ x44 . x44intx10 x43 x44 = add_SNo (x9 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)))(∀ x43 . x43intx11 x43 = x43)x12 = 1(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = If_i (SNoLe x43 0) x44 (x10 (x13 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx14 x43 = x13 (x11 x43) x12)(∀ x43 . x43intx15 x43 = x14 x43)(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = add_SNo (add_SNo (add_SNo x43 x43) x43) x44)(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = add_SNo x44 x44)(∀ x43 . x43intx18 x43 = x43)x19 = 1x20 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx21 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x16 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx22 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x17 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx23 x43 = x21 (x18 x43) x19 x20)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = x44)(∀ x43 . x43intx26 x43 = x43)x27 = 1x28 = add_SNo 1 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx31 x43 = x29 (x26 x43) x27 x28)(∀ x43 . x43intx32 x43 = mul_SNo (x23 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)))(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x15 x43 = x42 x43
Conjecture fa1f9..A20594 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (x14 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50))))(∀ x50 . x50intx16 x50 = x50)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 (x16 x50) x17)(∀ x50 . x50intx20 x50 = x19 x50)(∀ x50 . x50intx21 x50 = add_SNo x50 x50)(∀ x50 . x50intx22 x50 = x50)x23 = 2(∀ x50 . x50int∀ x51 . x51intx24 x50 x51 = If_i (SNoLe x50 0) x51 (x21 (x24 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx25 x50 = x24 (x22 x50) x23)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = x51)(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 1 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = mul_SNo (add_SNo (x25 x50) (minus_SNo 1)) (x33 x50))x35 = 1(∀ x50 . x50int∀ x51 . x51intx36 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx38 x50 x51 = x37 x35 (x36 x50 x51))(∀ x50 . x50int∀ x51 . x51intx39 x50 x51 = add_SNo (x38 x50 x51) (mul_SNo 2 (add_SNo x50 x50)))(∀ x50 . x50intx40 x50 = x50)x41 = 1(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx43 x50 = x42 (x40 x50) x41)(∀ x50 . x50intx44 x50 = add_SNo x50 x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = mul_SNo (x43 x50) (x48 x50))∀ x50 . x50intSNoLe 0 x50x20 x50 = x49 x50
Conjecture ec029..A20593 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 . x9int∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43)) (mul_SNo (mul_SNo x44 x44) x44))(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx2 x43 x44 = x44)x3 = 1x4 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx5 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x0 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx6 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x1 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x5 (x2 x43 x44) x3 x4)(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = mul_SNo (add_SNo 2 x44) x43)x9 = 2(∀ x43 . x43intx10 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx11 x43 x44 = If_i (SNoLe x43 0) x44 (x8 (x11 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx12 x43 = x11 x9 (x10 x43))(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (add_SNo (x7 x43 x44) (minus_SNo x43)) (x12 x43))(∀ x43 . x43intx14 x43 = x43)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx17 x43 = x16 (x14 x43) x15)(∀ x43 . x43intx18 x43 = x17 x43)(∀ x43 . x43int∀ x44 . x44intx19 x43 x44 = add_SNo (add_SNo (add_SNo (mul_SNo x44 x44) x43) x43) x43)(∀ x43 . x43int∀ x44 . x44intx20 x43 x44 = add_SNo x44 x44)(∀ x43 . x43intx21 x43 = x43)x22 = 1x23 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx24 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x19 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx25 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x20 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx26 x43 = x24 (x21 x43) x22 x23)(∀ x43 . x43intx27 x43 = add_SNo x43 x43)(∀ x43 . x43intx28 x43 = add_SNo x43 (minus_SNo 1))x29 = 2(∀ x43 . x43int∀ x44 . x44intx30 x43 x44 = If_i (SNoLe x43 0) x44 (x27 (x30 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx31 x43 = x30 (x28 x43) x29)(∀ x43 . x43intx32 x43 = mul_SNo (x26 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43))) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x18 x43 = x42 x43
Conjecture 836e9..A20579 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo (add_SNo x45 x45) x45)(∀ x45 . x45int∀ x46 . x46intx1 x45 x46 = add_SNo x46 x46)x2 = 1(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx4 x45 x46 = x3 (x1 x45 x46) x2)(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = add_SNo (x4 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (x9 x45 x46) (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))))(∀ x45 . x45intx11 x45 = x45)x12 = 1(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx14 x45 = x13 (x11 x45) x12)(∀ x45 . x45intx15 x45 = x14 x45)(∀ x45 . x45int∀ x46 . x46intx16 x45 x46 = mul_SNo x45 x46)(∀ x45 . x45int∀ x46 . x46intx17 x45 x46 = x46)(∀ x45 . x45intx18 x45 = add_SNo 1 x45)x19 = 1x20 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx21 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x16 (x21 (add_SNo x45 (minus_SNo 1)) x46 x47) (x22 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx22 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x17 (x21 (add_SNo x45 (minus_SNo 1)) x46 x47) (x22 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx23 x45 = x21 (x18 x45) x19 x20)(∀ x45 . x45intx24 x45 = mul_SNo (mul_SNo x45 x45) x45)x25 = 1(∀ x45 . x45intx26 x45 = add_SNo x45 x45)(∀ x45 . x45intx27 x45 = x45)x28 = 2(∀ x45 . x45int∀ x46 . x46intx29 x45 x46 = If_i (SNoLe x45 0) x46 (x26 (x29 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx30 x45 = x29 (x27 x45) x28)(∀ x45 . x45intx31 x45 = x30 x45)(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x24 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx33 x45 = x32 x25 (x31 x45))(∀ x45 . x45intx34 x45 = add_SNo (x23 x45) (minus_SNo (x33 x45)))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (add_SNo (add_SNo (add_SNo (add_SNo (x38 x45 x46) x45) x45) x45) x45) x45) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x15 x45 = x44 x45
Conjecture 39c5e..A20577 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))(∀ x45 . x45intx1 x45 = x45)(∀ x45 . x45intx2 x45 = add_SNo x45 x45)(∀ x45 . x45intx3 x45 = x45)x4 = 2(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = If_i (SNoLe x45 0) x46 (x2 (x5 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx6 x45 = x5 (x3 x45) x4)(∀ x45 . x45intx7 x45 = add_SNo (x6 x45) (minus_SNo 1))(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx9 x45 = x8 (x1 x45) (x7 x45))(∀ x45 . x45intx10 x45 = x9 x45)x11 = 1(∀ x45 . x45int∀ x46 . x46intx12 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx14 x45 x46 = x13 x11 (x12 x45 x46))(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = add_SNo (add_SNo (x14 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x45)(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = x19 x45)(∀ x45 . x45intx21 x45 = add_SNo x45 x45)(∀ x45 . x45intx22 x45 = x45)x23 = 2(∀ x45 . x45int∀ x46 . x46intx24 x45 x46 = If_i (SNoLe x45 0) x46 (x21 (x24 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx25 x45 = x24 (x22 x45) x23)(∀ x45 . x45int∀ x46 . x46intx26 x45 x46 = mul_SNo x45 x46)(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = x46)(∀ x45 . x45intx28 x45 = x45)x29 = 1x30 = add_SNo 2 (add_SNo 2 2)(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx33 x45 = x31 (x28 x45) x29 x30)(∀ x45 . x45intx34 x45 = mul_SNo (add_SNo (x25 x45) (minus_SNo 1)) (x33 x45))x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture e9936..A20573 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40int∀ x41 . x41intx0 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x1 = 2(∀ x40 . x40intx2 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx4 x40 = x3 x1 (x2 x40))(∀ x40 . x40intx5 x40 = add_SNo (x4 x40) (minus_SNo x40))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (mul_SNo (add_SNo 1 2) (add_SNo (add_SNo x40 x40) x41)) x40)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = mul_SNo 2 (add_SNo (add_SNo x41 x41) x41))(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) x40) (mul_SNo (add_SNo (mul_SNo (add_SNo x40 x40) 2) x40) 2))(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture 95615..A20572 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 . x26int∀ 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 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40intx0 x40 = mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = x41)x2 = 1(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx4 x40 x41 = x3 (x1 x40 x41) x2)(∀ x40 . x40int∀ x41 . x41intx5 x40 x41 = add_SNo (x4 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)))(∀ x40 . x40int∀ x41 . x41intx6 x40 x41 = x41)x7 = 1(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx9 x40 x41 = x8 (x6 x40 x41) x7)(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40intx11 x40 = x40)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx14 x40 = x13 (x11 x40) x12)(∀ x40 . x40intx15 x40 = x14 x40)(∀ x40 . x40int∀ x41 . x41intx16 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40) x41)(∀ x40 . x40int∀ x41 . x41intx17 x40 x41 = add_SNo (add_SNo x41 x41) x41)(∀ x40 . x40intx18 x40 = x40)x19 = 1x20 = add_SNo 1 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx21 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x16 (x21 (add_SNo x40 (minus_SNo 1)) x41 x42) (x22 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx22 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x17 (x21 (add_SNo x40 (minus_SNo 1)) x41 x42) (x22 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx23 x40 = x21 (x18 x40) x19 x20)(∀ x40 . x40intx24 x40 = add_SNo x40 x40)(∀ x40 . x40intx25 x40 = x40)x26 = 1(∀ x40 . x40int∀ x41 . x41intx27 x40 x41 = If_i (SNoLe x40 0) x41 (x24 (x27 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40intx28 x40 = x27 (x25 x40) x26)(∀ x40 . x40intx29 x40 = mul_SNo (x23 x40) (x28 x40))x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40)(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x15 x40 = x39 x40
Conjecture 38b42..A20571 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . 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 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43intx0 x43 = add_SNo (add_SNo x43 x43) x43)(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)x2 = 1(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx4 x43 x44 = x3 (x1 x43 x44) x2)(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (x4 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43)))(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = x44)x7 = 1(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = If_i (SNoLe x43 0) x44 (x5 (x8 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = x8 (x6 x43 x44) x7)(∀ x43 . x43int∀ x44 . x44intx10 x43 x44 = add_SNo (add_SNo (x9 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43)(∀ x43 . x43intx11 x43 = x43)x12 = 1(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = If_i (SNoLe x43 0) x44 (x10 (x13 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx14 x43 = x13 (x11 x43) x12)(∀ x43 . x43intx15 x43 = x14 x43)(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = add_SNo (add_SNo (add_SNo x43 x43) x43) x44)(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = add_SNo x44 x44)(∀ x43 . x43intx18 x43 = x43)x19 = 1x20 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx21 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x16 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx22 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x17 (x21 (add_SNo x43 (minus_SNo 1)) x44 x45) (x22 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx23 x43 = x21 (x18 x43) x19 x20)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = mul_SNo x43 x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = x44)(∀ x43 . x43intx26 x43 = x43)x27 = 1x28 = add_SNo 1 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx31 x43 = x29 (x26 x43) x27 x28)(∀ x43 . x43intx32 x43 = mul_SNo (x23 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x15 x43 = x42 x43
Conjecture 518fc..A20569 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45int∀ x46 . x46intx0 x45 x46 = mul_SNo (add_SNo 2 x46) x45)x1 = 2(∀ x45 . x45intx2 x45 = x45)(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx4 x45 = x3 x1 (x2 x45))(∀ x45 . x45intx5 x45 = add_SNo (x4 x45) (minus_SNo x45))(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = mul_SNo (add_SNo 2 x46) x45)x11 = 2(∀ x45 . x45intx12 x45 = x45)(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx14 x45 = x13 x11 (x12 x45))(∀ x45 . x45int∀ x46 . x46intx15 x45 x46 = add_SNo (x9 x45 x46) (x14 x45))(∀ x45 . x45int∀ x46 . x46intx16 x45 x46 = x46)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx19 x45 x46 = x18 (x16 x45 x46) x17)(∀ x45 . x45int∀ x46 . x46intx20 x45 x46 = add_SNo (add_SNo (x19 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45intx21 x45 = x45)x22 = 1(∀ x45 . x45int∀ x46 . x46intx23 x45 x46 = If_i (SNoLe x45 0) x46 (x20 (x23 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx24 x45 = x23 (x21 x45) x22)(∀ x45 . x45intx25 x45 = x24 x45)(∀ x45 . x45int∀ x46 . x46intx26 x45 x46 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x46)(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = add_SNo (mul_SNo 2 (add_SNo x46 x46)) x46)(∀ x45 . x45intx28 x45 = x45)x29 = 1x30 = add_SNo 1 (add_SNo 2 2)(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx33 x45 = x31 (x28 x45) x29 x30)(∀ x45 . x45intx34 x45 = x33 x45)x35 = 1(∀ x45 . x45int∀ x46 . x46intx36 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 x35 (x36 x45 x46))(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45))) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x25 x45 = x44 x45
Conjecture c4cd1..A20568 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 . x16int∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = mul_SNo (add_SNo 2 x51) x50)x16 = 2(∀ x50 . x50intx17 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 x16 (x17 x50))(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (x14 x50 x51) (x19 x50))(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50int∀ x51 . x51intx31 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = x51)(∀ x50 . x50intx33 x50 = x50)x34 = 1x35 = add_SNo 1 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx36 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x31 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx37 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x32 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx38 x50 = x36 (x33 x50) x34 x35)(∀ x50 . x50intx39 x50 = mul_SNo (add_SNo (x30 x50) (minus_SNo 1)) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (x43 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))))(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 1d45d..A20567 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 . x16int∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = mul_SNo (add_SNo 2 x51) x50)x16 = 2(∀ x50 . x50intx17 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 x16 (x17 x50))(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (x14 x50 x51) (add_SNo (x19 x50) (minus_SNo x50)))(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50int∀ x51 . x51intx31 x50 x51 = mul_SNo x50 x51)(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = x51)(∀ x50 . x50intx33 x50 = x50)x34 = 1x35 = add_SNo 1 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx36 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x31 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx37 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x32 (x36 (add_SNo x50 (minus_SNo 1)) x51 x52) (x37 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx38 x50 = x36 (x33 x50) x34 x35)(∀ x50 . x50intx39 x50 = mul_SNo (add_SNo (x30 x50) (minus_SNo 1)) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 1a6bd..A20566 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)(∀ x40 . x40intx0 x40 = add_SNo (add_SNo x40 x40) x40)(∀ x40 . x40int∀ x41 . x41intx1 x40 x41 = add_SNo x41 x41)x2 = 1(∀ x40 . x40int∀ x41 . x41intx3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx4 x40 x41 = x3 (x1 x40 x41) x2)(∀ x40 . x40int∀ x41 . x41intx5 x40 x41 = mul_SNo (add_SNo 2 x41) x40)x6 = 2(∀ x40 . x40intx7 x40 = x40)(∀ x40 . x40int∀ x41 . x41intx8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx9 x40 = x8 x6 (x7 x40))(∀ x40 . x40int∀ x41 . x41intx10 x40 x41 = add_SNo (x4 x40 x41) (x9 x40))(∀ x40 . x40int∀ x41 . x41intx11 x40 x41 = x41)x12 = 1(∀ x40 . x40int∀ x41 . x41intx13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40int∀ x41 . x41intx14 x40 x41 = x13 (x11 x40 x41) x12)(∀ x40 . x40int∀ x41 . x41intx15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40)(∀ x40 . x40intx16 x40 = x40)x17 = 1(∀ x40 . x40int∀ x41 . x41intx18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx19 x40 = x18 (x16 x40) x17)(∀ x40 . x40intx20 x40 = x19 x40)(∀ x40 . x40int∀ x41 . x41intx21 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x40 x40)) (mul_SNo x41 x41)) x40)(∀ x40 . x40int∀ x41 . x41intx22 x40 x41 = add_SNo (add_SNo x41 x41) x41)(∀ x40 . x40intx23 x40 = x40)x24 = 1x25 = add_SNo 1 2(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42)))(∀ x40 . x40intx28 x40 = x26 (x23 x40) x24 x25)(∀ x40 . x40intx29 x40 = x28 x40)x30 = 1(∀ x40 . x40int∀ x41 . x41intx31 x40 x41 = x41)(∀ x40 . x40int∀ x41 . x41intx32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41)))(∀ x40 . x40int∀ x41 . x41intx33 x40 x41 = x32 x30 (x31 x40 x41))(∀ x40 . x40int∀ x41 . x41intx34 x40 x41 = add_SNo (x33 x40 x41) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))))(∀ x40 . x40intx35 x40 = x40)x36 = 1(∀ x40 . x40int∀ x41 . x41intx37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40))(∀ x40 . x40intx38 x40 = x37 (x35 x40) x36)(∀ x40 . x40intx39 x40 = x38 x40)∀ x40 . x40intSNoLe 0 x40x20 x40 = x39 x40
Conjecture 7c4af..A20537 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = mul_SNo 2 (add_SNo 2 x22))(∀ x22 . x22intx3 x22 = add_SNo x22 x22)x4 = 0(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo 1 (x6 x22))(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (mul_SNo (mul_SNo x22 x22) x22) (minus_SNo x22)))) x22)x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 1(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = x17 x22)(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = x20 x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 0e624..A20530 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = add_SNo x22 x22)(∀ x22 . x22intx3 x22 = add_SNo x22 x22)x4 = 1(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo 2 (x6 x22))(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = mul_SNo (add_SNo 2 (mul_SNo x22 x22)) x22)x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 1(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = x17 x22)(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = x20 x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22