Proofgold Asset

Param int^int : ι
Param add_SNo^add_SNo : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Param minus_SNo^minus_SNo : ι → ι
Conjecture d59bf..^A22126 : ∀ 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 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ 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 . x18 ∈ 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 ⟶ ∀ x24 . x24 ∈ int ⟶ x0 x23 x24 = x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x1 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = x23) ⟶ x3 = add_SNo 1 2 ⟶ (∀ x23 . x23 ∈ int ⟶ x4 x23 = mul_SNo x23 x23) ⟶ x5 = 2 ⟶ x6 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x7 x23 x24 = If_i (SNoLe x23 0) x24 (x4 (x7 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ x8 = x7 x5 x6 ⟶ x9 = x8 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x2 x23) x3 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x15 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = x23) ⟶ x17 = add_SNo 1 2 ⟶ x18 = mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ 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 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 (x16 x23) x17 x18) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x13 x23 = x22 x23
Conjecture 0b316..^A22117 : ∀ 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 ⟶ ∀ 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 . x9 ∈ 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 ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ 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 x23 x23) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x5 x23 x24 = add_SNo x4 (minus_SNo x24)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x6 x23 x24 = add_SNo x24 (minus_SNo x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x7 x23 = x23) ⟶ x8 = 2 ⟶ x9 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x5 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x6 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x7 x23) x8 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x15 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = x23) ⟶ x17 = 2 ⟶ x18 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ 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 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 (x16 x23) x17 x18) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x13 x23 = x22 x23
Conjecture 4cd90..^A22107 : ∀ 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 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ 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 ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ 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 ⟶ ∀ x24 . x24 ∈ int ⟶ x0 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x1 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = x23) ⟶ x3 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ x4 x23 = mul_SNo x23 x23) ⟶ x5 = 2 ⟶ x6 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x7 x23 x24 = If_i (SNoLe x23 0) x24 (x4 (x7 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ x8 = x7 x5 x6 ⟶ x9 = x8 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x2 x23) x3 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x15 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = x23) ⟶ x17 = 1 ⟶ x18 = mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ 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 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 (x16 x23) x17 x18) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x13 x23 = x22 x23
Conjecture 7f030..^A22104 : ∀ 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 ⟶ ∀ 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 . x9 ∈ 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 ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ 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 x23 x23) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x5 x23 x24 = add_SNo x4 (minus_SNo x24)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x6 x23 x24 = add_SNo x24 (minus_SNo x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x7 x23 = x23) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x5 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x6 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x7 x23) x8 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x15 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = x23) ⟶ x17 = 1 ⟶ x18 = add_SNo 1 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ 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 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 (x16 x23) x17 x18) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x13 x23 = x22 x23
Conjecture 05710..^A220528 : ∀ 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 ⟶ x3 x4 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ 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 ⟶ 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 ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ 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 ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x20 x21 x22 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ 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 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x0 x28 x29 = mul_SNo (mul_SNo x28 x28) x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x1 x28 x29 = x29) ⟶ x2 = 2 ⟶ (∀ x28 . x28 ∈ int ⟶ x3 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x4 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x5 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 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x6 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 . x28 ∈ int ⟶ x7 x28 = x5 x2 (x3 x28) (x4 x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x8 x28 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x28 x28) x28)) x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x9 x28 = x28) ⟶ x10 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x11 x28 x29 = If_i (SNoLe x28 0) x29 (x8 (x11 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ (∀ x28 . x28 ∈ int ⟶ x12 x28 = x11 (x9 x28) x10) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = add_SNo (add_SNo (x7 x28) (x12 x28)) (add_SNo (mul_SNo 2 (add_SNo (add_SNo x28 x28) x28)) x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x14 x28 = mul_SNo (mul_SNo x28 x28) x28) ⟶ x15 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ x16 x28 = mul_SNo x28 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x17 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x17 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ (∀ x28 . x28 ∈ int ⟶ x18 x28 = x17 x15 (x16 x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x19 x28 x29 = mul_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x20 x28 x29 = x29) ⟶ (∀ x28 . x28 ∈ int ⟶ x21 x28 = x28) ⟶ x22 = 1 ⟶ x23 = add_SNo 1 (add_SNo 2 (add_SNo 2 2)) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x24 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x19 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x25 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x20 (x24 (add_SNo x28 (minus_SNo 1)) x29 x30) (x25 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ x26 x28 = x24 (x21 x28) x22 x23) ⟶ (∀ x28 . x28 ∈ int ⟶ x27 x28 = add_SNo (add_SNo (mul_SNo (x18 x28) x28) (x26 x28)) (add_SNo (mul_SNo (mul_SNo 2 x28) (add_SNo 1 2)) x28)) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x13 x28 = x27 x28
Conjecture 0fdb7..^A220186 : ∀ 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 ⟶ 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 ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 : ι → ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ 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 = add_SNo (mul_SNo (add_SNo 2 (minus_SNo (add_SNo x23 x23))) (add_SNo 1 (add_SNo 2 2))) (minus_SNo x24)) ⟶ (∀ x23 . x23 ∈ int ⟶ x1 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = add_SNo x23 x23) ⟶ x3 = 1 ⟶ x4 = 0 ⟶ (∀ 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))) ⟶ (∀ x23 . x23 ∈ int ⟶ x7 x23 = x5 (x2 x23) x3 x4) ⟶ (∀ x23 . x23 ∈ int ⟶ x8 x23 = add_SNo (x7 x23) (minus_SNo 1)) ⟶ (∀ x23 . x23 ∈ int ⟶ x9 x23 = mul_SNo (add_SNo x23 x23) x23) ⟶ x10 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x11 x23 x24 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x23 x23)) x23)) (minus_SNo x24)) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = add_SNo x23 (minus_SNo 1)) ⟶ (∀ x23 . x23 ∈ int ⟶ x14 x23 = If_i (SNoLe x23 0) 0 2) ⟶ x15 = 0 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x16 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 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x17 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x12 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x18 x23 = x16 (x13 x23) (x14 x23) x15) ⟶ (∀ x23 . x23 ∈ int ⟶ x19 x23 = x18 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x20 x23 x24 = If_i (SNoLe x23 0) x24 (x9 (x20 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x20 x10 (x19 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x8 x23 = x22 x23
Conjecture b56a7..^A22000 : ∀ 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 ⟶ ∀ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x20 x21 x22 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 : ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x26 x27 x28 ∈ int) ⟶ ∀ x27 : ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x31 x32 x33 x34 ∈ int) ⟶ ∀ x32 : ι → ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x32 x33 x34 x35 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 : ι → ι . (∀ x35 . x35 ∈ int ⟶ x34 x35 ∈ int) ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 : ι → ι → ι . (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x36 x37 x38 ∈ int) ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι → ι . (∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x38 x39 x40 ∈ int) ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι . (∀ x41 . x41 ∈ int ⟶ x40 x41 ∈ int) ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x0 x45 x46 = mul_SNo (add_SNo 2 x46) x45) ⟶ x1 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x2 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x4 x45 = x3 x1 (x2 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x5 x45 = add_SNo 1 (add_SNo (x4 x45) (minus_SNo x45))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x6 x45 x46 = x46) ⟶ x7 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x9 x45 x46 = x8 (x6 x45 x46) x7) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x10 x45 x46 = add_SNo (x9 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x11 x45 x46 = x46) ⟶ x12 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x14 x45 x46 = x13 (x11 x45 x46) x12) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x15 x45 x46 = mul_SNo (add_SNo 2 x46) x45) ⟶ x16 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x17 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x19 x45 = x18 x16 (x17 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x20 x45 x46 = add_SNo (x14 x45 x46) (x19 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x21 x45 = x45) ⟶ x22 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x23 x45 x46 = If_i (SNoLe x45 0) x46 (x20 (x23 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x24 x45 = x23 (x21 x45) x22) ⟶ (∀ x45 . x45 ∈ int ⟶ x25 x45 = x24 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x26 x45 x46 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x27 x45 x46 = add_SNo 1 (mul_SNo 2 (add_SNo x46 x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x45) ⟶ x29 = 1 ⟶ x30 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x33 x45 = x31 (x28 x45) x29 x30) ⟶ (∀ x45 . x45 ∈ int ⟶ x34 x45 = x33 x45) ⟶ x35 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x36 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x38 x45 x46 = x37 x35 (x36 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x40 x45 = x45) ⟶ x41 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x43 x45 = x42 (x40 x45) x41) ⟶ (∀ x45 . x45 ∈ int ⟶ x44 x45 = x43 x45) ⟶ ∀ x45 . x45 ∈ int ⟶ SNoLe 0 x45 ⟶ x25 x45 = x44 x45
Conjecture 1dffe..^A21964 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 ⟶ x5 x6 ∈ int) ⟶ ∀ x6 . x6 ∈ 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 ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x20 x21 x22 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 : ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x26 x27 x28 ∈ int) ⟶ ∀ x27 : ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x31 x32 x33 x34 ∈ int) ⟶ ∀ x32 : ι → ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x32 x33 x34 x35 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 : ι → ι . (∀ x35 . x35 ∈ int ⟶ x34 x35 ∈ int) ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 : ι → ι → ι . (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x36 x37 x38 ∈ int) ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι → ι . (∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x38 x39 x40 ∈ int) ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι . (∀ x41 . x41 ∈ int ⟶ x40 x41 ∈ int) ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ (∀ x45 . x45 ∈ int ⟶ x0 x45 = add_SNo 1 (mul_SNo 2 (add_SNo x45 x45))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x1 x45 x46 = x46) ⟶ x2 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x4 x45 x46 = x3 (x1 x45 x46) x2) ⟶ (∀ x45 . x45 ∈ int ⟶ x5 x45 = add_SNo (add_SNo x45 x45) x45) ⟶ x6 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x7 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x9 x45 = x8 x6 (x7 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x10 x45 x46 = add_SNo (x4 x45 x46) (x9 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x11 x45 x46 = x46) ⟶ x12 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x14 x45 x46 = x13 (x11 x45 x46) x12) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x15 x45 x46 = mul_SNo (add_SNo 2 x46) x45) ⟶ x16 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x17 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x19 x45 = x18 x16 (x17 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x20 x45 x46 = add_SNo (add_SNo (x14 x45 x46) (minus_SNo x45)) (x19 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x21 x45 = x45) ⟶ x22 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x23 x45 x46 = If_i (SNoLe x45 0) x46 (x20 (x23 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x24 x45 = x23 (x21 x45) x22) ⟶ (∀ x45 . x45 ∈ int ⟶ x25 x45 = x24 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x26 x45 x46 = add_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo x45 x45))) x45) x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x27 x45 x46 = add_SNo 1 (mul_SNo 2 (add_SNo x46 x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x45) ⟶ x29 = 1 ⟶ x30 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x33 x45 = x31 (x28 x45) x29 x30) ⟶ (∀ x45 . x45 ∈ int ⟶ x34 x45 = x33 x45) ⟶ x35 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x36 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x38 x45 x46 = x37 x35 (x36 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x40 x45 = x45) ⟶ x41 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x43 x45 = x42 (x40 x45) x41) ⟶ (∀ x45 . x45 ∈ int ⟶ x44 x45 = x43 x45) ⟶ ∀ x45 . x45 ∈ int ⟶ SNoLe 0 x45 ⟶ x25 x45 = x44 x45
Conjecture 8cd3f..^A219205 : ∀ 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 ⟶ x9 x10 ∈ int) ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 : ι → ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ 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 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo x24 x24) x23)) x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x1 x23 x24 = add_SNo (add_SNo x24 x24) x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = x23) ⟶ x3 = 0 ⟶ x4 = 1 ⟶ (∀ 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 ⟶ x9 x23 = add_SNo (mul_SNo (add_SNo 1 2) (mul_SNo x23 x23)) (minus_SNo x23)) ⟶ x10 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x11 x23 x24 = mul_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x12 x23 x24 = x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = add_SNo x23 (minus_SNo 1)) ⟶ x14 = 1 ⟶ x15 = add_SNo 1 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x16 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 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x17 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x12 (x16 (add_SNo x23 (minus_SNo 1)) x24 x25) (x17 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x18 x23 = x16 (x13 x23) x14 x15) ⟶ (∀ x23 . x23 ∈ int ⟶ x19 x23 = If_i (SNoLe x23 0) 0 (x18 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x20 x23 x24 = If_i (SNoLe x23 0) x24 (x9 (x20 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x20 x10 (x19 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x8 x23 = x22 x23
Conjecture c0c10..^A218738 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = mul_SNo 2 (add_SNo (add_SNo x25 x25) 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 ∈ int ⟶ x4 x25 = x3 x1 (x2 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x5 x25 = add_SNo 1 (add_SNo (x4 x25) (minus_SNo x25))) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 x25 = x25) ⟶ x7 = 0 ⟶ (∀ 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 ⟶ ∀ x26 . x26 ∈ int ⟶ x11 x25 x26 = add_SNo 1 (mul_SNo x25 x26)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x12 x25 x26 = x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x13 x25 = add_SNo x25 (minus_SNo 1)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = If_i (SNoLe x25 0) 0 1) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = mul_SNo x25 x25) ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x18 x25 x26 = If_i (SNoLe x25 0) x26 (x15 (x18 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ x19 = x18 x16 x17 ⟶ x20 = add_SNo x19 (minus_SNo 1) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x21 (x13 x25) (x14 x25) x20) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture 09e91..^A218734 : ∀ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ 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 ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x0 x20 x21 = mul_SNo (add_SNo 2 (add_SNo 2 x21)) x20) ⟶ x1 = 2 ⟶ (∀ x20 . x20 ∈ int ⟶ x2 x20 = x20) ⟶ (∀ 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 . x20 ∈ int ⟶ x4 x20 = x3 x1 (x2 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = add_SNo 1 (add_SNo (x4 x20) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = x20) ⟶ x7 = 0 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x9 x20 = x8 (x6 x20) x7) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x9 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x11 x20 x21 = add_SNo 1 (mul_SNo x20 x21)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x12 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x13 x20 = add_SNo x20 (minus_SNo 1)) ⟶ (∀ x20 . x20 ∈ int ⟶ x14 x20 = If_i (SNoLe x20 0) 0 1) ⟶ x15 = add_SNo (mul_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) (minus_SNo 1) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x16 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 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x17 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 . x20 ∈ int ⟶ x18 x20 = x16 (x13 x20) (x14 x20) x15) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x10 x20 = x19 x20
Conjecture 57c10..^A218726 : ∀ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ 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 ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x0 x20 x21 = mul_SNo x20 x21) ⟶ x1 = add_SNo 2 2 ⟶ (∀ x20 . x20 ∈ int ⟶ x2 x20 = x20) ⟶ (∀ 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 . x20 ∈ int ⟶ x4 x20 = x3 x1 (x2 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = add_SNo 1 (add_SNo (x4 x20) (minus_SNo x20))) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = x20) ⟶ x7 = 0 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x9 x20 = x8 (x6 x20) x7) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x9 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x11 x20 x21 = add_SNo 1 (mul_SNo x20 x21)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x12 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x13 x20 = add_SNo x20 (minus_SNo 1)) ⟶ (∀ x20 . x20 ∈ int ⟶ x14 x20 = If_i (SNoLe x20 0) 0 1) ⟶ x15 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2)))) (minus_SNo 1) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x16 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 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x17 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 . x20 ∈ int ⟶ x18 x20 = x16 (x13 x20) (x14 x20) x15) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x10 x20 = x19 x20
Conjecture 31d36..^A218722 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ 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 ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ 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) ⟶ x1 = 2 ⟶ (∀ x20 . x20 ∈ int ⟶ x2 x20 = x20) ⟶ (∀ 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 (x2 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x5 x20 = add_SNo 1 (add_SNo (mul_SNo 2 (x4 x20)) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = x20) ⟶ x7 = 0 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x9 x20 = x8 (x6 x20) x7) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x9 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x11 x20 x21 = add_SNo 1 (mul_SNo x20 x21)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x12 x20 x21 = x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x13 x20 = add_SNo x20 (minus_SNo 1)) ⟶ (∀ x20 . x20 ∈ int ⟶ x14 x20 = If_i (SNoLe x20 0) 0 1) ⟶ x15 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2)))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x16 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 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x17 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 . x20 ∈ int ⟶ x18 x20 = x16 (x13 x20) (x14 x20) x15) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = x18 x20) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x10 x20 = x19 x20
Conjecture a3021..^A21844 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 . x11 ∈ int ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ 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 ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ int) ⟶ ∀ x33 : ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x33 x34 x35 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ (∀ x40 . x40 ∈ int ⟶ x0 x40 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x1 x40 x41 = x41) ⟶ x2 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x4 x40 x41 = x3 (x1 x40 x41) x2) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x5 x40 x41 = add_SNo (x4 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x6 x40 x41 = x41) ⟶ x7 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x9 x40 x41 = x8 (x6 x40 x41) x7) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x10 x40 x41 = mul_SNo (add_SNo 2 x41) x40) ⟶ x11 = 2 ⟶ (∀ x40 . x40 ∈ int ⟶ x12 x40 = x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x14 x40 = x13 x11 (x12 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x15 x40 x41 = add_SNo (x9 x40 x41) (x14 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x16 x40 = x40) ⟶ x17 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x19 x40 = x18 (x16 x40) x17) ⟶ (∀ x40 . x40 ∈ int ⟶ x20 x40 = x19 x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x21 x40 x41 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)) x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x22 x40 x41 = add_SNo 1 (mul_SNo 2 (add_SNo x41 x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ x23 x40 = x40) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ x28 x40 = x26 (x23 x40) x24 x25) ⟶ (∀ x40 . x40 ∈ int ⟶ x29 x40 = x28 x40) ⟶ x30 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x31 x40 x41 = x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x33 x40 x41 = x32 x30 (x31 x40 x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x34 x40 x41 = add_SNo (x33 x40 x41) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40)))) ⟶ (∀ x40 . x40 ∈ int ⟶ x35 x40 = x40) ⟶ x36 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x38 x40 = x37 (x35 x40) x36) ⟶ (∀ x40 . x40 ∈ int ⟶ x39 x40 = x38 x40) ⟶ ∀ x40 . x40 ∈ int ⟶ SNoLe 0 x40 ⟶ x20 x40 = x39 x40
Conjecture 959b8..^A21784 : ∀ 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 ⟶ ∀ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ int) ⟶ ∀ x33 : ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x33 x34 x35 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x0 x40 x41 = mul_SNo (add_SNo 2 x41) x40) ⟶ x1 = 2 ⟶ (∀ x40 . x40 ∈ int ⟶ x2 x40 = x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x4 x40 = x3 x1 (x2 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x5 x40 = add_SNo 1 (add_SNo (x4 x40) (minus_SNo x40))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x6 x40 x41 = x41) ⟶ x7 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x9 x40 x41 = x8 (x6 x40 x41) x7) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x10 x40 x41 = add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x11 x40 x41 = x41) ⟶ x12 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x14 x40 x41 = x13 (x11 x40 x41) x12) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x15 x40 x41 = add_SNo (add_SNo (x14 x40 x41) (mul_SNo 2 (add_SNo x40 x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x16 x40 = x40) ⟶ x17 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x19 x40 = x18 (x16 x40) x17) ⟶ (∀ x40 . x40 ∈ int ⟶ x20 x40 = x19 x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x21 x40 x41 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40) x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x22 x40 x41 = add_SNo 1 (mul_SNo 2 (add_SNo x41 x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ x23 x40 = x40) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ x28 x40 = x26 (x23 x40) x24 x25) ⟶ (∀ x40 . x40 ∈ int ⟶ x29 x40 = x28 x40) ⟶ x30 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x31 x40 x41 = x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x33 x40 x41 = x32 x30 (x31 x40 x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x35 x40 = x40) ⟶ x36 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x38 x40 = x37 (x35 x40) x36) ⟶ (∀ x40 . x40 ∈ int ⟶ x39 x40 = x38 x40) ⟶ ∀ x40 . x40 ∈ int ⟶ SNoLe 0 x40 ⟶ x20 x40 = x39 x40
Conjecture 56f82..^A217471 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 . x6 ∈ int ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 : ι → ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x12 x13 x14 x15 ∈ int) ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ 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 . x19 ∈ 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 ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x26 x27 x28 ∈ int) ⟶ ∀ x27 : ι → ι . (∀ x28 . x28 ∈ int ⟶ x27 x28 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι . (∀ x33 . x33 ∈ int ⟶ x32 x33 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 : ι → ι → ι → ι . (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x36 x37 x38 x39 ∈ int) ⟶ ∀ x37 : ι → ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x37 x38 x39 x40 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ ∀ x40 : ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x40 x41 x42 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 . x43 ∈ int ⟶ ∀ x44 : ι → ι → ι . (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x44 x45 x46 ∈ int) ⟶ ∀ x45 : ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x45 x46 x47 ∈ int) ⟶ ∀ x46 : ι → ι → ι . (∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x46 x47 x48 ∈ int) ⟶ ∀ x47 : ι → ι → ι . (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x47 x48 x49 ∈ int) ⟶ ∀ x48 : ι → ι . (∀ x49 . x49 ∈ int ⟶ x48 x49 ∈ int) ⟶ ∀ x49 . x49 ∈ int ⟶ ∀ x50 : ι → ι → ι . (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x50 x51 x52 ∈ int) ⟶ ∀ x51 : ι → ι . (∀ x52 . x52 ∈ int ⟶ x51 x52 ∈ int) ⟶ ∀ x52 : ι → ι . (∀ x53 . x53 ∈ int ⟶ x52 x53 ∈ int) ⟶ (∀ x53 . x53 ∈ int ⟶ x0 x53 = mul_SNo x53 x53) ⟶ x1 = 2 ⟶ (∀ x53 . x53 ∈ int ⟶ x2 x53 = x53) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x3 x53 x54 = If_i (SNoLe x53 0) x54 (x0 (x3 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x4 x53 = x3 x1 (x2 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x5 x53 = mul_SNo (x4 x53) x53) ⟶ x6 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x7 x53 x54 = add_SNo x53 x54) ⟶ (∀ x53 . x53 ∈ int ⟶ x8 x53 = x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x9 x53 = add_SNo x53 x53) ⟶ x10 = 0 ⟶ x11 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x12 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x7 (x12 (add_SNo x53 (minus_SNo 1)) x54 x55) (x13 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x13 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x8 (x12 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ x14 x53 = x12 (x9 x53) x10 x11) ⟶ (∀ x53 . x53 ∈ int ⟶ x15 x53 = x14 x53) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x16 x53 x54 = If_i (SNoLe x53 0) x54 (x5 (x16 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x17 x53 = x16 x6 (x15 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x18 x53 = x17 x53) ⟶ x19 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x20 x53 x54 = x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x21 x53 x54 = If_i (SNoLe x53 0) x54 (x18 (x21 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x22 x53 x54 = x21 x19 (x20 x53 x54)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x23 x53 x54 = add_SNo (x22 x53 x54) x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x24 x53 = x53) ⟶ x25 = 0 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x26 x53 x54 = If_i (SNoLe x53 0) x54 (x23 (x26 (add_SNo x53 (minus_SNo 1)) x54) x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x27 x53 = x26 (x24 x53) x25) ⟶ (∀ x53 . x53 ∈ int ⟶ x28 x53 = x27 x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x29 x53 = mul_SNo (mul_SNo (mul_SNo (mul_SNo x53 x53) x53) x53) x53) ⟶ x30 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x31 x53 x54 = add_SNo x53 x54) ⟶ (∀ x53 . x53 ∈ int ⟶ x32 x53 = x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x33 x53 = add_SNo (add_SNo x53 (minus_SNo 2)) x53) ⟶ x34 = 1 ⟶ x35 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x36 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x31 (x36 (add_SNo x53 (minus_SNo 1)) x54 x55) (x37 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x37 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x32 (x36 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ x38 x53 = x36 (x33 x53) x34 x35) ⟶ (∀ x53 . x53 ∈ int ⟶ x39 x53 = x38 x53) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x40 x53 x54 = If_i (SNoLe x53 0) x54 (x29 (x40 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x41 x53 = x40 x30 (x39 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x42 x53 = x41 x53) ⟶ x43 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x44 x53 x54 = x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x45 x53 x54 = If_i (SNoLe x53 0) x54 (x42 (x45 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x46 x53 x54 = x45 x43 (x44 x53 x54)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x47 x53 x54 = add_SNo (x46 x53 x54) x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x48 x53 = x53) ⟶ x49 = 0 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x50 x53 x54 = If_i (SNoLe x53 0) x54 (x47 (x50 (add_SNo x53 (minus_SNo 1)) x54) x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x51 x53 = x50 (x48 x53) x49) ⟶ (∀ x53 . x53 ∈ int ⟶ x52 x53 = x51 x53) ⟶ ∀ x53 . x53 ∈ int ⟶ SNoLe 0 x53 ⟶ x28 x53 = x52 x53
Conjecture 47329..^A21734 : ∀ 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 ⟶ ∀ 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 . x11 ∈ int ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ 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 ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 : ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ x26 x27 x28 ∈ int) ⟶ ∀ x27 : ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x31 x32 x33 x34 ∈ int) ⟶ ∀ x32 : ι → ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x32 x33 x34 x35 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 : ι → ι . (∀ x35 . x35 ∈ int ⟶ x34 x35 ∈ int) ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 : ι → ι → ι . (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x36 x37 x38 ∈ int) ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι → ι . (∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x38 x39 x40 ∈ int) ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι . (∀ x41 . x41 ∈ int ⟶ x40 x41 ∈ int) ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x0 x45 x46 = mul_SNo (add_SNo 2 x46) x45) ⟶ x1 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x2 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x3 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x3 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x4 x45 = x3 x1 (x2 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x5 x45 = add_SNo 1 (add_SNo (x4 x45) (minus_SNo x45))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x6 x45 x46 = x46) ⟶ x7 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x8 x45 x46 = If_i (SNoLe x45 0) x46 (x5 (x8 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x9 x45 x46 = x8 (x6 x45 x46) x7) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x10 x45 x46 = mul_SNo (add_SNo 2 x46) x45) ⟶ x11 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ x12 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x13 x45 x46 = If_i (SNoLe x45 0) x46 (x10 (x13 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x14 x45 = x13 x11 (x12 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x15 x45 x46 = add_SNo (x9 x45 x46) (x14 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x16 x45 x46 = x46) ⟶ x17 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x18 x45 x46 = If_i (SNoLe x45 0) x46 (x15 (x18 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x19 x45 x46 = x18 (x16 x45 x46) x17) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x20 x45 x46 = add_SNo (add_SNo (add_SNo (x19 x45 x46) x45) x45) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x21 x45 = x45) ⟶ x22 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x23 x45 x46 = If_i (SNoLe x45 0) x46 (x20 (x23 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x24 x45 = x23 (x21 x45) x22) ⟶ (∀ x45 . x45 ∈ int ⟶ x25 x45 = x24 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x26 x45 x46 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45))) x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x27 x45 x46 = add_SNo 1 (add_SNo (add_SNo x46 x46) x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x45) ⟶ x29 = 1 ⟶ x30 = add_SNo 2 2 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x33 x45 = x31 (x28 x45) x29 x30) ⟶ (∀ x45 . x45 ∈ int ⟶ x34 x45 = x33 x45) ⟶ x35 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x36 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x38 x45 x46 = x37 x35 (x36 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x40 x45 = x45) ⟶ x41 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x42 x45 x46 = If_i (SNoLe x45 0) x46 (x39 (x42 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x43 x45 = x42 (x40 x45) x41) ⟶ (∀ x45 . x45 ∈ int ⟶ x44 x45 = x43 x45) ⟶ ∀ x45 . x45 ∈ int ⟶ SNoLe 0 x45 ⟶ x25 x45 = x44 x45
Conjecture 2030d..^A21714 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 . x6 ∈ 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 ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ int) ⟶ ∀ x33 : ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x33 x34 x35 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ (∀ x40 . x40 ∈ int ⟶ x0 x40 = add_SNo 1 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x1 x40 x41 = x41) ⟶ x2 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x4 x40 x41 = x3 (x1 x40 x41) x2) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x5 x40 x41 = mul_SNo (add_SNo 2 x41) x40) ⟶ x6 = 2 ⟶ (∀ x40 . x40 ∈ int ⟶ x7 x40 = x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x9 x40 = x8 x6 (x7 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x10 x40 x41 = add_SNo (add_SNo (x4 x40 x41) (minus_SNo x40)) (x9 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x11 x40 x41 = x41) ⟶ x12 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x14 x40 x41 = x13 (x11 x40 x41) x12) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x15 x40 x41 = add_SNo (add_SNo (add_SNo (x14 x40 x41) x40) x40) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x16 x40 = x40) ⟶ x17 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x19 x40 = x18 (x16 x40) x17) ⟶ (∀ x40 . x40 ∈ int ⟶ x20 x40 = x19 x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x21 x40 x41 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40)) x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x22 x40 x41 = add_SNo 1 (add_SNo (add_SNo x41 x41) x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ x23 x40 = x40) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 2 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ x28 x40 = x26 (x23 x40) x24 x25) ⟶ (∀ x40 . x40 ∈ int ⟶ x29 x40 = x28 x40) ⟶ x30 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x31 x40 x41 = x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x33 x40 x41 = x32 x30 (x31 x40 x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x35 x40 = x40) ⟶ x36 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x38 x40 = x37 (x35 x40) x36) ⟶ (∀ x40 . x40 ∈ int ⟶ x39 x40 = x38 x40) ⟶ ∀ x40 . x40 ∈ int ⟶ SNoLe 0 x40 ⟶ x20 x40 = x39 x40
Conjecture 9b0ce..^A21664 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ 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 . x6 ∈ 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 ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ int) ⟶ ∀ x33 : ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x33 x34 x35 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ (∀ x40 . x40 ∈ int ⟶ x0 x40 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x40 x40)))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x1 x40 x41 = x41) ⟶ x2 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x4 x40 x41 = x3 (x1 x40 x41) x2) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x5 x40 x41 = mul_SNo (add_SNo 2 x41) x40) ⟶ x6 = 2 ⟶ (∀ x40 . x40 ∈ int ⟶ x7 x40 = x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x9 x40 = x8 x6 (x7 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x10 x40 x41 = add_SNo (add_SNo (x4 x40 x41) (minus_SNo x40)) (x9 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x11 x40 x41 = x41) ⟶ x12 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x14 x40 x41 = x13 (x11 x40 x41) x12) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x15 x40 x41 = add_SNo (add_SNo (add_SNo (x14 x40 x41) x40) x40) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x16 x40 = x40) ⟶ x17 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x19 x40 = x18 (x16 x40) x17) ⟶ (∀ x40 . x40 ∈ int ⟶ x20 x40 = x19 x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x21 x40 x41 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo x40 x40))) x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x22 x40 x41 = add_SNo 1 (add_SNo (add_SNo x41 x41) x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ x23 x40 = x40) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 2 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ x28 x40 = x26 (x23 x40) x24 x25) ⟶ (∀ x40 . x40 ∈ int ⟶ x29 x40 = x28 x40) ⟶ x30 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x31 x40 x41 = x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x33 x40 x41 = x32 x30 (x31 x40 x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x40 x40)) x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x35 x40 = x40) ⟶ x36 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x38 x40 = x37 (x35 x40) x36) ⟶ (∀ x40 . x40 ∈ int ⟶ x39 x40 = x38 x40) ⟶ ∀ x40 . x40 ∈ int ⟶ SNoLe 0 x40 ⟶ x20 x40 = x39 x40
Conjecture 65182..^A21629 : ∀ 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 ⟶ ∀ 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 ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ int) ⟶ ∀ x33 : ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x33 x34 x35 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 : ι → ι . (∀ x40 . x40 ∈ int ⟶ x39 x40 ∈ int) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x0 x40 x41 = mul_SNo (add_SNo 2 x41) x40) ⟶ x1 = 2 ⟶ (∀ x40 . x40 ∈ int ⟶ x2 x40 = x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x3 x40 x41 = If_i (SNoLe x40 0) x41 (x0 (x3 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x4 x40 = x3 x1 (x2 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x5 x40 = add_SNo 1 (x4 x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x6 x40 x41 = x41) ⟶ x7 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x8 x40 x41 = If_i (SNoLe x40 0) x41 (x5 (x8 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x9 x40 x41 = x8 (x6 x40 x41) x7) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x10 x40 x41 = add_SNo (add_SNo (x9 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x11 x40 x41 = x41) ⟶ x12 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x13 x40 x41 = If_i (SNoLe x40 0) x41 (x10 (x13 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x14 x40 x41 = x13 (x11 x40 x41) x12) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x15 x40 x41 = add_SNo (add_SNo (add_SNo (x14 x40 x41) x40) x40) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x16 x40 = x40) ⟶ x17 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x18 x40 x41 = If_i (SNoLe x40 0) x41 (x15 (x18 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x19 x40 = x18 (x16 x40) x17) ⟶ (∀ x40 . x40 ∈ int ⟶ x20 x40 = x19 x40) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x21 x40 x41 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x22 x40 x41 = add_SNo 1 (add_SNo (add_SNo x41 x41) x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ x23 x40 = x40) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 2 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x26 x40 x41 x42 = If_i (SNoLe x40 0) x41 (x21 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x27 x40 x41 x42 = If_i (SNoLe x40 0) x42 (x22 (x26 (add_SNo x40 (minus_SNo 1)) x41 x42) (x27 (add_SNo x40 (minus_SNo 1)) x41 x42))) ⟶ (∀ x40 . x40 ∈ int ⟶ x28 x40 = x26 (x23 x40) x24 x25) ⟶ (∀ x40 . x40 ∈ int ⟶ x29 x40 = x28 x40) ⟶ x30 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x31 x40 x41 = x41) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x32 x40 x41 = If_i (SNoLe x40 0) x41 (x29 (x32 (add_SNo x40 (minus_SNo 1)) x41))) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x33 x40 x41 = x32 x30 (x31 x40 x41)) ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x34 x40 x41 = add_SNo (add_SNo (x33 x40 x41) (mul_SNo 2 (add_SNo (add_SNo x40 x40) x40))) x40) ⟶ (∀ x40 . x40 ∈ int ⟶ x35 x40 = x40) ⟶ x36 = 1 ⟶ (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x37 x40 x41 = If_i (SNoLe x40 0) x41 (x34 (x37 (add_SNo x40 (minus_SNo 1)) x41) x40)) ⟶ (∀ x40 . x40 ∈ int ⟶ x38 x40 = x37 (x35 x40) x36) ⟶ (∀ x40 . x40 ∈ int ⟶ x39 x40 = x38 x40) ⟶ ∀ x40 . x40 ∈ int ⟶ SNoLe 0 x40 ⟶ x20 x40 = x39 x40