Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrLEg../d0136..
PUQFh../fa2b5..
vout
PrLEg../c03cb.. 0.04 bars
PUTJ2../85a61.. doc published by PrGxv..
Param intint : ι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param add_SNoadd_SNo : ιιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Conjecture edba2..A28144 : ∀ 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 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 . x30int∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι . (∀ x36 . x36intx35 x36int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 . x37int∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 . x43int∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι . (∀ x46 . x46intx45 x46int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)∀ x48 . x48int∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 . x52int∀ x53 : ι → ι → ι . (∀ x54 . x54int∀ x55 . x55intx53 x54 x55int)∀ x54 : ι → ι → ι . (∀ x55 . x55int∀ x56 . x56intx54 x55 x56int)∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι → ι . (∀ x57 . x57int∀ x58 . x58intx56 x57 x58int)∀ x57 : ι → ι . (∀ x58 . x58intx57 x58int)∀ x58 . x58int∀ x59 : ι → ι → ι . (∀ x60 . x60int∀ x61 . x61intx59 x60 x61int)∀ x60 : ι → ι . (∀ x61 . x61intx60 x61int)∀ x61 : ι → ι . (∀ x62 . x62intx61 x62int)(∀ x62 . x62intx0 x62 = mul_SNo 2 (add_SNo (add_SNo x62 x62) x62))(∀ x62 . x62intx1 x62 = x62)(∀ x62 . x62intx2 x62 = add_SNo x62 x62)(∀ x62 . x62intx3 x62 = x62)x4 = 2(∀ x62 . x62int∀ x63 . x63intx5 x62 x63 = If_i (SNoLe x62 0) x63 (x2 (x5 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62intx6 x62 = x5 (x3 x62) x4)(∀ x62 . x62intx7 x62 = add_SNo (x6 x62) (minus_SNo 1))(∀ x62 . x62int∀ x63 . x63intx8 x62 x63 = If_i (SNoLe x62 0) x63 (x0 (x8 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62intx9 x62 = x8 (x1 x62) (x7 x62))(∀ x62 . x62intx10 x62 = x9 x62)x11 = 1(∀ x62 . x62int∀ x63 . x63intx12 x62 x63 = x63)(∀ x62 . x62int∀ x63 . x63intx13 x62 x63 = If_i (SNoLe x62 0) x63 (x10 (x13 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62int∀ x63 . x63intx14 x62 x63 = x13 x11 (x12 x62 x63))(∀ x62 . x62int∀ x63 . x63intx15 x62 x63 = add_SNo (x14 x62 x63) (mul_SNo 2 (add_SNo x62 x62)))(∀ x62 . x62int∀ x63 . x63intx16 x62 x63 = x63)x17 = 1(∀ x62 . x62int∀ x63 . x63intx18 x62 x63 = If_i (SNoLe x62 0) x63 (x15 (x18 (add_SNo x62 (minus_SNo 1)) x63) x62))(∀ x62 . x62int∀ x63 . x63intx19 x62 x63 = x18 (x16 x62 x63) x17)(∀ x62 . x62int∀ x63 . x63intx20 x62 x63 = add_SNo (add_SNo (x19 x62 x63) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x62 x62)) x62))) x62)(∀ x62 . x62intx21 x62 = x62)x22 = 1(∀ x62 . x62int∀ x63 . x63intx23 x62 x63 = If_i (SNoLe x62 0) x63 (x20 (x23 (add_SNo x62 (minus_SNo 1)) x63) x62))(∀ x62 . x62intx24 x62 = x23 (x21 x62) x22)(∀ x62 . x62intx25 x62 = x24 x62)(∀ x62 . x62intx26 x62 = add_SNo (add_SNo x62 x62) x62)(∀ x62 . x62intx27 x62 = x62)(∀ x62 . x62intx28 x62 = add_SNo x62 x62)(∀ x62 . x62intx29 x62 = x62)x30 = 2(∀ x62 . x62int∀ x63 . x63intx31 x62 x63 = If_i (SNoLe x62 0) x63 (x28 (x31 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62intx32 x62 = x31 (x29 x62) x30)(∀ x62 . x62intx33 x62 = add_SNo (x32 x62) (minus_SNo 1))(∀ x62 . x62int∀ x63 . x63intx34 x62 x63 = If_i (SNoLe x62 0) x63 (x26 (x34 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62intx35 x62 = x34 (x27 x62) (x33 x62))(∀ x62 . x62intx36 x62 = x35 x62)x37 = 1(∀ x62 . x62int∀ x63 . x63intx38 x62 x63 = x63)(∀ x62 . x62int∀ x63 . x63intx39 x62 x63 = If_i (SNoLe x62 0) x63 (x36 (x39 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62int∀ x63 . x63intx40 x62 x63 = x39 x37 (x38 x62 x63))(∀ x62 . x62int∀ x63 . x63intx41 x62 x63 = add_SNo (add_SNo (x40 x62 x63) x62) x62)(∀ x62 . x62intx42 x62 = x62)x43 = 1(∀ x62 . x62int∀ x63 . x63intx44 x62 x63 = If_i (SNoLe x62 0) x63 (x41 (x44 (add_SNo x62 (minus_SNo 1)) x63) x62))(∀ x62 . x62intx45 x62 = x44 (x42 x62) x43)(∀ x62 . x62intx46 x62 = add_SNo x62 x62)(∀ x62 . x62intx47 x62 = x62)x48 = 1(∀ x62 . x62int∀ x63 . x63intx49 x62 x63 = If_i (SNoLe x62 0) x63 (x46 (x49 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62intx50 x62 = x49 (x47 x62) x48)(∀ x62 . x62intx51 x62 = mul_SNo (x45 x62) (x50 x62))x52 = 1(∀ x62 . x62int∀ x63 . x63intx53 x62 x63 = x63)(∀ x62 . x62int∀ x63 . x63intx54 x62 x63 = If_i (SNoLe x62 0) x63 (x51 (x54 (add_SNo x62 (minus_SNo 1)) x63)))(∀ x62 . x62int∀ x63 . x63intx55 x62 x63 = x54 x52 (x53 x62 x63))(∀ x62 . x62int∀ x63 . x63intx56 x62 x63 = add_SNo (add_SNo (x55 x62 x63) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x62 x62)) x62))) x62)(∀ x62 . x62intx57 x62 = x62)x58 = 1(∀ x62 . x62int∀ x63 . x63intx59 x62 x63 = If_i (SNoLe x62 0) x63 (x56 (x59 (add_SNo x62 (minus_SNo 1)) x63) x62))(∀ x62 . x62intx60 x62 = x59 (x57 x62) x58)(∀ x62 . x62intx61 x62 = x60 x62)∀ x62 . x62intSNoLe 0 x62x25 x62 = x61 x62
Conjecture efe6e..A28141 : ∀ 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 (x17 x51 x52) (mul_SNo 2 (add_SNo 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 (x44 x51 x52) (mul_SNo 2 (add_SNo 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 74c7e..A28139 : ∀ 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 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . 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 . 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 (add_SNo x50 x50) x50)(∀ x50 . x50int∀ x51 . x51intx1 x50 x51 = add_SNo x51 x51)x2 = 1(∀ x50 . x50int∀ x51 . x51intx3 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x3 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx4 x50 x51 = x3 (x1 x50 x51) x2)(∀ x50 . x50int∀ x51 . x51intx5 x50 x51 = add_SNo (x4 x50 x51) (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)))(∀ x50 . x50int∀ x51 . x51intx6 x50 x51 = x51)x7 = 1(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = If_i (SNoLe x50 0) x51 (x5 (x8 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx9 x50 x51 = x8 (x6 x50 x51) x7)(∀ x50 . x50int∀ x51 . x51intx10 x50 x51 = add_SNo (x9 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50)))(∀ x50 . x50int∀ x51 . x51intx11 x50 x51 = x51)x12 = 1(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x13 (x11 x50 x51) x12)(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (x14 x50 x51) (mul_SNo 2 (add_SNo x50 x50)))(∀ x50 . x50intx16 x50 = x50)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx19 x50 = x18 (x16 x50) x17)(∀ x50 . x50intx20 x50 = x19 x50)(∀ x50 . x50int∀ x51 . x51intx21 x50 x51 = add_SNo (add_SNo (add_SNo x50 x50) x50) x51)(∀ x50 . x50int∀ x51 . x51intx22 x50 x51 = add_SNo x51 x51)(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = x51)x24 = 1x25 = 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx26 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x21 (x26 (add_SNo x50 (minus_SNo 1)) x51 x52) (x27 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx27 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x22 (x26 (add_SNo x50 (minus_SNo 1)) x51 x52) (x27 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51intx28 x50 x51 = x26 (x23 x50 x51) x24 x25)(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = add_SNo (add_SNo (x28 x50 x51) (mul_SNo 2 (add_SNo x50 x50))) x50)(∀ x50 . x50intx30 x50 = x50)x31 = 1(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = If_i (SNoLe x50 0) x51 (x29 (x32 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx33 x50 = x32 (x30 x50) x31)(∀ 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 (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 x50x20 x50 = x49 x50
Conjecture e0a40..A28130 : ∀ 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 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι → ι . (∀ x32 . x32int∀ x33 . x33intx31 x32 x33int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)(∀ x38 . x38int∀ x39 . x39intx0 x38 x39 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x39 (minus_SNo 1)) x39) (mul_SNo x39 x39)) x38) (mul_SNo 2 (add_SNo (add_SNo x38 x38) 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 (x7 x38 x39) (mul_SNo 2 (add_SNo (add_SNo 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 = x12 x38)(∀ x38 . x38int∀ x39 . x39intx14 x38 x39 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo x39 x39) x38)) (minus_SNo x39)) x38)(∀ x38 . x38int∀ x39 . x39intx15 x38 x39 = add_SNo x39 x39)(∀ x38 . x38intx16 x38 = x38)x17 = 1x18 = 2(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx19 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x14 (x19 (add_SNo x38 (minus_SNo 1)) x39 x40) (x20 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38int∀ x39 . x39int∀ x40 . x40intx20 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x15 (x19 (add_SNo x38 (minus_SNo 1)) x39 x40) (x20 (add_SNo x38 (minus_SNo 1)) x39 x40)))(∀ x38 . x38intx21 x38 = x19 (x16 x38) x17 x18)(∀ x38 . x38intx22 x38 = add_SNo x38 x38)(∀ x38 . x38intx23 x38 = x38)x24 = 1(∀ x38 . x38int∀ x39 . x39intx25 x38 x39 = If_i (SNoLe x38 0) x39 (x22 (x25 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38intx26 x38 = x25 (x23 x38) x24)(∀ x38 . x38intx27 x38 = mul_SNo (x21 x38) (x26 x38))x28 = 1(∀ x38 . x38int∀ x39 . x39intx29 x38 x39 = x39)(∀ x38 . x38int∀ x39 . x39intx30 x38 x39 = If_i (SNoLe x38 0) x39 (x27 (x30 (add_SNo x38 (minus_SNo 1)) x39)))(∀ x38 . x38int∀ x39 . x39intx31 x38 x39 = x30 x28 (x29 x38 x39))(∀ x38 . x38int∀ x39 . x39intx32 x38 x39 = add_SNo (add_SNo (x31 x38 x39) (mul_SNo 2 (add_SNo (add_SNo x38 x38) 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))(∀ x38 . x38intx36 x38 = x35 (x33 x38) x34)(∀ x38 . x38intx37 x38 = x36 x38)∀ x38 . x38intSNoLe 0 x38x13 x38 = x37 x38
Conjecture c88a9..A28122 : ∀ 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 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 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
Conjecture c8ccf..A28120 : ∀ 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 . x9intx8 x9int)∀ 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 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 . x33intx8 x33 = add_SNo (add_SNo x33 x33) 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 . 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 (add_SNo (add_SNo x34 (minus_SNo 1)) x34) (mul_SNo x34 x34)) x33) (mul_SNo 2 (add_SNo 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 (mul_SNo 2 (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 dd706..A28118 : ∀ 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)) (mul_SNo x44 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)) (mul_SNo x44 x44)) x43)(∀ 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 900e2..A28117 : ∀ 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 (x14 x60 x61) (mul_SNo 2 (add_SNo 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 (add_SNo x60 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 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 (x43 x60 x61) (mul_SNo 2 (add_SNo 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) (mul_SNo 2 (add_SNo (add_SNo x60 x60) x60))) x60)(∀ 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 3f660..A28115 : ∀ 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 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 . x18int∀ x19 : ι → ι → ι → ι . (∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx19 x20 x21 x22int)∀ x20 : ι → ι → ι → ι . (∀ x21 . x21int∀ x22 . x22int∀ x23 . x23intx20 x21 x22 x23int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28int∀ x29 . x29intx0 x28 x29 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x29 (minus_SNo 1)) x29) (mul_SNo x29 x29)) x28) (mul_SNo 2 (add_SNo (add_SNo x28 x28) x28)))(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = add_SNo x29 x29)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = x29)x3 = 1x4 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx5 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x0 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30) (x6 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx6 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x1 (x5 (add_SNo x28 (minus_SNo 1)) x29 x30) (x6 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29intx7 x28 x29 = x5 (x2 x28 x29) x3 x4)(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = add_SNo (add_SNo (x7 x28 x29) (mul_SNo 2 (add_SNo x28 x28))) x28)(∀ x28 . x28intx9 x28 = x28)x10 = 1(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = If_i (SNoLe x28 0) x29 (x8 (x11 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx12 x28 = x11 (x9 x28) x10)(∀ x28 . x28intx13 x28 = x12 x28)(∀ x28 . x28int∀ x29 . x29intx14 x28 x29 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x29 (minus_SNo 1)) x29) (mul_SNo x29 x29)) x28) (mul_SNo 2 (add_SNo x28 x28)))(∀ x28 . x28int∀ x29 . x29intx15 x28 x29 = add_SNo x29 x29)(∀ x28 . x28int∀ x29 . x29intx16 x28 x29 = x29)x17 = 1x18 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29intx21 x28 x29 = x19 (x16 x28 x29) x17 x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = add_SNo (add_SNo (x21 x28 x29) (mul_SNo 2 (add_SNo (add_SNo x28 x28) x28))) x28)(∀ x28 . x28intx23 x28 = x28)x24 = 1(∀ x28 . x28int∀ x29 . x29intx25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28))(∀ x28 . x28intx26 x28 = x25 (x23 x28) x24)(∀ x28 . x28intx27 x28 = x26 x28)∀ x28 . x28intSNoLe 0 x28x13 x28 = x27 x28
Conjecture 6fbd1..A28112 : ∀ 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 (x14 x60 x61) (mul_SNo 2 (add_SNo 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 (x19 x60 x61) (mul_SNo 2 (add_SNo (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 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 (x43 x60 x61) (mul_SNo 2 (add_SNo 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 (x53 x60 x61) (mul_SNo 2 (add_SNo (add_SNo x60 x60) x60)))(∀ 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 6d529..A28106 : ∀ 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 . 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 . x53intx0 x53 = add_SNo (add_SNo x53 x53) x53)(∀ x53 . x53int∀ x54 . x54intx1 x53 x54 = add_SNo x54 x54)x2 = 1(∀ x53 . x53int∀ x54 . x54intx3 x53 x54 = If_i (SNoLe x53 0) x54 (x0 (x3 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53int∀ x54 . x54intx4 x53 x54 = x3 (x1 x53 x54) x2)(∀ x53 . x53int∀ x54 . x54intx5 x53 x54 = add_SNo (x4 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53)))(∀ x53 . x53int∀ x54 . x54intx6 x53 x54 = x54)x7 = 1(∀ x53 . x53int∀ x54 . x54intx8 x53 x54 = If_i (SNoLe x53 0) x54 (x5 (x8 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53int∀ x54 . x54intx9 x53 x54 = x8 (x6 x53 x54) x7)(∀ x53 . x53int∀ x54 . x54intx10 x53 x54 = mul_SNo (add_SNo 2 x54) x53)x11 = 2(∀ x53 . x53intx12 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx13 x53 x54 = If_i (SNoLe x53 0) x54 (x10 (x13 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx14 x53 = x13 x11 (x12 x53))(∀ x53 . x53int∀ x54 . x54intx15 x53 x54 = add_SNo (x9 x53 x54) (x14 x53))(∀ x53 . x53int∀ x54 . x54intx16 x53 x54 = x54)x17 = 1(∀ x53 . x53int∀ x54 . x54intx18 x53 x54 = If_i (SNoLe x53 0) x54 (x15 (x18 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53int∀ x54 . x54intx19 x53 x54 = x18 (x16 x53 x54) x17)(∀ x53 . x53int∀ x54 . x54intx20 x53 x54 = add_SNo (add_SNo (add_SNo (x19 x53 x54) x53) x53) x53)(∀ x53 . x53intx21 x53 = x53)x22 = 1(∀ x53 . x53int∀ x54 . x54intx23 x53 x54 = If_i (SNoLe x53 0) x54 (x20 (x23 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx24 x53 = x23 (x21 x53) x22)(∀ x53 . x53intx25 x53 = x24 x53)(∀ x53 . x53int∀ x54 . x54intx26 x53 x54 = add_SNo (mul_SNo 2 (add_SNo x53 x53)) x54)(∀ x53 . x53int∀ x54 . x54intx27 x53 x54 = add_SNo 1 (add_SNo (add_SNo x54 x54) x54))(∀ x53 . x53intx28 x53 = x53)x29 = 1x30 = add_SNo 2 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx31 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x26 (x31 (add_SNo x53 (minus_SNo 1)) x54 x55) (x32 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx32 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x27 (x31 (add_SNo x53 (minus_SNo 1)) x54 x55) (x32 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx33 x53 = x31 (x28 x53) x29 x30)(∀ x53 . x53int∀ x54 . x54intx34 x53 x54 = mul_SNo x53 x54)(∀ x53 . x53int∀ x54 . x54intx35 x53 x54 = x54)(∀ x53 . x53intx36 x53 = x53)x37 = 1x38 = add_SNo 1 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx39 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x34 (x39 (add_SNo x53 (minus_SNo 1)) x54 x55) (x40 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx40 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x35 (x39 (add_SNo x53 (minus_SNo 1)) x54 x55) (x40 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx41 x53 = x39 (x36 x53) x37 x38)(∀ x53 . x53intx42 x53 = mul_SNo (x33 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 (x46 x53 x54) (mul_SNo 2 (add_SNo (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 x53x25 x53 = x52 x53
Conjecture d24e4..A28081 : ∀ 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 . 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 . x32intx31 x32int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ 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 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50int∀ x51 . x51intx0 x50 x51 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)) (mul_SNo (mul_SNo x51 x51) x51))(∀ x50 . x50int∀ x51 . x51intx1 x50 x51 = add_SNo x51 x51)(∀ x50 . x50int∀ x51 . x51intx2 x50 x51 = x51)x3 = 1x4 = 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx5 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x0 (x5 (add_SNo x50 (minus_SNo 1)) x51 x52) (x6 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx6 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x1 (x5 (add_SNo x50 (minus_SNo 1)) x51 x52) (x6 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51intx7 x50 x51 = x5 (x2 x50 x51) x3 x4)(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = mul_SNo (add_SNo 2 x51) x50)x9 = 2(∀ x50 . x50intx10 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx11 x50 x51 = If_i (SNoLe x50 0) x51 (x8 (x11 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx12 x50 = x11 x9 (x10 x50))(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = add_SNo (add_SNo (x7 x50 x51) (minus_SNo x50)) (x12 x50))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x51)x15 = 1(∀ x50 . x50int∀ x51 . x51intx16 x50 x51 = If_i (SNoLe x50 0) x51 (x13 (x16 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx17 x50 x51 = x16 (x14 x50 x51) x15)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = add_SNo (add_SNo (add_SNo (x17 x50 x51) x50) x50) x50)(∀ x50 . x50intx19 x50 = x50)x20 = 1(∀ x50 . x50int∀ x51 . x51intx21 x50 x51 = If_i (SNoLe x50 0) x51 (x18 (x21 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx22 x50 = x21 (x19 x50) x20)(∀ x50 . x50intx23 x50 = x22 x50)(∀ x50 . x50intx24 x50 = add_SNo (add_SNo x50 x50) x50)(∀ x50 . x50intx25 x50 = x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50intx31 x50 = add_SNo (x30 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = If_i (SNoLe x50 0) x51 (x24 (x32 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx33 x50 = x32 (x25 x50) (x31 x50))(∀ x50 . x50intx34 x50 = x33 x50)x35 = 1(∀ x50 . x50int∀ x51 . x51intx36 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx38 x50 x51 = x37 x35 (x36 x50 x51))(∀ x50 . x50int∀ x51 . x51intx39 x50 x51 = add_SNo (x38 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50))))(∀ x50 . x50int∀ x51 . x51intx40 x50 x51 = x51)x41 = 1(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 (x40 x50 x51) x41)(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x23 x50 = x49 x50
Conjecture 2f7d4..A28080 : ∀ 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)) (mul_SNo (mul_SNo x46 x46) 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 (x7 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 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 (x33 x45 x46) (mul_SNo 2 (mul_SNo 2 (add_SNo 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 (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 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 85ab0..A28071 : ∀ 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 = add_SNo (mul_SNo 2 (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 (add_SNo (x24 x65 x66) 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 1 (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 (add_SNo (x48 x65 x66) 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) (mul_SNo (add_SNo (mul_SNo (add_SNo x65 x65) 2) x65) 2)) x65)(∀ 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 82f5f..A28065 : ∀ 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 (x14 x60 x61) (mul_SNo 2 (mul_SNo 2 (add_SNo 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 (add_SNo (x19 x60 x61) 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 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 (add_SNo (x43 x60 x61) 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 (x53 x60 x61) (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 176d0..A28061 : ∀ 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 (add_SNo (x19 x60 x61) 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 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 (add_SNo (x43 x60 x61) 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 ceaa8..A28057 : ∀ 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 = 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 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 1 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 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 b8d2c..A28036 : ∀ 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 . 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 . x32intx31 x32int)∀ x32 : ι → ι → ι . (∀ x33 . x33int∀ x34 . x34intx32 x33 x34int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 . x35int∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι → ι . (∀ x39 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ 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 . x46intx45 x46int)∀ x46 . x46int∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)(∀ x50 . x50int∀ x51 . x51intx0 x50 x51 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)) (mul_SNo x51 x51))(∀ x50 . x50int∀ x51 . x51intx1 x50 x51 = add_SNo x51 x51)(∀ x50 . x50int∀ x51 . x51intx2 x50 x51 = x51)x3 = 1x4 = 2(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx5 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x0 (x5 (add_SNo x50 (minus_SNo 1)) x51 x52) (x6 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx6 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x1 (x5 (add_SNo x50 (minus_SNo 1)) x51 x52) (x6 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51intx7 x50 x51 = x5 (x2 x50 x51) x3 x4)(∀ x50 . x50int∀ x51 . x51intx8 x50 x51 = mul_SNo (add_SNo 2 x51) x50)x9 = 2(∀ x50 . x50intx10 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx11 x50 x51 = If_i (SNoLe x50 0) x51 (x8 (x11 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx12 x50 = x11 x9 (x10 x50))(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = add_SNo (add_SNo (x7 x50 x51) (minus_SNo x50)) (x12 x50))(∀ x50 . x50int∀ x51 . x51intx14 x50 x51 = x51)x15 = 1(∀ x50 . x50int∀ x51 . x51intx16 x50 x51 = If_i (SNoLe x50 0) x51 (x13 (x16 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx17 x50 x51 = x16 (x14 x50 x51) x15)(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = add_SNo (add_SNo (add_SNo (x17 x50 x51) x50) x50) x50)(∀ x50 . x50intx19 x50 = x50)x20 = 1(∀ x50 . x50int∀ x51 . x51intx21 x50 x51 = If_i (SNoLe x50 0) x51 (x18 (x21 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx22 x50 = x21 (x19 x50) x20)(∀ x50 . x50intx23 x50 = x22 x50)(∀ x50 . x50intx24 x50 = add_SNo (add_SNo x50 x50) x50)(∀ x50 . x50intx25 x50 = x50)(∀ x50 . x50intx26 x50 = add_SNo x50 x50)(∀ x50 . x50intx27 x50 = x50)x28 = 2(∀ x50 . x50int∀ x51 . x51intx29 x50 x51 = If_i (SNoLe x50 0) x51 (x26 (x29 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx30 x50 = x29 (x27 x50) x28)(∀ x50 . x50intx31 x50 = add_SNo (x30 x50) (minus_SNo 1))(∀ x50 . x50int∀ x51 . x51intx32 x50 x51 = If_i (SNoLe x50 0) x51 (x24 (x32 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx33 x50 = x32 (x25 x50) (x31 x50))(∀ x50 . x50intx34 x50 = x33 x50)x35 = 1(∀ x50 . x50int∀ x51 . x51intx36 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx38 x50 x51 = x37 x35 (x36 x50 x51))(∀ x50 . x50int∀ x51 . x51intx39 x50 x51 = add_SNo (x38 x50 x51) (mul_SNo 2 (add_SNo x50 x50)))(∀ x50 . x50int∀ x51 . x51intx40 x50 x51 = x51)x41 = 1(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 (x40 x50 x51) x41)(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x23 x50 = x49 x50
Conjecture dcfea..A28035 : ∀ 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)) (mul_SNo x46 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 (x7 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 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 (x33 x45 x46) (mul_SNo 2 (add_SNo 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 (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 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 e1ab2..A28030 : ∀ 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)) (mul_SNo x44 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 (mul_SNo x44 x44) x43) x43) x43)(∀ 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 (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