Proofgold Signed Transaction

Param int^int : ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Param add_SNo^add_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Conjecture 90e2e..^A13719 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = mul_SNo x25 x25) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x25 . x25 ∈ int ⟶ x5 x25 = mul_SNo (add_SNo x4 (minus_SNo 2)) x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 x25 = add_SNo 1 (add_SNo x25 x25)) ⟶ x7 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x9 x25 = x8 (x6 x25) x7) ⟶ (∀ x25 . x25 ∈ int ⟶ x10 x25 = x9 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = mul_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25)) x25)) x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = mul_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x14 x25 x26 = x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x25) ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x18 (x15 x25) x16 x17) ⟶ (∀ x25 . x25 ∈ int ⟶ x21 x25 = x20 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x22 x12 (x21 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture 52211..^A13718 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x0 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x1 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x2 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x4 x25 = x3 x1 (x2 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x5 x25 = add_SNo (x4 x25) x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 x25 = add_SNo 1 (add_SNo x25 x25)) ⟶ x7 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x9 x25 = x8 (x6 x25) x7) ⟶ (∀ x25 . x25 ∈ int ⟶ x10 x25 = x9 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = mul_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))) x25) x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = mul_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x14 x25 x26 = x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x25) ⟶ x16 = 1 ⟶ x17 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x18 (x15 x25) x16 x17) ⟶ (∀ x25 . x25 ∈ int ⟶ x21 x25 = x20 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x22 x12 (x21 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture fed16..^A13717 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x0 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x1 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x2 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x4 x25 = x3 x1 (x2 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x5 x25 = x4 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 x25 = add_SNo 1 (add_SNo x25 x25)) ⟶ x7 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x9 x25 = x8 (x6 x25) x7) ⟶ (∀ x25 . x25 ∈ int ⟶ x10 x25 = x9 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = mul_SNo (add_SNo (add_SNo x25 x25) x25) x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = mul_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x14 x25 x26 = x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x25) ⟶ x16 = 2 ⟶ x17 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x18 (x15 x25) x16 x17) ⟶ (∀ x25 . x25 ∈ int ⟶ x21 x25 = x20 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x22 x12 (x21 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture 0b361..^A13716 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x0 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x1 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x2 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x4 x25 = x3 x1 (x2 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x5 x25 = add_SNo (x4 x25) (minus_SNo x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 x25 = add_SNo 1 (add_SNo x25 x25)) ⟶ x7 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x9 x25 = x8 (x6 x25) x7) ⟶ (∀ x25 . x25 ∈ int ⟶ x10 x25 = x9 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25)) x25) x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = mul_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x14 x25 x26 = x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x25) ⟶ x16 = 1 ⟶ x17 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x18 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x13 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x19 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x14 (x18 (add_SNo x25 (minus_SNo 1)) x26 x27) (x19 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x18 (x15 x25) x16 x17) ⟶ (∀ x25 . x25 ∈ int ⟶ x21 x25 = x20 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x22 x25 x26 = If_i (SNoLe x25 0) x26 (x11 (x22 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x22 x12 (x21 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture e9cf2..^A13715 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ x0 x20 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x20 x20)) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x1 x20 = add_SNo 1 (add_SNo x20 x20)) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x3 (x1 x20) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = x4 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo x20 x20)) x20) (add_SNo x20 x20)) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x9 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ x11 = 1 ⟶ x12 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x13 (x10 x20) x11 x12) ⟶ (∀ x20 . x20 ∈ int ⟶ x16 x20 = x15 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 x7 (x16 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x5 x20 = x19 x20
Conjecture b3459..^A13714 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ x0 x20 = add_SNo (add_SNo x20 x20) x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x1 x20 = add_SNo 2 (mul_SNo 2 (add_SNo x20 x20))) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x3 (x1 x20) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = x4 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = mul_SNo x20 x20) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x9 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ x11 = add_SNo 1 2 ⟶ x12 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x13 (x10 x20) x11 x12) ⟶ (∀ x20 . x20 ∈ int ⟶ x16 x20 = x15 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 x7 (x16 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x5 x20 = x19 x20
Conjecture 1c96e..^A13713 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ (∀ x22 . x22 ∈ int ⟶ x0 x22 = add_SNo x22 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x1 x22 = add_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x22 x22) x22))) ⟶ x2 = 2 ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x3 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x3 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x4 x22 = x3 (x1 x22) x2) ⟶ (∀ x22 . x22 ∈ int ⟶ x5 x22 = x4 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x6 x22 = mul_SNo (mul_SNo x22 x22) x22) ⟶ x7 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ x8 x22 = mul_SNo x22 x22) ⟶ x9 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ x10 x22 = add_SNo x22 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x11 x22 = x22) ⟶ x12 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x13 x22 x23 = If_i (SNoLe x22 0) x23 (x10 (x13 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x14 x22 = x13 (x11 x22) x12) ⟶ (∀ x22 . x22 ∈ int ⟶ x15 x22 = x14 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x16 x22 x23 = If_i (SNoLe x22 0) x23 (x8 (x16 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x17 x22 = x16 x9 (x15 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ x18 x22 = mul_SNo 2 (x17 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x19 x22 x23 = If_i (SNoLe x22 0) x23 (x6 (x19 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x20 x22 = x19 x7 (x18 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ x21 x22 = x20 x22) ⟶ ∀ x22 . x22 ∈ int ⟶ SNoLe 0 x22 ⟶ x5 x22 = x21 x22
Conjecture 7baf5..^A13712 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ x0 x20 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x20 x20) x20)) x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x1 x20 = add_SNo 1 (add_SNo x20 x20)) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x3 (x1 x20) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = x4 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x20 x20) x20)) x20) x20) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x9 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ x11 = 1 ⟶ x12 = add_SNo 1 (add_SNo 2 (add_SNo 2 2)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x13 (x10 x20) x11 x12) ⟶ (∀ x20 . x20 ∈ int ⟶ x16 x20 = x15 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 x7 (x16 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x5 x20 = x19 x20
Conjecture 03021..^A13711 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ x0 x20 = mul_SNo 2 (add_SNo (add_SNo x20 x20) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x1 x20 = add_SNo 1 (add_SNo x20 x20)) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x3 (x1 x20) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = x4 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = mul_SNo (add_SNo (add_SNo x20 x20) x20) (add_SNo x20 x20)) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x9 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ x11 = 1 ⟶ x12 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x13 (x10 x20) x11 x12) ⟶ (∀ x20 . x20 ∈ int ⟶ x16 x20 = x15 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 x7 (x16 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x5 x20 = x19 x20
Conjecture 34fc2..^A13710 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ x0 x20 = add_SNo (mul_SNo 2 (add_SNo x20 x20)) x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x1 x20 = add_SNo 1 (add_SNo x20 x20)) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x3 (x1 x20) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = x4 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = mul_SNo (add_SNo (mul_SNo 2 (add_SNo x20 x20)) x20) x20) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x9 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ x11 = 1 ⟶ x12 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x13 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x8 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x14 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x9 (x13 (add_SNo x20 (minus_SNo 1)) x21 x22) (x14 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x13 (x10 x20) x11 x12) ⟶ (∀ x20 . x20 ∈ int ⟶ x16 x20 = x15 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x6 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 x7 (x16 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x5 x20 = x19 x20
Conjecture 75e18..^A13709 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ (∀ x17 . x17 ∈ int ⟶ x0 x17 = add_SNo x17 x17) ⟶ (∀ x17 . x17 ∈ int ⟶ x1 x17 = mul_SNo 2 (add_SNo x17 x17)) ⟶ x2 = 2 ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x4 x17 = x3 (x1 x17) x2) ⟶ (∀ x17 . x17 ∈ int ⟶ x5 x17 = mul_SNo 2 (x4 x17)) ⟶ (∀ x17 . x17 ∈ int ⟶ x6 x17 = mul_SNo x17 x17) ⟶ x7 = 2 ⟶ (∀ x17 . x17 ∈ int ⟶ x8 x17 = add_SNo x17 x17) ⟶ (∀ x17 . x17 ∈ int ⟶ x9 x17 = x17) ⟶ x10 = 1 ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x12 x17 = x11 (x9 x17) x10) ⟶ (∀ x17 . x17 ∈ int ⟶ x13 x17 = x12 x17) ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x15 x17 = x14 x7 (x13 x17)) ⟶ (∀ x17 . x17 ∈ int ⟶ x16 x17 = mul_SNo 2 (mul_SNo 2 (x15 x17))) ⟶ ∀ x17 . x17 ∈ int ⟶ SNoLe 0 x17 ⟶ x5 x17 = x16 x17
Conjecture d78e0..^A13708 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x12 x13 x14 x15 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ (∀ x15 . x15 ∈ int ⟶ x0 x15 = add_SNo (add_SNo x15 x15) x15) ⟶ (∀ x15 . x15 ∈ int ⟶ x1 x15 = add_SNo 1 (add_SNo x15 x15)) ⟶ x2 = 1 ⟶ (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x3 x15 x16 = If_i (SNoLe x15 0) x16 (x0 (x3 (add_SNo x15 (minus_SNo 1)) x16))) ⟶ (∀ x15 . x15 ∈ int ⟶ x4 x15 = x3 (x1 x15) x2) ⟶ (∀ x15 . x15 ∈ int ⟶ x5 x15 = x4 x15) ⟶ (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x6 x15 x16 = mul_SNo x15 x16) ⟶ (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x7 x15 x16 = x16) ⟶ (∀ x15 . x15 ∈ int ⟶ x8 x15 = x15) ⟶ x9 = add_SNo 1 2 ⟶ x10 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x11 x15 x16 x17 = If_i (SNoLe x15 0) x16 (x6 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17))) ⟶ (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x12 x15 x16 x17 = If_i (SNoLe x15 0) x17 (x7 (x11 (add_SNo x15 (minus_SNo 1)) x16 x17) (x12 (add_SNo x15 (minus_SNo 1)) x16 x17))) ⟶ (∀ x15 . x15 ∈ int ⟶ x13 x15 = x11 (x8 x15) x9 x10) ⟶ (∀ x15 . x15 ∈ int ⟶ x14 x15 = x13 x15) ⟶ ∀ x15 . x15 ∈ int ⟶ SNoLe 0 x15 ⟶ x5 x15 = x14 x15
Conjecture cda85..^A1367 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 . x3 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x5 x6 x7 x8 ∈ int) ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x6 x7 x8 x9 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x15 x16 x17 x18 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 : ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x20 x21 x22 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x0 x23 x24 = mul_SNo (add_SNo x23 x24) x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x1 x23 x24 = mul_SNo x24 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = x23) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x5 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 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x6 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 . x23 ∈ int ⟶ x7 x23 = x5 (x2 x23) x3 x4) ⟶ (∀ x23 . x23 ∈ int ⟶ x8 x23 = x7 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x9 x23 x24 = mul_SNo (mul_SNo x23 x24) x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x10 x23 x24 = add_SNo x24 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x11 x23 = add_SNo x23 (minus_SNo 1)) ⟶ x12 = 1 ⟶ x13 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x14 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 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x15 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 . x23 ∈ int ⟶ x16 x23 = x14 (x11 x23) x12 x13) ⟶ (∀ x23 . x23 ∈ int ⟶ x17 x23 = add_SNo x23 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x18 x23 = x23) ⟶ x19 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x20 x23 x24 = If_i (SNoLe x23 0) x24 (x17 (x20 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x20 (x18 x23) x19) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = mul_SNo (x16 x23) (mul_SNo (add_SNo 1 (add_SNo x23 x23)) (x21 x23))) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x8 x23 = x22 x23
Conjecture 574e4..^A136516 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x10 x11 x12 x13 ∈ int) ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x24 x25 x26 x27 ∈ int) ⟶ ∀ x25 : ι → ι → ι → ι . (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x25 x26 x27 x28 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 : ι → ι . (∀ x28 . x28 ∈ int ⟶ x27 x28 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 : ι → ι → ι . (∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x30 x31 x32 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 : ι → ι . (∀ x33 . x33 ∈ int ⟶ x32 x33 ∈ int) ⟶ (∀ x33 . x33 ∈ int ⟶ x0 x33 = add_SNo x33 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x1 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x2 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x4 x33 x34 = x3 (x1 x33 x34) (x2 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x5 x33 x34 = add_SNo (x4 x33 x34) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x6 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x7 x33 = x33) ⟶ x8 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ x9 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x10 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x5 (x10 (add_SNo x33 (minus_SNo 1)) x34 x35) (x11 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x11 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x6 (x10 (add_SNo x33 (minus_SNo 1)) x34 x35) (x11 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x12 x33 = x10 (x7 x33) x8 (x9 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x13 x33 = x12 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x14 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x15 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x16 x33 = add_SNo x33 (minus_SNo 1)) ⟶ x17 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = add_SNo x33 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x19 x33 = add_SNo x33 (minus_SNo 1)) ⟶ x20 = 2 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x21 x33 x34 = If_i (SNoLe x33 0) x34 (x18 (x21 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x22 x33 = x21 (x19 x33) x20) ⟶ (∀ x33 . x33 ∈ int ⟶ x23 x33 = add_SNo 1 (x22 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x14 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x15 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x26 x33 = x24 (x16 x33) x17 (x23 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x27 x33 = add_SNo x33 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x28 x33 = add_SNo x33 (minus_SNo 1)) ⟶ x29 = 2 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x30 x33 x34 = If_i (SNoLe x33 0) x34 (x27 (x30 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x31 x33 = x30 (x28 x33) x29) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = mul_SNo (x26 x33) (If_i (SNoLe x33 0) 1 (add_SNo 1 (x31 x33)))) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x13 x33 = x32 x33
Conjecture 25da8..^A136376 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ∈ int ⟶ x3 x4 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x5 x6 x7 x8 ∈ int) ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x6 x7 x8 x9 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x15 x16 x17 x18 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x0 x18 x19 = add_SNo x18 x19) ⟶ (∀ x18 . x18 ∈ int ⟶ x1 x18 = x18) ⟶ (∀ x18 . x18 ∈ int ⟶ x2 x18 = add_SNo 1 x18) ⟶ (∀ x18 . x18 ∈ int ⟶ x3 x18 = x18) ⟶ x4 = 1 ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x5 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 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x6 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x1 (x5 (add_SNo x18 (minus_SNo 1)) x19 x20))) ⟶ (∀ x18 . x18 ∈ int ⟶ x7 x18 = x5 (x2 x18) (x3 x18) x4) ⟶ (∀ x18 . x18 ∈ int ⟶ x8 x18 = x7 x18) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x9 x18 x19 = add_SNo x18 x19) ⟶ (∀ x18 . x18 ∈ int ⟶ x10 x18 = x18) ⟶ (∀ x18 . x18 ∈ int ⟶ x11 x18 = x18) ⟶ (∀ x18 . x18 ∈ int ⟶ x12 x18 = add_SNo 1 x18) ⟶ (∀ x18 . x18 ∈ int ⟶ x13 x18 = x18) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x14 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 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x15 x18 x19 x20 = If_i (SNoLe x18 0) x20 (x10 (x14 (add_SNo x18 (minus_SNo 1)) x19 x20))) ⟶ (∀ x18 . x18 ∈ int ⟶ x16 x18 = x14 (x11 x18) (x12 x18) (x13 x18)) ⟶ (∀ x18 . x18 ∈ int ⟶ x17 x18 = x16 x18) ⟶ ∀ x18 . x18 ∈ int ⟶ SNoLe 0 x18 ⟶ x8 x18 = x17 x18
Conjecture 49a1a..^A134494 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 . x3 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x5 x6 x7 x8 ∈ int) ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x6 x7 x8 x9 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x15 x16 x17 x18 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x23 x24 x25 x26 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x0 x26 x27 = add_SNo (mul_SNo 2 (add_SNo x26 x26)) x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x1 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x2 x26 = add_SNo x26 x26) ⟶ x3 = 1 ⟶ x4 = 1 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x5 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x0 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x6 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x1 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x7 x26 = x5 (x2 x26) x3 x4) ⟶ (∀ x26 . x26 ∈ int ⟶ x8 x26 = x7 x26) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x9 x26 x27 = add_SNo (mul_SNo 2 (add_SNo x26 x26)) x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x10 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x11 x26 = add_SNo x26 (minus_SNo 1)) ⟶ (∀ x26 . x26 ∈ int ⟶ x12 x26 = add_SNo (If_i (SNoLe x26 0) 0 2) 1) ⟶ x13 = 1 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x14 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x9 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x15 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x10 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x16 x26 = x14 (x11 x26) (x12 x26) x13) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x17 x26 x27 = add_SNo x26 x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x18 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x19 x26 = add_SNo (add_SNo x26 x26) x26) ⟶ x20 = 1 ⟶ x21 = 2 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x22 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x17 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x23 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x18 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x24 x26 = x22 (x19 x26) x20 x21) ⟶ (∀ x26 . x26 ∈ int ⟶ x25 x26 = mul_SNo (x16 x26) (x24 x26)) ⟶ ∀ x26 . x26 ∈ int ⟶ SNoLe 0 x26 ⟶ x8 x26 = x25 x26
Conjecture e3def..^A134492 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 . x3 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x5 x6 x7 x8 ∈ int) ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x6 x7 x8 x9 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x15 x16 x17 x18 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x23 x24 x25 x26 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x0 x26 x27 = add_SNo (mul_SNo 2 (add_SNo x26 x26)) x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x1 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x2 x26 = add_SNo x26 x26) ⟶ x3 = 0 ⟶ x4 = 2 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x5 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x0 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28) (x6 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x6 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x1 (x5 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x7 x26 = x5 (x2 x26) x3 x4) ⟶ (∀ x26 . x26 ∈ int ⟶ x8 x26 = x7 x26) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x9 x26 x27 = add_SNo (mul_SNo 2 (add_SNo x26 x26)) x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x10 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x11 x26 = add_SNo x26 (minus_SNo 1)) ⟶ (∀ x26 . x26 ∈ int ⟶ x12 x26 = If_i (SNoLe x26 0) 1 2) ⟶ x13 = 1 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x14 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x9 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28) (x15 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x15 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x10 (x14 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x16 x26 = x14 (x11 x26) (x12 x26) x13) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x17 x26 x27 = add_SNo (mul_SNo 2 (add_SNo x26 x26)) x27) ⟶ (∀ x26 . x26 ∈ int ⟶ x18 x26 = x26) ⟶ (∀ x26 . x26 ∈ int ⟶ x19 x26 = x26) ⟶ x20 = 0 ⟶ x21 = 2 ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x22 x26 x27 x28 = If_i (SNoLe x26 0) x27 (x17 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28) (x23 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x23 x26 x27 x28 = If_i (SNoLe x26 0) x28 (x18 (x22 (add_SNo x26 (minus_SNo 1)) x27 x28))) ⟶ (∀ x26 . x26 ∈ int ⟶ x24 x26 = x22 (x19 x26) x20 x21) ⟶ (∀ x26 . x26 ∈ int ⟶ x25 x26 = mul_SNo (mul_SNo (x16 x26) (x24 x26)) 2) ⟶ ∀ x26 . x26 ∈ int ⟶ SNoLe 0 x26 ⟶ x8 x26 = x25 x26
Conjecture f7f06..^A134169 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ∈ int ⟶ x3 x4 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ (∀ x22 . x22 ∈ int ⟶ x0 x22 = add_SNo (add_SNo x22 (minus_SNo 1)) x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x1 x22 = add_SNo x22 (minus_SNo 1)) ⟶ (∀ x22 . x22 ∈ int ⟶ x2 x22 = add_SNo x22 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x3 x22 = x22) ⟶ x4 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x5 x22 x23 = If_i (SNoLe x22 0) x23 (x2 (x5 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x6 x22 = x5 (x3 x22) x4) ⟶ (∀ x22 . x22 ∈ int ⟶ x7 x22 = x6 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x8 x22 x23 = If_i (SNoLe x22 0) x23 (x0 (x8 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x9 x22 = x8 (x1 x22) (x7 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ x10 x22 = x9 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x11 x22 = add_SNo (mul_SNo 2 (mul_SNo x22 x22)) (minus_SNo x22)) ⟶ x12 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ x13 x22 = add_SNo x22 x22) ⟶ (∀ x22 . x22 ∈ int ⟶ x14 x22 = add_SNo x22 (minus_SNo 1)) ⟶ x15 = 1 ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x16 x22 x23 = If_i (SNoLe x22 0) x23 (x13 (x16 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x17 x22 = x16 (x14 x22) x15) ⟶ (∀ x22 . x22 ∈ int ⟶ x18 x22 = If_i (SNoLe x22 0) 0 (x17 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x19 x22 x23 = If_i (SNoLe x22 0) x23 (x11 (x19 (add_SNo x22 (minus_SNo 1)) x23))) ⟶ (∀ x22 . x22 ∈ int ⟶ x20 x22 = x19 x12 (x18 x22)) ⟶ (∀ x22 . x22 ∈ int ⟶ x21 x22 = add_SNo 1 (x20 x22)) ⟶ ∀ x22 . x22 ∈ int ⟶ SNoLe 0 x22 ⟶ x10 x22 = x21 x22
Conjecture dc551..^A1338 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x20 x21 x22 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x24 x25 x26 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x0 x27 x28 = add_SNo 1 (mul_SNo x27 x28)) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x1 x27 x28 = x28) ⟶ x2 = 1 ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x3 x27 x28 = If_i (SNoLe x27 0) x28 (x0 (x3 (add_SNo x27 (minus_SNo 1)) x28) x27)) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x4 x27 x28 = x3 (x1 x27 x28) x2) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x5 x27 x28 = add_SNo (x4 x27 x28) x27) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x6 x27 x28 = add_SNo x28 (minus_SNo 1)) ⟶ x7 = 0 ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x8 x27 x28 = If_i (SNoLe x27 0) x28 (x5 (x8 (add_SNo x27 (minus_SNo 1)) x28) x27)) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x9 x27 x28 = x8 (x6 x27 x28) x7) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x10 x27 x28 = x9 x27 x28) ⟶ (∀ x27 . x27 ∈ int ⟶ x11 x27 = x27) ⟶ x12 = 1 ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x13 x27 x28 = If_i (SNoLe x27 0) x28 (x10 (x13 (add_SNo x27 (minus_SNo 1)) x28) x27)) ⟶ (∀ x27 . x27 ∈ int ⟶ x14 x27 = x13 (x11 x27) x12) ⟶ (∀ x27 . x27 ∈ int ⟶ x15 x27 = x14 x27) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x16 x27 x28 = add_SNo 1 (mul_SNo x27 x28)) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x17 x27 x28 = add_SNo x28 (minus_SNo 1)) ⟶ x18 = 1 ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x19 x27 x28 = If_i (SNoLe x27 0) x28 (x16 (x19 (add_SNo x27 (minus_SNo 1)) x28) x27)) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x20 x27 x28 = x19 (x17 x27 x28) x18) ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x21 x27 x28 = add_SNo (mul_SNo (x20 x27 x28) x28) x27) ⟶ (∀ x27 . x27 ∈ int ⟶ x22 x27 = add_SNo x27 (minus_SNo 1)) ⟶ x23 = 1 ⟶ (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x24 x27 x28 = If_i (SNoLe x27 0) x28 (x21 (x24 (add_SNo x27 (minus_SNo 1)) x28) x27)) ⟶ (∀ x27 . x27 ∈ int ⟶ x25 x27 = x24 (x22 x27) x23) ⟶ (∀ x27 . x27 ∈ int ⟶ x26 x27 = add_SNo (add_SNo (x25 x27) x27) (minus_SNo (If_i (SNoLe x27 0) 0 2))) ⟶ ∀ x27 . x27 ∈ int ⟶ SNoLe 0 x27 ⟶ x15 x27 = x26 x27
Conjecture fcb50..^A133384 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x12 x13 x14 x15 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x20 x21 x22 x23 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ (∀ x23 . x23 ∈ int ⟶ x0 x23 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x23 x23)) x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x1 x23 = add_SNo 1 x23) ⟶ x2 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ (∀ x23 . x23 ∈ int ⟶ x4 x23 = x3 (x1 x23) x2) ⟶ (∀ x23 . x23 ∈ int ⟶ x5 x23 = add_SNo 2 (x4 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x6 x23 x24 = mul_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x7 x23 x24 = x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x8 x23 x24 = x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x9 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x10 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x6 (x11 (add_SNo x23 (minus_SNo 1)) x24 x25) (x12 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x12 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x7 (x11 (add_SNo x23 (minus_SNo 1)) x24 x25) (x12 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x13 x23 x24 = x11 (x8 x23 x24) (x9 x23) (x10 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = x13 x23 x24) ⟶ x15 = 2 ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (mul_SNo (mul_SNo 2 2) 2) ⟶ (∀ x23 . x23 ∈ int ⟶ x18 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x20 x23 x24 x25 = If_i (SNoLe x23 0) x25 x15) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 x16 x17 (x18 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = add_SNo (x21 x23) 2) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x5 x23 = x22 x23