Search for blocks/addresses/...

Proofgold Address

address
PUTEjdnY5D1n9eweXtCXczymMSRBsdjbpJH
total
0
mg
-
conjpub
-
current assets
4b8a7../62463.. bday: 25624 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 91e03..A99953 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = add_SNo (mul_SNo 2 (mul_SNo x20 x21)) (minus_SNo x20))(∀ x20 . x20int∀ x21 . x21intx1 x20 x21 = x21)x2 = 1(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20int∀ x21 . x21intx4 x20 x21 = x3 (x1 x20 x21) x2)(∀ x20 . x20int∀ x21 . x21intx5 x20 x21 = add_SNo (x4 x20 x21) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 0(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (mul_SNo x20 x21))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo x21 (minus_SNo 2))(∀ x20 . x20intx13 x20 = x20)x14 = 0(∀ x20 . x20intx15 x20 = add_SNo 1 (add_SNo x20 x20))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 (x15 x20))(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture a6876..A9992 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . 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 . 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 . x31intx0 x30 x31 = mul_SNo x30 x31)x1 = add_SNo 2 2(∀ x30 . x30intx2 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx4 x30 = x3 x1 (x2 x30))(∀ x30 . x30intx5 x30 = mul_SNo 2 (x4 x30))(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = x9 x30)(∀ x30 . x30intx11 x30 = mul_SNo x30 x30)x12 = 2(∀ x30 . x30intx13 x30 = add_SNo x30 x30)(∀ x30 . x30intx14 x30 = x30)x15 = 1(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = If_i (SNoLe x30 0) x31 (x13 (x16 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx17 x30 = x16 (x14 x30) x15)(∀ x30 . x30intx18 x30 = x17 x30)(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x11 (x19 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx20 x30 = x19 x12 (x18 x30))(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = add_SNo 1 2(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx28 x30 = x26 (x23 x30) x24 x25)(∀ x30 . x30intx29 x30 = mul_SNo (x20 x30) (x28 x30))∀ x30 . x30intSNoLe 0 x30x10 x30 = x29 x30
Conjecture 8a4bc..A99924 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ 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 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ 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 1 (add_SNo 2 x19))(∀ x18 . x18int∀ x19 . x19intx1 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx2 x18 = x18)(∀ x18 . x18intx3 x18 = add_SNo (add_SNo (add_SNo x18 x18) 2) 2)(∀ x18 . x18intx4 x18 = x18)(∀ 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) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) (x3 x18) (x4 x18))(∀ x18 . x18intx8 x18 = x7 x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo 1 x19)(∀ x18 . x18int∀ x19 . x19intx10 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx11 x18 = x18)(∀ x18 . x18intx12 x18 = add_SNo 2 (add_SNo (add_SNo 2 x18) x18))(∀ x18 . x18intx13 x18 = add_SNo 2 x18)(∀ 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) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) (x12 x18) (x13 x18))(∀ x18 . x18intx17 x18 = x16 x18)∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture febc4..A9991 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo x20 x21)x1 = add_SNo 2 2(∀ x20 . x20intx2 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 x1 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo (mul_SNo 2 (x4 x20)) (minus_SNo x20))(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))))) (minus_SNo 1)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 43213..A9990 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ 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 . x26intx0 x25 x26 = mul_SNo x25 x26)x1 = add_SNo 2 2(∀ x25 . x25intx2 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx4 x25 = x3 x1 (x2 x25))(∀ x25 . x25intx5 x25 = mul_SNo 2 (add_SNo (x4 x25) (minus_SNo x25)))(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)x13 = 1(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 (x12 x25) x13)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))) (minus_SNo 1)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture ed422..A9989 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = mul_SNo (add_SNo 2 (add_SNo 2 x28)) x28)x1 = 2x2 = 1(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28intx5 x28 = mul_SNo x4 x28)(∀ x28 . x28intx6 x28 = x28)x7 = 1(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = If_i (SNoLe x28 0) x29 (x5 (x8 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx9 x28 = x8 (x6 x28) x7)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = x29)(∀ x28 . x28intx13 x28 = x28)x14 = 1x15 = add_SNo 1 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx18 x28 = x16 (x13 x28) x14 x15)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = x29)(∀ x28 . x28intx21 x28 = x28)x22 = 1x23 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) (minus_SNo 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) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (x18 x28) (x26 x28))∀ x28 . x28intSNoLe 0 x28x10 x28 = x27 x28
Conjecture 66e16..A9988 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . 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 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30intx0 x30 = add_SNo (mul_SNo x30 x30) x30)x1 = 2x2 = 2(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31)))x4 = x3 x1 x2(∀ x30 . x30intx5 x30 = mul_SNo (add_SNo 2 x4) x30)(∀ x30 . x30intx6 x30 = x30)x7 = 1(∀ x30 . x30int∀ x31 . x31intx8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx9 x30 = x8 (x6 x30) x7)(∀ x30 . x30intx10 x30 = x9 x30)(∀ x30 . x30intx11 x30 = mul_SNo x30 x30)x12 = 1(∀ x30 . x30intx13 x30 = add_SNo x30 x30)(∀ x30 . x30intx14 x30 = x30)x15 = 1(∀ x30 . x30int∀ x31 . x31intx16 x30 x31 = If_i (SNoLe x30 0) x31 (x13 (x16 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx17 x30 = x16 (x14 x30) x15)(∀ x30 . x30intx18 x30 = x17 x30)(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x11 (x19 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx20 x30 = x19 x12 (x18 x30))(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx28 x30 = x26 (x23 x30) x24 x25)(∀ x30 . x30intx29 x30 = mul_SNo (x20 x30) (x28 x30))∀ x30 . x30intSNoLe 0 x30x10 x30 = x29 x30
Conjecture a7651..A9987 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo (mul_SNo x25 x25) x25)x1 = 2x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = add_SNo (mul_SNo x4 x25) x25)(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = add_SNo (mul_SNo x25 x25) x25)x16 = 1x17 = add_SNo 2 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26intx18 x25 x26 = If_i (SNoLe x25 0) x26 (x15 (x18 (add_SNo x25 (minus_SNo 1)) x26)))x19 = x18 x16 x17x20 = add_SNo 1 x19(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x13 x25) x14 x20)(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 6e940..A9986 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ 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 . x25intx0 x25 = add_SNo (mul_SNo x25 x25) x25)x1 = 2x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = mul_SNo x4 x25)(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)x13 = 1(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 (x12 x25) x13)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 65ccd..A9985 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = add_SNo (mul_SNo x20 x20) x20)x1 = 2x2 = 2(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))x4 = x3 x1 x2(∀ x20 . x20intx5 x20 = add_SNo (mul_SNo x4 x20) (minus_SNo x20))(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture e6d61..A9984 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ 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 . x25intx0 x25 = mul_SNo 2 (add_SNo 2 x25))x1 = 2x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = mul_SNo 2 (mul_SNo x4 x25))(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)x13 = 1(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 (x12 x25) x13)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture bb459..A9983 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = add_SNo 2 (mul_SNo x28 x28))x1 = 2x2 = 2(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))x4 = x3 x1 x2(∀ x28 . x28intx5 x28 = add_SNo (mul_SNo x4 x28) x28)(∀ x28 . x28intx6 x28 = x28)x7 = 1(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = If_i (SNoLe x28 0) x29 (x5 (x8 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx9 x28 = x8 (x6 x28) x7)(∀ x28 . x28intx10 x28 = x9 x28)(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = x29)(∀ x28 . x28intx13 x28 = x28)x14 = 1x15 = add_SNo 1 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx18 x28 = x16 (x13 x28) x14 x15)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = x29)(∀ x28 . x28intx21 x28 = x28)x22 = 1x23 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (x18 x28) (x26 x28))∀ x28 . x28intSNoLe 0 x28x10 x28 = x27 x28
Conjecture dcaf0..A9982 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ 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 . x25intx0 x25 = add_SNo 2 (mul_SNo x25 x25))x1 = 2x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = mul_SNo x4 x25)(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)x13 = 1(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 (x12 x25) x13)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 49fec..A9981 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))x1 = 2(∀ x25 . x25intx2 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx4 x25 = x3 x1 (x2 x25))(∀ x25 . x25intx5 x25 = add_SNo (x4 x25) x25)(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = mul_SNo x25 x25)x16 = 1x17 = add_SNo 2 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26intx18 x25 x26 = If_i (SNoLe x25 0) x26 (x15 (x18 (add_SNo x25 (minus_SNo 1)) x26)))x19 = x18 x16 x17x20 = add_SNo 1 x19(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x13 x25) x14 x20)(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture d2273..A9980 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 . x12int∀ x13 : ι → ι → ι → ι . (∀ x14 . x14int∀ x15 . x15int∀ x16 . x16intx13 x14 x15 x16int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = mul_SNo 2 (add_SNo (add_SNo x20 x20) x20))(∀ x20 . x20intx1 x20 = add_SNo x20 x20)x2 = 1(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx4 x20 = x3 (x1 x20) x2)(∀ x20 . x20intx5 x20 = x4 x20)(∀ x20 . x20intx6 x20 = mul_SNo x20 x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx9 x20 x21 = x21)(∀ x20 . x20intx10 x20 = x20)x11 = 1x12 = add_SNo 2 (add_SNo 2 2)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx15 x20 = x13 (x10 x20) x11 x12)(∀ x20 . x20intx16 x20 = x15 x20)(∀ x20 . x20int∀ x21 . x21intx17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx18 x20 = x17 x7 (x16 x20))(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x5 x20 = x19 x20
Conjecture d7f09..A9979 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))x1 = 2(∀ x25 . x25intx2 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx4 x25 = x3 x1 (x2 x25))(∀ x25 . x25intx5 x25 = add_SNo (x4 x25) (minus_SNo x25))(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = mul_SNo x25 x25)x16 = 1x17 = add_SNo 2 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26intx18 x25 x26 = If_i (SNoLe x25 0) x26 (x15 (x18 (add_SNo x25 (minus_SNo 1)) x26)))x19 = x18 x16 x17x20 = add_SNo x19 (minus_SNo 1)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x13 x25) x14 x20)(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 917b1..A9978 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = mul_SNo x20 x20)x1 = 2x2 = 2(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))x4 = x3 x1 x2(∀ x20 . x20intx5 x20 = mul_SNo 2 (add_SNo (mul_SNo x4 x20) x20))(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 2 (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 55bed..A9977 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = mul_SNo x20 x20)x1 = 2x2 = 2(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))x4 = x3 x1 x2(∀ x20 . x20intx5 x20 = add_SNo (mul_SNo 2 (mul_SNo x4 x20)) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = x18 x20)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 4a984..A9976 : ∀ 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 (mul_SNo 2 (add_SNo x17 x17)) x17)x2 = 1(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = x4 x17)(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo (mul_SNo (mul_SNo x17 x17) x17) x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = x15 x17)∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture f891a..A9975 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo (add_SNo 2 (add_SNo 2 x21)) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 x1 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo (x4 x20) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = add_SNo x20 (minus_SNo 1))x14 = 1x15 = add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) (minus_SNo 1)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = mul_SNo (x18 x20) (If_i (SNoLe x20 0) 1 (add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) (minus_SNo 1))))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20

previous assets