Search for blocks/addresses/...

Proofgold Asset

asset id
012001b9047e5b07d31ad73bb7a2c974c190047433725d6f863b73e76ec10bda
asset hash
d8c8716ee5c406da365b17cadd2c074647280ad7944426f26ce11f94e3f6a8ac
bday / block
25655
tx
6dd8a..
preasset
doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param minus_SNominus_SNo : ιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Conjecture 9ca01..A28027 : ∀ 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 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 (add_SNo (x7 x28 x29) 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 (add_SNo (mul_SNo (add_SNo (add_SNo x29 (minus_SNo 1)) x29) (mul_SNo x29 x29)) x28) 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 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 7c1f5..A28025 : ∀ 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 (add_SNo (x7 x45 x46) (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 (add_SNo (x38 x45 x46) (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 cfa10..A28024 : ∀ 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 . x19int∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 . x43int∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 . x49int∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)(∀ x53 . x53int∀ x54 . x54intx0 x53 x54 = mul_SNo (add_SNo 2 x54) x53)x1 = 2(∀ x53 . x53intx2 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx3 x53 x54 = If_i (SNoLe x53 0) x54 (x0 (x3 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx4 x53 = x3 x1 (x2 x53))(∀ x53 . x53int∀ x54 . x54intx5 x53 x54 = add_SNo (add_SNo (x4 x53) (minus_SNo x53)) x54)(∀ x53 . x53int∀ x54 . x54intx6 x53 x54 = add_SNo x54 x54)(∀ x53 . x53int∀ x54 . x54intx7 x53 x54 = x54)x8 = 1x9 = 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx10 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x5 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx11 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x6 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54intx12 x53 x54 = x10 (x7 x53 x54) x8 x9)(∀ x53 . x53int∀ x54 . x54intx13 x53 x54 = add_SNo (x12 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53)))(∀ x53 . x53int∀ x54 . x54intx14 x53 x54 = x54)x15 = 1(∀ x53 . x53int∀ x54 . x54intx16 x53 x54 = If_i (SNoLe x53 0) x54 (x13 (x16 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53int∀ x54 . x54intx17 x53 x54 = x16 (x14 x53 x54) x15)(∀ x53 . x53int∀ x54 . x54intx18 x53 x54 = mul_SNo (add_SNo 2 x54) x53)x19 = 2(∀ x53 . x53intx20 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx21 x53 x54 = If_i (SNoLe x53 0) x54 (x18 (x21 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx22 x53 = x21 x19 (x20 x53))(∀ x53 . x53int∀ x54 . x54intx23 x53 x54 = add_SNo (x17 x53 x54) (x22 x53))(∀ x53 . x53intx24 x53 = x53)x25 = 1(∀ x53 . x53int∀ x54 . x54intx26 x53 x54 = If_i (SNoLe x53 0) x54 (x23 (x26 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx27 x53 = x26 (x24 x53) x25)(∀ x53 . x53intx28 x53 = x27 x53)(∀ x53 . x53int∀ x54 . x54intx29 x53 x54 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x53 x53) x53)) x54)(∀ x53 . x53int∀ x54 . x54intx30 x53 x54 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x54 x54)) x54))(∀ x53 . x53intx31 x53 = x53)x32 = 1x33 = add_SNo 2 (add_SNo 2 2)(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx34 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x29 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx35 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x30 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx36 x53 = x34 (x31 x53) x32 x33)(∀ x53 . x53intx37 x53 = add_SNo x53 x53)(∀ x53 . x53intx38 x53 = x53)x39 = 1(∀ x53 . x53int∀ x54 . x54intx40 x53 x54 = If_i (SNoLe x53 0) x54 (x37 (x40 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx41 x53 = x40 (x38 x53) x39)(∀ x53 . x53intx42 x53 = mul_SNo (x36 x53) (x41 x53))x43 = 1(∀ x53 . x53int∀ x54 . x54intx44 x53 x54 = x54)(∀ x53 . x53int∀ x54 . x54intx45 x53 x54 = If_i (SNoLe x53 0) x54 (x42 (x45 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53int∀ x54 . x54intx46 x53 x54 = x45 x43 (x44 x53 x54))(∀ x53 . x53int∀ x54 . x54intx47 x53 x54 = add_SNo (add_SNo (x46 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53))) x53)(∀ x53 . x53intx48 x53 = x53)x49 = 1(∀ x53 . x53int∀ x54 . x54intx50 x53 x54 = If_i (SNoLe x53 0) x54 (x47 (x50 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx51 x53 = x50 (x48 x53) x49)(∀ x53 . x53intx52 x53 = x51 x53)∀ x53 . x53intSNoLe 0 x53x28 x53 = x52 x53
Conjecture 10244..A28022 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 . x11int∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι . (∀ x26 . x26intx25 x26int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 . x30int∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι . (∀ 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 (mul_SNo 2 (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 = mul_SNo (add_SNo 2 x51) x50)x11 = 2(∀ x50 . x50intx12 x50 = x50)(∀ x50 . x50int∀ x51 . x51intx13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx14 x50 = x13 x11 (x12 x50))(∀ x50 . x50int∀ x51 . x51intx15 x50 x51 = add_SNo (x9 x50 x51) (x14 x50))(∀ x50 . x50int∀ x51 . x51intx16 x50 x51 = x51)x17 = 1(∀ x50 . x50int∀ x51 . x51intx18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50int∀ x51 . x51intx19 x50 x51 = x18 (x16 x50 x51) x17)(∀ x50 . x50int∀ x51 . x51intx20 x50 x51 = add_SNo (add_SNo (x19 x50 x51) x50) x50)(∀ x50 . x50intx21 x50 = x50)x22 = 1(∀ x50 . x50int∀ x51 . x51intx23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx24 x50 = x23 (x21 x50) x22)(∀ x50 . x50intx25 x50 = x24 x50)(∀ x50 . x50int∀ x51 . x51intx26 x50 x51 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)) x51)(∀ x50 . x50int∀ x51 . x51intx27 x50 x51 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x51 x51)) x51))(∀ x50 . x50intx28 x50 = x50)x29 = 1x30 = add_SNo 2 (add_SNo 2 2)(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50int∀ x51 . x51int∀ x52 . x52intx32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52)))(∀ x50 . x50intx33 x50 = x31 (x28 x50) x29 x30)(∀ x50 . x50intx34 x50 = add_SNo x50 x50)(∀ x50 . x50intx35 x50 = x50)x36 = 1(∀ x50 . x50int∀ x51 . x51intx37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50intx38 x50 = x37 (x35 x50) x36)(∀ x50 . x50intx39 x50 = mul_SNo (x33 x50) (x38 x50))x40 = 1(∀ x50 . x50int∀ x51 . x51intx41 x50 x51 = x51)(∀ x50 . x50int∀ x51 . x51intx42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51)))(∀ x50 . x50int∀ x51 . x51intx43 x50 x51 = x42 x40 (x41 x50 x51))(∀ x50 . x50int∀ x51 . x51intx44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50)))) x50)(∀ x50 . x50intx45 x50 = x50)x46 = 1(∀ x50 . x50int∀ x51 . x51intx47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50))(∀ x50 . x50intx48 x50 = x47 (x45 x50) x46)(∀ x50 . x50intx49 x50 = x48 x50)∀ x50 . x50intSNoLe 0 x50x25 x50 = x49 x50
Conjecture 41ba0..A280211 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)(∀ x28 . x28intx0 x28 = add_SNo x28 x28)(∀ x28 . x28intx1 x28 = mul_SNo x28 x28)(∀ x28 . x28intx2 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx4 x28 = x3 (x1 x28) (x2 x28))(∀ x28 . x28intx5 x28 = x4 x28)(∀ x28 . x28intx6 x28 = add_SNo x28 x28)(∀ x28 . x28intx7 x28 = add_SNo (add_SNo x28 x28) (minus_SNo 1))(∀ x28 . x28intx8 x28 = x28)(∀ x28 . x28int∀ x29 . x29intx9 x28 x29 = If_i (SNoLe x28 0) x29 (x6 (x9 (add_SNo x28 (minus_SNo 1)) x29)))(∀ x28 . x28intx10 x28 = x9 (x7 x28) (x8 x28))(∀ x28 . x28int∀ x29 . x29intx11 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx12 x28 x29 = add_SNo x29 x29)(∀ x28 . x28intx13 x28 = add_SNo x28 (minus_SNo 2))x14 = 1x15 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx18 x28 = x16 (x13 x28) x14 x15)(∀ x28 . x28int∀ x29 . x29intx19 x28 x29 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx20 x28 x29 = add_SNo x29 x29)(∀ x28 . x28intx21 x28 = add_SNo x28 (minus_SNo 1))x22 = 1x23 = 2(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28intx26 x28 = x24 (x21 x28) x22 x23)(∀ x28 . x28intx27 x28 = mul_SNo (mul_SNo (x10 x28) (x18 x28)) (x26 x28))∀ x28 . x28intSNoLe 0 x28x5 x28 = x27 x28
Conjecture 4941f..A28020 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 . x43int∀ x44 : ι → ι → ι . (∀ x45 . x45int∀ x46 . x46intx44 x45 x46int)∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι . (∀ x49 . x49intx48 x49int)∀ x49 . x49int∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι . (∀ x52 . x52intx51 x52int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)(∀ x53 . x53int∀ x54 . x54intx0 x53 x54 = mul_SNo (add_SNo 2 x54) x53)x1 = 2(∀ x53 . x53intx2 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx3 x53 x54 = If_i (SNoLe x53 0) x54 (x0 (x3 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx4 x53 = x3 x1 (x2 x53))(∀ x53 . x53int∀ x54 . x54intx5 x53 x54 = add_SNo (add_SNo (x4 x53) (minus_SNo x53)) (mul_SNo (mul_SNo x54 x54) x54))(∀ x53 . x53int∀ x54 . x54intx6 x53 x54 = add_SNo x54 x54)(∀ x53 . x53int∀ x54 . x54intx7 x53 x54 = x54)x8 = 1x9 = 2(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx10 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x5 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx11 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x6 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54intx12 x53 x54 = x10 (x7 x53 x54) x8 x9)(∀ x53 . x53int∀ x54 . x54intx13 x53 x54 = mul_SNo (add_SNo 2 x54) x53)x14 = 2(∀ x53 . x53intx15 x53 = x53)(∀ x53 . x53int∀ x54 . x54intx16 x53 x54 = If_i (SNoLe x53 0) x54 (x13 (x16 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx17 x53 = x16 x14 (x15 x53))(∀ x53 . x53int∀ x54 . x54intx18 x53 x54 = add_SNo (x12 x53 x54) (x17 x53))(∀ x53 . x53int∀ x54 . x54intx19 x53 x54 = x54)x20 = 1(∀ x53 . x53int∀ x54 . x54intx21 x53 x54 = If_i (SNoLe x53 0) x54 (x18 (x21 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53int∀ x54 . x54intx22 x53 x54 = x21 (x19 x53 x54) x20)(∀ x53 . x53int∀ x54 . x54intx23 x53 x54 = add_SNo (add_SNo (x22 x53 x54) x53) x53)(∀ x53 . x53intx24 x53 = x53)x25 = 1(∀ x53 . x53int∀ x54 . x54intx26 x53 x54 = If_i (SNoLe x53 0) x54 (x23 (x26 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx27 x53 = x26 (x24 x53) x25)(∀ x53 . x53intx28 x53 = x27 x53)(∀ x53 . x53int∀ x54 . x54intx29 x53 x54 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x53 x53) x53)) x54)(∀ x53 . x53int∀ x54 . x54intx30 x53 x54 = add_SNo 1 (mul_SNo 2 (add_SNo x54 x54)))(∀ x53 . x53intx31 x53 = x53)x32 = 1x33 = add_SNo 1 (add_SNo 2 2)(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx34 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x29 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53int∀ x54 . x54int∀ x55 . x55intx35 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x30 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55)))(∀ x53 . x53intx36 x53 = x34 (x31 x53) x32 x33)(∀ x53 . x53intx37 x53 = add_SNo x53 x53)(∀ x53 . x53intx38 x53 = x53)x39 = 1(∀ x53 . x53int∀ x54 . x54intx40 x53 x54 = If_i (SNoLe x53 0) x54 (x37 (x40 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53intx41 x53 = x40 (x38 x53) x39)(∀ x53 . x53intx42 x53 = mul_SNo (x36 x53) (x41 x53))x43 = 1(∀ x53 . x53int∀ x54 . x54intx44 x53 x54 = x54)(∀ x53 . x53int∀ x54 . x54intx45 x53 x54 = If_i (SNoLe x53 0) x54 (x42 (x45 (add_SNo x53 (minus_SNo 1)) x54)))(∀ x53 . x53int∀ x54 . x54intx46 x53 x54 = x45 x43 (x44 x53 x54))(∀ x53 . x53int∀ x54 . x54intx47 x53 x54 = add_SNo (add_SNo (x46 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53))) x53)(∀ x53 . x53intx48 x53 = x53)x49 = 1(∀ x53 . x53int∀ x54 . x54intx50 x53 x54 = If_i (SNoLe x53 0) x54 (x47 (x50 (add_SNo x53 (minus_SNo 1)) x54) x53))(∀ x53 . x53intx51 x53 = x50 (x48 x53) x49)(∀ x53 . x53intx52 x53 = x51 x53)∀ x53 . x53intSNoLe 0 x53x28 x53 = x52 x53
Conjecture f1171..A28019 : ∀ 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 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . 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 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45int∀ x46 . x46intx1 x45 x46 = x46)x2 = 1(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx4 x45 x46 = x3 (x1 x45 x46) x2)(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = add_SNo (x4 x45 x46) (mul_SNo 2 (add_SNo x45 x45)))(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (add_SNo (x9 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45intx11 x45 = x45)x12 = 1(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx14 x45 = x13 (x11 x45) x12)(∀ x45 . x45intx15 x45 = add_SNo x45 x45)(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = mul_SNo (x14 x45) (x19 x45))(∀ x45 . x45int∀ x46 . x46intx21 x45 x46 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) x46)(∀ x45 . x45int∀ x46 . x46intx22 x45 x46 = add_SNo 1 (mul_SNo 2 (add_SNo x46 x46)))(∀ x45 . x45intx23 x45 = x45)x24 = 1x25 = add_SNo 1 (add_SNo 2 2)(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx26 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x21 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx27 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x22 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx28 x45 = x26 (x23 x45) x24 x25)(∀ x45 . x45intx29 x45 = x28 x45)x30 = 1(∀ x45 . x45int∀ x46 . x46intx31 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx33 x45 x46 = x32 x30 (x31 x45 x46))(∀ x45 . x45int∀ x46 . x46intx34 x45 x46 = add_SNo (add_SNo (x33 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45intx35 x45 = x45)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 . x45intx38 x45 = x37 (x35 x45) x36)(∀ x45 . x45intx39 x45 = add_SNo 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 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = mul_SNo (x38 x45) (x43 x45))∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture 7b57a..A28018 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 . x9int∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 . x28int∀ x29 : ι → ι → ι → ι . (∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx29 x30 x31 x32int)∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)(∀ x48 . x48int∀ x49 . x49intx0 x48 x49 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48)) (mul_SNo (mul_SNo x49 x49) x49))(∀ x48 . x48int∀ x49 . x49intx1 x48 x49 = add_SNo x49 x49)(∀ x48 . x48int∀ x49 . x49intx2 x48 x49 = x49)x3 = 1x4 = 2(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx5 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x0 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx6 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x1 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49intx7 x48 x49 = x5 (x2 x48 x49) x3 x4)(∀ x48 . x48int∀ x49 . x49intx8 x48 x49 = mul_SNo (add_SNo 2 x49) x48)x9 = 2(∀ x48 . x48intx10 x48 = x48)(∀ x48 . x48int∀ x49 . x49intx11 x48 x49 = If_i (SNoLe x48 0) x49 (x8 (x11 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx12 x48 = x11 x9 (x10 x48))(∀ x48 . x48int∀ x49 . x49intx13 x48 x49 = add_SNo (add_SNo (x7 x48 x49) (minus_SNo x48)) (x12 x48))(∀ x48 . x48int∀ x49 . x49intx14 x48 x49 = x49)x15 = 1(∀ x48 . x48int∀ x49 . x49intx16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48int∀ x49 . x49intx17 x48 x49 = x16 (x14 x48 x49) x15)(∀ x48 . x48int∀ x49 . x49intx18 x48 x49 = add_SNo (add_SNo (x17 x48 x49) x48) x48)(∀ x48 . x48intx19 x48 = x48)x20 = 1(∀ x48 . x48int∀ x49 . x49intx21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx22 x48 = x21 (x19 x48) x20)(∀ x48 . x48intx23 x48 = x22 x48)(∀ x48 . x48int∀ x49 . x49intx24 x48 x49 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48) x49)(∀ x48 . x48int∀ x49 . x49intx25 x48 x49 = add_SNo 1 (mul_SNo 2 (add_SNo x49 x49)))(∀ x48 . x48intx26 x48 = x48)x27 = 1x28 = add_SNo 1 (add_SNo 2 2)(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx29 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x24 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48int∀ x49 . x49int∀ x50 . x50intx30 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x25 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50)))(∀ x48 . x48intx31 x48 = x29 (x26 x48) x27 x28)(∀ x48 . x48intx32 x48 = add_SNo x48 x48)(∀ x48 . x48intx33 x48 = x48)x34 = 1(∀ x48 . x48int∀ x49 . x49intx35 x48 x49 = If_i (SNoLe x48 0) x49 (x32 (x35 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48intx36 x48 = x35 (x33 x48) x34)(∀ x48 . x48intx37 x48 = mul_SNo (x31 x48) (x36 x48))x38 = 1(∀ x48 . x48int∀ x49 . x49intx39 x48 x49 = x49)(∀ x48 . x48int∀ x49 . x49intx40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49)))(∀ x48 . x48int∀ x49 . x49intx41 x48 x49 = x40 x38 (x39 x48 x49))(∀ x48 . x48int∀ x49 . x49intx42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48))) x48)(∀ x48 . x48intx43 x48 = x48)x44 = 1(∀ x48 . x48int∀ x49 . x49intx45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48))(∀ x48 . x48intx46 x48 = x45 (x43 x48) x44)(∀ x48 . x48intx47 x48 = x46 x48)∀ x48 . x48intSNoLe 0 x48x23 x48 = x47 x48
Conjecture a00ed..A28012 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 . x8int∀ x9 . x9int∀ x10 : ι → ι → ι → ι . (∀ x11 . x11int∀ x12 . x12int∀ x13 . x13intx10 x11 x12 x13int)∀ x11 : ι → ι → ι → ι . (∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intx11 x12 x13 x14int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι → ι . (∀ x25 . x25int∀ x26 . x26intx24 x25 x26int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 . x27int∀ x28 . x28int∀ x29 : ι → ι → ι → ι . (∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx29 x30 x31 x32int)∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ x34 . x34int∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)∀ x48 . x48int∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 . x54int∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι . (∀ x57 . x57intx56 x57int)∀ x57 : ι → ι . (∀ x58 . x58intx57 x58int)(∀ x58 . x58int∀ x59 . x59intx0 x58 x59 = mul_SNo (add_SNo 2 x59) x58)x1 = 2(∀ x58 . x58intx2 x58 = x58)(∀ x58 . x58int∀ x59 . x59intx3 x58 x59 = If_i (SNoLe x58 0) x59 (x0 (x3 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx4 x58 = x3 x1 (x2 x58))(∀ x58 . x58int∀ x59 . x59intx5 x58 x59 = add_SNo (add_SNo (x4 x58) (minus_SNo x58)) x59)(∀ x58 . x58int∀ x59 . x59intx6 x58 x59 = add_SNo x59 x59)(∀ x58 . x58int∀ x59 . x59intx7 x58 x59 = x59)x8 = 1x9 = 2(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx10 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x5 (x10 (add_SNo x58 (minus_SNo 1)) x59 x60) (x11 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx11 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x6 (x10 (add_SNo x58 (minus_SNo 1)) x59 x60) (x11 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59intx12 x58 x59 = x10 (x7 x58 x59) x8 x9)(∀ x58 . x58int∀ x59 . x59intx13 x58 x59 = add_SNo (x12 x58 x59) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x58 x58)) x58)))(∀ x58 . x58int∀ x59 . x59intx14 x58 x59 = x59)x15 = 1(∀ x58 . x58int∀ x59 . x59intx16 x58 x59 = If_i (SNoLe x58 0) x59 (x13 (x16 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx17 x58 x59 = x16 (x14 x58 x59) x15)(∀ x58 . x58int∀ x59 . x59intx18 x58 x59 = add_SNo (add_SNo (x17 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58)(∀ x58 . x58intx19 x58 = x58)x20 = 1(∀ x58 . x58int∀ x59 . x59intx21 x58 x59 = If_i (SNoLe x58 0) x59 (x18 (x21 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx22 x58 = x21 (x19 x58) x20)(∀ x58 . x58intx23 x58 = x22 x58)(∀ x58 . x58int∀ x59 . x59intx24 x58 x59 = add_SNo 1 (mul_SNo x58 x59))(∀ x58 . x58int∀ x59 . x59intx25 x58 x59 = x59)(∀ x58 . x58intx26 x58 = x58)x27 = 1x28 = add_SNo 1 (add_SNo 2 2)(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx29 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x24 (x29 (add_SNo x58 (minus_SNo 1)) x59 x60) (x30 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx30 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x25 (x29 (add_SNo x58 (minus_SNo 1)) x59 x60) (x30 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58intx31 x58 = x29 (x26 x58) x27 x28)(∀ x58 . x58intx32 x58 = add_SNo x58 x58)(∀ x58 . x58intx33 x58 = x58)x34 = 1(∀ x58 . x58int∀ x59 . x59intx35 x58 x59 = If_i (SNoLe x58 0) x59 (x32 (x35 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58intx36 x58 = x35 (x33 x58) x34)(∀ x58 . x58intx37 x58 = mul_SNo (x31 x58) (x36 x58))x38 = 1(∀ x58 . x58int∀ x59 . x59intx39 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx40 x58 x59 = If_i (SNoLe x58 0) x59 (x37 (x40 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx41 x58 x59 = x40 x38 (x39 x58 x59))(∀ x58 . x58int∀ x59 . x59intx42 x58 x59 = add_SNo (add_SNo (x41 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58)(∀ x58 . x58intx43 x58 = x58)x44 = 1(∀ x58 . x58int∀ x59 . x59intx45 x58 x59 = If_i (SNoLe x58 0) x59 (x42 (x45 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx46 x58 = x45 (x43 x58) x44)(∀ x58 . x58intx47 x58 = x46 x58)x48 = 1(∀ x58 . x58int∀ x59 . x59intx49 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx50 x58 x59 = If_i (SNoLe x58 0) x59 (x47 (x50 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx51 x58 x59 = x50 x48 (x49 x58 x59))(∀ x58 . x58int∀ x59 . x59intx52 x58 x59 = add_SNo (add_SNo (x51 x58 x59) (mul_SNo (add_SNo (mul_SNo (add_SNo x58 x58) 2) x58) 2)) x58)(∀ x58 . x58intx53 x58 = x58)x54 = 1(∀ x58 . x58int∀ x59 . x59intx55 x58 x59 = If_i (SNoLe x58 0) x59 (x52 (x55 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx56 x58 = x55 (x53 x58) x54)(∀ x58 . x58intx57 x58 = x56 x58)∀ x58 . x58intSNoLe 0 x58x23 x58 = x57 x58
Conjecture 7c225..A28009 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 . x31int∀ 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 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)∀ x45 . x45int∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι . (∀ x51 . x51intx50 x51int)∀ x51 . x51int∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 : ι → ι . (∀ x55 . x55intx54 x55int)(∀ x55 . x55intx0 x55 = add_SNo (add_SNo x55 x55) x55)(∀ x55 . x55int∀ x56 . x56intx1 x55 x56 = add_SNo x56 x56)x2 = 1(∀ x55 . x55int∀ x56 . x56intx3 x55 x56 = If_i (SNoLe x55 0) x56 (x0 (x3 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55int∀ x56 . x56intx4 x55 x56 = x3 (x1 x55 x56) x2)(∀ x55 . x55int∀ x56 . x56intx5 x55 x56 = add_SNo (x4 x55 x56) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x55 x55)) x55)))(∀ x55 . x55int∀ x56 . x56intx6 x55 x56 = x56)x7 = 1(∀ x55 . x55int∀ x56 . x56intx8 x55 x56 = If_i (SNoLe x55 0) x56 (x5 (x8 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55int∀ x56 . x56intx9 x55 x56 = x8 (x6 x55 x56) x7)(∀ x55 . x55int∀ x56 . x56intx10 x55 x56 = add_SNo (add_SNo (x9 x55 x56) (mul_SNo 2 (add_SNo (add_SNo x55 x55) x55))) x55)(∀ x55 . x55int∀ x56 . x56intx11 x55 x56 = x56)x12 = 1(∀ x55 . x55int∀ x56 . x56intx13 x55 x56 = If_i (SNoLe x55 0) x56 (x10 (x13 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55int∀ x56 . x56intx14 x55 x56 = x13 (x11 x55 x56) x12)(∀ x55 . x55int∀ x56 . x56intx15 x55 x56 = add_SNo (add_SNo (x14 x55 x56) x55) x55)(∀ x55 . x55intx16 x55 = x55)x17 = 1(∀ x55 . x55int∀ x56 . x56intx18 x55 x56 = If_i (SNoLe x55 0) x56 (x15 (x18 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx19 x55 = x18 (x16 x55) x17)(∀ x55 . x55intx20 x55 = x19 x55)(∀ x55 . x55int∀ x56 . x56intx21 x55 x56 = add_SNo 1 (mul_SNo x55 x56))(∀ x55 . x55int∀ x56 . x56intx22 x55 x56 = x56)(∀ x55 . x55intx23 x55 = x55)x24 = 1x25 = add_SNo 1 (add_SNo 2 2)(∀ x55 . x55int∀ x56 . x56int∀ x57 . x57intx26 x55 x56 x57 = If_i (SNoLe x55 0) x56 (x21 (x26 (add_SNo x55 (minus_SNo 1)) x56 x57) (x27 (add_SNo x55 (minus_SNo 1)) x56 x57)))(∀ x55 . x55int∀ x56 . x56int∀ x57 . x57intx27 x55 x56 x57 = If_i (SNoLe x55 0) x57 (x22 (x26 (add_SNo x55 (minus_SNo 1)) x56 x57) (x27 (add_SNo x55 (minus_SNo 1)) x56 x57)))(∀ x55 . x55intx28 x55 = x26 (x23 x55) x24 x25)(∀ x55 . x55intx29 x55 = add_SNo x55 x55)(∀ x55 . x55intx30 x55 = x55)x31 = 1(∀ x55 . x55int∀ x56 . x56intx32 x55 x56 = If_i (SNoLe x55 0) x56 (x29 (x32 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55intx33 x55 = x32 (x30 x55) x31)(∀ x55 . x55intx34 x55 = mul_SNo (x28 x55) (x33 x55))x35 = 1(∀ x55 . x55int∀ x56 . x56intx36 x55 x56 = x56)(∀ x55 . x55int∀ x56 . x56intx37 x55 x56 = If_i (SNoLe x55 0) x56 (x34 (x37 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55int∀ x56 . x56intx38 x55 x56 = x37 x35 (x36 x55 x56))(∀ x55 . x55int∀ x56 . x56intx39 x55 x56 = add_SNo (add_SNo (x38 x55 x56) x55) (mul_SNo (mul_SNo (add_SNo x55 x55) 2) 2))(∀ x55 . x55intx40 x55 = x55)x41 = 1(∀ x55 . x55int∀ x56 . x56intx42 x55 x56 = If_i (SNoLe x55 0) x56 (x39 (x42 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx43 x55 = x42 (x40 x55) x41)(∀ x55 . x55intx44 x55 = x43 x55)x45 = 1(∀ x55 . x55int∀ x56 . x56intx46 x55 x56 = x56)(∀ x55 . x55int∀ x56 . x56intx47 x55 x56 = If_i (SNoLe x55 0) x56 (x44 (x47 (add_SNo x55 (minus_SNo 1)) x56)))(∀ x55 . x55int∀ x56 . x56intx48 x55 x56 = x47 x45 (x46 x55 x56))(∀ x55 . x55int∀ x56 . x56intx49 x55 x56 = add_SNo (add_SNo (x48 x55 x56) x55) (mul_SNo (add_SNo (add_SNo x55 x55) x55) 2))(∀ x55 . x55intx50 x55 = x55)x51 = 1(∀ x55 . x55int∀ x56 . x56intx52 x55 x56 = If_i (SNoLe x55 0) x56 (x49 (x52 (add_SNo x55 (minus_SNo 1)) x56) x55))(∀ x55 . x55intx53 x55 = x52 (x50 x55) x51)(∀ x55 . x55intx54 x55 = x53 x55)∀ x55 . x55intSNoLe 0 x55x20 x55 = x54 x55
Conjecture edca8..A28006 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 . x4int∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι → ι . (∀ x8 . x8int∀ x9 . x9intx7 x8 x9int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 . x29int∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 . x33int∀ x34 : ι → ι → ι . (∀ x35 . x35int∀ x36 . x36intx34 x35 x36int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 . x39int∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι . (∀ x42 . x42intx41 x42int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)(∀ x43 . x43int∀ x44 . x44intx0 x43 x44 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)) (mul_SNo (mul_SNo x44 x44) x44))(∀ x43 . x43int∀ x44 . x44intx1 x43 x44 = add_SNo x44 x44)(∀ x43 . x43int∀ x44 . x44intx2 x43 x44 = x44)x3 = 1x4 = 2(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx5 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x0 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx6 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x1 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44intx7 x43 x44 = x5 (x2 x43 x44) x3 x4)(∀ x43 . x43int∀ x44 . x44intx8 x43 x44 = add_SNo (add_SNo (x7 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43)(∀ x43 . x43int∀ x44 . x44intx9 x43 x44 = x44)x10 = 1(∀ x43 . x43int∀ x44 . x44intx11 x43 x44 = If_i (SNoLe x43 0) x44 (x8 (x11 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43int∀ x44 . x44intx12 x43 x44 = x11 (x9 x43 x44) x10)(∀ x43 . x43int∀ x44 . x44intx13 x43 x44 = add_SNo (add_SNo (x12 x43 x44) x43) x43)(∀ x43 . x43intx14 x43 = x43)x15 = 1(∀ x43 . x43int∀ x44 . x44intx16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx17 x43 = x16 (x14 x43) x15)(∀ x43 . x43intx18 x43 = x17 x43)(∀ x43 . x43int∀ x44 . x44intx19 x43 x44 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43) x44)(∀ x43 . x43int∀ x44 . x44intx20 x43 x44 = add_SNo 1 (mul_SNo 2 (add_SNo x44 x44)))(∀ x43 . x43intx21 x43 = x43)x22 = 1x23 = add_SNo 1 (add_SNo 2 2)(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx24 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x19 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43int∀ x44 . x44int∀ x45 . x45intx25 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x20 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45)))(∀ x43 . x43intx26 x43 = x24 (x21 x43) x22 x23)(∀ x43 . x43intx27 x43 = add_SNo x43 x43)(∀ x43 . x43intx28 x43 = x43)x29 = 1(∀ x43 . x43int∀ x44 . x44intx30 x43 x44 = If_i (SNoLe x43 0) x44 (x27 (x30 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43intx31 x43 = x30 (x28 x43) x29)(∀ x43 . x43intx32 x43 = mul_SNo (x26 x43) (x31 x43))x33 = 1(∀ x43 . x43int∀ x44 . x44intx34 x43 x44 = x44)(∀ x43 . x43int∀ x44 . x44intx35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44)))(∀ x43 . x43int∀ x44 . x44intx36 x43 x44 = x35 x33 (x34 x43 x44))(∀ x43 . x43int∀ x44 . x44intx37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) x43) (mul_SNo (add_SNo (add_SNo x43 x43) x43) 2))(∀ x43 . x43intx38 x43 = x43)x39 = 1(∀ x43 . x43int∀ x44 . x44intx40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43))(∀ x43 . x43intx41 x43 = x40 (x38 x43) x39)(∀ x43 . x43intx42 x43 = x41 x43)∀ x43 . x43intSNoLe 0 x43x18 x43 = x42 x43
Conjecture 5b0ff..A28003 : ∀ 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 . x12intx11 x12int)∀ x12 . x12int∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 . x17int∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . 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 . x36intx35 x36int)∀ x36 . x36int∀ x37 : ι → ι → ι . (∀ x38 . x38int∀ x39 . x39intx37 x38 x39int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι . (∀ x41 . x41intx40 x41int)∀ x41 . x41int∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 : ι → ι . (∀ x45 . x45intx44 x45int)(∀ x45 . x45intx0 x45 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)))(∀ x45 . x45int∀ x46 . x46intx1 x45 x46 = x46)x2 = 1(∀ x45 . x45int∀ x46 . x46intx3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx4 x45 x46 = x3 (x1 x45 x46) x2)(∀ x45 . x45int∀ x46 . x46intx5 x45 x46 = add_SNo (add_SNo (x4 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45int∀ x46 . x46intx6 x45 x46 = x46)x7 = 1(∀ x45 . x45int∀ x46 . x46intx8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45int∀ x46 . x46intx9 x45 x46 = x8 (x6 x45 x46) x7)(∀ x45 . x45int∀ x46 . x46intx10 x45 x46 = add_SNo (add_SNo (add_SNo (x9 x45 x46) x45) x45) x45)(∀ x45 . x45intx11 x45 = x45)x12 = 1(∀ x45 . x45int∀ x46 . x46intx13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45))(∀ x45 . x45intx14 x45 = x13 (x11 x45) x12)(∀ x45 . x45intx15 x45 = add_SNo x45 x45)(∀ x45 . x45intx16 x45 = x45)x17 = 1(∀ x45 . x45int∀ x46 . x46intx18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45intx19 x45 = x18 (x16 x45) x17)(∀ x45 . x45intx20 x45 = mul_SNo (x14 x45) (x19 x45))(∀ x45 . x45int∀ x46 . x46intx21 x45 x46 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) x46)(∀ x45 . x45int∀ x46 . x46intx22 x45 x46 = add_SNo 1 (add_SNo (add_SNo x46 x46) x46))(∀ x45 . x45intx23 x45 = x45)x24 = 1x25 = add_SNo 2 2(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx26 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x21 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45int∀ x46 . x46int∀ x47 . x47intx27 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x22 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47)))(∀ x45 . x45intx28 x45 = x26 (x23 x45) x24 x25)(∀ x45 . x45intx29 x45 = x28 x45)x30 = 1(∀ x45 . x45int∀ x46 . x46intx31 x45 x46 = x46)(∀ x45 . x45int∀ x46 . x46intx32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46)))(∀ x45 . x45int∀ x46 . x46intx33 x45 x46 = x32 x30 (x31 x45 x46))(∀ x45 . x45int∀ x46 . x46intx34 x45 x46 = add_SNo (add_SNo (x33 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45)(∀ x45 . x45intx35 x45 = x45)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 . x45intx38 x45 = x37 (x35 x45) x36)(∀ x45 . x45intx39 x45 = add_SNo 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 . x45intx43 x45 = x42 (x40 x45) x41)(∀ x45 . x45intx44 x45 = mul_SNo (x38 x45) (x43 x45))∀ x45 . x45intSNoLe 0 x45x20 x45 = x44 x45
Conjecture 47c7a..A27992 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12intx0 x12 = add_SNo (add_SNo x12 (minus_SNo 1)) x12)(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = add_SNo (add_SNo x12 x12) x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = add_SNo 1 (x4 x12))(∀ x12 . x12intx6 x12 = add_SNo x12 x12)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = add_SNo (add_SNo (add_SNo x12 (minus_SNo 1)) x12) x12)(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13)))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = add_SNo 2 (x10 x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 39146..A27990 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ 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 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ 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 = x29)(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = add_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = add_SNo x29 x29)(∀ x28 . x28int∀ x29 . x29intx3 x28 x29 = add_SNo 1 x29)x4 = 1(∀ 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 x28 x29) x4)(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = add_SNo (x7 x28 x29) (minus_SNo 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 x28 x29)(∀ x28 . x28int∀ x29 . x29intx15 x28 x29 = add_SNo (add_SNo x28 x29) x29)(∀ x28 . x28int∀ x29 . x29intx16 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx17 x28 x29 = add_SNo 1 x29)x18 = 1(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30)))(∀ x28 . x28int∀ x29 . x29intx21 x28 x29 = x19 (x16 x28 x29) (x17 x28 x29) x18)(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = add_SNo (x21 x28 x29) (minus_SNo 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 654b0..A27982 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 . x16int∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo x20 x21))))(∀ x20 . x20int∀ x21 . x21intx1 x20 x21 = add_SNo 2 x21)(∀ x20 . x20intx2 x20 = x20)x3 = 1(∀ x20 . x20intx4 x20 = x20)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx5 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x0 (x5 (add_SNo x20 (minus_SNo 1)) x21 x22) (x6 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx6 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x1 (x5 (add_SNo x20 (minus_SNo 1)) x21 x22) (x6 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx7 x20 = x5 (x2 x20) x3 (x4 x20))(∀ x20 . x20intx8 x20 = x7 x20)(∀ x20 . x20intx9 x20 = add_SNo x20 x20)(∀ x20 . x20intx10 x20 = x20)(∀ x20 . x20intx11 x20 = add_SNo 1 (add_SNo 2 (add_SNo 2 x20)))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = If_i (SNoLe x20 0) x21 (x9 (x12 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx13 x20 = x12 (x10 x20) (x11 x20))(∀ x20 . x20intx14 x20 = add_SNo x20 x20)(∀ x20 . x20intx15 x20 = x20)x16 = 1(∀ x20 . x20int∀ x21 . x21intx17 x20 x21 = If_i (SNoLe x20 0) x21 (x14 (x17 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx18 x20 = x17 (x15 x20) x16)(∀ x20 . x20intx19 x20 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo (x13 x20) (minus_SNo (mul_SNo 2 (add_SNo 2 x20)))) (minus_SNo x20)) 2) (minus_SNo 2)) (x18 x20))∀ x20 . x20intSNoLe 0 x20x8 x20 = x19 x20
Conjecture 3d2d6..A27964 : ∀ 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 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι → ι . (∀ x24 . x24int∀ x25 . x25intx23 x24 x25int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 . x25int∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι → ι . (∀ x30 . x30int∀ x31 . x31intx29 x30 x31int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 . x32int∀ x33 . x33int∀ x34 : ι → ι → ι → ι . (∀ x35 . x35int∀ x36 . x36int∀ x37 . x37intx34 x35 x36 x37int)∀ x35 : ι → ι → ι → ι . (∀ x36 . x36int∀ x37 . x37int∀ x38 . x38intx35 x36 x37 x38int)∀ x36 : ι → ι . (∀ x37 . x37intx36 x37int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 . x38int∀ x39 : ι → ι → ι . (∀ x40 . x40int∀ x41 . x41intx39 x40 x41int)∀ x40 : ι → ι → ι . (∀ x41 . x41int∀ x42 . x42intx40 x41 x42int)∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι → ι . (∀ x43 . x43int∀ x44 . x44intx42 x43 x44int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι . (∀ x47 . x47intx46 x47int)∀ x47 : ι → ι . (∀ x48 . x48intx47 x48int)∀ x48 . x48int∀ x49 : ι → ι → ι . (∀ x50 . x50int∀ x51 . x51intx49 x50 x51int)∀ x50 : ι → ι → ι . (∀ x51 . x51int∀ x52 . x52intx50 x51 x52int)∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι → ι . (∀ x53 . x53int∀ x54 . x54intx52 x53 x54int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)∀ x54 . x54int∀ x55 : ι → ι → ι . (∀ x56 . x56int∀ x57 . x57intx55 x56 x57int)∀ x56 : ι → ι . (∀ x57 . x57intx56 x57int)∀ x57 : ι → ι . (∀ x58 . x58intx57 x58int)(∀ x58 . x58int∀ x59 . x59intx0 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx1 x58 x59 = add_SNo x58 x59)(∀ x58 . x58int∀ x59 . x59intx2 x58 x59 = x59)x3 = 2x4 = 1(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx5 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x0 (x5 (add_SNo x58 (minus_SNo 1)) x59 x60) (x6 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx6 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x1 (x5 (add_SNo x58 (minus_SNo 1)) x59 x60) (x6 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59intx7 x58 x59 = x5 (x2 x58 x59) x3 x4)(∀ x58 . x58int∀ x59 . x59intx8 x58 x59 = add_SNo (x7 x58 x59) x58)(∀ x58 . x58int∀ x59 . x59intx9 x58 x59 = x59)(∀ x58 . x58intx10 x58 = x58)(∀ x58 . x58int∀ x59 . x59intx11 x58 x59 = If_i (SNoLe x58 0) x59 (x8 (x11 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx12 x58 x59 = x11 (x9 x58 x59) (x10 x58))(∀ x58 . x58int∀ x59 . x59intx13 x58 x59 = x12 x58 x59)(∀ x58 . x58int∀ x59 . x59intx14 x58 x59 = x59)(∀ x58 . x58intx15 x58 = x58)(∀ x58 . x58int∀ x59 . x59intx16 x58 x59 = If_i (SNoLe x58 0) x59 (x13 (x16 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx17 x58 x59 = x16 (x14 x58 x59) (x15 x58))(∀ x58 . x58int∀ x59 . x59intx18 x58 x59 = x17 x58 x59)(∀ x58 . x58int∀ x59 . x59intx19 x58 x59 = add_SNo 1 x59)(∀ x58 . x58intx20 x58 = x58)(∀ x58 . x58int∀ x59 . x59intx21 x58 x59 = If_i (SNoLe x58 0) x59 (x18 (x21 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58int∀ x59 . x59intx22 x58 x59 = x21 (x19 x58 x59) (x20 x58))(∀ x58 . x58int∀ x59 . x59intx23 x58 x59 = x22 x58 x59)(∀ x58 . x58intx24 x58 = x58)x25 = 1(∀ x58 . x58int∀ x59 . x59intx26 x58 x59 = If_i (SNoLe x58 0) x59 (x23 (x26 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx27 x58 = x26 (x24 x58) x25)(∀ x58 . x58intx28 x58 = x27 x58)(∀ x58 . x58int∀ x59 . x59intx29 x58 x59 = add_SNo x58 x59)(∀ x58 . x58intx30 x58 = x58)(∀ x58 . x58intx31 x58 = x58)x32 = add_SNo 2 2x33 = add_SNo 1 2(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx34 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x29 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60) (x35 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58int∀ x59 . x59int∀ x60 . x60intx35 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x30 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60)))(∀ x58 . x58intx36 x58 = x34 (x31 x58) x32 x33)(∀ x58 . x58intx37 x58 = add_SNo (add_SNo (add_SNo (add_SNo (x36 x58) (minus_SNo 2)) (minus_SNo x58)) (minus_SNo x58)) (minus_SNo x58))x38 = 1(∀ x58 . x58int∀ x59 . x59intx39 x58 x59 = add_SNo 2 x59)(∀ x58 . x58int∀ x59 . x59intx40 x58 x59 = If_i (SNoLe x58 0) x59 (x37 (x40 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx41 x58 x59 = x40 x38 (x39 x58 x59))(∀ x58 . x58int∀ x59 . x59intx42 x58 x59 = add_SNo (x41 x58 x59) x58)(∀ x58 . x58intx43 x58 = x58)x44 = 0(∀ x58 . x58int∀ x59 . x59intx45 x58 x59 = If_i (SNoLe x58 0) x59 (x42 (x45 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx46 x58 = x45 (x43 x58) x44)(∀ x58 . x58intx47 x58 = x46 x58)x48 = 1(∀ x58 . x58int∀ x59 . x59intx49 x58 x59 = x59)(∀ x58 . x58int∀ x59 . x59intx50 x58 x59 = If_i (SNoLe x58 0) x59 (x47 (x50 (add_SNo x58 (minus_SNo 1)) x59)))(∀ x58 . x58int∀ x59 . x59intx51 x58 x59 = x50 x48 (x49 x58 x59))(∀ x58 . x58int∀ x59 . x59intx52 x58 x59 = add_SNo (x51 x58 x59) x58)(∀ x58 . x58intx53 x58 = x58)x54 = 1(∀ x58 . x58int∀ x59 . x59intx55 x58 x59 = If_i (SNoLe x58 0) x59 (x52 (x55 (add_SNo x58 (minus_SNo 1)) x59) x58))(∀ x58 . x58intx56 x58 = x55 (x53 x58) x54)(∀ x58 . x58intx57 x58 = add_SNo (x56 x58) (minus_SNo (mul_SNo x58 x58)))∀ x58 . x58intSNoLe 0 x58x28 x58 = x57 x58
Conjecture b6988..A27942 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ 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 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 . x22int∀ x23 . x23int∀ x24 : ι → ι → ι → ι . (∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx24 x25 x26 x27int)∀ x25 : ι → ι → ι → ι . (∀ x26 . x26int∀ x27 . x27int∀ x28 . x28intx25 x26 x27 x28int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι → ι . (∀ x31 . x31int∀ x32 . x32intx30 x31 x32int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)(∀ x33 . x33int∀ x34 . x34intx0 x33 x34 = add_SNo 2 (add_SNo x33 x34))(∀ x33 . x33intx1 x33 = x33)(∀ x33 . x33int∀ x34 . x34intx2 x33 x34 = x34)x3 = 1x4 = 0(∀ 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)))(∀ x33 . x33int∀ x34 . x34intx7 x33 x34 = x5 (x2 x33 x34) x3 x4)(∀ x33 . x33int∀ x34 . x34intx8 x33 x34 = add_SNo (x7 x33 x34) x33)(∀ x33 . x33int∀ x34 . x34intx9 x33 x34 = add_SNo x34 x34)(∀ 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 . x33int∀ x34 . x34intx12 x33 x34 = x11 (x9 x33 x34) (x10 x33))(∀ x33 . x33int∀ x34 . x34intx13 x33 x34 = x12 x33 x34)(∀ 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 = add_SNo (x17 x33) x33)(∀ x33 . x33int∀ x34 . x34intx19 x33 x34 = add_SNo x33 x34)(∀ x33 . x33intx20 x33 = x33)(∀ x33 . x33intx21 x33 = add_SNo x33 x33)x22 = 2x23 = 1(∀ 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)))(∀ x33 . x33intx26 x33 = x24 (x21 x33) x22 x23)(∀ x33 . x33intx27 x33 = add_SNo (add_SNo (add_SNo (x26 x33) (minus_SNo (mul_SNo (add_SNo x33 x33) x33))) (minus_SNo x33)) (minus_SNo x33))x28 = 1(∀ x33 . x33intx29 x33 = add_SNo 2 x33)(∀ x33 . x33int∀ x34 . x34intx30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34)))(∀ x33 . x33intx31 x33 = x30 x28 (x29 x33))(∀ x33 . x33intx32 x33 = add_SNo (x31 x33) x33)∀ x33 . x33intSNoLe 0 x33x18 x33 = x32 x33
Conjecture 77e50..A27871 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 . x21int∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo (add_SNo x25 x25) x25)(∀ x25 . x25int∀ x26 . x26intx1 x25 x26 = x26)(∀ x25 . x25intx2 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25int∀ x26 . x26intx4 x25 x26 = x3 (x1 x25 x26) (x2 x25))(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = add_SNo (x4 x25 x26) (minus_SNo x25))(∀ x25 . x25intx6 x25 = x25)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx9 x25 = x8 (x6 x25) x7)(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = add_SNo 1 (add_SNo (add_SNo x26 x26) x26))(∀ x25 . x25intx13 x25 = add_SNo x25 (minus_SNo 1))x14 = 1x15 = add_SNo 2 2(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx16 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx17 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx18 x25 = x16 (x13 x25) x14 x15)(∀ x25 . x25intx19 x25 = add_SNo x25 x25)(∀ x25 . x25intx20 x25 = x25)x21 = 1(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx23 x25 = x22 (x20 x25) x21)(∀ x25 . x25intx24 x25 = mul_SNo (x18 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture ae2ae..A277748 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 . x9int∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι → ι . (∀ x14 . x14int∀ x15 . x15intx13 x14 x15int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι . (∀ x22 . x22int∀ x23 . x23intx21 x22 x23int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 . x24int∀ x25 . x25int∀ x26 : ι → ι → ι → ι . (∀ x27 . x27int∀ x28 . x28int∀ x29 . x29intx26 x27 x28 x29int)∀ x27 : ι → ι → ι → ι . (∀ x28 . x28int∀ x29 . x29int∀ x30 . x30intx27 x28 x29 x30int)∀ x28 : ι → ι . (∀ x29 . x29intx28 x29int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)(∀ x30 . x30intx0 x30 = add_SNo x30 x30)(∀ x30 . x30int∀ x31 . x31intx1 x30 x31 = x31)(∀ x30 . x30intx2 x30 = x30)(∀ x30 . x30int∀ x31 . x31intx3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30int∀ x31 . x31intx4 x30 x31 = x3 (x1 x30 x31) (x2 x30))(∀ x30 . x30int∀ x31 . x31intx5 x30 x31 = x4 x30 x31)(∀ x30 . x30intx6 x30 = x30)(∀ x30 . x30intx7 x30 = add_SNo x30 x30)(∀ x30 . x30intx8 x30 = x30)x9 = 2(∀ x30 . x30int∀ x31 . x31intx10 x30 x31 = If_i (SNoLe x30 0) x31 (x7 (x10 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx11 x30 = x10 (x8 x30) x9)(∀ x30 . x30intx12 x30 = add_SNo (x11 x30) (minus_SNo (add_SNo 1 x30)))(∀ x30 . x30int∀ x31 . x31intx13 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x13 (add_SNo x30 (minus_SNo 1)) x31) x30))(∀ x30 . x30intx14 x30 = x13 (x6 x30) (x12 x30))(∀ x30 . x30intx15 x30 = x14 x30)(∀ x30 . x30intx16 x30 = add_SNo x30 x30)(∀ x30 . x30intx17 x30 = x30)x18 = 2(∀ x30 . x30int∀ x31 . x31intx19 x30 x31 = If_i (SNoLe x30 0) x31 (x16 (x19 (add_SNo x30 (minus_SNo 1)) x31)))(∀ x30 . x30intx20 x30 = x19 (x17 x30) x18)(∀ x30 . x30int∀ x31 . x31intx21 x30 x31 = mul_SNo x30 x31)(∀ x30 . x30int∀ x31 . x31intx22 x30 x31 = add_SNo x31 x31)(∀ x30 . x30intx23 x30 = x30)x24 = 1x25 = 2(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30int∀ x31 . x31int∀ x32 . x32intx27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32)))(∀ x30 . x30intx28 x30 = x26 (x23 x30) x24 x25)(∀ x30 . x30intx29 x30 = mul_SNo (add_SNo (add_SNo (x20 x30) (minus_SNo 1)) (minus_SNo x30)) (x28 x30))∀ x30 . x30intSNoLe 0 x30x15 x30 = x29 x30
Conjecture 21466..A277491 : ∀ 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 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 . x12int∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo (add_SNo x19 x19) x19)(∀ x18 . x18int∀ x19 . x19intx1 x18 x19 = add_SNo (add_SNo x18 x18) x19)(∀ x18 . x18intx2 x18 = add_SNo x18 x18)x3 = 1x4 = 2(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx5 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x0 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx6 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x1 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 x4)(∀ x18 . x18intx8 x18 = x7 x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = mul_SNo 2 (add_SNo (mul_SNo x19 x19) (add_SNo x18 x18)))(∀ x18 . x18int∀ x19 . x19intx10 x18 x19 = add_SNo (add_SNo x19 x19) x19)(∀ x18 . x18intx11 x18 = x18)x12 = 1x13 = 2(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) x12 x13)(∀ x18 . x18intx17 x18 = x16 x18)∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18