Search for blocks/addresses/...

Proofgold Asset

asset id
89d680db861beab2191df97ab14ccbab14084c2e57662dbd9397102ed5e4402d
asset hash
c6f442cefcf01132c27085d47fd59d3cd8b8eff2921ea8acf7348f9e9ce26150
bday / block
25625
tx
971cf..
preasset
doc published by PrGxv..
Param intint : ι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param add_SNoadd_SNo : ιιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Conjecture de652..A60365 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 . x10int∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι → ι . (∀ x13 . x13int∀ x14 . x14int∀ x15 . x15intx12 x13 x14 x15int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23intx0 x23 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x23 x23)) x23))(∀ x23 . x23intx1 x23 = mul_SNo (add_SNo 1 2) (add_SNo 1 x23))x2 = 1(∀ x23 . x23int∀ x24 . x24intx3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx4 x23 = x3 (x1 x23) x2)(∀ x23 . x23intx5 x23 = x4 x23)(∀ x23 . x23int∀ x24 . x24intx6 x23 x24 = mul_SNo x23 x24)(∀ x23 . x23int∀ x24 . x24intx7 x23 x24 = x24)(∀ x23 . x23intx8 x23 = add_SNo 1 x23)x9 = 1x10 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx11 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x6 (x11 (add_SNo x23 (minus_SNo 1)) x24 x25) (x12 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx12 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x7 (x11 (add_SNo x23 (minus_SNo 1)) x24 x25) (x12 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx13 x23 = x11 (x8 x23) x9 x10)(∀ x23 . x23int∀ x24 . x24intx14 x23 x24 = mul_SNo x23 x24)(∀ x23 . x23int∀ x24 . x24intx15 x23 x24 = x24)(∀ x23 . x23intx16 x23 = add_SNo 1 x23)x17 = 1x18 = mul_SNo 2 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx21 x23 = x19 (x16 x23) x17 x18)(∀ x23 . x23intx22 x23 = mul_SNo (x13 x23) (x21 x23))∀ x23 . x23intSNoLe 0 x23x5 x23 = x22 x23
Conjecture c6e5a..A5970 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 . x31int∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι → ι → ι . (∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx33 x34 x35 x36int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)(∀ x36 . x36intx0 x36 = mul_SNo x36 x36)x1 = 1(∀ x36 . x36int∀ x37 . x37intx2 x36 x37 = add_SNo x36 x37)(∀ x36 . x36intx3 x36 = x36)(∀ x36 . x36int∀ x37 . x37intx4 x36 x37 = x37)x5 = 1x6 = 2(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx7 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x2 (x7 (add_SNo x36 (minus_SNo 1)) x37 x38) (x8 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx8 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x3 (x7 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37intx9 x36 x37 = x7 (x4 x36 x37) x5 x6)(∀ x36 . x36int∀ x37 . x37intx10 x36 x37 = x9 x36 x37)(∀ x36 . x36int∀ x37 . x37intx11 x36 x37 = If_i (SNoLe x36 0) x37 (x0 (x11 (add_SNo x36 (minus_SNo 1)) x37)))(∀ x36 . x36int∀ x37 . x37intx12 x36 x37 = x11 x1 (x10 x36 x37))(∀ x36 . x36int∀ x37 . x37intx13 x36 x37 = add_SNo (x12 x36 x37) x36)(∀ x36 . x36intx14 x36 = x36)x15 = 1(∀ x36 . x36int∀ x37 . x37intx16 x36 x37 = If_i (SNoLe x36 0) x37 (x13 (x16 (add_SNo x36 (minus_SNo 1)) x37) x36))(∀ x36 . x36intx17 x36 = x16 (x14 x36) x15)(∀ x36 . x36intx18 x36 = x17 x36)(∀ x36 . x36int∀ x37 . x37intx19 x36 x37 = add_SNo x36 x37)(∀ x36 . x36intx20 x36 = x36)(∀ x36 . x36intx21 x36 = x36)x22 = 1x23 = 2(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx24 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x19 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38) (x25 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx25 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x20 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36intx26 x36 = x24 (x21 x36) x22 x23)(∀ x36 . x36int∀ x37 . x37intx27 x36 x37 = add_SNo x36 x37)(∀ x36 . x36intx28 x36 = x36)(∀ x36 . x36intx29 x36 = x36)x30 = add_SNo 1 2x31 = 1(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx32 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x27 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38) (x33 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx33 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x28 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38)))(∀ x36 . x36intx34 x36 = x32 (x29 x36) x30 x31)(∀ x36 . x36intx35 x36 = add_SNo (mul_SNo (x26 x36) (x34 x36)) (minus_SNo 2))∀ x36 . x36intSNoLe 0 x36x18 x36 = x35 x36
Conjecture 7a8b0..A5969 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ 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 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38intx0 x38 = mul_SNo x38 x38)x1 = 2(∀ x38 . x38int∀ x39 . x39intx2 x38 x39 = add_SNo x38 x39)(∀ x38 . x38intx3 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx4 x38 x39 = x39)x5 = 1x6 = 0(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx7 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x2 (x7 (add_SNo x38 (minus_SNo 1)) x39 x40) (x8 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx8 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x3 (x7 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx9 x38 x39 = x7 (x4 x38 x39) x5 x6)(∀ x38 . x38int∀ x39 . x39intx10 x38 x39 = x9 x38 x39)(∀ x38 . x38int∀ x39 . x39intx11 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x11 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx12 x38 x39 = x11 x1 (x10 x38 x39))(∀ x38 . x38int∀ x39 . x39intx13 x38 x39 = add_SNo (x12 x38 x39) x38)(∀ x38 . x38intx14 x38 = x38)x15 = 1(∀ x38 . x38int∀ x39 . x39intx16 x38 x39 = If_i (SNoLe x38 0) x39 (x13 (x16 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx17 x38 = x16 (x14 x38) x15)(∀ x38 . x38intx18 x38 = x17 x38)(∀ x38 . x38intx19 x38 = mul_SNo x38 x38)x20 = 2(∀ x38 . x38int∀ x39 . x39intx21 x38 x39 = add_SNo x38 x39)(∀ x38 . x38intx22 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx23 x38 x39 = add_SNo x39 (minus_SNo 1))x24 = 1x25 = 1(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx26 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x21 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40) (x27 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx27 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x22 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx28 x38 x39 = x26 (x23 x38 x39) x24 x25)(∀ x38 . x38int∀ x39 . x39intx29 x38 x39 = x28 x38 x39)(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = If_i (SNoLe x38 0) x39 (x19 (x30 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx31 x38 x39 = x30 x20 (x29 x38 x39))(∀ x38 . x38int∀ x39 . x39intx32 x38 x39 = add_SNo (x31 x38 x39) x38)(∀ x38 . x38intx33 x38 = x38)x34 = 1(∀ x38 . x38int∀ x39 . x39intx35 x38 x39 = If_i (SNoLe x38 0) x39 (x32 (x35 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx36 x38 = x35 (x33 x38) x34)(∀ x38 . x38intx37 x38 = x36 x38)∀ x38 . x38intSNoLe 0 x38x18 x38 = x37 x38
Conjecture 1ee5e..A5968 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ 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 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38intx0 x38 = mul_SNo (mul_SNo x38 x38) x38)x1 = 1(∀ x38 . x38int∀ x39 . x39intx2 x38 x39 = add_SNo x38 x39)(∀ x38 . x38intx3 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx4 x38 x39 = x39)x5 = 0x6 = 1(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx7 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x2 (x7 (add_SNo x38 (minus_SNo 1)) x39 x40) (x8 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx8 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x3 (x7 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx9 x38 x39 = x7 (x4 x38 x39) x5 x6)(∀ x38 . x38int∀ x39 . x39intx10 x38 x39 = x9 x38 x39)(∀ x38 . x38int∀ x39 . x39intx11 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x11 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx12 x38 x39 = x11 x1 (x10 x38 x39))(∀ x38 . x38int∀ x39 . x39intx13 x38 x39 = add_SNo (x12 x38 x39) x38)(∀ x38 . x38intx14 x38 = x38)x15 = 0(∀ x38 . x38int∀ x39 . x39intx16 x38 x39 = If_i (SNoLe x38 0) x39 (x13 (x16 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx17 x38 = x16 (x14 x38) x15)(∀ x38 . x38intx18 x38 = x17 x38)(∀ x38 . x38intx19 x38 = mul_SNo (mul_SNo x38 x38) x38)x20 = 1(∀ x38 . x38int∀ x39 . x39intx21 x38 x39 = add_SNo x38 x39)(∀ x38 . x38intx22 x38 = x38)(∀ x38 . x38int∀ x39 . x39intx23 x38 x39 = add_SNo x39 (minus_SNo 2))x24 = 1x25 = 1(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx26 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x21 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40) (x27 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx27 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x22 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx28 x38 x39 = x26 (x23 x38 x39) x24 x25)(∀ x38 . x38int∀ x39 . x39intx29 x38 x39 = x28 x38 x39)(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = If_i (SNoLe x38 0) x39 (x19 (x30 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx31 x38 x39 = x30 x20 (x29 x38 x39))(∀ x38 . x38int∀ x39 . x39intx32 x38 x39 = add_SNo (x31 x38 x39) x38)(∀ x38 . x38intx33 x38 = x38)x34 = 1(∀ x38 . x38int∀ x39 . x39intx35 x38 x39 = If_i (SNoLe x38 0) x39 (x32 (x35 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx36 x38 = x35 (x33 x38) x34)(∀ x38 . x38intx37 x38 = add_SNo (x36 x38) (minus_SNo 1))∀ x38 . x38intSNoLe 0 x38x18 x38 = x37 x38
Conjecture e02e8..A59673 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12intx0 x12 = add_SNo (add_SNo x12 (minus_SNo 1)) x12)(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = add_SNo x12 x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = add_SNo (x4 x12) (minus_SNo x12))(∀ x12 . x12intx6 x12 = add_SNo x12 x12)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = add_SNo (add_SNo x12 (minus_SNo 1)) x12)(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo 1 (add_SNo (x10 x12) (minus_SNo x12)))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 8c487..A5922 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ 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 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = add_SNo (mul_SNo x28 x29) x28)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = x28)x5 = 2x6 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = If_i (SNoLe x28 0) 1 (x9 x28))(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx16 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx17 x28 = x28)(∀ x28 . x28intx18 x28 = x28)x19 = 2x20 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx21 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x16 (x21 (add_SNo x28 (minus_SNo 1)) x29 x30) (x22 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx22 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x17 (x21 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx23 x28 = x21 (x18 x28) x19 x20)(∀ x28 . x28intx24 x28 = x23 x28)(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x15 x28) (x24 x28))(∀ x28 . x28intx27 x28 = mul_SNo (If_i (SNoLe x28 0) 1 (x26 x28)) (add_SNo 1 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture 48f79..A5921 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = x28)x5 = 2x6 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = If_i (SNoLe x28 0) 1 (x12 x28))(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx15 x28 = x28)(∀ x28 . x28intx16 x28 = x28)x17 = 2x18 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx21 x28 = x19 (x16 x28) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = mul_SNo (If_i (SNoLe x28 0) 1 (x21 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture e3933..A59174 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ 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 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)(∀ x42 . x42int∀ x43 . x43intx0 x42 x43 = add_SNo x42 x43)(∀ x42 . x42int∀ x43 . x43intx1 x42 x43 = add_SNo x43 (minus_SNo 2))(∀ x42 . x42intx2 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx3 x42 x43 = If_i (SNoLe x42 0) x43 (x0 (x3 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx4 x42 x43 = x3 (x1 x42 x43) (x2 x42))(∀ x42 . x42int∀ x43 . x43intx5 x42 x43 = x4 x42 x43)(∀ x42 . x42int∀ x43 . x43intx6 x42 x43 = x43)(∀ x42 . x42intx7 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx8 x42 x43 = If_i (SNoLe x42 0) x43 (x5 (x8 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx9 x42 x43 = x8 (x6 x42 x43) (x7 x42))(∀ x42 . x42int∀ x43 . x43intx10 x42 x43 = add_SNo (x9 x42 x43) x43)(∀ x42 . x42int∀ x43 . x43intx11 x42 x43 = add_SNo x43 (minus_SNo 2))(∀ x42 . x42intx12 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx13 x42 x43 = If_i (SNoLe x42 0) x43 (x10 (x13 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx14 x42 x43 = x13 (x11 x42 x43) (x12 x42))(∀ x42 . x42int∀ x43 . x43intx15 x42 x43 = x14 x42 x43)(∀ x42 . x42intx16 x42 = x42)x17 = 1(∀ x42 . x42int∀ x43 . x43intx18 x42 x43 = If_i (SNoLe x42 0) x43 (x15 (x18 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42intx19 x42 = x18 (x16 x42) x17)(∀ x42 . x42intx20 x42 = add_SNo (mul_SNo (add_SNo (x19 x42) x42) 2) (minus_SNo (If_i (SNoLe x42 0) 1 2)))(∀ x42 . x42int∀ x43 . x43intx21 x42 x43 = add_SNo x42 x43)(∀ x42 . x42int∀ x43 . x43intx22 x42 x43 = x43)(∀ x42 . x42intx23 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx24 x42 x43 = If_i (SNoLe x42 0) x43 (x21 (x24 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx25 x42 x43 = x24 (x22 x42 x43) (x23 x42))(∀ x42 . x42int∀ x43 . x43intx26 x42 x43 = x25 x42 x43)(∀ x42 . x42int∀ x43 . x43intx27 x42 x43 = add_SNo x43 (minus_SNo 2))(∀ x42 . x42intx28 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx29 x42 x43 = If_i (SNoLe x42 0) x43 (x26 (x29 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx30 x42 x43 = x29 (x27 x42 x43) (x28 x42))(∀ x42 . x42int∀ x43 . x43intx31 x42 x43 = add_SNo (x30 x42 x43) x43)(∀ x42 . x42int∀ x43 . x43intx32 x42 x43 = add_SNo x43 (minus_SNo 2))(∀ x42 . x42intx33 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx34 x42 x43 = If_i (SNoLe x42 0) x43 (x31 (x34 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx35 x42 x43 = x34 (x32 x42 x43) (x33 x42))(∀ x42 . x42int∀ x43 . x43intx36 x42 x43 = x35 x42 x43)(∀ x42 . x42intx37 x42 = x42)x38 = 1(∀ x42 . x42int∀ x43 . x43intx39 x42 x43 = If_i (SNoLe x42 0) x43 (x36 (x39 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42intx40 x42 = x39 (x37 x42) x38)(∀ x42 . x42intx41 x42 = add_SNo (mul_SNo (add_SNo (x40 x42) x42) 2) (minus_SNo (If_i (SNoLe x42 0) 1 2)))∀ x42 . x42intSNoLe 0 x42x20 x42 = x41 x42
Conjecture 0aa13..A59142 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15int∀ x16 . x16intx0 x15 x16 = add_SNo x15 x16)(∀ x15 . x15int∀ x16 . x16intx1 x15 x16 = mul_SNo (add_SNo 2 (add_SNo 2 x16)) 2)(∀ x15 . x15intx2 x15 = add_SNo 2 x15)(∀ x15 . x15intx3 x15 = x15)x4 = 1(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx5 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x0 (x5 (add_SNo x15 (minus_SNo 1)) x16 x17) (x6 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx6 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x1 (x5 (add_SNo x15 (minus_SNo 1)) x16 x17) (x6 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx7 x15 = x5 (x2 x15) (x3 x15) x4)(∀ x15 . x15intx8 x15 = x7 x15)(∀ x15 . x15intx9 x15 = add_SNo x15 x15)(∀ x15 . x15intx10 x15 = x15)x11 = add_SNo 1 2(∀ x15 . x15int∀ x16 . x16intx12 x15 x16 = If_i (SNoLe x15 0) x16 (x9 (x12 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx13 x15 = x12 (x10 x15) x11)(∀ x15 . x15intx14 x15 = add_SNo (add_SNo (mul_SNo (mul_SNo (add_SNo (mul_SNo (add_SNo (x13 x15) (minus_SNo 2)) 2) (minus_SNo x15)) 2) (add_SNo 1 2)) (minus_SNo 1)) (minus_SNo x15))∀ x15 . x15intSNoLe 0 x15x8 x15 = x14 x15
Conjecture 6c5aa..A58966 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)(∀ x15 . x15int∀ x16 . x16intx0 x15 x16 = add_SNo (mul_SNo x15 x16) x16)x1 = 2(∀ x15 . x15intx2 x15 = x15)x3 = 1(∀ x15 . x15intx4 x15 = x15)(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx5 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x0 (x5 (add_SNo x15 (minus_SNo 1)) x16 x17) (x6 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx6 x15 x16 x17 = If_i (SNoLe x15 0) x17 x1)(∀ x15 . x15intx7 x15 = x5 (x2 x15) x3 (x4 x15))(∀ x15 . x15intx8 x15 = x7 x15)(∀ x15 . x15intx9 x15 = add_SNo x15 x15)(∀ x15 . x15intx10 x15 = x15)(∀ x15 . x15intx11 x15 = add_SNo 1 (If_i (SNoLe x15 0) 2 x15))(∀ x15 . x15int∀ x16 . x16intx12 x15 x16 = If_i (SNoLe x15 0) x16 (x9 (x12 (add_SNo x15 (minus_SNo 1)) x16)))(∀ x15 . x15intx13 x15 = x12 (x10 x15) (x11 x15))(∀ x15 . x15intx14 x15 = add_SNo (x13 x15) (minus_SNo 2))∀ x15 . x15intSNoLe 0 x15x8 x15 = x14 x15
Conjecture d8e29..A58896 : ∀ 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 = 1(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = add_SNo (add_SNo (x4 x17) (minus_SNo 2)) (minus_SNo 2))(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = add_SNo (add_SNo (x15 x17) (minus_SNo 2)) (minus_SNo 2))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 4e965..A5571 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . 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 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17int∀ x18 . x18intx0 x17 x18 = add_SNo 2 (add_SNo x17 x18))(∀ x17 . x17int∀ x18 . x18intx1 x17 x18 = mul_SNo 2 (add_SNo x18 x18))(∀ x17 . x17intx2 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17int∀ x18 . x18intx4 x17 x18 = x3 (x1 x17 x18) (x2 x17))(∀ x17 . x17int∀ x18 . x18intx5 x17 x18 = x4 x17 x18)(∀ x17 . x17intx6 x17 = add_SNo 1 x17)x7 = 1(∀ x17 . x17int∀ x18 . x18intx8 x17 x18 = If_i (SNoLe x17 0) x18 (x5 (x8 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx9 x17 = x8 (x6 x17) x7)(∀ x17 . x17intx10 x17 = mul_SNo (mul_SNo (add_SNo (x9 x17) x17) 2) 2)(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = add_SNo (mul_SNo (add_SNo (mul_SNo (add_SNo 1 x18) (add_SNo 2 2)) 1) (mul_SNo 2 x18)) x17)(∀ x17 . x17intx12 x17 = add_SNo x17 1)x13 = 1(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x11 (x14 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx15 x17 = x14 (x12 x17) x13)(∀ x17 . x17intx16 x17 = mul_SNo (mul_SNo (add_SNo (x15 x17) x17) 2) 2)∀ x17 . x17intSNoLe 0 x17x10 x17 = x16 x17
Conjecture 8085e..A55580 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12intx0 x12 = add_SNo 2 (add_SNo x12 x12))(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = add_SNo (mul_SNo x12 x12) x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = add_SNo 1 (x4 x12))(∀ x12 . x12intx6 x12 = add_SNo x12 x12)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = add_SNo 2 (add_SNo (mul_SNo x12 x12) x12))(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo (x10 x12) (minus_SNo 1))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture bc191..A554 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17int∀ x18 . x18intx0 x17 x18 = add_SNo (add_SNo x17 x17) x18)(∀ x17 . x17intx1 x17 = x17)(∀ x17 . x17intx2 x17 = x17)(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx4 x17 = x3 (x1 x17) (x2 x17))(∀ x17 . x17intx5 x17 = mul_SNo (add_SNo 1 (add_SNo 2 x17)) (x4 x17))x6 = 1(∀ x17 . x17intx7 x17 = add_SNo 1 x17)(∀ x17 . x17int∀ x18 . x18intx8 x17 x18 = If_i (SNoLe x17 0) x18 (x5 (x8 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx9 x17 = x8 x6 (x7 x17))(∀ x17 . x17intx10 x17 = x9 x17)(∀ x17 . x17intx11 x17 = add_SNo x17 x17)(∀ x17 . x17intx12 x17 = x17)x13 = 2(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x11 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 (x12 x17) x13)(∀ x17 . x17intx16 x17 = mul_SNo (mul_SNo (add_SNo 2 (add_SNo 2 x17)) (add_SNo (x15 x17) (minus_SNo 1))) (add_SNo 1 (add_SNo 2 x17)))∀ x17 . x17intSNoLe 0 x17x10 x17 = x16 x17
Conjecture 5b29f..A5477 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ 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 . x33int∀ x34 . x34intx0 x33 x34 = mul_SNo 2 (add_SNo (mul_SNo x33 x34) x33))(∀ x33 . x33int∀ x34 . x34intx1 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx2 x33 = x33)x3 = 1x4 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx5 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x0 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35) (x6 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx6 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x1 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35) (x6 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33intx7 x33 = x5 (x2 x33) x3 x4)(∀ x33 . x33intx8 x33 = add_SNo 1 (add_SNo x33 x33))(∀ x33 . x33intx9 x33 = x33)x10 = 1(∀ x33 . x33int∀ x34 . x34intx11 x33 x34 = If_i (SNoLe x33 0) x34 (x8 (x11 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx12 x33 = x11 (x9 x33) x10)(∀ x33 . x33intx13 x33 = mul_SNo (x7 x33) (x12 x33))(∀ x33 . x33intx14 x33 = mul_SNo (add_SNo (add_SNo x33 (minus_SNo 1)) x33) x33)x15 = 1(∀ x33 . x33intx16 x33 = add_SNo x33 x33)(∀ x33 . x33intx17 x33 = x33)x18 = 1(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = If_i (SNoLe x33 0) x34 (x16 (x19 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx20 x33 = x19 (x17 x33) x18)(∀ x33 . x33intx21 x33 = x20 x33)(∀ x33 . x33int∀ x34 . x34intx22 x33 x34 = If_i (SNoLe x33 0) x34 (x14 (x22 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx23 x33 = x22 x15 (x21 x33))(∀ x33 . x33int∀ x34 . x34intx24 x33 x34 = mul_SNo (add_SNo 1 x34) x33)(∀ x33 . x33int∀ x34 . x34intx25 x33 x34 = add_SNo x34 x34)(∀ x33 . x33intx26 x33 = x33)x27 = 1x28 = 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 x33x13 x33 = x32 x33
Conjecture 8490d..A54605 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)(∀ x7 . x7int∀ x8 . x8intx0 x7 x8 = add_SNo x7 x8)(∀ x7 . x7intx1 x7 = mul_SNo x7 (mul_SNo x7 x7))(∀ x7 . x7intx2 x7 = add_SNo (mul_SNo x7 x7) x7)(∀ x7 . x7int∀ x8 . x8intx3 x7 x8 = If_i (SNoLe x7 0) x8 (x0 (x3 (add_SNo x7 (minus_SNo 1)) x8) x7))(∀ x7 . x7intx4 x7 = x3 (x1 x7) (x2 x7))(∀ x7 . x7intx5 x7 = mul_SNo 2 (x4 x7))(∀ x7 . x7intx6 x7 = mul_SNo (add_SNo 2 (mul_SNo (add_SNo 2 (add_SNo (mul_SNo (mul_SNo (mul_SNo x7 x7) x7) x7) x7)) x7)) x7)∀ x7 . x7intSNoLe 0 x7x5 x7 = x6 x7
Conjecture e9531..A54603 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)(∀ x7 . x7int∀ x8 . x8intx0 x7 x8 = add_SNo x7 x8)(∀ x7 . x7intx1 x7 = mul_SNo x7 x7)(∀ x7 . x7intx2 x7 = x7)(∀ x7 . x7int∀ x8 . x8intx3 x7 x8 = If_i (SNoLe x7 0) x8 (x0 (x3 (add_SNo x7 (minus_SNo 1)) x8) x7))(∀ x7 . x7intx4 x7 = x3 (x1 x7) (x2 x7))(∀ x7 . x7intx5 x7 = mul_SNo 2 (x4 x7))(∀ x7 . x7intx6 x7 = mul_SNo (add_SNo 2 (add_SNo (mul_SNo (mul_SNo x7 x7) x7) x7)) x7)∀ x7 . x7intSNoLe 0 x7x5 x7 = x6 x7
Conjecture 9fda3..A5443 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = x28)x5 = 0x6 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx15 x28 = add_SNo x28 (minus_SNo 1))x16 = 1(∀ x28 . x28int∀ x29 . x29intx17 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x17 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx18 x28 = x17 (x15 x28) x16)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx20 x28 = x28)(∀ x28 . x28intx21 x28 = add_SNo x28 (minus_SNo 2))(∀ x28 . x28intx22 x28 = x28)(∀ x28 . x28intx23 x28 = x28)(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) (x22 x28) (x23 x28))(∀ x28 . x28intx27 x28 = mul_SNo (x18 x28) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture bdf1d..A5442 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 . x5int∀ x6 . x6int∀ x7 : ι → ι → ι → ι . (∀ x8 . x8int∀ x9 . x9int∀ x10 . x10intx7 x8 x9 x10int)∀ x8 : ι → ι → ι → ι . (∀ x9 . x9int∀ x10 . x10int∀ x11 . x11intx8 x9 x10 x11int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx1 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx3 x28 = x28)(∀ x28 . x28intx4 x28 = x28)x5 = 1x6 = 0(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx7 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x2 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30) (x8 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx8 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x3 (x7 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx9 x28 = x7 (x4 x28) x5 x6)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x1 x28) (x10 x28))(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28intx15 x28 = x28)x16 = 1(∀ x28 . x28int∀ x29 . x29intx17 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x17 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx18 x28 = x17 (x15 x28) x16)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = add_SNo x28 x29)(∀ x28 . x28intx20 x28 = x28)(∀ x28 . x28intx21 x28 = add_SNo x28 (minus_SNo 1))x22 = 1x23 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (x18 x28) (x26 x28))∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture c99a7..A53539 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . 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 (add_SNo 1 2) (add_SNo x17 (minus_SNo 1)))(∀ x17 . x17intx2 x17 = x17)(∀ 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))(∀ x17 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = add_SNo x17 (minus_SNo 1))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 (x15 x17) x17)∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17