Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPFB../94c73..
PUS88../ee05d..
vout
PrPFB../498d4.. 0.03 bars
PUQci../e9980.. doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Param mul_SNomul_SNo : ιιι
Conjecture cc0f4..A289255 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . 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 . x17int∀ x18 . x18intx0 x17 x18 = add_SNo (add_SNo x17 x17) x18)(∀ x17 . x17intx1 x17 = add_SNo x17 x17)x2 = 2(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18) x17))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = add_SNo (x4 x17) (minus_SNo 1))(∀ x17 . x17intx6 x17 = mul_SNo x17 x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 2(∀ 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 1 (add_SNo (x15 x17) (minus_SNo (mul_SNo 2 (add_SNo 2 x17)))))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture c259c..A288516 : ∀ 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 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)(∀ x27 . x27int∀ x28 . x28intx0 x27 x28 = add_SNo x27 x28)(∀ x27 . x27int∀ x28 . x28intx1 x27 x28 = x28)(∀ x27 . x27intx2 x27 = x27)(∀ x27 . x27int∀ x28 . x28intx3 x27 x28 = If_i (SNoLe x27 0) x28 (x0 (x3 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx4 x27 x28 = x3 (x1 x27 x28) (x2 x27))(∀ x27 . x27int∀ x28 . x28intx5 x27 x28 = x4 x27 x28)(∀ x27 . x27int∀ x28 . x28intx6 x27 x28 = add_SNo 1 x28)(∀ x27 . x27intx7 x27 = x27)(∀ x27 . x27int∀ x28 . x28intx8 x27 x28 = If_i (SNoLe x27 0) x28 (x5 (x8 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx9 x27 x28 = x8 (x6 x27 x28) (x7 x27))(∀ x27 . x27int∀ x28 . x28intx10 x27 x28 = add_SNo (add_SNo (x9 x27 x28) x27) x28)(∀ x27 . x27intx11 x27 = x27)x12 = 1(∀ x27 . x27int∀ x28 . x28intx13 x27 x28 = If_i (SNoLe x27 0) x28 (x10 (x13 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx14 x27 = x13 (x11 x27) x12)(∀ x27 . x27intx15 x27 = add_SNo (add_SNo (mul_SNo (x14 x27) 2) (minus_SNo 1)) (minus_SNo x27))(∀ x27 . x27int∀ x28 . x28intx16 x27 x28 = add_SNo (add_SNo (mul_SNo x28 x28) x27) x28)(∀ x27 . x27int∀ x28 . x28intx17 x27 x28 = add_SNo 1 x28)(∀ x27 . x27intx18 x27 = add_SNo 1 x27)(∀ x27 . x27int∀ x28 . x28intx19 x27 x28 = If_i (SNoLe x27 0) x28 (x16 (x19 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27int∀ x28 . x28intx20 x27 x28 = x19 (x17 x27 x28) (x18 x27))(∀ x27 . x27int∀ x28 . x28intx21 x27 x28 = add_SNo (add_SNo (add_SNo (x20 x27 x28) x27) x28) x28)(∀ x27 . x27intx22 x27 = x27)x23 = 1(∀ x27 . x27int∀ x28 . x28intx24 x27 x28 = If_i (SNoLe x27 0) x28 (x21 (x24 (add_SNo x27 (minus_SNo 1)) x28) x27))(∀ x27 . x27intx25 x27 = x24 (x22 x27) x23)(∀ x27 . x27intx26 x27 = add_SNo (x25 x27) (minus_SNo x27))∀ x27 . x27intSNoLe 0 x27x15 x27 = x26 x27
Conjecture f3c9b..A287335 : ∀ 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 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo (add_SNo (mul_SNo x13 x13) x12) x13)(∀ x12 . x12intx1 x12 = add_SNo 1 (add_SNo (add_SNo x12 x12) x12))(∀ x12 . x12intx2 x12 = x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = x4 x12)(∀ x12 . x12intx6 x12 = mul_SNo x12 x12)x7 = 1(∀ x12 . x12intx8 x12 = mul_SNo (add_SNo 1 2) (add_SNo 1 x12))(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 x7 (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo 2 (add_SNo (mul_SNo (add_SNo 2 (x10 x12)) x12) x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 21833..A2866 : ∀ 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 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ 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 . x21int∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25int∀ x26 . x26intx0 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx1 x25 x26 = x26)(∀ 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 . x25int∀ x26 . x26intx4 x25 x26 = x3 (x1 x25 x26) (x2 x25))(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = x4 x25 x26)x6 = 2(∀ x25 . x25intx7 x25 = x25)x8 = 1(∀ x25 . x25intx9 x25 = x25)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx10 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x5 (x10 (add_SNo x25 (minus_SNo 1)) x26 x27) (x11 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx11 x25 x26 x27 = If_i (SNoLe x25 0) x27 x6)(∀ x25 . x25intx12 x25 = x10 (x7 x25) x8 (x9 x25))(∀ x25 . x25intx13 x25 = x12 x25)(∀ x25 . x25intx14 x25 = add_SNo x25 x25)(∀ x25 . x25intx15 x25 = add_SNo x25 (minus_SNo 1))x16 = 1(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = If_i (SNoLe x25 0) x26 (x14 (x17 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx18 x25 = x17 (x15 x25) x16)(∀ x25 . x25int∀ x26 . x26intx19 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25intx20 x25 = x25)x21 = 1(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx23 x25 = x22 (x20 x25) x21)(∀ x25 . x25intx24 x25 = mul_SNo (x18 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x13 x25 = x24 x25
Conjecture de8b3..A286286 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ 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 . x15intx14 x15int)(∀ x15 . x15int∀ x16 . x16intx0 x15 x16 = add_SNo 1 (add_SNo (mul_SNo 2 (mul_SNo x15 x16)) (minus_SNo x15)))(∀ x15 . x15intx1 x15 = x15)x2 = 0(∀ x15 . x15int∀ x16 . x16intx3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16) x15))(∀ x15 . x15intx4 x15 = x3 (x1 x15) x2)(∀ x15 . x15intx5 x15 = x4 x15)(∀ x15 . x15int∀ x16 . x16intx6 x15 x16 = add_SNo 1 (mul_SNo x15 x16))(∀ x15 . x15int∀ x16 . x16intx7 x15 x16 = add_SNo 2 x16)(∀ x15 . x15intx8 x15 = add_SNo x15 (minus_SNo 1))(∀ x15 . x15intx9 x15 = If_i (SNoLe x15 0) 0 1)x10 = add_SNo 1 2(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17)))(∀ x15 . x15intx13 x15 = x11 (x8 x15) (x9 x15) x10)(∀ x15 . x15intx14 x15 = x13 x15)∀ x15 . x15intSNoLe 0 x15x5 x15 = x14 x15
Conjecture 1d3e2..A284434 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ 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 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22int∀ x23 . x23intx1 x22 x23 = add_SNo 1 (add_SNo x23 (minus_SNo x22)))(∀ x22 . x22intx2 x22 = x22)x3 = 0(∀ x22 . x22int∀ x23 . x23intx4 x22 x23 = If_i (SNoLe x22 0) x23 (x1 (x4 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx5 x22 = x4 (x2 x22) x3)(∀ x22 . x22intx6 x22 = x5 x22)x7 = 1(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx9 x22 = x8 (x6 x22) x7)(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22int∀ x23 . x23intx11 x22 x23 = add_SNo (mul_SNo x22 x23) x22)(∀ x22 . x22int∀ x23 . x23intx12 x22 x23 = add_SNo x23 (minus_SNo x22))(∀ x22 . x22intx13 x22 = x22)x14 = 1(∀ x22 . x22int∀ x23 . x23intx15 x22 x23 = If_i (SNoLe x22 0) x23 (x12 (x15 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx16 x22 = x15 (x13 x22) x14)(∀ x22 . x22intx17 x22 = add_SNo x22 (minus_SNo (x16 x22)))x18 = 1(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx20 x22 = x19 (x17 x22) x18)(∀ x22 . x22intx21 x22 = x20 x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 1ebfe..A28403 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22intx2 x22 = add_SNo x22 x22)(∀ x22 . x22intx3 x22 = x22)x4 = 2(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = add_SNo 2 (x6 x22))(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22intx11 x22 = add_SNo (mul_SNo x22 x22) x22)x12 = 1(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 1(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = x17 x22)(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 x12 (x18 x22))(∀ x22 . x22intx21 x22 = mul_SNo 2 (x20 x22))∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 6d22c..A282901 : ∀ 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 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo x18 x19)(∀ x18 . x18int∀ x19 . x19intx1 x18 x19 = add_SNo (add_SNo (add_SNo x18 x19) x19) x19)(∀ x18 . x18intx2 x18 = x18)(∀ x18 . x18intx3 x18 = If_i (SNoLe x18 0) 1 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 = mul_SNo 2 (add_SNo (add_SNo x18 (minus_SNo x19)) x18))(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = add_SNo x18 (minus_SNo 1))(∀ x18 . x18intx12 x18 = add_SNo 2 x18)x13 = 2(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) (x12 x18) x13)(∀ x18 . x18intx17 x18 = If_i (SNoLe x18 0) 1 (x16 x18))∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 44d88..A28224 : ∀ 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 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)∀ x48 . x48int∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 . x54int∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι . (∀ x57 . x57intx56 x57int)∀ x57 : ι → ι . (∀ x58 . x58intx57 x58int)∀ x58 . x58int∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι → ι . (∀ x61 . x61int∀ x62 . x62intx60 x61 x62int)∀ x61 : ι → ι → ι . (∀ x62 . x62int∀ x63 . x63intx61 x62 x63int)∀ x62 : ι → ι → ι . (∀ x63 . x63int∀ x64 . x64intx62 x63 x64int)∀ x63 : ι → ι . (∀ x64 . x64intx63 x64int)∀ x64 . x64int∀ x65 : ι → ι → ι . (∀ x66 . x66int∀ x67 . x67intx65 x66 x67int)∀ x66 : ι → ι . (∀ x67 . x67intx66 x67int)∀ x67 : ι → ι . (∀ x68 . x68intx67 x68int)(∀ x68 . x68int∀ x69 . x69intx0 x68 x69 = mul_SNo (add_SNo 2 x69) x68)x1 = 2(∀ x68 . x68intx2 x68 = x68)(∀ x68 . x68int∀ x69 . x69intx3 x68 x69 = If_i (SNoLe x68 0) x69 (x0 (x3 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68intx4 x68 = x3 x1 (x2 x68))(∀ x68 . x68int∀ x69 . x69intx5 x68 x69 = add_SNo (add_SNo (x4 x68) (minus_SNo x68)) (mul_SNo (mul_SNo x69 x69) x69))(∀ x68 . x68int∀ x69 . x69intx6 x68 x69 = add_SNo x69 x69)(∀ x68 . x68int∀ x69 . x69intx7 x68 x69 = x69)x8 = 1x9 = 2(∀ x68 . x68int∀ x69 . x69int∀ x70 . x70intx10 x68 x69 x70 = If_i (SNoLe x68 0) x69 (x5 (x10 (add_SNo x68 (minus_SNo 1)) x69 x70) (x11 (add_SNo x68 (minus_SNo 1)) x69 x70)))(∀ x68 . x68int∀ x69 . x69int∀ x70 . x70intx11 x68 x69 x70 = If_i (SNoLe x68 0) x70 (x6 (x10 (add_SNo x68 (minus_SNo 1)) x69 x70) (x11 (add_SNo x68 (minus_SNo 1)) x69 x70)))(∀ x68 . x68int∀ x69 . x69intx12 x68 x69 = x10 (x7 x68 x69) x8 x9)(∀ x68 . x68int∀ x69 . x69intx13 x68 x69 = mul_SNo (add_SNo 2 x69) x68)x14 = 2(∀ x68 . x68intx15 x68 = x68)(∀ x68 . x68int∀ x69 . x69intx16 x68 x69 = If_i (SNoLe x68 0) x69 (x13 (x16 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68intx17 x68 = x16 x14 (x15 x68))(∀ x68 . x68int∀ x69 . x69intx18 x68 x69 = add_SNo (x12 x68 x69) (x17 x68))(∀ x68 . x68int∀ x69 . x69intx19 x68 x69 = x69)x20 = 1(∀ x68 . x68int∀ x69 . x69intx21 x68 x69 = If_i (SNoLe x68 0) x69 (x18 (x21 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68int∀ x69 . x69intx22 x68 x69 = x21 (x19 x68 x69) x20)(∀ x68 . x68int∀ x69 . x69intx23 x68 x69 = add_SNo (add_SNo (x22 x68 x69) (mul_SNo 2 (add_SNo (add_SNo x68 x68) x68))) x68)(∀ x68 . x68intx24 x68 = x68)x25 = 1(∀ x68 . x68int∀ x69 . x69intx26 x68 x69 = If_i (SNoLe x68 0) x69 (x23 (x26 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68intx27 x68 = x26 (x24 x68) x25)(∀ x68 . x68intx28 x68 = x27 x68)(∀ x68 . x68int∀ x69 . x69intx29 x68 x69 = add_SNo (add_SNo (add_SNo x68 x68) x68) x69)(∀ x68 . x68int∀ x69 . x69intx30 x68 x69 = add_SNo x69 x69)(∀ x68 . x68intx31 x68 = x68)x32 = 1x33 = 2(∀ x68 . x68int∀ x69 . x69int∀ x70 . x70intx34 x68 x69 x70 = If_i (SNoLe x68 0) x69 (x29 (x34 (add_SNo x68 (minus_SNo 1)) x69 x70) (x35 (add_SNo x68 (minus_SNo 1)) x69 x70)))(∀ x68 . x68int∀ x69 . x69int∀ x70 . x70intx35 x68 x69 x70 = If_i (SNoLe x68 0) x70 (x30 (x34 (add_SNo x68 (minus_SNo 1)) x69 x70) (x35 (add_SNo x68 (minus_SNo 1)) x69 x70)))(∀ x68 . x68intx36 x68 = x34 (x31 x68) x32 x33)(∀ x68 . x68intx37 x68 = mul_SNo x68 x68)x38 = 1(∀ x68 . x68intx39 x68 = add_SNo x68 x68)(∀ x68 . x68intx40 x68 = x68)x41 = 1(∀ x68 . x68int∀ x69 . x69intx42 x68 x69 = If_i (SNoLe x68 0) x69 (x39 (x42 (add_SNo x68 (minus_SNo 1)) x69)))(∀ x68 . x68intx43 x68 = x42 (x40 x68) x41)(∀ x68 . x68intx44 x68 = x43 x68)(∀ x68 . x68int∀ x69 . x69intx45 x68 x69 = If_i (SNoLe x68 0) x69 (x37 (x45 (add_SNo x68 (minus_SNo 1)) x69)))(∀ x68 . x68intx46 x68 = x45 x38 (x44 x68))(∀ x68 . x68intx47 x68 = mul_SNo (x36 x68) (x46 x68))x48 = 1(∀ x68 . x68int∀ x69 . x69intx49 x68 x69 = x69)(∀ x68 . x68int∀ x69 . x69intx50 x68 x69 = If_i (SNoLe x68 0) x69 (x47 (x50 (add_SNo x68 (minus_SNo 1)) x69)))(∀ x68 . x68int∀ x69 . x69intx51 x68 x69 = x50 x48 (x49 x68 x69))(∀ x68 . x68int∀ x69 . x69intx52 x68 x69 = add_SNo (add_SNo (x51 x68 x69) (mul_SNo 2 (add_SNo (add_SNo x68 x68) x68))) x68)(∀ x68 . x68intx53 x68 = x68)x54 = 1(∀ x68 . x68int∀ x69 . x69intx55 x68 x69 = If_i (SNoLe x68 0) x69 (x52 (x55 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68intx56 x68 = x55 (x53 x68) x54)(∀ x68 . x68intx57 x68 = x56 x68)x58 = 1(∀ x68 . x68int∀ x69 . x69intx59 x68 x69 = x69)(∀ x68 . x68int∀ x69 . x69intx60 x68 x69 = If_i (SNoLe x68 0) x69 (x57 (x60 (add_SNo x68 (minus_SNo 1)) x69)))(∀ x68 . x68int∀ x69 . x69intx61 x68 x69 = x60 x58 (x59 x68 x69))(∀ x68 . x68int∀ x69 . x69intx62 x68 x69 = add_SNo (add_SNo (x61 x68 x69) (mul_SNo (add_SNo (mul_SNo (add_SNo x68 x68) 2) x68) 2)) x68)(∀ x68 . x68intx63 x68 = x68)x64 = 1(∀ x68 . x68int∀ x69 . x69intx65 x68 x69 = If_i (SNoLe x68 0) x69 (x62 (x65 (add_SNo x68 (minus_SNo 1)) x69) x68))(∀ x68 . x68intx66 x68 = x65 (x63 x68) x64)(∀ x68 . x68intx67 x68 = x66 x68)∀ x68 . x68intSNoLe 0 x68x28 x68 = x67 x68
Conjecture dda7d..A28221 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 . x51int∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 . x55int∀ x56 : ι → ι → ι . (∀ x57 . x57int∀ x58 . x58intx56 x57 x58int)∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι → ι . (∀ x59 . x59int∀ x60 . x60intx58 x59 x60int)∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι . (∀ x61 . x61intx60 x61int)∀ x61 . x61int∀ x62 : ι → ι → ι . (∀ x63 . x63int∀ x64 . x64intx62 x63 x64int)∀ x63 : ι → ι . (∀ x64 . x64intx63 x64int)∀ x64 : ι → ι . (∀ x65 . x65intx64 x65int)(∀ x65 . x65intx0 x65 = add_SNo (add_SNo x65 x65) x65)(∀ x65 . x65int∀ x66 . x66intx1 x65 x66 = add_SNo x66 x66)x2 = 1(∀ x65 . x65int∀ x66 . x66intx3 x65 x66 = If_i (SNoLe x65 0) x66 (x0 (x3 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx4 x65 x66 = x3 (x1 x65 x66) x2)(∀ x65 . x65int∀ x66 . x66intx5 x65 x66 = add_SNo (x4 x65 x66) (mul_SNo 2 (mul_SNo 2 (add_SNo x65 x65))))(∀ x65 . x65int∀ x66 . x66intx6 x65 x66 = x66)x7 = 1(∀ x65 . x65int∀ x66 . x66intx8 x65 x66 = If_i (SNoLe x65 0) x66 (x5 (x8 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65int∀ x66 . x66intx9 x65 x66 = x8 (x6 x65 x66) x7)(∀ x65 . x65int∀ x66 . x66intx10 x65 x66 = mul_SNo (add_SNo 2 x66) x65)x11 = 2(∀ x65 . x65intx12 x65 = x65)(∀ x65 . x65int∀ x66 . x66intx13 x65 x66 = If_i (SNoLe x65 0) x66 (x10 (x13 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx14 x65 = x13 x11 (x12 x65))(∀ x65 . x65int∀ x66 . x66intx15 x65 x66 = add_SNo (x9 x65 x66) (x14 x65))(∀ x65 . x65int∀ x66 . x66intx16 x65 x66 = x66)x17 = 1(∀ x65 . x65int∀ x66 . x66intx18 x65 x66 = If_i (SNoLe x65 0) x66 (x15 (x18 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65int∀ x66 . x66intx19 x65 x66 = x18 (x16 x65 x66) x17)(∀ x65 . x65int∀ x66 . x66intx20 x65 x66 = add_SNo (add_SNo (x19 x65 x66) (mul_SNo 2 (add_SNo (add_SNo x65 x65) x65))) x65)(∀ x65 . x65intx21 x65 = x65)x22 = 1(∀ x65 . x65int∀ x66 . x66intx23 x65 x66 = If_i (SNoLe x65 0) x66 (x20 (x23 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx24 x65 = x23 (x21 x65) x22)(∀ x65 . x65intx25 x65 = x24 x65)(∀ x65 . x65int∀ x66 . x66intx26 x65 x66 = add_SNo (add_SNo (add_SNo x65 x65) x65) x66)(∀ x65 . x65int∀ x66 . x66intx27 x65 x66 = add_SNo x66 x66)(∀ x65 . x65intx28 x65 = x65)x29 = 1x30 = 2(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx31 x65 x66 x67 = If_i (SNoLe x65 0) x66 (x26 (x31 (add_SNo x65 (minus_SNo 1)) x66 x67) (x32 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx32 x65 x66 x67 = If_i (SNoLe x65 0) x67 (x27 (x31 (add_SNo x65 (minus_SNo 1)) x66 x67) (x32 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65intx33 x65 = x31 (x28 x65) x29 x30)(∀ x65 . x65intx34 x65 = mul_SNo x65 x65)x35 = 1(∀ x65 . x65intx36 x65 = add_SNo x65 x65)(∀ x65 . x65intx37 x65 = x65)x38 = 1(∀ x65 . x65int∀ x66 . x66intx39 x65 x66 = If_i (SNoLe x65 0) x66 (x36 (x39 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx40 x65 = x39 (x37 x65) x38)(∀ x65 . x65intx41 x65 = x40 x65)(∀ x65 . x65int∀ x66 . x66intx42 x65 x66 = If_i (SNoLe x65 0) x66 (x34 (x42 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx43 x65 = x42 x35 (x41 x65))(∀ x65 . x65intx44 x65 = mul_SNo (x33 x65) (x43 x65))x45 = 1(∀ x65 . x65int∀ x66 . x66intx46 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx47 x65 x66 = If_i (SNoLe x65 0) x66 (x44 (x47 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx48 x65 x66 = x47 x45 (x46 x65 x66))(∀ x65 . x65int∀ x66 . x66intx49 x65 x66 = add_SNo (add_SNo (x48 x65 x66) (mul_SNo 2 (add_SNo (add_SNo x65 x65) x65))) x65)(∀ x65 . x65intx50 x65 = x65)x51 = 1(∀ x65 . x65int∀ x66 . x66intx52 x65 x66 = If_i (SNoLe x65 0) x66 (x49 (x52 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx53 x65 = x52 (x50 x65) x51)(∀ x65 . x65intx54 x65 = x53 x65)x55 = 1(∀ x65 . x65int∀ x66 . x66intx56 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx57 x65 x66 = If_i (SNoLe x65 0) x66 (x54 (x57 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx58 x65 x66 = x57 x55 (x56 x65 x66))(∀ x65 . x65int∀ x66 . x66intx59 x65 x66 = add_SNo (add_SNo (x58 x65 x66) x65) (mul_SNo (mul_SNo (add_SNo x65 x65) 2) 2))(∀ x65 . x65intx60 x65 = x65)x61 = 1(∀ x65 . x65int∀ x66 . x66intx62 x65 x66 = If_i (SNoLe x65 0) x66 (x59 (x62 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx63 x65 = x62 (x60 x65) x61)(∀ x65 . x65intx64 x65 = x63 x65)∀ x65 . x65intSNoLe 0 x65x25 x65 = x64 x65
Conjecture 72e97..A28218 : ∀ 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 . x14int∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ 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 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 . x36int∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι → ι → ι . (∀ x39 . x39int∀ x40 . x40int∀ x41 . x41intx38 x39 x40 x41int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 . x47int∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)(∀ x51 . x51int∀ x52 . x52intx0 x51 x52 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo x52 x52) x51)) (minus_SNo x52)) x51)(∀ x51 . x51int∀ x52 . x52intx1 x51 x52 = add_SNo x52 x52)(∀ x51 . x51intx2 x51 = x51)x3 = 1x4 = 2(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx5 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x0 (x5 (add_SNo x51 (minus_SNo 1)) x52 x53) (x6 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx6 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x1 (x5 (add_SNo x51 (minus_SNo 1)) x52 x53) (x6 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51intx7 x51 = x5 (x2 x51) x3 x4)(∀ x51 . x51intx8 x51 = add_SNo (add_SNo x51 x51) x51)(∀ x51 . x51intx9 x51 = x51)x10 = 1(∀ x51 . x51int∀ x52 . x52intx11 x51 x52 = If_i (SNoLe x51 0) x52 (x8 (x11 (add_SNo x51 (minus_SNo 1)) x52)))(∀ x51 . x51intx12 x51 = x11 (x9 x51) x10)(∀ x51 . x51intx13 x51 = mul_SNo (x7 x51) (x12 x51))x14 = 1(∀ x51 . x51int∀ x52 . x52intx15 x51 x52 = x52)(∀ x51 . x51int∀ x52 . x52intx16 x51 x52 = If_i (SNoLe x51 0) x52 (x13 (x16 (add_SNo x51 (minus_SNo 1)) x52)))(∀ x51 . x51int∀ x52 . x52intx17 x51 x52 = x16 x14 (x15 x51 x52))(∀ x51 . x51int∀ x52 . x52intx18 x51 x52 = add_SNo (add_SNo (x17 x51 x52) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x51 x51)) x51))) x51)(∀ x51 . x51intx19 x51 = x51)x20 = 1(∀ x51 . x51int∀ x52 . x52intx21 x51 x52 = If_i (SNoLe x51 0) x52 (x18 (x21 (add_SNo x51 (minus_SNo 1)) x52) x51))(∀ x51 . x51intx22 x51 = x21 (x19 x51) x20)(∀ x51 . x51intx23 x51 = x22 x51)(∀ x51 . x51int∀ x52 . x52intx24 x51 x52 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo x52 x52) x51)) (minus_SNo x52)) x51)(∀ x51 . x51int∀ x52 . x52intx25 x51 x52 = add_SNo x52 x52)(∀ x51 . x51intx26 x51 = x51)x27 = 1x28 = 2(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx29 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x24 (x29 (add_SNo x51 (minus_SNo 1)) x52 x53) (x30 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx30 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x25 (x29 (add_SNo x51 (minus_SNo 1)) x52 x53) (x30 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51intx31 x51 = x29 (x26 x51) x27 x28)(∀ x51 . x51int∀ x52 . x52intx32 x51 x52 = mul_SNo x51 x52)(∀ x51 . x51int∀ x52 . x52intx33 x51 x52 = x52)(∀ x51 . x51intx34 x51 = x51)x35 = 1x36 = add_SNo 1 2(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx37 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x32 (x37 (add_SNo x51 (minus_SNo 1)) x52 x53) (x38 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51int∀ x52 . x52int∀ x53 . x53intx38 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x33 (x37 (add_SNo x51 (minus_SNo 1)) x52 x53) (x38 (add_SNo x51 (minus_SNo 1)) x52 x53)))(∀ x51 . x51intx39 x51 = x37 (x34 x51) x35 x36)(∀ x51 . x51intx40 x51 = mul_SNo (x31 x51) (x39 x51))x41 = 1(∀ x51 . x51int∀ x52 . x52intx42 x51 x52 = x52)(∀ x51 . x51int∀ x52 . x52intx43 x51 x52 = If_i (SNoLe x51 0) x52 (x40 (x43 (add_SNo x51 (minus_SNo 1)) x52)))(∀ x51 . x51int∀ x52 . x52intx44 x51 x52 = x43 x41 (x42 x51 x52))(∀ x51 . x51int∀ x52 . x52intx45 x51 x52 = add_SNo (add_SNo (x44 x51 x52) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x51 x51)) x51))) x51)(∀ x51 . x51intx46 x51 = x51)x47 = 1(∀ x51 . x51int∀ x52 . x52intx48 x51 x52 = If_i (SNoLe x51 0) x52 (x45 (x48 (add_SNo x51 (minus_SNo 1)) x52) x51))(∀ x51 . x51intx49 x51 = x48 (x46 x51) x47)(∀ x51 . x51intx50 x51 = x49 x51)∀ x51 . x51intSNoLe 0 x51x23 x51 = x50 x51
Conjecture a644d..A28209 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 . x16int∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 . x40int∀ x41 : ι → ι → ι → ι . (∀ x42 . x42int∀ x43 . x43int∀ x44 . x44intx41 x42 x43 x44int)∀ x42 : ι → ι → ι → ι . (∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx42 x43 x44 x45int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 . x51int∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 . x55int∀ x56 : ι → ι → ι . (∀ x57 . x57int∀ x58 . x58intx56 x57 x58int)∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι → ι . (∀ x59 . x59int∀ x60 . x60intx58 x59 x60int)∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι . (∀ x61 . x61intx60 x61int)∀ x61 . x61int∀ x62 : ι → ι → ι . (∀ x63 . x63int∀ x64 . x64intx62 x63 x64int)∀ x63 : ι → ι . (∀ x64 . x64intx63 x64int)∀ x64 : ι → ι . (∀ x65 . x65intx64 x65int)(∀ x65 . x65intx0 x65 = mul_SNo 2 (add_SNo (add_SNo x65 x65) x65))(∀ x65 . x65intx1 x65 = x65)(∀ x65 . x65intx2 x65 = add_SNo x65 x65)(∀ x65 . x65intx3 x65 = x65)x4 = 2(∀ x65 . x65int∀ x66 . x66intx5 x65 x66 = If_i (SNoLe x65 0) x66 (x2 (x5 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx6 x65 = x5 (x3 x65) x4)(∀ x65 . x65intx7 x65 = add_SNo (x6 x65) (minus_SNo 1))(∀ x65 . x65int∀ x66 . x66intx8 x65 x66 = If_i (SNoLe x65 0) x66 (x0 (x8 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx9 x65 = x8 (x1 x65) (x7 x65))(∀ x65 . x65intx10 x65 = x9 x65)x11 = 1(∀ x65 . x65int∀ x66 . x66intx12 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx13 x65 x66 = If_i (SNoLe x65 0) x66 (x10 (x13 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx14 x65 x66 = x13 x11 (x12 x65 x66))(∀ x65 . x65int∀ x66 . x66intx15 x65 x66 = mul_SNo (add_SNo 2 x66) x65)x16 = 2(∀ x65 . x65intx17 x65 = x65)(∀ x65 . x65int∀ x66 . x66intx18 x65 x66 = If_i (SNoLe x65 0) x66 (x15 (x18 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx19 x65 = x18 x16 (x17 x65))(∀ x65 . x65int∀ x66 . x66intx20 x65 x66 = add_SNo (x14 x65 x66) (add_SNo (x19 x65) (minus_SNo x65)))(∀ x65 . x65int∀ x66 . x66intx21 x65 x66 = x66)x22 = 1(∀ x65 . x65int∀ x66 . x66intx23 x65 x66 = If_i (SNoLe x65 0) x66 (x20 (x23 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65int∀ x66 . x66intx24 x65 x66 = x23 (x21 x65 x66) x22)(∀ x65 . x65int∀ x66 . x66intx25 x65 x66 = add_SNo (add_SNo (x24 x65 x66) (mul_SNo 2 (add_SNo (add_SNo x65 x65) x65))) x65)(∀ x65 . x65intx26 x65 = x65)x27 = 1(∀ x65 . x65int∀ x66 . x66intx28 x65 x66 = If_i (SNoLe x65 0) x66 (x25 (x28 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx29 x65 = x28 (x26 x65) x27)(∀ x65 . x65intx30 x65 = x29 x65)(∀ x65 . x65intx31 x65 = add_SNo x65 x65)(∀ x65 . x65intx32 x65 = x65)x33 = 2(∀ x65 . x65int∀ x66 . x66intx34 x65 x66 = If_i (SNoLe x65 0) x66 (x31 (x34 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx35 x65 = x34 (x32 x65) x33)(∀ x65 . x65int∀ x66 . x66intx36 x65 x66 = mul_SNo x65 x66)(∀ x65 . x65int∀ x66 . x66intx37 x65 x66 = x66)(∀ x65 . x65intx38 x65 = x65)x39 = 1x40 = add_SNo 2 (add_SNo 2 2)(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx41 x65 x66 x67 = If_i (SNoLe x65 0) x66 (x36 (x41 (add_SNo x65 (minus_SNo 1)) x66 x67) (x42 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx42 x65 x66 x67 = If_i (SNoLe x65 0) x67 (x37 (x41 (add_SNo x65 (minus_SNo 1)) x66 x67) (x42 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65intx43 x65 = x41 (x38 x65) x39 x40)(∀ x65 . x65intx44 x65 = mul_SNo (add_SNo (x35 x65) (minus_SNo 1)) (x43 x65))x45 = 1(∀ x65 . x65int∀ x66 . x66intx46 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx47 x65 x66 = If_i (SNoLe x65 0) x66 (x44 (x47 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx48 x65 x66 = x47 x45 (x46 x65 x66))(∀ x65 . x65int∀ x66 . x66intx49 x65 x66 = add_SNo (add_SNo (x48 x65 x66) (mul_SNo 2 (add_SNo (add_SNo x65 x65) x65))) x65)(∀ x65 . x65intx50 x65 = x65)x51 = 1(∀ x65 . x65int∀ x66 . x66intx52 x65 x66 = If_i (SNoLe x65 0) x66 (x49 (x52 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx53 x65 = x52 (x50 x65) x51)(∀ x65 . x65intx54 x65 = x53 x65)x55 = 1(∀ x65 . x65int∀ x66 . x66intx56 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx57 x65 x66 = If_i (SNoLe x65 0) x66 (x54 (x57 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx58 x65 x66 = x57 x55 (x56 x65 x66))(∀ x65 . x65int∀ x66 . x66intx59 x65 x66 = add_SNo (add_SNo (x58 x65 x66) x65) (mul_SNo (add_SNo (mul_SNo (mul_SNo x65 2) 2) x65) 2))(∀ x65 . x65intx60 x65 = x65)x61 = 1(∀ x65 . x65int∀ x66 . x66intx62 x65 x66 = If_i (SNoLe x65 0) x66 (x59 (x62 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx63 x65 = x62 (x60 x65) x61)(∀ x65 . x65intx64 x65 = x63 x65)∀ x65 . x65intSNoLe 0 x65x30 x65 = x64 x65
Conjecture 5296c..A28204 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)∀ x48 . x48int∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 . x54int∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι . (∀ x57 . x57intx56 x57int)∀ x57 : ι → ι . (∀ x58 . x58intx57 x58int)(∀ x58 . x58intx0 x58 = add_SNo (add_SNo x58 x58) x58)(∀ x58 . x58int∀ x59 . x59intx1 x58 x59 = add_SNo x59 x59)x2 = 1(∀ x58 . x58int∀ x59 . x59intx3 x58 x59 = If_i (SNoLe x58 0) x59 (x0 (x3 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx4 x58 x59 = x3 (x1 x58 x59) x2)(∀ x58 . x58int∀ x59 . x59intx5 x58 x59 = add_SNo (x4 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58)))(∀ x58 . x58int∀ x59 . x59intx6 x58 x59 = x59)x7 = 1(∀ x58 . x58int∀ x59 . x59intx8 x58 x59 = If_i (SNoLe x58 0) x59 (x5 (x8 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx9 x58 x59 = x8 (x6 x58 x59) x7)(∀ x58 . x58int∀ x59 . x59intx10 x58 x59 = add_SNo (x9 x58 x59) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x58 x58)) x58)))(∀ x58 . x58int∀ x59 . x59intx11 x58 x59 = x59)x12 = 1(∀ x58 . x58int∀ x59 . x59intx13 x58 x59 = If_i (SNoLe x58 0) x59 (x10 (x13 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx14 x58 x59 = x13 (x11 x58 x59) x12)(∀ x58 . x58int∀ x59 . x59intx15 x58 x59 = add_SNo (add_SNo (x14 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58)(∀ x58 . x58intx16 x58 = x58)x17 = 1(∀ x58 . x58int∀ x59 . x59intx18 x58 x59 = If_i (SNoLe x58 0) x59 (x15 (x18 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx19 x58 = x18 (x16 x58) x17)(∀ x58 . x58intx20 x58 = x19 x58)(∀ x58 . x58int∀ x59 . x59intx21 x58 x59 = add_SNo (add_SNo (add_SNo x58 x58) x58) x59)(∀ x58 . x58int∀ x59 . x59intx22 x58 x59 = add_SNo x59 x59)(∀ x58 . x58intx23 x58 = x58)x24 = 1x25 = 2(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx26 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x21 (x26 (add_SNo x58 (minus_SNo 1)) x59 x60) (x27 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx27 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x22 (x26 (add_SNo x58 (minus_SNo 1)) x59 x60) (x27 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58intx28 x58 = x26 (x23 x58) x24 x25)(∀ x58 . x58int∀ x59 . x59intx29 x58 x59 = mul_SNo x58 x59)(∀ x58 . x58int∀ x59 . x59intx30 x58 x59 = x59)(∀ x58 . x58intx31 x58 = x58)x32 = 1x33 = add_SNo 1 2(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx34 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x29 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60) (x35 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx35 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x30 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60) (x35 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58intx36 x58 = x34 (x31 x58) x32 x33)(∀ x58 . x58intx37 x58 = mul_SNo (x28 x58) (x36 x58))x38 = 1(∀ x58 . x58int∀ x59 . x59intx39 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx40 x58 x59 = If_i (SNoLe x58 0) x59 (x37 (x40 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx41 x58 x59 = x40 x38 (x39 x58 x59))(∀ x58 . x58int∀ x59 . x59intx42 x58 x59 = add_SNo (x41 x58 x59) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x58 x58)) x58)))(∀ x58 . x58intx43 x58 = x58)x44 = 1(∀ x58 . x58int∀ x59 . x59intx45 x58 x59 = If_i (SNoLe x58 0) x59 (x42 (x45 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx46 x58 = x45 (x43 x58) x44)(∀ x58 . x58intx47 x58 = x46 x58)x48 = 1(∀ x58 . x58int∀ x59 . x59intx49 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx50 x58 x59 = If_i (SNoLe x58 0) x59 (x47 (x50 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx51 x58 x59 = x50 x48 (x49 x58 x59))(∀ x58 . x58int∀ x59 . x59intx52 x58 x59 = add_SNo (add_SNo (x51 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58)(∀ x58 . x58intx53 x58 = x58)x54 = 1(∀ x58 . x58int∀ x59 . x59intx55 x58 x59 = If_i (SNoLe x58 0) x59 (x52 (x55 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx56 x58 = x55 (x53 x58) x54)(∀ x58 . x58intx57 x58 = x56 x58)∀ x58 . x58intSNoLe 0 x58x20 x58 = x57 x58
Conjecture 1e6dd..A28201 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 . x10int∀ 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 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)(∀ x48 . x48int∀ x49 . x49intx0 x48 x49 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48)) (mul_SNo (mul_SNo x49 x49) x49))(∀ x48 . x48int∀ x49 . x49intx1 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx2 x48 x49 = x49)x3 = 1x4 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx5 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x0 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx6 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x1 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx7 x48 x49 = x5 (x2 x48 x49) x3 x4)(∀ x48 . x48int∀ x49 . x49intx8 x48 x49 = add_SNo (x7 x48 x49) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48)))(∀ x48 . x48int∀ x49 . x49intx9 x48 x49 = x49)x10 = 1(∀ x48 . x48int∀ x49 . x49intx11 x48 x49 = If_i (SNoLe x48 0) x49 (x8 (x11 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48int∀ x49 . x49intx12 x48 x49 = x11 (x9 x48 x49) x10)(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = add_SNo (add_SNo (x12 x48 x49) (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48))) x48)(∀ x48 . x48intx14 x48 = x48)x15 = 1(∀ x48 . x48int∀ x49 . x49intx16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx17 x48 = x16 (x14 x48) x15)(∀ x48 . x48intx18 x48 = x17 x48)(∀ x48 . x48int∀ x49 . x49intx19 x48 x49 = add_SNo (add_SNo (add_SNo (mul_SNo x49 x49) x48) x48) x48)(∀ x48 . x48int∀ x49 . x49intx20 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = x49)x22 = 1x23 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx24 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x19 (x24 (add_SNo x48 (minus_SNo 1)) x49 x50) (x25 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx25 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x20 (x24 (add_SNo x48 (minus_SNo 1)) x49 x50) (x25 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx26 x48 x49 = x24 (x21 x48 x49) x22 x23)(∀ x48 . x48int∀ x49 . x49intx27 x48 x49 = add_SNo (add_SNo (x26 x48 x49) (mul_SNo 2 (add_SNo x48 x48))) x48)(∀ x48 . x48intx28 x48 = x48)x29 = 1(∀ x48 . x48int∀ x49 . x49intx30 x48 x49 = If_i (SNoLe x48 0) x49 (x27 (x30 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx31 x48 = x30 (x28 x48) x29)(∀ x48 . x48intx32 x48 = add_SNo x48 x48)(∀ x48 . x48intx33 x48 = x48)x34 = 1(∀ x48 . x48int∀ x49 . x49intx35 x48 x49 = If_i (SNoLe x48 0) x49 (x32 (x35 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx36 x48 = x35 (x33 x48) x34)(∀ x48 . x48intx37 x48 = mul_SNo (x31 x48) (x36 x48))x38 = 1(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 x38 (x39 x48 x49))(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48))) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 1(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x18 x48 = x47 x48
Conjecture 68ef4..A28192 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 . x51int∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 . x55int∀ x56 : ι → ι → ι . (∀ x57 . x57int∀ x58 . x58intx56 x57 x58int)∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι → ι . (∀ x59 . x59int∀ x60 . x60intx58 x59 x60int)∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι . (∀ x61 . x61intx60 x61int)∀ x61 . x61int∀ x62 : ι → ι → ι . (∀ x63 . x63int∀ x64 . x64intx62 x63 x64int)∀ x63 : ι → ι . (∀ x64 . x64intx63 x64int)∀ x64 : ι → ι . (∀ x65 . x65intx64 x65int)(∀ x65 . x65intx0 x65 = add_SNo (add_SNo x65 x65) x65)(∀ x65 . x65int∀ x66 . x66intx1 x65 x66 = add_SNo x66 x66)x2 = 1(∀ x65 . x65int∀ x66 . x66intx3 x65 x66 = If_i (SNoLe x65 0) x66 (x0 (x3 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx4 x65 x66 = x3 (x1 x65 x66) x2)(∀ x65 . x65int∀ x66 . x66intx5 x65 x66 = add_SNo (x4 x65 x66) (mul_SNo 2 (mul_SNo 2 (add_SNo x65 x65))))(∀ x65 . x65int∀ x66 . x66intx6 x65 x66 = x66)x7 = 1(∀ x65 . x65int∀ x66 . x66intx8 x65 x66 = If_i (SNoLe x65 0) x66 (x5 (x8 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65int∀ x66 . x66intx9 x65 x66 = x8 (x6 x65 x66) x7)(∀ x65 . x65int∀ x66 . x66intx10 x65 x66 = mul_SNo (add_SNo 2 x66) x65)x11 = 2(∀ x65 . x65intx12 x65 = x65)(∀ x65 . x65int∀ x66 . x66intx13 x65 x66 = If_i (SNoLe x65 0) x66 (x10 (x13 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx14 x65 = x13 x11 (x12 x65))(∀ x65 . x65int∀ x66 . x66intx15 x65 x66 = add_SNo (x9 x65 x66) (x14 x65))(∀ x65 . x65int∀ x66 . x66intx16 x65 x66 = x66)x17 = 1(∀ x65 . x65int∀ x66 . x66intx18 x65 x66 = If_i (SNoLe x65 0) x66 (x15 (x18 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65int∀ x66 . x66intx19 x65 x66 = x18 (x16 x65 x66) x17)(∀ x65 . x65int∀ x66 . x66intx20 x65 x66 = add_SNo (add_SNo (x19 x65 x66) (mul_SNo 2 (add_SNo x65 x65))) x65)(∀ x65 . x65intx21 x65 = x65)x22 = 1(∀ x65 . x65int∀ x66 . x66intx23 x65 x66 = If_i (SNoLe x65 0) x66 (x20 (x23 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx24 x65 = x23 (x21 x65) x22)(∀ x65 . x65intx25 x65 = x24 x65)(∀ x65 . x65int∀ x66 . x66intx26 x65 x66 = add_SNo (add_SNo (add_SNo x65 x65) x65) x66)(∀ x65 . x65int∀ x66 . x66intx27 x65 x66 = add_SNo x66 x66)(∀ x65 . x65intx28 x65 = x65)x29 = 1x30 = 2(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx31 x65 x66 x67 = If_i (SNoLe x65 0) x66 (x26 (x31 (add_SNo x65 (minus_SNo 1)) x66 x67) (x32 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65int∀ x66 . x66int∀ x67 . x67intx32 x65 x66 x67 = If_i (SNoLe x65 0) x67 (x27 (x31 (add_SNo x65 (minus_SNo 1)) x66 x67) (x32 (add_SNo x65 (minus_SNo 1)) x66 x67)))(∀ x65 . x65intx33 x65 = x31 (x28 x65) x29 x30)(∀ x65 . x65intx34 x65 = mul_SNo x65 x65)x35 = 1(∀ x65 . x65intx36 x65 = add_SNo x65 x65)(∀ x65 . x65intx37 x65 = x65)x38 = 1(∀ x65 . x65int∀ x66 . x66intx39 x65 x66 = If_i (SNoLe x65 0) x66 (x36 (x39 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx40 x65 = x39 (x37 x65) x38)(∀ x65 . x65intx41 x65 = x40 x65)(∀ x65 . x65int∀ x66 . x66intx42 x65 x66 = If_i (SNoLe x65 0) x66 (x34 (x42 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65intx43 x65 = x42 x35 (x41 x65))(∀ x65 . x65intx44 x65 = mul_SNo (x33 x65) (x43 x65))x45 = 1(∀ x65 . x65int∀ x66 . x66intx46 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx47 x65 x66 = If_i (SNoLe x65 0) x66 (x44 (x47 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx48 x65 x66 = x47 x45 (x46 x65 x66))(∀ x65 . x65int∀ x66 . x66intx49 x65 x66 = add_SNo (add_SNo (x48 x65 x66) (mul_SNo 2 (add_SNo x65 x65))) x65)(∀ x65 . x65intx50 x65 = x65)x51 = 1(∀ x65 . x65int∀ x66 . x66intx52 x65 x66 = If_i (SNoLe x65 0) x66 (x49 (x52 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx53 x65 = x52 (x50 x65) x51)(∀ x65 . x65intx54 x65 = x53 x65)x55 = 1(∀ x65 . x65int∀ x66 . x66intx56 x65 x66 = x66)(∀ x65 . x65int∀ x66 . x66intx57 x65 x66 = If_i (SNoLe x65 0) x66 (x54 (x57 (add_SNo x65 (minus_SNo 1)) x66)))(∀ x65 . x65int∀ x66 . x66intx58 x65 x66 = x57 x55 (x56 x65 x66))(∀ x65 . x65int∀ x66 . x66intx59 x65 x66 = add_SNo (add_SNo (x58 x65 x66) x65) (mul_SNo (mul_SNo (add_SNo x65 x65) 2) 2))(∀ x65 . x65intx60 x65 = x65)x61 = 1(∀ x65 . x65int∀ x66 . x66intx62 x65 x66 = If_i (SNoLe x65 0) x66 (x59 (x62 (add_SNo x65 (minus_SNo 1)) x66) x65))(∀ x65 . x65intx63 x65 = x62 (x60 x65) x61)(∀ x65 . x65intx64 x65 = x63 x65)∀ x65 . x65intSNoLe 0 x65x25 x65 = x64 x65
Conjecture d9b0a..A28178 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 . x21int∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 . x40int∀ x41 : ι → ι → ι → ι . (∀ x42 . x42int∀ x43 . x43int∀ x44 . x44intx41 x42 x43 x44int)∀ x42 : ι → ι → ι → ι . (∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx42 x43 x44 x45int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 . x51int∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)∀ x55 : ι → ι . (∀ x56 . x56intx55 x56int)∀ x56 . x56int∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι . (∀ x59 . x59intx58 x59int)∀ x59 : ι → ι . (∀ x60 . x60intx59 x60int)∀ x60 . x60int∀ x61 : ι → ι → ι . (∀ x62 . x62int∀ x63 . x63intx61 x62 x63int)∀ x62 : ι → ι → ι . (∀ x63 . x63int∀ x64 . x64intx62 x63 x64int)∀ x63 : ι → ι → ι . (∀ x64 . x64int∀ x65 . x65intx63 x64 x65int)∀ x64 : ι → ι → ι . (∀ x65 . x65int∀ x66 . x66intx64 x65 x66int)∀ x65 : ι → ι . (∀ x66 . x66intx65 x66int)∀ x66 . x66int∀ x67 : ι → ι → ι . (∀ x68 . x68int∀ x69 . x69intx67 x68 x69int)∀ x68 : ι → ι . (∀ x69 . x69intx68 x69int)∀ x69 : ι → ι . (∀ x70 . x70intx69 x70int)(∀ x70 . x70intx0 x70 = add_SNo (mul_SNo 2 (add_SNo x70 x70)) x70)(∀ x70 . x70intx1 x70 = x70)(∀ x70 . x70intx2 x70 = add_SNo x70 x70)(∀ x70 . x70intx3 x70 = x70)x4 = 2(∀ x70 . x70int∀ x71 . x71intx5 x70 x71 = If_i (SNoLe x70 0) x71 (x2 (x5 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70intx6 x70 = x5 (x3 x70) x4)(∀ x70 . x70intx7 x70 = add_SNo (x6 x70) (minus_SNo 1))(∀ x70 . x70int∀ x71 . x71intx8 x70 x71 = If_i (SNoLe x70 0) x71 (x0 (x8 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70intx9 x70 = x8 (x1 x70) (x7 x70))(∀ x70 . x70intx10 x70 = x9 x70)x11 = 1(∀ x70 . x70int∀ x71 . x71intx12 x70 x71 = x71)(∀ x70 . x70int∀ x71 . x71intx13 x70 x71 = If_i (SNoLe x70 0) x71 (x10 (x13 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70int∀ x71 . x71intx14 x70 x71 = x13 x11 (x12 x70 x71))(∀ x70 . x70int∀ x71 . x71intx15 x70 x71 = add_SNo (x14 x70 x71) (mul_SNo 2 (add_SNo (add_SNo x70 x70) x70)))(∀ x70 . x70int∀ x71 . x71intx16 x70 x71 = x71)x17 = 1(∀ x70 . x70int∀ x71 . x71intx18 x70 x71 = If_i (SNoLe x70 0) x71 (x15 (x18 (add_SNo x70 (minus_SNo 1)) x71) x70))(∀ x70 . x70int∀ x71 . x71intx19 x70 x71 = x18 (x16 x70 x71) x17)(∀ x70 . x70int∀ x71 . x71intx20 x70 x71 = mul_SNo (add_SNo 2 x71) x70)x21 = 2(∀ x70 . x70intx22 x70 = x70)(∀ x70 . x70int∀ x71 . x71intx23 x70 x71 = If_i (SNoLe x70 0) x71 (x20 (x23 (add_SNo x70 (minus_SNo 1)) x71) x70))(∀ x70 . x70intx24 x70 = x23 x21 (x22 x70))(∀ x70 . x70int∀ x71 . x71intx25 x70 x71 = add_SNo (x19 x70 x71) (x24 x70))(∀ x70 . x70intx26 x70 = x70)x27 = 1(∀ x70 . x70int∀ x71 . x71intx28 x70 x71 = If_i (SNoLe x70 0) x71 (x25 (x28 (add_SNo x70 (minus_SNo 1)) x71) x70))(∀ x70 . x70intx29 x70 = x28 (x26 x70) x27)(∀ x70 . x70intx30 x70 = x29 x70)(∀ x70 . x70intx31 x70 = add_SNo x70 x70)(∀ x70 . x70intx32 x70 = x70)x33 = 2(∀ x70 . x70int∀ x71 . x71intx34 x70 x71 = If_i (SNoLe x70 0) x71 (x31 (x34 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70intx35 x70 = x34 (x32 x70) x33)(∀ x70 . x70int∀ x71 . x71intx36 x70 x71 = mul_SNo x70 x71)(∀ x70 . x70int∀ x71 . x71intx37 x70 x71 = x71)(∀ x70 . x70intx38 x70 = x70)x39 = 1x40 = add_SNo 1 2(∀ x70 . x70int∀ x71 . x71int∀ x72 . x72intx41 x70 x71 x72 = If_i (SNoLe x70 0) x71 (x36 (x41 (add_SNo x70 (minus_SNo 1)) x71 x72) (x42 (add_SNo x70 (minus_SNo 1)) x71 x72)))(∀ x70 . x70int∀ x71 . x71int∀ x72 . x72intx42 x70 x71 x72 = If_i (SNoLe x70 0) x72 (x37 (x41 (add_SNo x70 (minus_SNo 1)) x71 x72) (x42 (add_SNo x70 (minus_SNo 1)) x71 x72)))(∀ x70 . x70intx43 x70 = x41 (x38 x70) x39 x40)(∀ x70 . x70intx44 x70 = mul_SNo (add_SNo (x35 x70) (minus_SNo 1)) (x43 x70))x45 = 1(∀ x70 . x70int∀ x71 . x71intx46 x70 x71 = x71)(∀ x70 . x70int∀ x71 . x71intx47 x70 x71 = If_i (SNoLe x70 0) x71 (x44 (x47 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70int∀ x71 . x71intx48 x70 x71 = x47 x45 (x46 x70 x71))(∀ x70 . x70int∀ x71 . x71intx49 x70 x71 = add_SNo (add_SNo (x48 x70 x71) (mul_SNo 2 (add_SNo x70 x70))) x70)(∀ x70 . x70intx50 x70 = x70)x51 = 1(∀ x70 . x70int∀ x71 . x71intx52 x70 x71 = If_i (SNoLe x70 0) x71 (x49 (x52 (add_SNo x70 (minus_SNo 1)) x71) x70))(∀ x70 . x70intx53 x70 = x52 (x50 x70) x51)(∀ x70 . x70intx54 x70 = add_SNo x70 x70)(∀ x70 . x70intx55 x70 = x70)x56 = 1(∀ x70 . x70int∀ x71 . x71intx57 x70 x71 = If_i (SNoLe x70 0) x71 (x54 (x57 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70intx58 x70 = x57 (x55 x70) x56)(∀ x70 . x70intx59 x70 = mul_SNo (x53 x70) (x58 x70))x60 = 1(∀ x70 . x70int∀ x71 . x71intx61 x70 x71 = x71)(∀ x70 . x70int∀ x71 . x71intx62 x70 x71 = If_i (SNoLe x70 0) x71 (x59 (x62 (add_SNo x70 (minus_SNo 1)) x71)))(∀ x70 . x70int∀ x71 . x71intx63 x70 x71 = x62 x60 (x61 x70 x71))(∀ x70 . x70int∀ x71 . x71intx64 x70 x71 = add_SNo (add_SNo (x63 x70 x71) (mul_SNo 2 (add_SNo x70 x70))) x70)(∀ x70 . x70intx65 x70 = x70)x66 = 1(∀ x70 . x70int∀ x71 . x71intx67 x70 x71 = If_i (SNoLe x70 0) x71 (x64 (x67 (add_SNo x70 (minus_SNo 1)) x71) x70))(∀ x70 . x70intx68 x70 = x67 (x65 x70) x66)(∀ x70 . x70intx69 x70 = x68 x70)∀ x70 . x70intSNoLe 0 x70x30 x70 = x69 x70
Conjecture d0f23..A28175 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 . x6int∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 . x37int∀ x38 . x38int∀ x39 : ι → ι → ι → ι . (∀ x40 . x40int∀ x41 . x41int∀ x42 . x42intx39 x40 x41 x42int)∀ x40 : ι → ι → ι → ι . (∀ x41 . x41int∀ x42 . x42int∀ x43 . x43intx40 x41 x42 x43int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 . x43int∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 . x49int∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)∀ x53 . x53int∀ x54 : ι → ι → ι . (∀ x55 . x55int∀ x56 . x56intx54 x55 x56int)∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι → ι . (∀ x57 . x57int∀ x58 . x58intx56 x57 x58int)∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι . (∀ x59 . x59intx58 x59int)∀ x59 . x59int∀ x60 : ι → ι → ι . (∀ x61 . x61int∀ x62 . x62intx60 x61 x62int)∀ x61 : ι → ι . (∀ x62 . x62intx61 x62int)∀ x62 : ι → ι . (∀ x63 . x63intx62 x63int)(∀ x63 . x63intx0 x63 = add_SNo (add_SNo x63 x63) x63)(∀ x63 . x63int∀ x64 . x64intx1 x63 x64 = add_SNo x64 x64)x2 = 1(∀ x63 . x63int∀ x64 . x64intx3 x63 x64 = If_i (SNoLe x63 0) x64 (x0 (x3 (add_SNo x63 (minus_SNo 1)) x64)))(∀ x63 . x63int∀ x64 . x64intx4 x63 x64 = x3 (x1 x63 x64) x2)(∀ x63 . x63int∀ x64 . x64intx5 x63 x64 = mul_SNo (add_SNo 2 x64) x63)x6 = 2(∀ x63 . x63intx7 x63 = x63)(∀ x63 . x63int∀ x64 . x64intx8 x63 x64 = If_i (SNoLe x63 0) x64 (x5 (x8 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63intx9 x63 = x8 x6 (x7 x63))(∀ x63 . x63int∀ x64 . x64intx10 x63 x64 = add_SNo (x4 x63 x64) (add_SNo (x9 x63) (minus_SNo x63)))(∀ x63 . x63int∀ x64 . x64intx11 x63 x64 = x64)x12 = 1(∀ x63 . x63int∀ x64 . x64intx13 x63 x64 = If_i (SNoLe x63 0) x64 (x10 (x13 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63int∀ x64 . x64intx14 x63 x64 = x13 (x11 x63 x64) x12)(∀ x63 . x63int∀ x64 . x64intx15 x63 x64 = add_SNo (x14 x63 x64) (mul_SNo 2 (add_SNo (add_SNo x63 x63) x63)))(∀ x63 . x63int∀ x64 . x64intx16 x63 x64 = x64)x17 = 1(∀ x63 . x63int∀ x64 . x64intx18 x63 x64 = If_i (SNoLe x63 0) x64 (x15 (x18 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63int∀ x64 . x64intx19 x63 x64 = x18 (x16 x63 x64) x17)(∀ x63 . x63int∀ x64 . x64intx20 x63 x64 = add_SNo (add_SNo (x19 x63 x64) (mul_SNo 2 (add_SNo x63 x63))) x63)(∀ x63 . x63intx21 x63 = x63)x22 = 1(∀ x63 . x63int∀ x64 . x64intx23 x63 x64 = If_i (SNoLe x63 0) x64 (x20 (x23 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63intx24 x63 = x23 (x21 x63) x22)(∀ x63 . x63intx25 x63 = x24 x63)(∀ x63 . x63int∀ x64 . x64intx26 x63 x64 = add_SNo (add_SNo (add_SNo x63 x63) x63) x64)(∀ x63 . x63int∀ x64 . x64intx27 x63 x64 = add_SNo x64 x64)(∀ x63 . x63intx28 x63 = x63)x29 = 1x30 = 2(∀ x63 . x63int∀ x64 . x64int∀ x65 . x65intx31 x63 x64 x65 = If_i (SNoLe x63 0) x64 (x26 (x31 (add_SNo x63 (minus_SNo 1)) x64 x65) (x32 (add_SNo x63 (minus_SNo 1)) x64 x65)))(∀ x63 . x63int∀ x64 . x64int∀ x65 . x65intx32 x63 x64 x65 = If_i (SNoLe x63 0) x65 (x27 (x31 (add_SNo x63 (minus_SNo 1)) x64 x65) (x32 (add_SNo x63 (minus_SNo 1)) x64 x65)))(∀ x63 . x63intx33 x63 = x31 (x28 x63) x29 x30)(∀ x63 . x63int∀ x64 . x64intx34 x63 x64 = mul_SNo x63 x64)(∀ x63 . x63int∀ x64 . x64intx35 x63 x64 = x64)(∀ x63 . x63intx36 x63 = x63)x37 = 1x38 = add_SNo 1 2(∀ x63 . x63int∀ x64 . x64int∀ x65 . x65intx39 x63 x64 x65 = If_i (SNoLe x63 0) x64 (x34 (x39 (add_SNo x63 (minus_SNo 1)) x64 x65) (x40 (add_SNo x63 (minus_SNo 1)) x64 x65)))(∀ x63 . x63int∀ x64 . x64int∀ x65 . x65intx40 x63 x64 x65 = If_i (SNoLe x63 0) x65 (x35 (x39 (add_SNo x63 (minus_SNo 1)) x64 x65) (x40 (add_SNo x63 (minus_SNo 1)) x64 x65)))(∀ x63 . x63intx41 x63 = x39 (x36 x63) x37 x38)(∀ x63 . x63intx42 x63 = mul_SNo (x33 x63) (x41 x63))x43 = 1(∀ x63 . x63int∀ x64 . x64intx44 x63 x64 = x64)(∀ x63 . x63int∀ x64 . x64intx45 x63 x64 = If_i (SNoLe x63 0) x64 (x42 (x45 (add_SNo x63 (minus_SNo 1)) x64)))(∀ x63 . x63int∀ x64 . x64intx46 x63 x64 = x45 x43 (x44 x63 x64))(∀ x63 . x63int∀ x64 . x64intx47 x63 x64 = add_SNo (add_SNo (x46 x63 x64) (mul_SNo 2 (add_SNo x63 x63))) x63)(∀ x63 . x63intx48 x63 = x63)x49 = 1(∀ x63 . x63int∀ x64 . x64intx50 x63 x64 = If_i (SNoLe x63 0) x64 (x47 (x50 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63intx51 x63 = x50 (x48 x63) x49)(∀ x63 . x63intx52 x63 = x51 x63)x53 = 1(∀ x63 . x63int∀ x64 . x64intx54 x63 x64 = x64)(∀ x63 . x63int∀ x64 . x64intx55 x63 x64 = If_i (SNoLe x63 0) x64 (x52 (x55 (add_SNo x63 (minus_SNo 1)) x64)))(∀ x63 . x63int∀ x64 . x64intx56 x63 x64 = x55 x53 (x54 x63 x64))(∀ x63 . x63int∀ x64 . x64intx57 x63 x64 = add_SNo (add_SNo (x56 x63 x64) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x63 x63)) x63))) x63)(∀ x63 . x63intx58 x63 = x63)x59 = 1(∀ x63 . x63int∀ x64 . x64intx60 x63 x64 = If_i (SNoLe x63 0) x64 (x57 (x60 (add_SNo x63 (minus_SNo 1)) x64) x63))(∀ x63 . x63intx61 x63 = x60 (x58 x63) x59)(∀ x63 . x63intx62 x63 = x61 x63)∀ x63 . x63intSNoLe 0 x63x25 x63 = x62 x63
Conjecture 612c4..A28169 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 . x11int∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 . x35int∀ x36 : ι → ι → ι → ι . (∀ x37 . x37int∀ x38 . x38int∀ x39 . x39intx36 x37 x38 x39int)∀ x37 : ι → ι → ι → ι . (∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx37 x38 x39 x40int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)∀ x50 . x50int∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι → ι . (∀ x54 . x54int∀ x55 . x55intx53 x54 x55int)∀ x54 : ι → ι → ι . (∀ x55 . x55int∀ x56 . x56intx54 x55 x56int)∀ x55 : ι → ι . (∀ x56 . x56intx55 x56int)∀ x56 . x56int∀ x57 : ι → ι → ι . (∀ x58 . x58int∀ x59 . x59intx57 x58 x59int)∀ x58 : ι → ι . (∀ x59 . x59intx58 x59int)∀ x59 : ι → ι . (∀ x60 . x60intx59 x60int)(∀ x60 . x60intx0 x60 = mul_SNo 2 (add_SNo (add_SNo x60 x60) x60))(∀ x60 . x60intx1 x60 = x60)(∀ x60 . x60intx2 x60 = add_SNo x60 x60)(∀ x60 . x60intx3 x60 = x60)x4 = 2(∀ x60 . x60int∀ x61 . x61intx5 x60 x61 = If_i (SNoLe x60 0) x61 (x2 (x5 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60intx6 x60 = x5 (x3 x60) x4)(∀ x60 . x60intx7 x60 = add_SNo (x6 x60) (minus_SNo 1))(∀ x60 . x60int∀ x61 . x61intx8 x60 x61 = If_i (SNoLe x60 0) x61 (x0 (x8 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60intx9 x60 = x8 (x1 x60) (x7 x60))(∀ x60 . x60intx10 x60 = x9 x60)x11 = 1(∀ x60 . x60int∀ x61 . x61intx12 x60 x61 = x61)(∀ x60 . x60int∀ x61 . x61intx13 x60 x61 = If_i (SNoLe x60 0) x61 (x10 (x13 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60int∀ x61 . x61intx14 x60 x61 = x13 x11 (x12 x60 x61))(∀ x60 . x60int∀ x61 . x61intx15 x60 x61 = add_SNo (add_SNo (x14 x60 x61) (mul_SNo 2 (add_SNo (add_SNo x60 x60) x60))) x60)(∀ x60 . x60int∀ x61 . x61intx16 x60 x61 = x61)x17 = 1(∀ x60 . x60int∀ x61 . x61intx18 x60 x61 = If_i (SNoLe x60 0) x61 (x15 (x18 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60int∀ x61 . x61intx19 x60 x61 = x18 (x16 x60 x61) x17)(∀ x60 . x60int∀ x61 . x61intx20 x60 x61 = add_SNo (add_SNo (x19 x60 x61) (mul_SNo 2 (add_SNo x60 x60))) x60)(∀ x60 . x60intx21 x60 = x60)x22 = 1(∀ x60 . x60int∀ x61 . x61intx23 x60 x61 = If_i (SNoLe x60 0) x61 (x20 (x23 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60intx24 x60 = x23 (x21 x60) x22)(∀ x60 . x60intx25 x60 = x24 x60)(∀ x60 . x60intx26 x60 = add_SNo x60 x60)(∀ x60 . x60intx27 x60 = x60)x28 = 2(∀ x60 . x60int∀ x61 . x61intx29 x60 x61 = If_i (SNoLe x60 0) x61 (x26 (x29 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60intx30 x60 = x29 (x27 x60) x28)(∀ x60 . x60int∀ x61 . x61intx31 x60 x61 = mul_SNo x60 x61)(∀ x60 . x60int∀ x61 . x61intx32 x60 x61 = x61)(∀ x60 . x60intx33 x60 = x60)x34 = 1x35 = add_SNo 2 (add_SNo 2 2)(∀ x60 . x60int∀ x61 . x61int∀ x62 . x62intx36 x60 x61 x62 = If_i (SNoLe x60 0) x61 (x31 (x36 (add_SNo x60 (minus_SNo 1)) x61 x62) (x37 (add_SNo x60 (minus_SNo 1)) x61 x62)))(∀ x60 . x60int∀ x61 . x61int∀ x62 . x62intx37 x60 x61 x62 = If_i (SNoLe x60 0) x62 (x32 (x36 (add_SNo x60 (minus_SNo 1)) x61 x62) (x37 (add_SNo x60 (minus_SNo 1)) x61 x62)))(∀ x60 . x60intx38 x60 = x36 (x33 x60) x34 x35)(∀ x60 . x60intx39 x60 = mul_SNo (add_SNo (x30 x60) (minus_SNo 1)) (x38 x60))x40 = 1(∀ x60 . x60int∀ x61 . x61intx41 x60 x61 = x61)(∀ x60 . x60int∀ x61 . x61intx42 x60 x61 = If_i (SNoLe x60 0) x61 (x39 (x42 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60int∀ x61 . x61intx43 x60 x61 = x42 x40 (x41 x60 x61))(∀ x60 . x60int∀ x61 . x61intx44 x60 x61 = add_SNo (add_SNo (x43 x60 x61) (mul_SNo 2 (add_SNo x60 x60))) x60)(∀ x60 . x60intx45 x60 = x60)x46 = 1(∀ x60 . x60int∀ x61 . x61intx47 x60 x61 = If_i (SNoLe x60 0) x61 (x44 (x47 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60intx48 x60 = x47 (x45 x60) x46)(∀ x60 . x60intx49 x60 = x48 x60)x50 = 1(∀ x60 . x60int∀ x61 . x61intx51 x60 x61 = x61)(∀ x60 . x60int∀ x61 . x61intx52 x60 x61 = If_i (SNoLe x60 0) x61 (x49 (x52 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60int∀ x61 . x61intx53 x60 x61 = x52 x50 (x51 x60 x61))(∀ x60 . x60int∀ x61 . x61intx54 x60 x61 = add_SNo (add_SNo (x53 x60 x61) x60) (mul_SNo (add_SNo (add_SNo x60 x60) x60) 2))(∀ x60 . x60intx55 x60 = x60)x56 = 1(∀ x60 . x60int∀ x61 . x61intx57 x60 x61 = If_i (SNoLe x60 0) x61 (x54 (x57 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60intx58 x60 = x57 (x55 x60) x56)(∀ x60 . x60intx59 x60 = x58 x60)∀ x60 . x60intSNoLe 0 x60x25 x60 = x59 x60
Conjecture 6c531..A28155 : ∀ 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 . x14int∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 . x43int∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 . x49int∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)(∀ x53 . x53int∀ x54 . x54intx0 x53 x54 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo (mul_SNo x54 x54) x53) x53)) (minus_SNo x54)) x53)(∀ x53 . x53int∀ x54 . x54intx1 x53 x54 = add_SNo x54 x54)(∀ x53 . x53intx2 x53 = x53)x3 = 1x4 = 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx5 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x0 (x5 (add_SNo x53 (minus_SNo 1)) x54 x55) (x6 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx6 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x1 (x5 (add_SNo x53 (minus_SNo 1)) x54 x55) (x6 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx7 x53 = x5 (x2 x53) x3 x4)(∀ x53 . x53intx8 x53 = add_SNo x53 x53)(∀ x53 . x53intx9 x53 = x53)x10 = 1(∀ x53 . x53int∀ x54 . x54intx11 x53 x54 = If_i (SNoLe x53 0) x54 (x8 (x11 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx12 x53 = x11 (x9 x53) x10)(∀ x53 . x53intx13 x53 = mul_SNo (x7 x53) (x12 x53))x14 = 1(∀ x53 . x53int∀ x54 . x54intx15 x53 x54 = x54)(∀ x53 . x53int∀ x54 . x54intx16 x53 x54 = If_i (SNoLe x53 0) x54 (x13 (x16 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53int∀ x54 . x54intx17 x53 x54 = x16 x14 (x15 x53 x54))(∀ x53 . x53intx18 x53 = add_SNo (add_SNo x53 x53) x53)x19 = 2(∀ x53 . x53intx20 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx21 x53 x54 = If_i (SNoLe x53 0) x54 (x18 (x21 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx22 x53 = x21 x19 (x20 x53))(∀ x53 . x53int∀ x54 . x54intx23 x53 x54 = add_SNo (x17 x53 x54) (x22 x53))(∀ x53 . x53intx24 x53 = x53)x25 = 1(∀ x53 . x53int∀ x54 . x54intx26 x53 x54 = If_i (SNoLe x53 0) x54 (x23 (x26 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx27 x53 = x26 (x24 x53) x25)(∀ x53 . x53intx28 x53 = x27 x53)(∀ x53 . x53int∀ x54 . x54intx29 x53 x54 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo (mul_SNo x54 x54) x53) x53)) (minus_SNo x54)) x53)(∀ x53 . x53int∀ x54 . x54intx30 x53 x54 = add_SNo x54 x54)(∀ x53 . x53intx31 x53 = x53)x32 = 1x33 = 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx34 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x29 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx35 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x30 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx36 x53 = x34 (x31 x53) x32 x33)(∀ x53 . x53intx37 x53 = add_SNo x53 x53)(∀ x53 . x53intx38 x53 = x53)x39 = 1(∀ x53 . x53int∀ x54 . x54intx40 x53 x54 = If_i (SNoLe x53 0) x54 (x37 (x40 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx41 x53 = x40 (x38 x53) x39)(∀ x53 . x53intx42 x53 = mul_SNo (x36 x53) (x41 x53))x43 = 1(∀ x53 . x53int∀ x54 . x54intx44 x53 x54 = x54)(∀ x53 . x53int∀ x54 . x54intx45 x53 x54 = If_i (SNoLe x53 0) x54 (x42 (x45 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53int∀ x54 . x54intx46 x53 x54 = x45 x43 (x44 x53 x54))(∀ x53 . x53int∀ x54 . x54intx47 x53 x54 = add_SNo (add_SNo (x46 x53 x54) (mul_SNo 2 (mul_SNo 2 (add_SNo x53 x53)))) x53)(∀ x53 . x53intx48 x53 = x53)x49 = 1(∀ x53 . x53int∀ x54 . x54intx50 x53 x54 = If_i (SNoLe x53 0) x54 (x47 (x50 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx51 x53 = x50 (x48 x53) x49)(∀ x53 . x53intx52 x53 = x51 x53)∀ x53 . x53intSNoLe 0 x53x28 x53 = x52 x53
Conjecture 927b4..A28147 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 . x9int∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33int∀ x34 . x34intx0 x33 x34 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x34 (minus_SNo 1)) x34) (mul_SNo x34 x34)) x33) (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)))(∀ x33 . x33int∀ x34 . x34intx1 x33 x34 = add_SNo x34 x34)(∀ x33 . x33int∀ x34 . x34intx2 x33 x34 = x34)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 . x33int∀ x34 . x34intx7 x33 x34 = x5 (x2 x33 x34) x3 x4)(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = mul_SNo (add_SNo 2 x34) x33)x9 = 2(∀ x33 . x33intx10 x33 = x33)(∀ x33 . x33int∀ x34 . x34intx11 x33 x34 = If_i (SNoLe x33 0) x34 (x8 (x11 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx12 x33 = x11 x9 (x10 x33))(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = add_SNo (x7 x33 x34) (add_SNo (x12 x33) (minus_SNo x33)))(∀ x33 . x33intx14 x33 = x33)x15 = 1(∀ x33 . x33int∀ x34 . x34intx16 x33 x34 = If_i (SNoLe x33 0) x34 (x13 (x16 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx17 x33 = x16 (x14 x33) x15)(∀ x33 . x33intx18 x33 = x17 x33)(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x34 (minus_SNo 1)) x34) (mul_SNo x34 x34)) x33) (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)))(∀ x33 . x33int∀ x34 . x34intx20 x33 x34 = add_SNo x34 x34)(∀ x33 . x33int∀ x34 . x34intx21 x33 x34 = x34)x22 = 1x23 = 2(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x19 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x20 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35)))(∀ x33 . x33int∀ x34 . x34intx26 x33 x34 = x24 (x21 x33 x34) x22 x23)(∀ x33 . x33int∀ x34 . x34intx27 x33 x34 = add_SNo (add_SNo (x26 x33 x34) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33))) x33)(∀ x33 . x33intx28 x33 = x33)x29 = 1(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34) x33))(∀ x33 . x33intx31 x33 = x30 (x28 x33) x29)(∀ x33 . x33intx32 x33 = x31 x33)∀ x33 . x33intSNoLe 0 x33x18 x33 = x32 x33