Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNtZ../10f01..
PUdBk../3e5a6..
vout
PrNtZ../fea2b.. 0.06 bars
PUapB../c5617.. doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param ordsuccordsucc : ιι
Param mul_SNomul_SNo : ιιι
Param minus_SNominus_SNo : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Conjecture f0561..A262594 : ∀ 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 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)(∀ x42 . x42intx0 x42 = add_SNo 1 (mul_SNo 2 (add_SNo x42 x42)))(∀ x42 . x42int∀ x43 . x43intx1 x42 x43 = add_SNo x43 (minus_SNo 1))x2 = 1(∀ x42 . x42int∀ x43 . x43intx3 x42 x43 = If_i (SNoLe x42 0) x43 (x0 (x3 (add_SNo x42 (minus_SNo 1)) x43)))(∀ x42 . x42int∀ x43 . x43intx4 x42 x43 = x3 (x1 x42 x43) x2)(∀ x42 . x42int∀ x43 . x43intx5 x42 x43 = add_SNo (x4 x42 x43) x42)(∀ x42 . x42int∀ x43 . x43intx6 x42 x43 = x43)x7 = 1(∀ x42 . x42int∀ x43 . x43intx8 x42 x43 = If_i (SNoLe x42 0) x43 (x5 (x8 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx9 x42 x43 = x8 (x6 x42 x43) x7)(∀ x42 . x42int∀ x43 . x43intx10 x42 x43 = add_SNo (x9 x42 x43) x42)(∀ x42 . x42int∀ x43 . x43intx11 x42 x43 = x43)(∀ x42 . x42intx12 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx13 x42 x43 = If_i (SNoLe x42 0) x43 (x10 (x13 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx14 x42 x43 = x13 (x11 x42 x43) (x12 x42))(∀ x42 . x42int∀ x43 . x43intx15 x42 x43 = x14 x42 x43)(∀ x42 . x42intx16 x42 = x42)x17 = 1(∀ x42 . x42int∀ x43 . x43intx18 x42 x43 = If_i (SNoLe x42 0) x43 (x15 (x18 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42intx19 x42 = x18 (x16 x42) x17)(∀ x42 . x42intx20 x42 = add_SNo (x19 x42) x42)(∀ x42 . x42int∀ x43 . x43intx21 x42 x43 = add_SNo x42 x43)(∀ x42 . x42int∀ x43 . x43intx22 x42 x43 = add_SNo x43 (minus_SNo 2))(∀ x42 . x42intx23 x42 = x42)(∀ x42 . x42int∀ x43 . x43intx24 x42 x43 = If_i (SNoLe x42 0) x43 (x21 (x24 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42int∀ x43 . x43intx25 x42 x43 = x24 (x22 x42 x43) (x23 x42))(∀ x42 . x42int∀ x43 . x43intx26 x42 x43 = add_SNo (x25 x42 x43) (minus_SNo x43))(∀ x42 . x42intx27 x42 = x42)x28 = 1(∀ x42 . x42int∀ x43 . x43intx29 x42 x43 = If_i (SNoLe x42 0) x43 (x26 (x29 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42intx30 x42 = x29 (x27 x42) x28)(∀ x42 . x42intx31 x42 = x30 x42)x32 = 1(∀ x42 . x42int∀ x43 . x43intx33 x42 x43 = x43)(∀ x42 . x42int∀ x43 . x43intx34 x42 x43 = If_i (SNoLe x42 0) x43 (x31 (x34 (add_SNo x42 (minus_SNo 1)) x43)))(∀ x42 . x42int∀ x43 . x43intx35 x42 x43 = x34 x32 (x33 x42 x43))(∀ x42 . x42int∀ x43 . x43intx36 x42 x43 = add_SNo (add_SNo (add_SNo (add_SNo (x35 x42 x43) x42) x42) x42) (If_i (SNoLe (add_SNo x42 (minus_SNo 1)) 0) 1 x42))(∀ x42 . x42intx37 x42 = x42)x38 = 1(∀ x42 . x42int∀ x43 . x43intx39 x42 x43 = If_i (SNoLe x42 0) x43 (x36 (x39 (add_SNo x42 (minus_SNo 1)) x43) x42))(∀ x42 . x42intx40 x42 = x39 (x37 x42) x38)(∀ x42 . x42intx41 x42 = x40 x42)∀ x42 . x42intSNoLe 0 x42x20 x42 = x41 x42
Conjecture f41ec..A261391 : ∀ 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 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo 2 (add_SNo x12 x13))(∀ x12 . x12intx1 x12 = mul_SNo x12 x12)x2 = 2(∀ 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 . x12intx5 x12 = add_SNo (mul_SNo (mul_SNo 2 (x4 x12)) x12) x12)(∀ x12 . x12intx6 x12 = add_SNo (mul_SNo x12 x12) x12)x7 = 1(∀ x12 . x12intx8 x12 = add_SNo 2 (mul_SNo x12 x12))(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 x7 (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo (mul_SNo (x10 x12) x12) (minus_SNo x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 4bddd..A26108 : ∀ 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 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ 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 = add_SNo (add_SNo x60 x60) x60)(∀ x60 . x60int∀ x61 . x61intx1 x60 x61 = add_SNo x61 x61)x2 = 1(∀ x60 . x60int∀ x61 . x61intx3 x60 x61 = If_i (SNoLe x60 0) x61 (x0 (x3 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60int∀ x61 . x61intx4 x60 x61 = x3 (x1 x60 x61) x2)(∀ x60 . x60int∀ x61 . x61intx5 x60 x61 = mul_SNo (add_SNo 2 x61) x60)x6 = 2(∀ x60 . x60intx7 x60 = x60)(∀ x60 . x60int∀ x61 . x61intx8 x60 x61 = If_i (SNoLe x60 0) x61 (x5 (x8 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60intx9 x60 = x8 x6 (x7 x60))(∀ x60 . x60int∀ x61 . x61intx10 x60 x61 = add_SNo (x4 x60 x61) (x9 x60))(∀ x60 . x60int∀ x61 . x61intx11 x60 x61 = x61)x12 = 1(∀ x60 . x60int∀ x61 . x61intx13 x60 x61 = If_i (SNoLe x60 0) x61 (x10 (x13 (add_SNo x60 (minus_SNo 1)) x61) x60))(∀ x60 . x60int∀ x61 . x61intx14 x60 x61 = x13 (x11 x60 x61) x12)(∀ x60 . x60int∀ x61 . x61intx15 x60 x61 = add_SNo (add_SNo (x14 x60 x61) (mul_SNo 2 (add_SNo 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) 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 . x60int∀ x61 . x61intx26 x60 x61 = add_SNo 1 (mul_SNo x60 x61))(∀ x60 . x60int∀ x61 . x61intx27 x60 x61 = x61)(∀ x60 . x60intx28 x60 = x60)x29 = 1x30 = add_SNo 2 (add_SNo 2 2)(∀ x60 . x60int∀ x61 . x61int∀ x62 . x62intx31 x60 x61 x62 = If_i (SNoLe x60 0) x61 (x26 (x31 (add_SNo x60 (minus_SNo 1)) x61 x62) (x32 (add_SNo x60 (minus_SNo 1)) x61 x62)))(∀ x60 . x60int∀ x61 . x61int∀ x62 . x62intx32 x60 x61 x62 = If_i (SNoLe x60 0) x62 (x27 (x31 (add_SNo x60 (minus_SNo 1)) x61 x62) (x32 (add_SNo x60 (minus_SNo 1)) x61 x62)))(∀ x60 . x60intx33 x60 = x31 (x28 x60) x29 x30)(∀ x60 . x60intx34 x60 = add_SNo x60 x60)(∀ x60 . x60intx35 x60 = x60)x36 = 1(∀ x60 . x60int∀ x61 . x61intx37 x60 x61 = If_i (SNoLe x60 0) x61 (x34 (x37 (add_SNo x60 (minus_SNo 1)) x61)))(∀ x60 . x60intx38 x60 = x37 (x35 x60) x36)(∀ x60 . x60intx39 x60 = mul_SNo (x33 x60) (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 (mul_SNo (add_SNo x60 x60) 2) 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 b9564..A25998 : ∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (x14 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50))))(∀ x50 . x50int∀ x51 . x51intx16 x50 x51 = x51)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx19 x50 x51 = x18 (x16 x50 x51) x17)(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (add_SNo (x19 x50 x51) x50) x50)(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50) x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = add_SNo 1 (mul_SNo 2 (add_SNo x51 x51)))(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 1 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = add_SNo x50 x50)(∀ x50 . x50intx35 x50 = x50)x36 = 1(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx38 x50 = x37 (x35 x50) x36)(∀ x50 . x50intx39 x50 = mul_SNo (x33 x50) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 4d3ad..A25995 : ∀ 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 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ 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 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = mul_SNo (add_SNo 2 x44) x43)x1 = 2(∀ x43 . x43intx2 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx4 x43 = x3 x1 (x2 x43))(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (add_SNo (x4 x43) (minus_SNo x43)) x44)(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x44)x8 = 1x9 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx10 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x5 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx11 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x6 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x10 (x7 x43 x44) x8 x9)(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (add_SNo (x12 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43)(∀ x43 . x43int∀ x44 . x44intx14 x43 x44 = x44)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = x16 (x14 x43 x44) x15)(∀ x43 . x43int∀ x44 . x44intx18 x43 x44 = add_SNo (add_SNo (x17 x43 x44) (mul_SNo 2 (add_SNo x43 x43))) x43)(∀ x43 . x43intx19 x43 = x43)x20 = 1(∀ x43 . x43int∀ x44 . x44intx21 x43 x44 = If_i (SNoLe x43 0) x44 (x18 (x21 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx22 x43 = x21 (x19 x43) x20)(∀ x43 . x43intx23 x43 = x22 x43)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43) x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx26 x43 x44 = x44)x27 = 1x28 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx31 x43 x44 = x29 (x26 x43 x44) x27 x28)(∀ x43 . x43int∀ x44 . x44intx32 x43 x44 = add_SNo (add_SNo (x31 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43)(∀ x43 . x43int∀ x44 . x44intx33 x43 x44 = x44)x34 = 1(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 (x33 x43 x44) x34)(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43))) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x23 x43 = x42 x43
Conjecture 41e98..A25994 : ∀ 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 = add_SNo (mul_SNo 2 (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) 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 1 (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) 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 3dd81..A25991 : ∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι → ι . (∀ x44 . x44int∀ x45 . x45intx43 x44 x45int)∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50intx0 x50 = mul_SNo 2 (add_SNo (add_SNo x50 x50) x50))(∀ x50 . x50intx1 x50 = x50)(∀ x50 . x50intx2 x50 = add_SNo x50 x50)(∀ x50 . x50intx3 x50 = x50)x4 = 2(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = If_i (SNoLe x50 0) x51 (x2 (x5 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx6 x50 = x5 (x3 x50) x4)(∀ x50 . x50intx7 x50 = add_SNo (x6 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x8 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx9 x50 = x8 (x1 x50) (x7 x50))(∀ x50 . x50intx10 x50 = x9 x50)x11 = 1(∀ x50 . x50int∀ x51 . x51intx12 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 x11 (x12 x50 x51))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (add_SNo (x14 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50int∀ x51 . x51intx16 x50 x51 = x51)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx19 x50 x51 = x18 (x16 x50 x51) x17)(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (add_SNo (x19 x50 x51) x50) x50)(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)) x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = add_SNo 1 (add_SNo (add_SNo x51 x51) x51))(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 2 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = add_SNo x50 x50)(∀ x50 . x50intx35 x50 = x50)x36 = 1(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx38 x50 = x37 (x35 x50) x36)(∀ x50 . x50intx39 x50 = mul_SNo (x33 x50) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 6e888..A25985 : ∀ 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 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ 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 . 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 . x56intx0 x55 x56 = mul_SNo (add_SNo 2 x56) x55)x1 = 2(∀ x55 . x55intx2 x55 = x55)(∀ x55 . x55int∀ x56 . x56intx3 x55 x56 = If_i (SNoLe x55 0) x56 (x0 (x3 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx4 x55 = x3 x1 (x2 x55))(∀ x55 . x55int∀ x56 . x56intx5 x55 x56 = add_SNo (add_SNo (x4 x55) (minus_SNo x55)) (mul_SNo x56 x56))(∀ x55 . x55int∀ x56 . x56intx6 x55 x56 = add_SNo x56 x56)(∀ x55 . x55int∀ x56 . x56intx7 x55 x56 = x56)x8 = 1x9 = 2(∀ x55 . x55int∀ x56 . x56int∀ x57 . x57intx10 x55 x56 x57 = If_i (SNoLe x55 0) x56 (x5 (x10 (add_SNo x55 (minus_SNo 1)) x56 x57) (x11 (add_SNo x55 (minus_SNo 1)) x56 x57)))(∀ x55 . x55int∀ x56 . x56int∀ x57 . x57intx11 x55 x56 x57 = If_i (SNoLe x55 0) x57 (x6 (x10 (add_SNo x55 (minus_SNo 1)) x56 x57) (x11 (add_SNo x55 (minus_SNo 1)) x56 x57)))(∀ x55 . x55int∀ x56 . x56intx12 x55 x56 = x10 (x7 x55 x56) x8 x9)(∀ x55 . x55int∀ x56 . x56intx13 x55 x56 = mul_SNo (add_SNo 2 x56) x55)x14 = 2(∀ x55 . x55intx15 x55 = x55)(∀ x55 . x55int∀ x56 . x56intx16 x55 x56 = If_i (SNoLe x55 0) x56 (x13 (x16 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx17 x55 = x16 x14 (x15 x55))(∀ x55 . x55int∀ x56 . x56intx18 x55 x56 = add_SNo (x12 x55 x56) (x17 x55))(∀ x55 . x55int∀ x56 . x56intx19 x55 x56 = x56)x20 = 1(∀ x55 . x55int∀ x56 . x56intx21 x55 x56 = If_i (SNoLe x55 0) x56 (x18 (x21 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55int∀ x56 . x56intx22 x55 x56 = x21 (x19 x55 x56) x20)(∀ x55 . x55int∀ x56 . x56intx23 x55 x56 = add_SNo (add_SNo (x22 x55 x56) x55) x55)(∀ x55 . x55intx24 x55 = x55)x25 = 1(∀ x55 . x55int∀ x56 . x56intx26 x55 x56 = If_i (SNoLe x55 0) x56 (x23 (x26 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx27 x55 = x26 (x24 x55) x25)(∀ x55 . x55intx28 x55 = x27 x55)(∀ x55 . x55intx29 x55 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x55 x55) x55)) (minus_SNo 1))(∀ x55 . x55intx30 x55 = x55)x31 = 2(∀ x55 . x55int∀ x56 . x56intx32 x55 x56 = If_i (SNoLe x55 0) x56 (x29 (x32 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55intx33 x55 = x32 (x30 x55) x31)(∀ x55 . x55intx34 x55 = add_SNo x55 x55)(∀ x55 . x55intx35 x55 = x55)x36 = 1(∀ x55 . x55int∀ x56 . x56intx37 x55 x56 = If_i (SNoLe x55 0) x56 (x34 (x37 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55intx38 x55 = x37 (x35 x55) x36)(∀ x55 . x55intx39 x55 = add_SNo x55 x55)(∀ x55 . x55intx40 x55 = x55)x41 = 1(∀ x55 . x55int∀ x56 . x56intx42 x55 x56 = If_i (SNoLe x55 0) x56 (x39 (x42 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55intx43 x55 = x42 (x40 x55) x41)(∀ x55 . x55intx44 x55 = mul_SNo (add_SNo (x33 x55) (minus_SNo (x38 x55))) (x43 x55))x45 = 1(∀ x55 . x55int∀ x56 . x56intx46 x55 x56 = x56)(∀ x55 . x55int∀ x56 . x56intx47 x55 x56 = If_i (SNoLe x55 0) x56 (x44 (x47 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55int∀ x56 . x56intx48 x55 x56 = x47 x45 (x46 x55 x56))(∀ x55 . x55int∀ x56 . x56intx49 x55 x56 = add_SNo (add_SNo (x48 x55 x56) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x55 x55)) x55))) x55)(∀ x55 . x55intx50 x55 = x55)x51 = 1(∀ x55 . x55int∀ x56 . x56intx52 x55 x56 = If_i (SNoLe x55 0) x56 (x49 (x52 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx53 x55 = x52 (x50 x55) x51)(∀ x55 . x55intx54 x55 = x53 x55)∀ x55 . x55intSNoLe 0 x55x28 x55 = x54 x55
Conjecture 83a44..A25968 : ∀ 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 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . 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 . x39intx0 x38 x39 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x38 x38) x39)) (minus_SNo 1)) x38)(∀ x38 . x38int∀ x39 . x39intx1 x38 x39 = add_SNo x39 x39)(∀ x38 . x38int∀ x39 . x39intx2 x38 x39 = x39)x3 = 1x4 = 2(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx5 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x0 (x5 (add_SNo x38 (minus_SNo 1)) x39 x40) (x6 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx6 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x1 (x5 (add_SNo x38 (minus_SNo 1)) x39 x40) (x6 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx7 x38 x39 = x5 (x2 x38 x39) x3 x4)(∀ x38 . x38int∀ x39 . x39intx8 x38 x39 = add_SNo (add_SNo (add_SNo (x7 x38 x39) x38) x38) x38)(∀ x38 . x38intx9 x38 = x38)x10 = 1(∀ x38 . x38int∀ x39 . x39intx11 x38 x39 = If_i (SNoLe x38 0) x39 (x8 (x11 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx12 x38 = x11 (x9 x38) x10)(∀ x38 . x38intx13 x38 = add_SNo x38 x38)(∀ x38 . x38intx14 x38 = x38)x15 = 1(∀ x38 . x38int∀ x39 . x39intx16 x38 x39 = If_i (SNoLe x38 0) x39 (x13 (x16 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx17 x38 = x16 (x14 x38) x15)(∀ x38 . x38intx18 x38 = mul_SNo (x12 x38) (x17 x38))(∀ x38 . x38int∀ x39 . x39intx19 x38 x39 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x38 x39)) (minus_SNo 1)) x38)(∀ x38 . x38int∀ x39 . x39intx20 x38 x39 = add_SNo x39 x39)(∀ x38 . x38int∀ x39 . x39intx21 x38 x39 = x39)x22 = 1x23 = 2(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx24 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x19 (x24 (add_SNo x38 (minus_SNo 1)) x39 x40) (x25 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx25 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x20 (x24 (add_SNo x38 (minus_SNo 1)) x39 x40) (x25 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39intx26 x38 x39 = x24 (x21 x38 x39) x22 x23)(∀ x38 . x38int∀ x39 . x39intx27 x38 x39 = add_SNo (add_SNo (x26 x38 x39) (mul_SNo 2 (add_SNo x38 x38))) x38)(∀ x38 . x38intx28 x38 = x38)x29 = 1(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = If_i (SNoLe x38 0) x39 (x27 (x30 (add_SNo x38 (minus_SNo 1)) x39) x38))(∀ x38 . x38intx31 x38 = x30 (x28 x38) x29)(∀ x38 . x38intx32 x38 = add_SNo x38 x38)(∀ x38 . x38intx33 x38 = x38)x34 = 1(∀ x38 . x38int∀ x39 . x39intx35 x38 x39 = If_i (SNoLe x38 0) x39 (x32 (x35 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx36 x38 = x35 (x33 x38) x34)(∀ x38 . x38intx37 x38 = mul_SNo (x31 x38) (x36 x38))∀ x38 . x38intSNoLe 0 x38x18 x38 = x37 x38
Conjecture 2899b..A25957 : ∀ 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 . x32int∀ x33 . x33intx31 x32 x33int)∀ 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 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 . x39int∀ 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 = mul_SNo (add_SNo 2 x49) x48)x1 = 2(∀ x48 . x48intx2 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx3 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x3 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx4 x48 = x3 x1 (x2 x48))(∀ x48 . x48int∀ x49 . x49intx5 x48 x49 = add_SNo (add_SNo (x4 x48) (minus_SNo x48)) x49)(∀ x48 . x48int∀ x49 . x49intx6 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx7 x48 x49 = x49)x8 = 1x9 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx10 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x5 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx11 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x6 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx12 x48 x49 = x10 (x7 x48 x49) x8 x9)(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = mul_SNo (add_SNo 2 x49) x48)x14 = 2(∀ x48 . x48intx15 x48 = x48)(∀ 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 (x15 x48))(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = add_SNo (x12 x48 x49) (x17 x48))(∀ x48 . x48int∀ x49 . x49intx19 x48 x49 = x49)x20 = 1(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48int∀ x49 . x49intx22 x48 x49 = x21 (x19 x48 x49) x20)(∀ x48 . x48int∀ x49 . x49intx23 x48 x49 = add_SNo (add_SNo (add_SNo (x22 x48 x49) x48) x48) x48)(∀ x48 . x48intx24 x48 = x48)x25 = 1(∀ x48 . x48int∀ x49 . x49intx26 x48 x49 = If_i (SNoLe x48 0) x49 (x23 (x26 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx27 x48 = x26 (x24 x48) x25)(∀ x48 . x48intx28 x48 = x27 x48)(∀ x48 . x48int∀ x49 . x49intx29 x48 x49 = add_SNo (add_SNo (add_SNo x48 x48) x48) x49)(∀ x48 . x48int∀ x49 . x49intx30 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx31 x48 x49 = x49)x32 = 1x33 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx34 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x29 (x34 (add_SNo x48 (minus_SNo 1)) x49 x50) (x35 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx35 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x30 (x34 (add_SNo x48 (minus_SNo 1)) x49 x50) (x35 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx36 x48 x49 = x34 (x31 x48 x49) x32 x33)(∀ x48 . x48int∀ x49 . x49intx37 x48 x49 = add_SNo (x36 x48 x49) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48))))(∀ x48 . x48int∀ x49 . x49intx38 x48 x49 = x49)x39 = 1(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 (x38 x48 x49) x39)(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48))) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 1(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x28 x48 = x47 x48
Conjecture b790a..A25956 : ∀ 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 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ 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 . 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 (mul_SNo 2 (add_SNo x48 x48)) x48)) 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 = mul_SNo (add_SNo 2 x49) x48)x9 = 2(∀ x48 . x48intx10 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx11 x48 x49 = If_i (SNoLe x48 0) x49 (x8 (x11 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx12 x48 = x11 x9 (x10 x48))(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = add_SNo (x7 x48 x49) (x12 x48))(∀ x48 . x48int∀ x49 . x49intx14 x48 x49 = x49)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 . x48int∀ x49 . x49intx17 x48 x49 = x16 (x14 x48 x49) x15)(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = add_SNo (add_SNo (add_SNo (x17 x48 x49) x48) x48) x48)(∀ x48 . x48intx19 x48 = x48)x20 = 1(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx22 x48 = x21 (x19 x48) x20)(∀ x48 . x48intx23 x48 = x22 x48)(∀ x48 . x48int∀ x49 . x49intx24 x48 x49 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48)) x49)(∀ x48 . x48int∀ x49 . x49intx25 x48 x49 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x49 x49)) x49))(∀ x48 . x48intx26 x48 = x48)x27 = 1x28 = add_SNo 2 (add_SNo 2 2)(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx29 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x24 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx30 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x25 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx31 x48 = x29 (x26 x48) x27 x28)(∀ 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 (add_SNo (x41 x48 x49) 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 x48x23 x48 = x47 x48
Conjecture 93d3d..A25955 : ∀ 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 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ 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 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = mul_SNo (add_SNo 2 x44) x43)x1 = 2(∀ x43 . x43intx2 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx4 x43 = x3 x1 (x2 x43))(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (add_SNo (x4 x43) (minus_SNo x43)) x44)(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x44)x8 = 1x9 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx10 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x5 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx11 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x6 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x10 (x7 x43 x44) x8 x9)(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (x12 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)))(∀ x43 . x43int∀ x44 . x44intx14 x43 x44 = x44)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = x16 (x14 x43 x44) x15)(∀ x43 . x43int∀ x44 . x44intx18 x43 x44 = add_SNo (add_SNo (add_SNo (x17 x43 x44) x43) x43) x43)(∀ x43 . x43intx19 x43 = x43)x20 = 1(∀ x43 . x43int∀ x44 . x44intx21 x43 x44 = If_i (SNoLe x43 0) x44 (x18 (x21 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx22 x43 = x21 (x19 x43) x20)(∀ x43 . x43intx23 x43 = x22 x43)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = add_SNo (add_SNo (add_SNo x43 x43) x43) x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx26 x43 x44 = x44)x27 = 1x28 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx31 x43 x44 = x29 (x26 x43 x44) x27 x28)(∀ x43 . x43int∀ x44 . x44intx32 x43 x44 = add_SNo (x31 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)))(∀ x43 . x43int∀ x44 . x44intx33 x43 x44 = x44)x34 = 1(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 (x33 x43 x44) x34)(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43))) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x23 x43 = x42 x43
Conjecture d06e2..A259546 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx1 x18 = x18)(∀ x18 . x18intx2 x18 = x18)x3 = 0(∀ 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)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 (x4 x18))(∀ x18 . x18intx8 x18 = mul_SNo (mul_SNo x18 x18) (x7 x18))(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = add_SNo x18 (minus_SNo 2))(∀ x18 . x18intx12 x18 = x18)(∀ x18 . x18intx13 x18 = x18)(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) (x12 x18) (x13 x18))(∀ x18 . x18intx17 x18 = mul_SNo (mul_SNo x18 x18) (x16 x18))∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 1b967..A25951 : ∀ 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 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ 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 . 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 = mul_SNo (add_SNo 2 x49) x48)x1 = 2(∀ x48 . x48intx2 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx3 x48 x49 = If_i (SNoLe x48 0) x49 (x0 (x3 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx4 x48 = x3 x1 (x2 x48))(∀ x48 . x48int∀ x49 . x49intx5 x48 x49 = add_SNo (x4 x48) (mul_SNo (mul_SNo x49 x49) x49))(∀ x48 . x48int∀ x49 . x49intx6 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx7 x48 x49 = x49)x8 = 1x9 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx10 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x5 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx11 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x6 (x10 (add_SNo x48 (minus_SNo 1)) x49 x50) (x11 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx12 x48 x49 = x10 (x7 x48 x49) x8 x9)(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = add_SNo (add_SNo (x12 x48 x49) x48) x48)(∀ x48 . x48int∀ x49 . x49intx14 x48 x49 = x49)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 . x48int∀ x49 . x49intx17 x48 x49 = x16 (x14 x48 x49) x15)(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = add_SNo (add_SNo (add_SNo (x17 x48 x49) x48) x48) x48)(∀ x48 . x48intx19 x48 = x48)x20 = 1(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx22 x48 = x21 (x19 x48) x20)(∀ x48 . x48intx23 x48 = x22 x48)(∀ x48 . x48int∀ x49 . x49intx24 x48 x49 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x48 x48) x48)) x49)(∀ x48 . x48int∀ x49 . x49intx25 x48 x49 = add_SNo 1 (mul_SNo 2 (add_SNo x49 x49)))(∀ x48 . x48intx26 x48 = x48)x27 = 1x28 = add_SNo 1 (add_SNo 2 2)(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx29 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x24 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx30 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x25 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx31 x48 = x29 (x26 x48) x27 x28)(∀ 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 (add_SNo (x41 x48 x49) 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 x48x23 x48 = x47 x48
Conjecture b6269..A25940 : ∀ 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 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43)) x44)(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx2 x43 x44 = x44)x3 = 1x4 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx5 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x0 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx6 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x1 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x5 (x2 x43 x44) x3 x4)(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = add_SNo (x7 x43 x44) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)))(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = x44)x10 = 1(∀ x43 . x43int∀ x44 . x44intx11 x43 x44 = If_i (SNoLe x43 0) x44 (x8 (x11 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x11 (x9 x43 x44) x10)(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (add_SNo (add_SNo (x12 x43 x44) x43) x43) x43)(∀ x43 . x43intx14 x43 = x43)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx17 x43 = x16 (x14 x43) x15)(∀ x43 . x43intx18 x43 = x17 x43)(∀ x43 . x43int∀ x44 . x44intx19 x43 x44 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43) x44)(∀ x43 . x43int∀ x44 . x44intx20 x43 x44 = add_SNo 1 (add_SNo (add_SNo x44 x44) x44))(∀ x43 . x43intx21 x43 = x43)x22 = 1x23 = add_SNo 2 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx24 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x19 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx25 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x20 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx26 x43 = x24 (x21 x43) x22 x23)(∀ x43 . x43intx27 x43 = add_SNo x43 x43)(∀ x43 . x43intx28 x43 = x43)x29 = 1(∀ x43 . x43int∀ x44 . x44intx30 x43 x44 = If_i (SNoLe x43 0) x44 (x27 (x30 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx31 x43 = x30 (x28 x43) x29)(∀ x43 . x43intx32 x43 = mul_SNo (x26 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (add_SNo (x36 x43 x44) x43) x43) x43)(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x18 x43 = x42 x43
Conjecture 27c8c..A25937 : ∀ 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 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 . x23int∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45int∀ x46 . x46intx0 x45 x46 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) x46)(∀ x45 . x45int∀ x46 . x46intx1 x45 x46 = add_SNo x46 x46)(∀ x45 . x45int∀ x46 . x46intx2 x45 x46 = x46)x3 = 1x4 = 2(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx5 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x0 (x5 (add_SNo x45 (minus_SNo 1)) x46 x47) (x6 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx6 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x1 (x5 (add_SNo x45 (minus_SNo 1)) x46 x47) (x6 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46intx7 x45 x46 = x5 (x2 x45 x46) x3 x4)(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = add_SNo (add_SNo (x7 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x45)(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x46)x10 = 1(∀ x45 . x45int∀ x46 . x46intx11 x45 x46 = If_i (SNoLe x45 0) x46 (x8 (x11 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx12 x45 x46 = x11 (x9 x45 x46) x10)(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = add_SNo (add_SNo (add_SNo (x12 x45 x46) x45) x45) x45)(∀ x45 . x45intx14 x45 = x45)x15 = 1(∀ x45 . x45int∀ x46 . x46intx16 x45 x46 = If_i (SNoLe x45 0) x46 (x13 (x16 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx17 x45 = x16 (x14 x45) x15)(∀ x45 . x45intx18 x45 = x17 x45)(∀ x45 . x45intx19 x45 = add_SNo (add_SNo x45 x45) x45)(∀ x45 . x45intx20 x45 = x45)(∀ x45 . x45intx21 x45 = add_SNo x45 x45)(∀ x45 . x45intx22 x45 = x45)x23 = 2(∀ x45 . x45int∀ x46 . x46intx24 x45 x46 = If_i (SNoLe x45 0) x46 (x21 (x24 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx25 x45 = x24 (x22 x45) x23)(∀ x45 . x45intx26 x45 = add_SNo (x25 x45) (minus_SNo 1))(∀ x45 . x45int∀ x46 . x46intx27 x45 x46 = If_i (SNoLe x45 0) x46 (x19 (x27 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx28 x45 = x27 (x20 x45) (x26 x45))(∀ x45 . x45intx29 x45 = x28 x45)x30 = 1(∀ x45 . x45int∀ x46 . x46intx31 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx33 x45 x46 = x32 x30 (x31 x45 x46))(∀ x45 . x45int∀ x46 . x46intx34 x45 x46 = add_SNo (add_SNo (x33 x45 x46) x45) x45)(∀ x45 . x45int∀ x46 . x46intx35 x45 x46 = x46)x36 = 1(∀ x45 . x45int∀ x46 . x46intx37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx38 x45 x46 = x37 (x35 x45 x46) x36)(∀ x45 . x45int∀ x46 . x46intx39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x45)(∀ x45 . x45intx40 x45 = x45)x41 = 1(∀ x45 . x45int∀ x46 . x46intx42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = x43 x45)∀ x45 . x45intSNoLe 0 x45x18 x45 = x44 x45
Conjecture 70e65..A25936 : ∀ 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 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ 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 . x27int∀ x28 . x28intx26 x27 x28int)∀ 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 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι → ι . (∀ x34 . x34int∀ x35 . x35intx33 x34 x35int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = mul_SNo (add_SNo 2 x44) x43)x1 = 2(∀ x43 . x43intx2 x43 = x43)(∀ x43 . x43int∀ x44 . x44intx3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx4 x43 = x3 x1 (x2 x43))(∀ x43 . x43int∀ x44 . x44intx5 x43 x44 = add_SNo (x4 x43) x44)(∀ x43 . x43int∀ x44 . x44intx6 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x44)x8 = 1x9 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx10 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x5 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx11 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x6 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x10 (x7 x43 x44) x8 x9)(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (add_SNo (x12 x43 x44) (mul_SNo 2 (add_SNo x43 x43))) x43)(∀ x43 . x43int∀ x44 . x44intx14 x43 x44 = x44)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx17 x43 x44 = x16 (x14 x43 x44) x15)(∀ x43 . x43int∀ x44 . x44intx18 x43 x44 = add_SNo (add_SNo (add_SNo (x17 x43 x44) x43) x43) x43)(∀ x43 . x43intx19 x43 = x43)x20 = 1(∀ x43 . x43int∀ x44 . x44intx21 x43 x44 = If_i (SNoLe x43 0) x44 (x18 (x21 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx22 x43 = x21 (x19 x43) x20)(∀ x43 . x43intx23 x43 = x22 x43)(∀ x43 . x43int∀ x44 . x44intx24 x43 x44 = add_SNo (add_SNo (add_SNo x43 x43) x43) x44)(∀ x43 . x43int∀ x44 . x44intx25 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx26 x43 x44 = x44)x27 = 1x28 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx29 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x24 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx30 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x25 (x29 (add_SNo x43 (minus_SNo 1)) x44 x45) (x30 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx31 x43 x44 = x29 (x26 x43 x44) x27 x28)(∀ x43 . x43int∀ x44 . x44intx32 x43 x44 = add_SNo (add_SNo (x31 x43 x44) (mul_SNo 2 (add_SNo x43 x43))) x43)(∀ x43 . x43int∀ x44 . x44intx33 x43 x44 = x44)x34 = 1(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 (x33 x43 x44) x34)(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (x36 x43 x44) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))))(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x23 x43 = x42 x43
Conjecture 9662e..A259319 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20intx0 x20 = mul_SNo x20 x20)x1 = 2(∀ x20 . x20int∀ x21 . x21intx2 x20 x21 = add_SNo 1 (add_SNo x21 x21))(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20int∀ x21 . x21intx4 x20 x21 = x3 x1 (x2 x20 x21))(∀ x20 . x20int∀ x21 . x21intx5 x20 x21 = add_SNo (x4 x20 x21) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = mul_SNo (x9 x20) 2)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo (mul_SNo (mul_SNo (mul_SNo x21 x21) x21) x21) x20)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo 2 x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 2(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = mul_SNo (x18 x20) 2)∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 419f5..A25929 : ∀ 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 2 (add_SNo (mul_SNo x34 x34) x33)) (minus_SNo x34)) 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) (x12 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 2 (add_SNo (mul_SNo x34 x34) x33)) (minus_SNo x34)) 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 (x26 x33 x34) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo 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
Conjecture ffac1..A257583 : ∀ 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 . x8intx7 x8int)∀ x8 . x8int∀ 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 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25int∀ x26 . x26intx0 x25 x26 = mul_SNo 2 (mul_SNo x25 x26))(∀ x25 . x25intx1 x25 = add_SNo x25 x25)x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx4 x25 = x3 (x1 x25) x2)(∀ x25 . x25intx5 x25 = mul_SNo 2 (x4 x25))(∀ x25 . x25int∀ x26 . x26intx6 x25 x26 = mul_SNo 2 (mul_SNo x25 x26))(∀ x25 . x25intx7 x25 = x25)x8 = 2(∀ x25 . x25int∀ x26 . x26intx9 x25 x26 = If_i (SNoLe x25 0) x26 (x6 (x9 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx10 x25 = x9 (x7 x25) x8)(∀ x25 . x25intx11 x25 = add_SNo x25 x25)(∀ x25 . x25intx12 x25 = x25)x13 = 1(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx15 x25 = x14 (x12 x25) x13)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = add_SNo 1 x26)(∀ x25 . x25intx18 x25 = x25)x19 = 1(∀ x25 . x25intx20 x25 = add_SNo 1 x25)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 (x20 x25))(∀ x25 . x25intx24 x25 = mul_SNo (mul_SNo (mul_SNo 2 (x10 x25)) (x15 x25)) (x23 x25))∀ x25 . x25intSNoLe 0 x25x5 x25 = x24 x25