Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrMH8../92b67..
PUK4c../91f63..
vout
PrMH8../b796e.. 0.08 bars
PURs3../aebc1.. doc published by PrGxv..
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param If_iIf_i : οιιι
Param SNoLeSNoLe : ιιο
Param minus_SNominus_SNo : ιι
Conjecture 748b5..A6523 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 . x8int∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25int∀ x26 . x26intx0 x25 x26 = add_SNo (mul_SNo x25 x26) x25)(∀ x25 . x25intx1 x25 = mul_SNo 2 (add_SNo x25 x25))x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx4 x25 = x3 (x1 x25) x2)(∀ x25 . x25intx5 x25 = x4 x25)(∀ x25 . x25int∀ x26 . x26intx6 x25 x26 = mul_SNo 2 (mul_SNo x25 x26))(∀ x25 . x25intx7 x25 = x25)x8 = 2(∀ x25 . x25int∀ x26 . x26intx9 x25 x26 = If_i (SNoLe x25 0) x26 (x6 (x9 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx10 x25 = x9 (x7 x25) x8)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = add_SNo 2 x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1x15 = add_SNo 1 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 = mul_SNo (x10 x25) (x18 x25))x20 = 1(∀ x25 . x25intx21 x25 = add_SNo x25 x25)(∀ 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 (x21 x25))(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x5 x25 = x24 x25
Conjecture c5c90..A65142 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι . (∀ x23 . x23int∀ x24 . x24intx22 x23 x24int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo x25 x25)(∀ x25 . x25intx1 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx2 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25intx3 x25 = add_SNo (add_SNo x25 x25) x25)(∀ x25 . x25intx4 x25 = add_SNo 1 x25)(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = If_i (SNoLe x25 0) x26 (x2 (x5 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx6 x25 = x5 (x3 x25) (x4 x25))(∀ x25 . x25intx7 x25 = x6 x25)(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x1 x25) (x7 x25))(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo 2 (mul_SNo x25 x26))(∀ x25 . x25int∀ x26 . x26intx12 x25 x26 = add_SNo 1 x26)(∀ x25 . x25intx13 x25 = x25)x14 = 1(∀ x25 . x25intx15 x25 = add_SNo 1 (add_SNo x25 x25))(∀ 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))(∀ x25 . x25int∀ x26 . x26intx19 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25intx20 x25 = add_SNo x25 x25)(∀ x25 . x25intx21 x25 = add_SNo 1 x25)(∀ x25 . x25int∀ x26 . x26intx22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx23 x25 = x22 (x20 x25) (x21 x25))(∀ x25 . x25intx24 x25 = mul_SNo (x18 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture 4b044..A65140 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = add_SNo x25 x25)(∀ x25 . x25intx1 x25 = x25)(∀ x25 . x25int∀ x26 . x26intx2 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25intx3 x25 = add_SNo x25 x25)x4 = 1(∀ x25 . x25int∀ x26 . x26intx5 x25 x26 = If_i (SNoLe x25 0) x26 (x2 (x5 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx6 x25 = x5 (x3 x25) x4)(∀ x25 . x25intx7 x25 = x6 x25)(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25intx9 x25 = x8 (x1 x25) (x7 x25))(∀ x25 . x25intx10 x25 = x9 x25)(∀ x25 . x25int∀ x26 . x26intx11 x25 x26 = mul_SNo 2 (mul_SNo x25 x26))(∀ x25 . x25intx12 x25 = x25)(∀ x25 . x25intx13 x25 = add_SNo 1 x25)(∀ x25 . x25int∀ x26 . x26intx14 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x14 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx15 x25 = x14 (x12 x25) (x13 x25))(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = mul_SNo x25 x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = add_SNo 1 x26)(∀ x25 . x25intx18 x25 = add_SNo x25 (minus_SNo 1))x19 = 1(∀ x25 . x25intx20 x25 = add_SNo 2 x25)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 (x20 x25))(∀ x25 . x25intx24 x25 = mul_SNo (x15 x25) (x23 x25))∀ x25 . x25intSNoLe 0 x25x10 x25 = x24 x25
Conjecture fc1a3..A6483 : ∀ 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 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ 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 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = add_SNo x24 x24)(∀ x23 . x23int∀ x24 . x24intx1 x23 x24 = mul_SNo 2 (add_SNo x23 x24))(∀ x23 . x23intx2 x23 = x23)x3 = 0x4 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx7 x23 = x5 (x2 x23) x3 x4)(∀ x23 . x23intx8 x23 = add_SNo 1 (x7 x23))(∀ x23 . x23intx9 x23 = add_SNo x23 x23)(∀ x23 . x23intx10 x23 = add_SNo x23 (minus_SNo 1))(∀ x23 . x23int∀ x24 . x24intx11 x23 x24 = add_SNo x23 x24)(∀ x23 . x23intx12 x23 = x23)(∀ x23 . x23intx13 x23 = add_SNo x23 (minus_SNo 2))x14 = 2x15 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx16 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x11 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25) (x17 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx17 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x12 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx18 x23 = x16 (x13 x23) x14 x15)(∀ x23 . x23intx19 x23 = If_i (SNoLe x23 0) 0 (x18 x23))(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x9 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x10 x23) (x19 x23))(∀ x23 . x23intx22 x23 = add_SNo 1 (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23
Conjecture af699..A64752 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ 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 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = add_SNo (add_SNo (mul_SNo x20 x21) x20) x21)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 x1 (x2 x20))(∀ x20 . x20intx5 x20 = x4 x20)(∀ x20 . x20intx6 x20 = add_SNo 1 x20)(∀ x20 . x20intx7 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) (x7 x20))(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = add_SNo 1 x20)(∀ x20 . x20intx14 x20 = add_SNo 1 x20)x15 = add_SNo 2 (add_SNo 2 2)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) (x14 x20) x15)(∀ x20 . x20intx19 x20 = add_SNo (x18 x20) (minus_SNo 1))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 11d0d..A64749 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 . x15int∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo (add_SNo 2 x21) x20)x1 = 2(∀ x20 . x20intx2 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx4 x20 = x3 x1 (x2 x20))(∀ x20 . x20intx5 x20 = add_SNo (x4 x20) (minus_SNo x20))(∀ x20 . x20intx6 x20 = x20)(∀ x20 . x20intx7 x20 = x20)(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21)))(∀ x20 . x20intx9 x20 = x8 (x6 x20) (x7 x20))(∀ x20 . x20intx10 x20 = add_SNo 1 (x9 x20))(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = mul_SNo x20 x21)(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = x21)(∀ x20 . x20intx13 x20 = x20)x14 = 1x15 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 x15)(∀ x20 . x20intx19 x20 = add_SNo 1 (mul_SNo x20 (x18 x20)))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture 32829..A64671 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 : ι → ι . (∀ x4 . x4intx3 x4int)∀ x4 . x4int∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι . (∀ x15 . x15intx14 x15int)∀ x15 . x15int∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22intx0 x22 = add_SNo x22 x22)(∀ x22 . x22intx1 x22 = x22)(∀ x22 . x22int∀ x23 . x23intx2 x22 x23 = add_SNo (add_SNo x22 x23) x22)(∀ x22 . x22intx3 x22 = x22)x4 = 0(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx6 x22 = x5 (x3 x22) x4)(∀ x22 . x22intx7 x22 = x6 x22)(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx9 x22 = x8 (x1 x22) (x7 x22))(∀ x22 . x22intx10 x22 = add_SNo (x9 x22) x22)(∀ x22 . x22intx11 x22 = add_SNo x22 x22)(∀ x22 . x22intx12 x22 = x22)(∀ x22 . x22intx13 x22 = add_SNo x22 x22)(∀ x22 . x22intx14 x22 = x22)x15 = 2(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx17 x22 = x16 (x14 x22) x15)(∀ x22 . x22intx18 x22 = add_SNo (x17 x22) (minus_SNo (add_SNo 2 x22)))(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23)))(∀ x22 . x22intx20 x22 = x19 (x12 x22) (x18 x22))(∀ x22 . x22intx21 x22 = add_SNo (x20 x22) x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 3329c..A62395 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 . x10int∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)(∀ x17 . x17intx0 x17 = add_SNo x17 x17)(∀ x17 . x17intx1 x17 = add_SNo (add_SNo x17 x17) x17)x2 = 1(∀ x17 . x17int∀ x18 . x18intx3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx4 x17 = x3 (x1 x17) x2)(∀ x17 . x17intx5 x17 = add_SNo 1 (x4 x17))(∀ x17 . x17intx6 x17 = mul_SNo (mul_SNo x17 x17) x17)x7 = 1(∀ x17 . x17intx8 x17 = add_SNo x17 x17)(∀ x17 . x17intx9 x17 = x17)x10 = 1(∀ x17 . x17int∀ x18 . x18intx11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx12 x17 = x11 (x9 x17) x10)(∀ x17 . x17intx13 x17 = x12 x17)(∀ x17 . x17int∀ x18 . x18intx14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18)))(∀ x17 . x17intx15 x17 = x14 x7 (x13 x17))(∀ x17 . x17intx16 x17 = add_SNo 1 (x15 x17))∀ x17 . x17intSNoLe 0 x17x5 x17 = x16 x17
Conjecture 46e8b..A6234 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 . x1int∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι → ι . (∀ x11 . x11int∀ x12 . x12intx10 x11 x12int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo (add_SNo (add_SNo x18 x18) x18) x19)x1 = 0(∀ x18 . x18intx2 x18 = x18)x3 = 1(∀ x18 . x18intx4 x18 = x18)(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx5 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x0 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx6 x18 x19 x20 = If_i (SNoLe x18 0) x20 x1)(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 (x4 x18))(∀ x18 . x18intx8 x18 = x7 x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = mul_SNo x18 x19)(∀ x18 . x18int∀ x19 . x19intx10 x18 x19 = x19)(∀ x18 . x18intx11 x18 = add_SNo x18 (minus_SNo 1))(∀ x18 . x18intx12 x18 = add_SNo 1 (add_SNo 2 x18))x13 = add_SNo 1 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 x18) x13)(∀ x18 . x18intx17 x18 = If_i (SNoLe x18 0) 1 (x16 x18))∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture c2780..A6231 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 . x13int∀ x14 : ι → ι → ι . (∀ x15 . x15int∀ x16 . x16intx14 x15 x16int)∀ x15 : ι → ι → ι . (∀ x16 . x16int∀ x17 . x17intx15 x16 x17int)∀ x16 : ι → ι → ι . (∀ x17 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22int∀ x23 . x23intx0 x22 x23 = add_SNo (mul_SNo x22 x23) x23)(∀ x22 . x22int∀ x23 . x23intx1 x22 x23 = x23)x2 = 0(∀ x22 . x22int∀ x23 . x23intx3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22int∀ x23 . x23intx4 x22 x23 = x3 (x1 x22 x23) x2)(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = add_SNo (x4 x22 x23) x22)(∀ x22 . x22intx6 x22 = x22)x7 = 0(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x5 (x8 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx9 x22 = x8 (x6 x22) x7)(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22int∀ x23 . x23intx11 x22 x23 = add_SNo 1 (mul_SNo x22 x23))(∀ x22 . x22int∀ x23 . x23intx12 x22 x23 = add_SNo x23 (minus_SNo 1))x13 = 1(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x14 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22int∀ x23 . x23intx15 x22 x23 = x14 (x12 x22 x23) x13)(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = add_SNo (mul_SNo (x15 x22 x23) x23) x22)(∀ x22 . x22intx17 x22 = x22)x18 = 0(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x16 (x19 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx20 x22 = x19 (x17 x22) x18)(∀ x22 . x22intx21 x22 = x20 x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 83b45..A62119 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ x6 : ι → ι → ι . (∀ x7 . x7int∀ x8 . x8intx6 x7 x8int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)(∀ x12 . x12int∀ x13 . x13intx0 x12 x13 = add_SNo (mul_SNo x12 x13) x12)(∀ x12 . x12intx1 x12 = x12)(∀ x12 . x12intx2 x12 = x12)(∀ x12 . x12int∀ x13 . x13intx3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx4 x12 = x3 (x1 x12) (x2 x12))(∀ x12 . x12intx5 x12 = x4 x12)(∀ x12 . x12int∀ x13 . x13intx6 x12 x13 = mul_SNo x12 x13)(∀ x12 . x12intx7 x12 = x12)(∀ x12 . x12intx8 x12 = x12)(∀ x12 . x12int∀ x13 . x13intx9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13) x12))(∀ x12 . x12intx10 x12 = x9 (x7 x12) (x8 x12))(∀ x12 . x12intx11 x12 = mul_SNo (add_SNo 1 x12) (x10 x12))∀ x12 . x12intSNoLe 0 x12x5 x12 = x11 x12
Conjecture 66ba6..A61788 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x11int∀ x12 . x12int∀ x13 : ι → ι → ι → ι . (∀ x14 . x14int∀ x15 . x15int∀ x16 . x16intx13 x14 x15 x16int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ 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 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι . (∀ x27 . x27intx26 x27int)∀ x27 : ι → ι → ι . (∀ x28 . x28int∀ x29 . x29intx27 x28 x29int)∀ x28 : ι → ι → ι . (∀ x29 . x29int∀ x30 . x30intx28 x29 x30int)∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι . (∀ x31 . x31intx30 x31int)∀ x31 : ι → ι . (∀ x32 . x32intx31 x32int)∀ x32 : ι → ι → ι → ι . (∀ x33 . x33int∀ x34 . x34int∀ x35 . x35intx32 x33 x34 x35int)∀ x33 : ι → ι → ι → ι . (∀ x34 . x34int∀ x35 . x35int∀ x36 . x36intx33 x34 x35 x36int)∀ x34 : ι → ι . (∀ x35 . x35intx34 x35int)∀ x35 : ι → ι → ι . (∀ x36 . x36int∀ x37 . x37intx35 x36 x37int)∀ x36 : ι → ι → ι . (∀ x37 . x37int∀ x38 . x38intx36 x37 x38int)∀ x37 : ι → ι . (∀ x38 . x38intx37 x38int)∀ x38 : ι → ι . (∀ x39 . x39intx38 x39int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 : ι → ι → ι → ι . (∀ x41 . x41int∀ x42 . x42int∀ x43 . x43intx40 x41 x42 x43int)∀ x41 : ι → ι → ι → ι . (∀ x42 . x42int∀ x43 . x43int∀ x44 . x44intx41 x42 x43 x44int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)∀ x44 . x44int∀ x45 : ι → ι → ι . (∀ x46 . x46int∀ x47 . x47intx45 x46 x47int)∀ x46 : ι → ι → ι . (∀ x47 . x47int∀ x48 . x48intx46 x47 x48int)∀ x47 : ι → ι → ι . (∀ x48 . x48int∀ x49 . x49intx47 x48 x49int)∀ x48 : ι → ι → ι . (∀ x49 . x49int∀ x50 . x50intx48 x49 x50int)∀ x49 : ι → ι . (∀ x50 . x50intx49 x50int)∀ x50 . x50int∀ x51 : ι → ι → ι . (∀ x52 . x52int∀ x53 . x53intx51 x52 x53int)∀ x52 : ι → ι . (∀ x53 . x53intx52 x53int)∀ x53 : ι → ι . (∀ x54 . x54intx53 x54int)(∀ x54 . x54int∀ x55 . x55intx0 x54 x55 = mul_SNo x54 x55)(∀ x54 . x54int∀ x55 . x55intx1 x54 x55 = x55)(∀ x54 . x54int∀ x55 . x55intx2 x54 x55 = x55)x3 = 1(∀ x54 . x54int∀ x55 . x55intx4 x54 x55 = x55)(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx5 x54 x55 x56 = If_i (SNoLe x54 0) x55 (x0 (x5 (add_SNo x54 (minus_SNo 1)) x55 x56) (x6 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx6 x54 x55 x56 = If_i (SNoLe x54 0) x56 (x1 (x5 (add_SNo x54 (minus_SNo 1)) x55 x56) (x6 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54int∀ x55 . x55intx7 x54 x55 = x5 (x2 x54 x55) x3 (x4 x54 x55))(∀ x54 . x54int∀ x55 . x55intx8 x54 x55 = add_SNo (x7 x54 x55) x54)(∀ x54 . x54int∀ x55 . x55intx9 x54 x55 = add_SNo 2 x55)(∀ x54 . x54intx10 x54 = add_SNo x54 1)x11 = 0x12 = 2(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx13 x54 x55 x56 = If_i (SNoLe x54 0) x55 (x8 (x13 (add_SNo x54 (minus_SNo 1)) x55 x56) (x14 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx14 x54 x55 x56 = If_i (SNoLe x54 0) x56 (x9 (x13 (add_SNo x54 (minus_SNo 1)) x55 x56) (x14 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54intx15 x54 = x13 (x10 x54) x11 x12)(∀ x54 . x54intx16 x54 = x15 x54)(∀ x54 . x54intx17 x54 = mul_SNo x54 x54)x18 = 1(∀ x54 . x54intx19 x54 = add_SNo x54 x54)(∀ x54 . x54intx20 x54 = x54)x21 = 1(∀ x54 . x54int∀ x55 . x55intx22 x54 x55 = If_i (SNoLe x54 0) x55 (x19 (x22 (add_SNo x54 (minus_SNo 1)) x55)))(∀ x54 . x54intx23 x54 = x22 (x20 x54) x21)(∀ x54 . x54intx24 x54 = x23 x54)(∀ x54 . x54int∀ x55 . x55intx25 x54 x55 = If_i (SNoLe x54 0) x55 (x17 (x25 (add_SNo x54 (minus_SNo 1)) x55)))(∀ x54 . x54intx26 x54 = x25 x18 (x24 x54))(∀ x54 . x54int∀ x55 . x55intx27 x54 x55 = mul_SNo x54 x55)(∀ x54 . x54int∀ x55 . x55intx28 x54 x55 = x55)(∀ x54 . x54intx29 x54 = x54)(∀ x54 . x54intx30 x54 = add_SNo 1 x54)(∀ x54 . x54intx31 x54 = add_SNo 1 x54)(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx32 x54 x55 x56 = If_i (SNoLe x54 0) x55 (x27 (x32 (add_SNo x54 (minus_SNo 1)) x55 x56) (x33 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx33 x54 x55 x56 = If_i (SNoLe x54 0) x56 (x28 (x32 (add_SNo x54 (minus_SNo 1)) x55 x56) (x33 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54intx34 x54 = x32 (x29 x54) (x30 x54) (x31 x54))(∀ x54 . x54int∀ x55 . x55intx35 x54 x55 = mul_SNo x54 x55)(∀ x54 . x54int∀ x55 . x55intx36 x54 x55 = x55)(∀ x54 . x54intx37 x54 = x54)(∀ x54 . x54intx38 x54 = add_SNo 1 x54)(∀ x54 . x54intx39 x54 = add_SNo 1 x54)(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx40 x54 x55 x56 = If_i (SNoLe x54 0) x55 (x35 (x40 (add_SNo x54 (minus_SNo 1)) x55 x56) (x41 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54int∀ x55 . x55int∀ x56 . x56intx41 x54 x55 x56 = If_i (SNoLe x54 0) x56 (x36 (x40 (add_SNo x54 (minus_SNo 1)) x55 x56) (x41 (add_SNo x54 (minus_SNo 1)) x55 x56)))(∀ x54 . x54intx42 x54 = x40 (x37 x54) (x38 x54) (x39 x54))(∀ x54 . x54intx43 x54 = mul_SNo (mul_SNo (mul_SNo 2 (x26 x54)) (x34 x54)) (x42 x54))x44 = 1(∀ x54 . x54int∀ x55 . x55intx45 x54 x55 = x55)(∀ x54 . x54int∀ x55 . x55intx46 x54 x55 = If_i (SNoLe x54 0) x55 (x43 (x46 (add_SNo x54 (minus_SNo 1)) x55)))(∀ x54 . x54int∀ x55 . x55intx47 x54 x55 = x46 x44 (x45 x54 x55))(∀ x54 . x54int∀ x55 . x55intx48 x54 x55 = add_SNo (x47 x54 x55) x54)(∀ x54 . x54intx49 x54 = x54)x50 = 1(∀ x54 . x54int∀ x55 . x55intx51 x54 x55 = If_i (SNoLe x54 0) x55 (x48 (x51 (add_SNo x54 (minus_SNo 1)) x55) x54))(∀ x54 . x54intx52 x54 = x51 (x49 x54) x50)(∀ x54 . x54intx53 x54 = add_SNo (mul_SNo (x52 x54) 2) 2)∀ x54 . x54intSNoLe 0 x54x16 x54 = x53 x54
Conjecture 6584a..A61787 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 . x11int∀ x12 . x12int∀ x13 : ι → ι → ι → ι . (∀ x14 . x14int∀ x15 . x15int∀ x16 . x16intx13 x14 x15 x16int)∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)∀ x20 . x20int∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι → ι → ι . (∀ x24 . x24int∀ x25 . x25int∀ x26 . x26intx23 x24 x25 x26int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)∀ x25 : ι → ι → ι . (∀ x26 . x26int∀ x27 . x27intx25 x26 x27int)∀ x26 : ι → ι → ι . (∀ x27 . x27int∀ x28 . x28intx26 x27 x28int)∀ x27 : ι → ι . (∀ x28 . x28intx27 x28int)∀ x28 . x28int∀ x29 : ι → ι . (∀ x30 . x30intx29 x30int)∀ x30 : ι → ι → ι → ι . (∀ x31 . x31int∀ x32 . x32int∀ x33 . x33intx30 x31 x32 x33int)∀ x31 : ι → ι → ι → ι . (∀ x32 . x32int∀ x33 . x33int∀ x34 . x34intx31 x32 x33 x34int)∀ x32 : ι → ι . (∀ x33 . x33intx32 x33int)∀ x33 : ι → ι . (∀ x34 . x34intx33 x34int)∀ 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 . x39int∀ x40 . x40intx38 x39 x40int)∀ x39 : ι → ι . (∀ x40 . x40intx39 x40int)∀ x40 . x40int∀ x41 : ι → ι → ι . (∀ x42 . x42int∀ x43 . x43intx41 x42 x43int)∀ x42 : ι → ι . (∀ x43 . x43intx42 x43int)∀ x43 : ι → ι . (∀ x44 . x44intx43 x44int)(∀ x44 . x44int∀ x45 . x45intx0 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx1 x44 x45 = x45)(∀ x44 . x44int∀ x45 . x45intx2 x44 x45 = x45)x3 = 1(∀ x44 . x44int∀ x45 . x45intx4 x44 x45 = x45)(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx5 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x0 (x5 (add_SNo x44 (minus_SNo 1)) x45 x46) (x6 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx6 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x1 (x5 (add_SNo x44 (minus_SNo 1)) x45 x46) (x6 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45intx7 x44 x45 = x5 (x2 x44 x45) x3 (x4 x44 x45))(∀ x44 . x44int∀ x45 . x45intx8 x44 x45 = add_SNo (x7 x44 x45) x44)(∀ x44 . x44int∀ x45 . x45intx9 x44 x45 = add_SNo 2 x45)(∀ x44 . x44intx10 x44 = x44)x11 = 1x12 = add_SNo 1 2(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx13 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x8 (x13 (add_SNo x44 (minus_SNo 1)) x45 x46) (x14 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx14 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x9 (x13 (add_SNo x44 (minus_SNo 1)) x45 x46) (x14 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx15 x44 = x13 (x10 x44) x11 x12)(∀ x44 . x44intx16 x44 = x15 x44)(∀ x44 . x44int∀ x45 . x45intx17 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx18 x44 x45 = x45)(∀ x44 . x44intx19 x44 = add_SNo 1 x44)x20 = 1(∀ x44 . x44intx21 x44 = add_SNo 1 (add_SNo x44 x44))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx22 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x17 (x22 (add_SNo x44 (minus_SNo 1)) x45 x46) (x23 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx23 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x18 (x22 (add_SNo x44 (minus_SNo 1)) x45 x46) (x23 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx24 x44 = x22 (x19 x44) x20 (x21 x44))(∀ x44 . x44int∀ x45 . x45intx25 x44 x45 = mul_SNo x44 x45)(∀ x44 . x44int∀ x45 . x45intx26 x44 x45 = x45)(∀ x44 . x44intx27 x44 = x44)x28 = 1(∀ x44 . x44intx29 x44 = add_SNo 1 (add_SNo x44 x44))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx30 x44 x45 x46 = If_i (SNoLe x44 0) x45 (x25 (x30 (add_SNo x44 (minus_SNo 1)) x45 x46) (x31 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44int∀ x45 . x45int∀ x46 . x46intx31 x44 x45 x46 = If_i (SNoLe x44 0) x46 (x26 (x30 (add_SNo x44 (minus_SNo 1)) x45 x46) (x31 (add_SNo x44 (minus_SNo 1)) x45 x46)))(∀ x44 . x44intx32 x44 = x30 (x27 x44) x28 (x29 x44))(∀ x44 . x44intx33 x44 = mul_SNo (x24 x44) (x32 x44))x34 = 1(∀ x44 . x44int∀ x45 . x45intx35 x44 x45 = x45)(∀ x44 . x44int∀ x45 . x45intx36 x44 x45 = If_i (SNoLe x44 0) x45 (x33 (x36 (add_SNo x44 (minus_SNo 1)) x45)))(∀ x44 . x44int∀ x45 . x45intx37 x44 x45 = x36 x34 (x35 x44 x45))(∀ x44 . x44int∀ x45 . x45intx38 x44 x45 = add_SNo (x37 x44 x45) x44)(∀ x44 . x44intx39 x44 = x44)x40 = 1(∀ x44 . x44int∀ x45 . x45intx41 x44 x45 = If_i (SNoLe x44 0) x45 (x38 (x41 (add_SNo x44 (minus_SNo 1)) x45) x44))(∀ x44 . x44intx42 x44 = x41 (x39 x44) x40)(∀ x44 . x44intx43 x44 = x42 x44)∀ x44 . x44intSNoLe 0 x44x16 x44 = x43 x44
Conjecture 22bc7..A61705 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι . (∀ x2 . x2intx1 x2int)∀ x2 : ι → ι . (∀ x3 . x3intx2 x3int)∀ x3 . x3int∀ x4 : ι → ι . (∀ x5 . x5intx4 x5int)∀ x5 : ι → ι → ι → ι . (∀ x6 . x6int∀ x7 . x7int∀ x8 . x8intx5 x6 x7 x8int)∀ x6 : ι → ι → ι → ι . (∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx6 x7 x8 x9int)∀ x7 : ι → ι . (∀ x8 . x8intx7 x8int)∀ x8 : ι → ι . (∀ x9 . x9intx8 x9int)∀ x9 : ι → ι → ι . (∀ x10 . x10int∀ x11 . x11intx9 x10 x11int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι . (∀ x12 . x12intx11 x12int)∀ x12 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)(∀ x18 . x18int∀ x19 . x19intx0 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx1 x18 = x18)(∀ x18 . x18intx2 x18 = add_SNo 1 x18)x3 = 2(∀ x18 . x18intx4 x18 = x18)(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx5 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x0 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx6 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x1 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx7 x18 = x5 (x2 x18) x3 (x4 x18))(∀ x18 . x18intx8 x18 = x7 x18)(∀ x18 . x18int∀ x19 . x19intx9 x18 x19 = add_SNo x18 x19)(∀ x18 . x18intx10 x18 = x18)(∀ x18 . x18intx11 x18 = x18)(∀ x18 . x18intx12 x18 = add_SNo 2 x18)x13 = 2(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx14 x18 x19 x20 = If_i (SNoLe x18 0) x19 (x9 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20)))(∀ x18 . x18intx16 x18 = x14 (x11 x18) (x12 x18) x13)(∀ x18 . x18intx17 x18 = x16 x18)∀ x18 . x18intSNoLe 0 x18x8 x18 = x17 x18
Conjecture 60e8e..A61572 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι → ι . (∀ x14 . 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 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 . x18int∀ x19 : ι → ι → ι . (∀ x20 . x20int∀ x21 . x21intx19 x20 x21int)∀ x20 : ι → ι . (∀ x21 . x21intx20 x21int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)(∀ x22 . x22int∀ x23 . x23intx0 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22int∀ x23 . x23intx1 x22 x23 = x23)x2 = 1(∀ x22 . x22int∀ x23 . x23intx3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22int∀ x23 . x23intx4 x22 x23 = x3 (x1 x22 x23) x2)(∀ x22 . x22int∀ x23 . x23intx5 x22 x23 = add_SNo (add_SNo (mul_SNo (add_SNo 2 x23) (mul_SNo x22 x23)) (x4 x22 x23)) x22)(∀ x22 . x22intx6 x22 = x22)x7 = 1(∀ x22 . x22int∀ x23 . x23intx8 x22 x23 = If_i (SNoLe x22 0) x23 (x5 (x8 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx9 x22 = x8 (x6 x22) x7)(∀ x22 . x22intx10 x22 = x9 x22)(∀ x22 . x22int∀ x23 . x23intx11 x22 x23 = mul_SNo x22 x23)(∀ x22 . x22int∀ x23 . x23intx12 x22 x23 = add_SNo x23 (minus_SNo 1))(∀ x22 . x22int∀ x23 . x23intx13 x22 x23 = x23)(∀ x22 . x22int∀ x23 . x23intx14 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x14 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22int∀ x23 . x23intx15 x22 x23 = x14 (x12 x22 x23) (x13 x22 x23))(∀ x22 . x22int∀ x23 . x23intx16 x22 x23 = add_SNo (x15 x22 x23) (mul_SNo (mul_SNo (add_SNo 1 x23) (add_SNo 1 x23)) x22))(∀ x22 . x22intx17 x22 = x22)x18 = 1(∀ x22 . x22int∀ x23 . x23intx19 x22 x23 = If_i (SNoLe x22 0) x23 (x16 (x19 (add_SNo x22 (minus_SNo 1)) x23) x22))(∀ x22 . x22intx20 x22 = x19 (x17 x22) x18)(∀ x22 . x22intx21 x22 = x20 x22)∀ x22 . x22intSNoLe 0 x22x10 x22 = x21 x22
Conjecture 69259..A6125 : ∀ 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 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = mul_SNo x23 x24)(∀ x23 . x23int∀ x24 . x24intx1 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx2 x23 = x23)x3 = 1x4 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx7 x23 = x5 (x2 x23) x3 x4)(∀ x23 . x23intx8 x23 = x7 x23)(∀ x23 . x23int∀ x24 . x24intx9 x23 x24 = mul_SNo x23 x24)(∀ x23 . x23int∀ x24 . x24intx10 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx11 x23 = add_SNo x23 (minus_SNo 2))x12 = 1x13 = 1(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx14 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x9 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx15 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x10 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx16 x23 = x14 (x11 x23) x12 x13)(∀ x23 . x23intx17 x23 = add_SNo x23 x23)(∀ x23 . x23intx18 x23 = add_SNo (add_SNo (add_SNo x23 (minus_SNo 1)) x23) (minus_SNo 2))x19 = 1(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x17 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x18 x23) x19)(∀ x23 . x23intx22 x23 = mul_SNo (x16 x23) (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23
Conjecture 69b3c..A61062 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ x5 : ι → ι → ι . (∀ x6 . x6int∀ x7 . x7intx5 x6 x7int)∀ x6 : ι → ι . (∀ x7 . x7intx6 x7int)∀ x7 . x7int∀ x8 : ι → ι → ι . (∀ x9 . x9int∀ x10 . x10intx8 x9 x10int)∀ x9 : ι → ι . (∀ x10 . x10intx9 x10int)∀ x10 : ι → ι . (∀ x11 . x11intx10 x11int)∀ x11 : ι → ι → ι . (∀ x12 . x12int∀ x13 . x13intx11 x12 x13int)∀ x12 : ι → ι → ι . (∀ x13 . x13int∀ x14 . x14intx12 x13 x14int)∀ x13 : ι → ι . (∀ x14 . x14intx13 x14int)∀ x14 . x14int∀ x15 : ι → ι . (∀ x16 . x16intx15 x16int)∀ x16 : ι → ι → ι → ι . (∀ x17 . x17int∀ x18 . x18int∀ x19 . x19intx16 x17 x18 x19int)∀ x17 : ι → ι → ι → ι . (∀ x18 . x18int∀ x19 . x19int∀ x20 . x20intx17 x18 x19 x20int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 : ι → ι . (∀ x20 . x20intx19 x20int)(∀ x20 . x20int∀ x21 . x21intx0 x20 x21 = mul_SNo (mul_SNo x20 x21) x21)(∀ x20 . x20int∀ x21 . x21intx1 x20 x21 = x21)x2 = 1(∀ x20 . x20int∀ x21 . x21intx3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20int∀ x21 . x21intx4 x20 x21 = x3 (x1 x20 x21) x2)(∀ x20 . x20int∀ x21 . x21intx5 x20 x21 = add_SNo (x4 x20 x21) x20)(∀ x20 . x20intx6 x20 = x20)x7 = 1(∀ x20 . x20int∀ x21 . x21intx8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20))(∀ x20 . x20intx9 x20 = x8 (x6 x20) x7)(∀ x20 . x20intx10 x20 = x9 x20)(∀ x20 . x20int∀ x21 . x21intx11 x20 x21 = add_SNo 1 (mul_SNo (mul_SNo x21 x21) x20))(∀ x20 . x20int∀ x21 . x21intx12 x20 x21 = add_SNo x21 (minus_SNo 1))(∀ x20 . x20intx13 x20 = add_SNo x20 (minus_SNo 1))x14 = 1(∀ x20 . x20intx15 x20 = x20)(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20int∀ x21 . x21int∀ x22 . x22intx17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22)))(∀ x20 . x20intx18 x20 = x16 (x13 x20) x14 (x15 x20))(∀ x20 . x20intx19 x20 = add_SNo (x18 x20) (If_i (SNoLe x20 0) 0 1))∀ x20 . x20intSNoLe 0 x20x10 x20 = x19 x20
Conjecture d22da..A6105 : ∀ x0 : ι → ι . (∀ x1 . x1intx0 x1int)∀ x1 . x1int∀ x2 . x2int∀ x3 : ι → ι → ι . (∀ x4 . x4int∀ x5 . x5intx3 x4 x5int)∀ x4 . x4int∀ x5 : ι → ι . (∀ x6 . x6intx5 x6int)∀ 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 . x17int∀ x18 . x18intx16 x17 x18int)∀ x17 : ι → ι → ι . (∀ x18 . x18int∀ x19 . x19intx17 x18 x19int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 . x20int∀ x21 : ι → ι → ι → ι . (∀ x22 . x22int∀ x23 . x23int∀ x24 . x24intx21 x22 x23 x24int)∀ x22 : ι → ι → ι → ι . (∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx22 x23 x24 x25int)∀ x23 : ι → ι . (∀ x24 . x24intx23 x24int)∀ x24 : ι → ι . (∀ x25 . x25intx24 x25int)(∀ x25 . x25intx0 x25 = mul_SNo x25 x25)x1 = 2x2 = 2(∀ x25 . x25int∀ x26 . x26intx3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26)))x4 = x3 x1 x2(∀ x25 . x25intx5 x25 = add_SNo 1 (mul_SNo 2 (add_SNo x25 x25)))(∀ x25 . x25int∀ x26 . x26intx6 x25 x26 = x26)x7 = 1(∀ x25 . x25int∀ x26 . x26intx8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26)))(∀ x25 . x25int∀ x26 . x26intx9 x25 x26 = x8 (x6 x25 x26) x7)(∀ x25 . x25int∀ x26 . x26intx10 x25 x26 = add_SNo (mul_SNo x4 x25) (x9 x25 x26))(∀ x25 . x25intx11 x25 = x25)x12 = 1(∀ x25 . x25int∀ x26 . x26intx13 x25 x26 = If_i (SNoLe x25 0) x26 (x10 (x13 (add_SNo x25 (minus_SNo 1)) x26) x25))(∀ x25 . x25intx14 x25 = x13 (x11 x25) x12)(∀ x25 . x25intx15 x25 = x14 x25)(∀ x25 . x25int∀ x26 . x26intx16 x25 x26 = add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo x25 x25)))) x26)(∀ x25 . x25int∀ x26 . x26intx17 x25 x26 = add_SNo 1 (mul_SNo 2 (add_SNo x26 x26)))(∀ x25 . x25intx18 x25 = x25)x19 = 1x20 = add_SNo 1 (add_SNo 2 2)(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25int∀ x26 . x26int∀ x27 . x27intx22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27)))(∀ x25 . x25intx23 x25 = x21 (x18 x25) x19 x20)(∀ x25 . x25intx24 x25 = x23 x25)∀ x25 . x25intSNoLe 0 x25x15 x25 = x24 x25
Conjecture 6ebc6..A60946 : ∀ x0 : ι → ι → ι . (∀ x1 . x1int∀ x2 . x2intx0 x1 x2int)∀ x1 : ι → ι → ι . (∀ x2 . x2int∀ x3 . x3intx1 x2 x3int)∀ x2 : ι → ι → ι . (∀ x3 . x3int∀ x4 . x4intx2 x3 x4int)∀ x3 . x3int∀ x4 : ι → ι → ι . (∀ x5 . x5int∀ x6 . x6intx4 x5 x6int)∀ 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 : ι → ι → ι . (∀ x19 . x19int∀ x20 . x20intx18 x19 x20int)∀ 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 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx1 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx2 x28 x29 = x29)x3 = 1(∀ x28 . x28int∀ x29 . x29intx4 x28 x29 = add_SNo 1 x29)(∀ 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 x29))(∀ x28 . x28int∀ x29 . x29intx8 x28 x29 = add_SNo x28 (x7 x28 x29))(∀ 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 = mul_SNo x28 x29)(∀ x28 . x28int∀ x29 . x29intx15 x28 x29 = x29)(∀ x28 . x28int∀ x29 . x29intx16 x28 x29 = add_SNo x29 (minus_SNo 1))x17 = 1(∀ x28 . x28int∀ x29 . x29intx18 x28 x29 = add_SNo 1 x29)(∀ 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 x29))(∀ x28 . x28int∀ x29 . x29intx22 x28 x29 = add_SNo (mul_SNo (x21 x28 x29) (add_SNo 1 x29)) 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 a36e2..A6088 : ∀ 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 : ι → ι . (∀ x13 . x13intx12 x13int)∀ x13 . x13int∀ x14 : ι → ι → ι → ι . (∀ x15 . x15int∀ x16 . x16int∀ x17 . x17intx14 x15 x16 x17int)∀ x15 : ι → ι → ι → ι . (∀ x16 . x16int∀ x17 . x17int∀ x18 . x18intx15 x16 x17 x18int)∀ x16 : ι → ι . (∀ x17 . x17intx16 x17int)∀ x17 : ι → ι . (∀ x18 . x18intx17 x18int)∀ x18 : ι → ι . (∀ x19 . x19intx18 x19int)∀ x19 . x19int∀ x20 : ι → ι → ι . (∀ x21 . x21int∀ x22 . x22intx20 x21 x22int)∀ x21 : ι → ι . (∀ x22 . x22intx21 x22int)∀ x22 : ι → ι . (∀ x23 . x23intx22 x23int)(∀ x23 . x23int∀ x24 . x24intx0 x23 x24 = mul_SNo (add_SNo 2 x24) x23)(∀ x23 . x23int∀ x24 . x24intx1 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx2 x23 = x23)x3 = 1x4 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx5 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx6 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x5 (add_SNo x23 (minus_SNo 1)) x24 x25) (x6 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx7 x23 = x5 (x2 x23) x3 x4)(∀ x23 . x23intx8 x23 = x7 x23)(∀ x23 . x23int∀ x24 . x24intx9 x23 x24 = mul_SNo (add_SNo 1 x24) x23)(∀ x23 . x23int∀ x24 . x24intx10 x23 x24 = add_SNo x24 x24)(∀ x23 . x23intx11 x23 = add_SNo x23 (minus_SNo 1))(∀ x23 . x23intx12 x23 = If_i (SNoLe x23 0) 1 2)x13 = 2(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx14 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x9 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23int∀ x24 . x24int∀ x25 . x25intx15 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x10 (x14 (add_SNo x23 (minus_SNo 1)) x24 x25) (x15 (add_SNo x23 (minus_SNo 1)) x24 x25)))(∀ x23 . x23intx16 x23 = x14 (x11 x23) (x12 x23) x13)(∀ x23 . x23intx17 x23 = add_SNo x23 x23)(∀ x23 . x23intx18 x23 = x23)x19 = 1(∀ x23 . x23int∀ x24 . x24intx20 x23 x24 = If_i (SNoLe x23 0) x24 (x17 (x20 (add_SNo x23 (minus_SNo 1)) x24)))(∀ x23 . x23intx21 x23 = x20 (x18 x23) x19)(∀ x23 . x23intx22 x23 = mul_SNo (x16 x23) (x21 x23))∀ x23 . x23intSNoLe 0 x23x8 x23 = x22 x23