Proofgold Signed Transaction

Param int^int : ι
Param add_SNo^add_SNo : ι → ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Conjecture 9ca01..^A28027 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ 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 . 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ 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 ⟶ ∀ 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 : ι → ι → ι . (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x25 x26 x27 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 : ι → ι . (∀ x28 . x28 ∈ int ⟶ x27 x28 ∈ int) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x0 x28 x29 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x29 (minus_SNo 1)) x29) (mul_SNo x29 x29)) x28) (mul_SNo 2 (add_SNo x28 x28))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x1 x28 x29 = add_SNo x29 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x2 x28 x29 = x29) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ 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 ⟶ ∀ x29 . x29 ∈ int ⟶ x7 x28 x29 = x5 (x2 x28 x29) x3 x4) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x8 x28 x29 = add_SNo (add_SNo (add_SNo (x7 x28 x29) 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 . x28 ∈ int ⟶ x12 x28 = x11 (x9 x28) x10) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = x12 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x14 x28 x29 = add_SNo (add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo x29 (minus_SNo 1)) x29) (mul_SNo x29 x29)) x28) x28) x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x15 x28 x29 = add_SNo x29 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x16 x28 x29 = x29) ⟶ x17 = 1 ⟶ x18 = 2 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x21 x28 x29 = x19 (x16 x28 x29) x17 x18) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x22 x28 x29 = add_SNo (add_SNo (x21 x28 x29) (mul_SNo 2 (add_SNo x28 x28))) x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x23 x28 = x28) ⟶ x24 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x26 x28 = x25 (x23 x28) x24) ⟶ (∀ x28 . x28 ∈ int ⟶ x27 x28 = x26 x28) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x13 x28 = x27 x28
Conjecture 7c1f5..^A28025 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ 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 ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ 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 ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ 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 : ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ 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 ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ int) ⟶ ∀ x36 . x36 ∈ 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 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) (mul_SNo x46 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x1 x45 x46 = add_SNo x46 x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x2 x45 x46 = x46) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x5 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x0 (x5 (add_SNo x45 (minus_SNo 1)) x46 x47) (x6 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x6 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x1 (x5 (add_SNo x45 (minus_SNo 1)) x46 x47) (x6 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x7 x45 x46 = x5 (x2 x45 x46) x3 x4) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x8 x45 x46 = add_SNo (add_SNo (x7 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x9 x45 x46 = x46) ⟶ x10 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x11 x45 x46 = If_i (SNoLe x45 0) x46 (x8 (x11 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x12 x45 x46 = x11 (x9 x45 x46) x10) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x13 x45 x46 = add_SNo (add_SNo (add_SNo (x12 x45 x46) x45) x45) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x14 x45 = x45) ⟶ x15 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x16 x45 x46 = If_i (SNoLe x45 0) x46 (x13 (x16 (add_SNo x45 (minus_SNo 1)) x46) x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x17 x45 = x16 (x14 x45) x15) ⟶ (∀ x45 . x45 ∈ int ⟶ x18 x45 = x17 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x19 x45 = add_SNo (add_SNo x45 x45) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x20 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x21 x45 = add_SNo x45 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x22 x45 = x45) ⟶ x23 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x24 x45 x46 = If_i (SNoLe x45 0) x46 (x21 (x24 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x25 x45 = x24 (x22 x45) x23) ⟶ (∀ x45 . x45 ∈ int ⟶ x26 x45 = add_SNo (x25 x45) (minus_SNo 1)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x27 x45 x46 = If_i (SNoLe x45 0) x46 (x19 (x27 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x27 (x20 x45) (x26 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x29 x45 = x28 x45) ⟶ x30 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x31 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x33 x45 x46 = x32 x30 (x31 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x34 x45 x46 = add_SNo (x33 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x35 x45 x46 = x46) ⟶ x36 = 1 ⟶ (∀ 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 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x38 x45 x46 = x37 (x35 x45 x46) x36) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) (mul_SNo 2 (add_SNo 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 ⟶ x18 x45 = x44 x45
Conjecture cfa10..^A28024 : ∀ 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 ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ 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 ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ 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 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ 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 ⟶ ∀ x31 . x31 ∈ int ⟶ x29 x30 x31 ∈ int) ⟶ ∀ x30 : ι → ι → ι . (∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x30 x31 x32 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 : ι → ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x34 x35 x36 x37 ∈ int) ⟶ ∀ x35 : ι → ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x35 x36 x37 x38 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 . x39 ∈ 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 ⟶ ∀ x54 . x54 ∈ int ⟶ x0 x53 x54 = mul_SNo (add_SNo 2 x54) 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 . x53 ∈ int ⟶ x4 x53 = x3 x1 (x2 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x5 x53 x54 = add_SNo (add_SNo (x4 x53) (minus_SNo x53)) x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x6 x53 x54 = add_SNo x54 x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x7 x53 x54 = x54) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x10 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x5 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x11 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x6 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x12 x53 x54 = x10 (x7 x53 x54) x8 x9) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x13 x53 x54 = add_SNo (x12 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x14 x53 x54 = x54) ⟶ x15 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x16 x53 x54 = If_i (SNoLe x53 0) x54 (x13 (x16 (add_SNo x53 (minus_SNo 1)) x54) x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x17 x53 x54 = x16 (x14 x53 x54) x15) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x18 x53 x54 = mul_SNo (add_SNo 2 x54) x53) ⟶ x19 = 2 ⟶ (∀ x53 . x53 ∈ int ⟶ x20 x53 = x53) ⟶ (∀ 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 . x53 ∈ int ⟶ x22 x53 = x21 x19 (x20 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x23 x53 x54 = add_SNo (x17 x53 x54) (x22 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x24 x53 = x53) ⟶ x25 = 1 ⟶ (∀ 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 ⟶ ∀ x54 . x54 ∈ int ⟶ x29 x53 x54 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x53 x53) x53)) x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x30 x53 x54 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x54 x54)) x54)) ⟶ (∀ x53 . x53 ∈ int ⟶ x31 x53 = x53) ⟶ x32 = 1 ⟶ x33 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x34 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x29 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x35 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x30 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ x36 x53 = x34 (x31 x53) x32 x33) ⟶ (∀ x53 . x53 ∈ int ⟶ x37 x53 = add_SNo x53 x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x38 x53 = x53) ⟶ x39 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x40 x53 x54 = If_i (SNoLe x53 0) x54 (x37 (x40 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x41 x53 = x40 (x38 x53) x39) ⟶ (∀ x53 . x53 ∈ int ⟶ x42 x53 = mul_SNo (x36 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 (add_SNo (x46 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53))) x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x48 x53 = x53) ⟶ x49 = 1 ⟶ (∀ 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 10244..^A28022 : ∀ 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 ⟶ ∀ 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 : ι → ι . (∀ 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 : ι → ι → ι . (∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x41 x42 x43 ∈ int) ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι → ι . (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x44 x45 x46 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 : ι → ι → ι . (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x47 x48 x49 ∈ int) ⟶ ∀ x48 : ι → ι . (∀ x49 . x49 ∈ int ⟶ x48 x49 ∈ int) ⟶ ∀ x49 : ι → ι . (∀ x50 . x50 ∈ int ⟶ x49 x50 ∈ int) ⟶ (∀ x50 . x50 ∈ int ⟶ x0 x50 = add_SNo (add_SNo x50 x50) x50) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x1 x50 x51 = add_SNo x51 x51) ⟶ x2 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x3 x50 x51 = If_i (SNoLe x50 0) x51 (x0 (x3 (add_SNo x50 (minus_SNo 1)) x51))) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x4 x50 x51 = x3 (x1 x50 x51) x2) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x5 x50 x51 = add_SNo (x4 x50 x51) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x50 x50)) x50))) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x6 x50 x51 = x51) ⟶ x7 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x8 x50 x51 = If_i (SNoLe x50 0) x51 (x5 (x8 (add_SNo x50 (minus_SNo 1)) x51) x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x9 x50 x51 = x8 (x6 x50 x51) x7) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x10 x50 x51 = mul_SNo (add_SNo 2 x51) x50) ⟶ x11 = 2 ⟶ (∀ x50 . x50 ∈ int ⟶ x12 x50 = x50) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x13 x50 x51 = If_i (SNoLe x50 0) x51 (x10 (x13 (add_SNo x50 (minus_SNo 1)) x51) x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ x14 x50 = x13 x11 (x12 x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x15 x50 x51 = add_SNo (x9 x50 x51) (x14 x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x16 x50 x51 = x51) ⟶ x17 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x18 x50 x51 = If_i (SNoLe x50 0) x51 (x15 (x18 (add_SNo x50 (minus_SNo 1)) x51) x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x19 x50 x51 = x18 (x16 x50 x51) x17) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x20 x50 x51 = add_SNo (add_SNo (x19 x50 x51) x50) x50) ⟶ (∀ x50 . x50 ∈ int ⟶ x21 x50 = x50) ⟶ x22 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x23 x50 x51 = If_i (SNoLe x50 0) x51 (x20 (x23 (add_SNo x50 (minus_SNo 1)) x51) x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ x24 x50 = x23 (x21 x50) x22) ⟶ (∀ x50 . x50 ∈ int ⟶ x25 x50 = x24 x50) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x26 x50 x51 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x50 x50) x50)) x51) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x27 x50 x51 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x51 x51)) x51)) ⟶ (∀ x50 . x50 ∈ int ⟶ x28 x50 = x50) ⟶ x29 = 1 ⟶ x30 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x31 x50 x51 x52 = If_i (SNoLe x50 0) x51 (x26 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52))) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x32 x50 x51 x52 = If_i (SNoLe x50 0) x52 (x27 (x31 (add_SNo x50 (minus_SNo 1)) x51 x52) (x32 (add_SNo x50 (minus_SNo 1)) x51 x52))) ⟶ (∀ x50 . x50 ∈ int ⟶ x33 x50 = x31 (x28 x50) x29 x30) ⟶ (∀ x50 . x50 ∈ int ⟶ x34 x50 = add_SNo x50 x50) ⟶ (∀ x50 . x50 ∈ int ⟶ x35 x50 = x50) ⟶ x36 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x37 x50 x51 = If_i (SNoLe x50 0) x51 (x34 (x37 (add_SNo x50 (minus_SNo 1)) x51))) ⟶ (∀ x50 . x50 ∈ int ⟶ x38 x50 = x37 (x35 x50) x36) ⟶ (∀ x50 . x50 ∈ int ⟶ x39 x50 = mul_SNo (x33 x50) (x38 x50)) ⟶ x40 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x41 x50 x51 = x51) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x42 x50 x51 = If_i (SNoLe x50 0) x51 (x39 (x42 (add_SNo x50 (minus_SNo 1)) x51))) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x43 x50 x51 = x42 x40 (x41 x50 x51)) ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x44 x50 x51 = add_SNo (add_SNo (x43 x50 x51) (mul_SNo 2 (mul_SNo 2 (add_SNo x50 x50)))) x50) ⟶ (∀ x50 . x50 ∈ int ⟶ x45 x50 = x50) ⟶ x46 = 1 ⟶ (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x47 x50 x51 = If_i (SNoLe x50 0) x51 (x44 (x47 (add_SNo x50 (minus_SNo 1)) x51) x50)) ⟶ (∀ x50 . x50 ∈ int ⟶ x48 x50 = x47 (x45 x50) x46) ⟶ (∀ x50 . x50 ∈ int ⟶ x49 x50 = x48 x50) ⟶ ∀ x50 . x50 ∈ int ⟶ SNoLe 0 x50 ⟶ x25 x50 = x49 x50
Conjecture 41ba0..^A280211 : ∀ 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 ⟶ ∀ 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 : ι → ι . (∀ 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 ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x0 x28 = add_SNo x28 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x1 x28 = mul_SNo x28 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x2 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ (∀ x28 . x28 ∈ int ⟶ x4 x28 = x3 (x1 x28) (x2 x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x5 x28 = x4 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x6 x28 = add_SNo x28 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x7 x28 = add_SNo (add_SNo x28 x28) (minus_SNo 1)) ⟶ (∀ x28 . x28 ∈ int ⟶ x8 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x9 x28 x29 = If_i (SNoLe x28 0) x29 (x6 (x9 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ (∀ x28 . x28 ∈ int ⟶ x10 x28 = x9 (x7 x28) (x8 x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x11 x28 x29 = mul_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x12 x28 x29 = add_SNo x29 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = add_SNo x28 (minus_SNo 2)) ⟶ x14 = 1 ⟶ x15 = 2 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x16 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x11 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x17 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x12 (x16 (add_SNo x28 (minus_SNo 1)) x29 x30) (x17 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ x18 x28 = x16 (x13 x28) x14 x15) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x19 x28 x29 = mul_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x20 x28 x29 = add_SNo x29 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ x21 x28 = add_SNo x28 (minus_SNo 1)) ⟶ x22 = 1 ⟶ x23 = 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 = mul_SNo (mul_SNo (x10 x28) (x18 x28)) (x26 x28)) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x5 x28 = x27 x28
Conjecture 4941f..^A28020 : ∀ 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 ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ 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 ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 . x14 ∈ 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 ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 . x20 ∈ 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 ⟶ ∀ x31 . x31 ∈ int ⟶ x29 x30 x31 ∈ int) ⟶ ∀ x30 : ι → ι → ι . (∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x30 x31 x32 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 : ι → ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x34 x35 x36 x37 ∈ int) ⟶ ∀ x35 : ι → ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x35 x36 x37 x38 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ ∀ x38 : ι → ι . (∀ x39 . x39 ∈ int ⟶ x38 x39 ∈ int) ⟶ ∀ x39 . x39 ∈ 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 ⟶ ∀ x54 . x54 ∈ int ⟶ x0 x53 x54 = mul_SNo (add_SNo 2 x54) 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 . x53 ∈ int ⟶ x4 x53 = x3 x1 (x2 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x5 x53 x54 = add_SNo (add_SNo (x4 x53) (minus_SNo x53)) (mul_SNo (mul_SNo x54 x54) x54)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x6 x53 x54 = add_SNo x54 x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x7 x53 x54 = x54) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x10 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x5 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x11 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x6 (x10 (add_SNo x53 (minus_SNo 1)) x54 x55) (x11 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x12 x53 x54 = x10 (x7 x53 x54) x8 x9) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x13 x53 x54 = mul_SNo (add_SNo 2 x54) x53) ⟶ x14 = 2 ⟶ (∀ x53 . x53 ∈ int ⟶ x15 x53 = x53) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x16 x53 x54 = If_i (SNoLe x53 0) x54 (x13 (x16 (add_SNo x53 (minus_SNo 1)) x54) x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ x17 x53 = x16 x14 (x15 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x18 x53 x54 = add_SNo (x12 x53 x54) (x17 x53)) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x19 x53 x54 = x54) ⟶ x20 = 1 ⟶ (∀ 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 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x22 x53 x54 = x21 (x19 x53 x54) x20) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x23 x53 x54 = add_SNo (add_SNo (x22 x53 x54) x53) x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x24 x53 = x53) ⟶ x25 = 1 ⟶ (∀ 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 ⟶ ∀ x54 . x54 ∈ int ⟶ x29 x53 x54 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x53 x53) x53)) x54) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x30 x53 x54 = add_SNo 1 (mul_SNo 2 (add_SNo x54 x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x31 x53 = x53) ⟶ x32 = 1 ⟶ x33 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x34 x53 x54 x55 = If_i (SNoLe x53 0) x54 (x29 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 . x55 ∈ int ⟶ x35 x53 x54 x55 = If_i (SNoLe x53 0) x55 (x30 (x34 (add_SNo x53 (minus_SNo 1)) x54 x55) (x35 (add_SNo x53 (minus_SNo 1)) x54 x55))) ⟶ (∀ x53 . x53 ∈ int ⟶ x36 x53 = x34 (x31 x53) x32 x33) ⟶ (∀ x53 . x53 ∈ int ⟶ x37 x53 = add_SNo x53 x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x38 x53 = x53) ⟶ x39 = 1 ⟶ (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x40 x53 x54 = If_i (SNoLe x53 0) x54 (x37 (x40 (add_SNo x53 (minus_SNo 1)) x54))) ⟶ (∀ x53 . x53 ∈ int ⟶ x41 x53 = x40 (x38 x53) x39) ⟶ (∀ x53 . x53 ∈ int ⟶ x42 x53 = mul_SNo (x36 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 (add_SNo (x46 x53 x54) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x53 x53)) x53))) x53) ⟶ (∀ x53 . x53 ∈ int ⟶ x48 x53 = x53) ⟶ x49 = 1 ⟶ (∀ 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 f1171..^A28019 : ∀ 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 : ι → ι . (∀ 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 ⟶ 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 : ι → ι . (∀ 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 (add_SNo x45 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 ⟶ ∀ x46 . x46 ∈ int ⟶ x5 x45 x46 = add_SNo (x4 x45 x46) (mul_SNo 2 (add_SNo x45 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 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x9 x45 x46 = x8 (x6 x45 x46) x7) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x10 x45 x46 = add_SNo (add_SNo (x9 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x11 x45 = x45) ⟶ 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 ⟶ x14 x45 = x13 (x11 x45) x12) ⟶ (∀ x45 . x45 ∈ int ⟶ x15 x45 = add_SNo x45 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x16 x45 = x45) ⟶ 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 ∈ int ⟶ x19 x45 = x18 (x16 x45) x17) ⟶ (∀ x45 . x45 ∈ int ⟶ x20 x45 = mul_SNo (x14 x45) (x19 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x21 x45 x46 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x22 x45 x46 = add_SNo 1 (mul_SNo 2 (add_SNo x46 x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x23 x45 = x45) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x26 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x21 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x27 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x22 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x26 (x23 x45) x24 x25) ⟶ (∀ x45 . x45 ∈ int ⟶ x29 x45 = x28 x45) ⟶ x30 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x31 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x33 x45 x46 = x32 x30 (x31 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x34 x45 x46 = add_SNo (add_SNo (x33 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x35 x45 = x45) ⟶ x36 = 1 ⟶ (∀ 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 . x45 ∈ int ⟶ x38 x45 = x37 (x35 x45) x36) ⟶ (∀ x45 . x45 ∈ int ⟶ x39 x45 = add_SNo 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 ∈ int ⟶ x43 x45 = x42 (x40 x45) x41) ⟶ (∀ x45 . x45 ∈ int ⟶ x44 x45 = mul_SNo (x38 x45) (x43 x45)) ⟶ ∀ x45 . x45 ∈ int ⟶ SNoLe 0 x45 ⟶ x20 x45 = x44 x45
Conjecture 7b57a..^A28018 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ 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 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ 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 ⟶ x24 x25 x26 ∈ int) ⟶ ∀ x25 : ι → ι → ι . (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x25 x26 x27 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 : ι → ι → ι → ι . (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x29 x30 x31 x32 ∈ int) ⟶ ∀ x30 : ι → ι → ι → ι . (∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x30 x31 x32 x33 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 : ι → ι . (∀ x33 . x33 ∈ int ⟶ x32 x33 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 : ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x40 x41 x42 ∈ int) ⟶ ∀ x41 : ι → ι → ι . (∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x41 x42 x43 ∈ int) ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 : ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x45 x46 x47 ∈ int) ⟶ ∀ x46 : ι → ι . (∀ x47 . x47 ∈ int ⟶ x46 x47 ∈ int) ⟶ ∀ x47 : ι → ι . (∀ x48 . x48 ∈ int ⟶ x47 x48 ∈ int) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x0 x48 x49 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48)) (mul_SNo (mul_SNo x49 x49) x49)) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x1 x48 x49 = add_SNo x49 x49) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x2 x48 x49 = x49) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x5 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x0 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50))) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x6 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x1 (x5 (add_SNo x48 (minus_SNo 1)) x49 x50) (x6 (add_SNo x48 (minus_SNo 1)) x49 x50))) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x7 x48 x49 = x5 (x2 x48 x49) x3 x4) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x8 x48 x49 = mul_SNo (add_SNo 2 x49) x48) ⟶ x9 = 2 ⟶ (∀ x48 . x48 ∈ int ⟶ x10 x48 = x48) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x11 x48 x49 = If_i (SNoLe x48 0) x49 (x8 (x11 (add_SNo x48 (minus_SNo 1)) x49) x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ x12 x48 = x11 x9 (x10 x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x13 x48 x49 = add_SNo (add_SNo (x7 x48 x49) (minus_SNo x48)) (x12 x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x14 x48 x49 = x49) ⟶ x15 = 1 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x16 x48 x49 = If_i (SNoLe x48 0) x49 (x13 (x16 (add_SNo x48 (minus_SNo 1)) x49) x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x17 x48 x49 = x16 (x14 x48 x49) x15) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x18 x48 x49 = add_SNo (add_SNo (x17 x48 x49) x48) x48) ⟶ (∀ x48 . x48 ∈ int ⟶ x19 x48 = x48) ⟶ x20 = 1 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x21 x48 x49 = If_i (SNoLe x48 0) x49 (x18 (x21 (add_SNo x48 (minus_SNo 1)) x49) x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ x22 x48 = x21 (x19 x48) x20) ⟶ (∀ x48 . x48 ∈ int ⟶ x23 x48 = x22 x48) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x24 x48 x49 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48) x49) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x25 x48 x49 = add_SNo 1 (mul_SNo 2 (add_SNo x49 x49))) ⟶ (∀ x48 . x48 ∈ int ⟶ x26 x48 = x48) ⟶ x27 = 1 ⟶ x28 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x29 x48 x49 x50 = If_i (SNoLe x48 0) x49 (x24 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50))) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x30 x48 x49 x50 = If_i (SNoLe x48 0) x50 (x25 (x29 (add_SNo x48 (minus_SNo 1)) x49 x50) (x30 (add_SNo x48 (minus_SNo 1)) x49 x50))) ⟶ (∀ x48 . x48 ∈ int ⟶ x31 x48 = x29 (x26 x48) x27 x28) ⟶ (∀ x48 . x48 ∈ int ⟶ x32 x48 = add_SNo x48 x48) ⟶ (∀ x48 . x48 ∈ int ⟶ x33 x48 = x48) ⟶ x34 = 1 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x35 x48 x49 = If_i (SNoLe x48 0) x49 (x32 (x35 (add_SNo x48 (minus_SNo 1)) x49))) ⟶ (∀ x48 . x48 ∈ int ⟶ x36 x48 = x35 (x33 x48) x34) ⟶ (∀ x48 . x48 ∈ int ⟶ x37 x48 = mul_SNo (x31 x48) (x36 x48)) ⟶ x38 = 1 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x39 x48 x49 = x49) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x40 x48 x49 = If_i (SNoLe x48 0) x49 (x37 (x40 (add_SNo x48 (minus_SNo 1)) x49))) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x41 x48 x49 = x40 x38 (x39 x48 x49)) ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x42 x48 x49 = add_SNo (add_SNo (x41 x48 x49) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x48 x48)) x48))) x48) ⟶ (∀ x48 . x48 ∈ int ⟶ x43 x48 = x48) ⟶ x44 = 1 ⟶ (∀ x48 . x48 ∈ int ⟶ ∀ x49 . x49 ∈ int ⟶ x45 x48 x49 = If_i (SNoLe x48 0) x49 (x42 (x45 (add_SNo x48 (minus_SNo 1)) x49) x48)) ⟶ (∀ x48 . x48 ∈ int ⟶ x46 x48 = x45 (x43 x48) x44) ⟶ (∀ x48 . x48 ∈ int ⟶ x47 x48 = x46 x48) ⟶ ∀ x48 . x48 ∈ int ⟶ SNoLe 0 x48 ⟶ x23 x48 = x47 x48
Conjecture a00ed..^A28012 : ∀ 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 ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ 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 ⟶ ∀ x14 . x14 ∈ int ⟶ x12 x13 x14 ∈ 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 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ 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 ⟶ x24 x25 x26 ∈ int) ⟶ ∀ x25 : ι → ι → ι . (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x25 x26 x27 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 : ι → ι → ι → ι . (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x29 x30 x31 x32 ∈ int) ⟶ ∀ x30 : ι → ι → ι → ι . (∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x30 x31 x32 x33 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 : ι → ι . (∀ x33 . x33 ∈ int ⟶ x32 x33 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 : ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x40 x41 x42 ∈ int) ⟶ ∀ x41 : ι → ι → ι . (∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x41 x42 x43 ∈ int) ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 : ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x45 x46 x47 ∈ int) ⟶ ∀ x46 : ι → ι . (∀ x47 . x47 ∈ int ⟶ x46 x47 ∈ int) ⟶ ∀ x47 : ι → ι . (∀ x48 . x48 ∈ int ⟶ x47 x48 ∈ int) ⟶ ∀ x48 . x48 ∈ int ⟶ ∀ x49 : ι → ι → ι . (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x49 x50 x51 ∈ int) ⟶ ∀ x50 : ι → ι → ι . (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x50 x51 x52 ∈ int) ⟶ ∀ x51 : ι → ι → ι . (∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x51 x52 x53 ∈ int) ⟶ ∀ x52 : ι → ι → ι . (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x52 x53 x54 ∈ int) ⟶ ∀ x53 : ι → ι . (∀ x54 . x54 ∈ int ⟶ x53 x54 ∈ int) ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 : ι → ι → ι . (∀ x56 . x56 ∈ int ⟶ ∀ x57 . x57 ∈ int ⟶ x55 x56 x57 ∈ int) ⟶ ∀ x56 : ι → ι . (∀ x57 . x57 ∈ int ⟶ x56 x57 ∈ int) ⟶ ∀ x57 : ι → ι . (∀ x58 . x58 ∈ int ⟶ x57 x58 ∈ int) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x0 x58 x59 = mul_SNo (add_SNo 2 x59) x58) ⟶ x1 = 2 ⟶ (∀ x58 . x58 ∈ int ⟶ x2 x58 = x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x3 x58 x59 = If_i (SNoLe x58 0) x59 (x0 (x3 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x4 x58 = x3 x1 (x2 x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x5 x58 x59 = add_SNo (add_SNo (x4 x58) (minus_SNo x58)) x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x6 x58 x59 = add_SNo x59 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x7 x58 x59 = x59) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x10 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x5 (x10 (add_SNo x58 (minus_SNo 1)) x59 x60) (x11 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x11 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x6 (x10 (add_SNo x58 (minus_SNo 1)) x59 x60) (x11 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x12 x58 x59 = x10 (x7 x58 x59) x8 x9) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x13 x58 x59 = add_SNo (x12 x58 x59) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x58 x58)) x58))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x14 x58 x59 = x59) ⟶ x15 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x16 x58 x59 = If_i (SNoLe x58 0) x59 (x13 (x16 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x17 x58 x59 = x16 (x14 x58 x59) x15) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x18 x58 x59 = add_SNo (add_SNo (x17 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x19 x58 = x58) ⟶ x20 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x21 x58 x59 = If_i (SNoLe x58 0) x59 (x18 (x21 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x22 x58 = x21 (x19 x58) x20) ⟶ (∀ x58 . x58 ∈ int ⟶ x23 x58 = x22 x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x24 x58 x59 = add_SNo 1 (mul_SNo x58 x59)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x25 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x26 x58 = x58) ⟶ x27 = 1 ⟶ x28 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x29 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x24 (x29 (add_SNo x58 (minus_SNo 1)) x59 x60) (x30 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x30 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x25 (x29 (add_SNo x58 (minus_SNo 1)) x59 x60) (x30 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ x31 x58 = x29 (x26 x58) x27 x28) ⟶ (∀ x58 . x58 ∈ int ⟶ x32 x58 = add_SNo x58 x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x33 x58 = x58) ⟶ x34 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x35 x58 x59 = If_i (SNoLe x58 0) x59 (x32 (x35 (add_SNo x58 (minus_SNo 1)) x59))) ⟶ (∀ x58 . x58 ∈ int ⟶ x36 x58 = x35 (x33 x58) x34) ⟶ (∀ x58 . x58 ∈ int ⟶ x37 x58 = mul_SNo (x31 x58) (x36 x58)) ⟶ x38 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x39 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x40 x58 x59 = If_i (SNoLe x58 0) x59 (x37 (x40 (add_SNo x58 (minus_SNo 1)) x59))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x41 x58 x59 = x40 x38 (x39 x58 x59)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x42 x58 x59 = add_SNo (add_SNo (x41 x58 x59) (mul_SNo 2 (add_SNo (add_SNo x58 x58) x58))) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x43 x58 = x58) ⟶ x44 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x45 x58 x59 = If_i (SNoLe x58 0) x59 (x42 (x45 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x46 x58 = x45 (x43 x58) x44) ⟶ (∀ x58 . x58 ∈ int ⟶ x47 x58 = x46 x58) ⟶ x48 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x49 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x50 x58 x59 = If_i (SNoLe x58 0) x59 (x47 (x50 (add_SNo x58 (minus_SNo 1)) x59))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x51 x58 x59 = x50 x48 (x49 x58 x59)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x52 x58 x59 = add_SNo (add_SNo (x51 x58 x59) (mul_SNo (add_SNo (mul_SNo (add_SNo x58 x58) 2) x58) 2)) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x53 x58 = x58) ⟶ x54 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x55 x58 x59 = If_i (SNoLe x58 0) x59 (x52 (x55 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x56 x58 = x55 (x53 x58) x54) ⟶ (∀ x58 . x58 ∈ int ⟶ x57 x58 = x56 x58) ⟶ ∀ x58 . x58 ∈ int ⟶ SNoLe 0 x58 ⟶ x23 x58 = x57 x58
Conjecture 7c225..^A28009 : ∀ 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 : ι → ι → ι . (∀ 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 : ι → ι . (∀ x31 . x31 ∈ int ⟶ x30 x31 ∈ int) ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 : ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x32 x33 x34 ∈ 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 : ι → ι → ι . (∀ 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 ⟶ ∀ x50 . x50 ∈ int ⟶ x48 x49 x50 ∈ int) ⟶ ∀ x49 : ι → ι → ι . (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x49 x50 x51 ∈ int) ⟶ ∀ x50 : ι → ι . (∀ x51 . x51 ∈ int ⟶ x50 x51 ∈ int) ⟶ ∀ x51 . x51 ∈ int ⟶ ∀ x52 : ι → ι → ι . (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x52 x53 x54 ∈ int) ⟶ ∀ x53 : ι → ι . (∀ x54 . x54 ∈ int ⟶ x53 x54 ∈ int) ⟶ ∀ x54 : ι → ι . (∀ x55 . x55 ∈ int ⟶ x54 x55 ∈ int) ⟶ (∀ x55 . x55 ∈ int ⟶ x0 x55 = add_SNo (add_SNo x55 x55) x55) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x1 x55 x56 = add_SNo x56 x56) ⟶ x2 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x3 x55 x56 = If_i (SNoLe x55 0) x56 (x0 (x3 (add_SNo x55 (minus_SNo 1)) x56))) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x4 x55 x56 = x3 (x1 x55 x56) x2) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x5 x55 x56 = add_SNo (x4 x55 x56) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x55 x55)) x55))) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x6 x55 x56 = x56) ⟶ x7 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x8 x55 x56 = If_i (SNoLe x55 0) x56 (x5 (x8 (add_SNo x55 (minus_SNo 1)) x56) x55)) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x9 x55 x56 = x8 (x6 x55 x56) x7) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x10 x55 x56 = add_SNo (add_SNo (x9 x55 x56) (mul_SNo 2 (add_SNo (add_SNo x55 x55) x55))) x55) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x11 x55 x56 = x56) ⟶ x12 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x13 x55 x56 = If_i (SNoLe x55 0) x56 (x10 (x13 (add_SNo x55 (minus_SNo 1)) x56) x55)) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x14 x55 x56 = x13 (x11 x55 x56) x12) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x15 x55 x56 = add_SNo (add_SNo (x14 x55 x56) x55) x55) ⟶ (∀ x55 . x55 ∈ int ⟶ x16 x55 = x55) ⟶ x17 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x18 x55 x56 = If_i (SNoLe x55 0) x56 (x15 (x18 (add_SNo x55 (minus_SNo 1)) x56) x55)) ⟶ (∀ x55 . x55 ∈ int ⟶ x19 x55 = x18 (x16 x55) x17) ⟶ (∀ x55 . x55 ∈ int ⟶ x20 x55 = x19 x55) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x21 x55 x56 = add_SNo 1 (mul_SNo x55 x56)) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x22 x55 x56 = x56) ⟶ (∀ x55 . x55 ∈ int ⟶ x23 x55 = x55) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ ∀ x57 . x57 ∈ int ⟶ x26 x55 x56 x57 = If_i (SNoLe x55 0) x56 (x21 (x26 (add_SNo x55 (minus_SNo 1)) x56 x57) (x27 (add_SNo x55 (minus_SNo 1)) x56 x57))) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ ∀ x57 . x57 ∈ int ⟶ x27 x55 x56 x57 = If_i (SNoLe x55 0) x57 (x22 (x26 (add_SNo x55 (minus_SNo 1)) x56 x57) (x27 (add_SNo x55 (minus_SNo 1)) x56 x57))) ⟶ (∀ x55 . x55 ∈ int ⟶ x28 x55 = x26 (x23 x55) x24 x25) ⟶ (∀ x55 . x55 ∈ int ⟶ x29 x55 = add_SNo x55 x55) ⟶ (∀ x55 . x55 ∈ int ⟶ x30 x55 = x55) ⟶ x31 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x32 x55 x56 = If_i (SNoLe x55 0) x56 (x29 (x32 (add_SNo x55 (minus_SNo 1)) x56))) ⟶ (∀ x55 . x55 ∈ int ⟶ x33 x55 = x32 (x30 x55) x31) ⟶ (∀ x55 . x55 ∈ int ⟶ x34 x55 = mul_SNo (x28 x55) (x33 x55)) ⟶ x35 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x36 x55 x56 = x56) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x37 x55 x56 = If_i (SNoLe x55 0) x56 (x34 (x37 (add_SNo x55 (minus_SNo 1)) x56))) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x38 x55 x56 = x37 x35 (x36 x55 x56)) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x39 x55 x56 = add_SNo (add_SNo (x38 x55 x56) x55) (mul_SNo (mul_SNo (add_SNo x55 x55) 2) 2)) ⟶ (∀ x55 . x55 ∈ int ⟶ x40 x55 = x55) ⟶ x41 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x42 x55 x56 = If_i (SNoLe x55 0) x56 (x39 (x42 (add_SNo x55 (minus_SNo 1)) x56) x55)) ⟶ (∀ x55 . x55 ∈ int ⟶ x43 x55 = x42 (x40 x55) x41) ⟶ (∀ x55 . x55 ∈ int ⟶ x44 x55 = x43 x55) ⟶ x45 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x46 x55 x56 = x56) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x47 x55 x56 = If_i (SNoLe x55 0) x56 (x44 (x47 (add_SNo x55 (minus_SNo 1)) x56))) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x48 x55 x56 = x47 x45 (x46 x55 x56)) ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x49 x55 x56 = add_SNo (add_SNo (x48 x55 x56) x55) (mul_SNo (add_SNo (add_SNo x55 x55) x55) 2)) ⟶ (∀ x55 . x55 ∈ int ⟶ x50 x55 = x55) ⟶ x51 = 1 ⟶ (∀ x55 . x55 ∈ int ⟶ ∀ x56 . x56 ∈ int ⟶ x52 x55 x56 = If_i (SNoLe x55 0) x56 (x49 (x52 (add_SNo x55 (minus_SNo 1)) x56) x55)) ⟶ (∀ x55 . x55 ∈ int ⟶ x53 x55 = x52 (x50 x55) x51) ⟶ (∀ x55 . x55 ∈ int ⟶ x54 x55 = x53 x55) ⟶ ∀ x55 . x55 ∈ int ⟶ SNoLe 0 x55 ⟶ x20 x55 = x54 x55
Conjecture edca8..^A28006 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ 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 ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ 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 ⟶ ∀ 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 : ι → ι . (∀ 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 ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ 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 ⟶ x38 x39 ∈ int) ⟶ ∀ x39 . x39 ∈ 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 . x44 ∈ int ⟶ x0 x43 x44 = add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43)) (mul_SNo (mul_SNo x44 x44) x44)) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x1 x43 x44 = add_SNo x44 x44) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x2 x43 x44 = x44) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x5 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x0 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x6 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x1 (x5 (add_SNo x43 (minus_SNo 1)) x44 x45) (x6 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x7 x43 x44 = x5 (x2 x43 x44) x3 x4) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x8 x43 x44 = add_SNo (add_SNo (x7 x43 x44) (mul_SNo 2 (add_SNo (add_SNo x43 x43) x43))) x43) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x9 x43 x44 = x44) ⟶ x10 = 1 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x11 x43 x44 = If_i (SNoLe x43 0) x44 (x8 (x11 (add_SNo x43 (minus_SNo 1)) x44) x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x12 x43 x44 = x11 (x9 x43 x44) x10) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x13 x43 x44 = add_SNo (add_SNo (x12 x43 x44) x43) x43) ⟶ (∀ x43 . x43 ∈ int ⟶ x14 x43 = x43) ⟶ x15 = 1 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x16 x43 x44 = If_i (SNoLe x43 0) x44 (x13 (x16 (add_SNo x43 (minus_SNo 1)) x44) x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ x17 x43 = x16 (x14 x43) x15) ⟶ (∀ x43 . x43 ∈ int ⟶ x18 x43 = x17 x43) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x19 x43 x44 = add_SNo (add_SNo (mul_SNo 2 (add_SNo x43 x43)) x43) x44) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x20 x43 x44 = add_SNo 1 (mul_SNo 2 (add_SNo x44 x44))) ⟶ (∀ x43 . x43 ∈ int ⟶ x21 x43 = x43) ⟶ x22 = 1 ⟶ x23 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x24 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x19 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x25 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x20 (x24 (add_SNo x43 (minus_SNo 1)) x44 x45) (x25 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ x26 x43 = x24 (x21 x43) x22 x23) ⟶ (∀ x43 . x43 ∈ int ⟶ x27 x43 = add_SNo x43 x43) ⟶ (∀ x43 . x43 ∈ int ⟶ x28 x43 = x43) ⟶ x29 = 1 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x30 x43 x44 = If_i (SNoLe x43 0) x44 (x27 (x30 (add_SNo x43 (minus_SNo 1)) x44))) ⟶ (∀ x43 . x43 ∈ int ⟶ x31 x43 = x30 (x28 x43) x29) ⟶ (∀ x43 . x43 ∈ int ⟶ x32 x43 = mul_SNo (x26 x43) (x31 x43)) ⟶ x33 = 1 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x34 x43 x44 = x44) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x35 x43 x44 = If_i (SNoLe x43 0) x44 (x32 (x35 (add_SNo x43 (minus_SNo 1)) x44))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x36 x43 x44 = x35 x33 (x34 x43 x44)) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x37 x43 x44 = add_SNo (add_SNo (x36 x43 x44) x43) (mul_SNo (add_SNo (add_SNo x43 x43) x43) 2)) ⟶ (∀ x43 . x43 ∈ int ⟶ x38 x43 = x43) ⟶ x39 = 1 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x40 x43 x44 = If_i (SNoLe x43 0) x44 (x37 (x40 (add_SNo x43 (minus_SNo 1)) x44) x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ x41 x43 = x40 (x38 x43) x39) ⟶ (∀ x43 . x43 ∈ int ⟶ x42 x43 = x41 x43) ⟶ ∀ x43 . x43 ∈ int ⟶ SNoLe 0 x43 ⟶ x18 x43 = x42 x43
Conjecture 5b0ff..^A28003 : ∀ 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 : ι → ι . (∀ 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 ⟶ 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 : ι → ι . (∀ 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 (add_SNo x45 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 ⟶ ∀ x46 . x46 ∈ int ⟶ x5 x45 x46 = add_SNo (add_SNo (x4 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) 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 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x9 x45 x46 = x8 (x6 x45 x46) x7) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x10 x45 x46 = add_SNo (add_SNo (add_SNo (x9 x45 x46) x45) x45) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x11 x45 = x45) ⟶ 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 ⟶ x14 x45 = x13 (x11 x45) x12) ⟶ (∀ x45 . x45 ∈ int ⟶ x15 x45 = add_SNo x45 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x16 x45 = x45) ⟶ 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 ∈ int ⟶ x19 x45 = x18 (x16 x45) x17) ⟶ (∀ x45 . x45 ∈ int ⟶ x20 x45 = mul_SNo (x14 x45) (x19 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x21 x45 x46 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x45 x45) x45)) x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x22 x45 x46 = add_SNo 1 (add_SNo (add_SNo x46 x46) x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ x23 x45 = x45) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 2 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x26 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x21 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x27 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x22 (x26 (add_SNo x45 (minus_SNo 1)) x46 x47) (x27 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x26 (x23 x45) x24 x25) ⟶ (∀ x45 . x45 ∈ int ⟶ x29 x45 = x28 x45) ⟶ x30 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x31 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x32 x45 x46 = If_i (SNoLe x45 0) x46 (x29 (x32 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x33 x45 x46 = x32 x30 (x31 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x34 x45 x46 = add_SNo (add_SNo (x33 x45 x46) (mul_SNo 2 (add_SNo x45 x45))) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x35 x45 = x45) ⟶ x36 = 1 ⟶ (∀ 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 . x45 ∈ int ⟶ x38 x45 = x37 (x35 x45) x36) ⟶ (∀ x45 . x45 ∈ int ⟶ x39 x45 = add_SNo 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 ∈ int ⟶ x43 x45 = x42 (x40 x45) x41) ⟶ (∀ x45 . x45 ∈ int ⟶ x44 x45 = mul_SNo (x38 x45) (x43 x45)) ⟶ ∀ x45 . x45 ∈ int ⟶ SNoLe 0 x45 ⟶ x20 x45 = x44 x45
Conjecture 47c7a..^A27992 : ∀ 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 ⟶ ∀ 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 : ι → ι . (∀ 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 . x12 ∈ int ⟶ x0 x12 = add_SNo (add_SNo x12 (minus_SNo 1)) x12) ⟶ (∀ x12 . x12 ∈ int ⟶ x1 x12 = x12) ⟶ (∀ x12 . x12 ∈ int ⟶ x2 x12 = add_SNo (add_SNo x12 x12) x12) ⟶ (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x3 x12 x13 = If_i (SNoLe x12 0) x13 (x0 (x3 (add_SNo x12 (minus_SNo 1)) x13))) ⟶ (∀ x12 . x12 ∈ int ⟶ x4 x12 = x3 (x1 x12) (x2 x12)) ⟶ (∀ x12 . x12 ∈ int ⟶ x5 x12 = add_SNo 1 (x4 x12)) ⟶ (∀ x12 . x12 ∈ int ⟶ x6 x12 = add_SNo x12 x12) ⟶ (∀ x12 . x12 ∈ int ⟶ x7 x12 = x12) ⟶ (∀ x12 . x12 ∈ int ⟶ x8 x12 = add_SNo (add_SNo (add_SNo x12 (minus_SNo 1)) x12) x12) ⟶ (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x9 x12 x13 = If_i (SNoLe x12 0) x13 (x6 (x9 (add_SNo x12 (minus_SNo 1)) x13))) ⟶ (∀ x12 . x12 ∈ int ⟶ x10 x12 = x9 (x7 x12) (x8 x12)) ⟶ (∀ x12 . x12 ∈ int ⟶ x11 x12 = add_SNo 2 (x10 x12)) ⟶ ∀ x12 . x12 ∈ int ⟶ SNoLe 0 x12 ⟶ x5 x12 = x11 x12
Conjecture 39146..^A27990 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ 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 ⟶ ∀ 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 . 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 ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ 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 ⟶ ∀ 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 ⟶ ∀ 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 : ι → ι → ι . (∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x25 x26 x27 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 : ι → ι . (∀ x28 . x28 ∈ int ⟶ x27 x28 ∈ int) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x0 x28 x29 = x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x1 x28 x29 = add_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x2 x28 x29 = add_SNo x29 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x3 x28 x29 = add_SNo 1 x29) ⟶ x4 = 1 ⟶ (∀ 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 ⟶ ∀ x29 . x29 ∈ int ⟶ x7 x28 x29 = x5 (x2 x28 x29) (x3 x28 x29) x4) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x8 x28 x29 = add_SNo (x7 x28 x29) (minus_SNo 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 . x28 ∈ int ⟶ x12 x28 = x11 (x9 x28) x10) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = x12 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x14 x28 x29 = add_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x15 x28 x29 = add_SNo (add_SNo x28 x29) x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x16 x28 x29 = x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x17 x28 x29 = add_SNo 1 x29) ⟶ x18 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x19 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x14 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x20 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x15 (x19 (add_SNo x28 (minus_SNo 1)) x29 x30) (x20 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x21 x28 x29 = x19 (x16 x28 x29) (x17 x28 x29) x18) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x22 x28 x29 = add_SNo (x21 x28 x29) (minus_SNo x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x23 x28 = x28) ⟶ x24 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x25 x28 x29 = If_i (SNoLe x28 0) x29 (x22 (x25 (add_SNo x28 (minus_SNo 1)) x29) x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x26 x28 = x25 (x23 x28) x24) ⟶ (∀ x28 . x28 ∈ int ⟶ x27 x28 = x26 x28) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x13 x28 = x27 x28
Conjecture 654b0..^A27982 : ∀ 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 : ι → ι → ι → ι . (∀ 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 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ 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 : ι → ι → ι . (∀ 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 ⟶ x0 x20 x21 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo x20 x21)))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x1 x20 x21 = add_SNo 2 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ x2 x20 = x20) ⟶ x3 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ x4 x20 = x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x5 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x0 (x5 (add_SNo x20 (minus_SNo 1)) x21 x22) (x6 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x6 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x1 (x5 (add_SNo x20 (minus_SNo 1)) x21 x22) (x6 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x7 x20 = x5 (x2 x20) x3 (x4 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x8 x20 = x7 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x9 x20 = add_SNo x20 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x11 x20 = add_SNo 1 (add_SNo 2 (add_SNo 2 x20))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x12 x20 x21 = If_i (SNoLe x20 0) x21 (x9 (x12 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x13 x20 = x12 (x10 x20) (x11 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x14 x20 = add_SNo x20 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = x20) ⟶ x16 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x17 x20 x21 = If_i (SNoLe x20 0) x21 (x14 (x17 (add_SNo x20 (minus_SNo 1)) x21))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x17 (x15 x20) x16) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = add_SNo (add_SNo (mul_SNo (add_SNo (add_SNo (x13 x20) (minus_SNo (mul_SNo 2 (add_SNo 2 x20)))) (minus_SNo x20)) 2) (minus_SNo 2)) (x18 x20)) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x8 x20 = x19 x20
Conjecture 3d2d6..^A27964 : ∀ 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 ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ 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 : ι → ι → ι . (∀ 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 ⟶ ∀ 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 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ 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 ⟶ 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 ⟶ ∀ 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 ⟶ ∀ x31 . x31 ∈ int ⟶ x29 x30 x31 ∈ int) ⟶ ∀ x30 : ι → ι . (∀ x31 . x31 ∈ int ⟶ x30 x31 ∈ int) ⟶ ∀ x31 : ι → ι . (∀ x32 . x32 ∈ int ⟶ x31 x32 ∈ int) ⟶ ∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 : ι → ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x34 x35 x36 x37 ∈ int) ⟶ ∀ x35 : ι → ι → ι → ι . (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x35 x36 x37 x38 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x40 x41 x42 ∈ int) ⟶ ∀ x41 : ι → ι → ι . (∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x41 x42 x43 ∈ int) ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 : ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x45 x46 x47 ∈ int) ⟶ ∀ x46 : ι → ι . (∀ x47 . x47 ∈ int ⟶ x46 x47 ∈ int) ⟶ ∀ x47 : ι → ι . (∀ x48 . x48 ∈ int ⟶ x47 x48 ∈ int) ⟶ ∀ x48 . x48 ∈ int ⟶ ∀ x49 : ι → ι → ι . (∀ x50 . x50 ∈ int ⟶ ∀ x51 . x51 ∈ int ⟶ x49 x50 x51 ∈ int) ⟶ ∀ x50 : ι → ι → ι . (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x50 x51 x52 ∈ int) ⟶ ∀ x51 : ι → ι → ι . (∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x51 x52 x53 ∈ int) ⟶ ∀ x52 : ι → ι → ι . (∀ x53 . x53 ∈ int ⟶ ∀ x54 . x54 ∈ int ⟶ x52 x53 x54 ∈ int) ⟶ ∀ x53 : ι → ι . (∀ x54 . x54 ∈ int ⟶ x53 x54 ∈ int) ⟶ ∀ x54 . x54 ∈ int ⟶ ∀ x55 : ι → ι → ι . (∀ x56 . x56 ∈ int ⟶ ∀ x57 . x57 ∈ int ⟶ x55 x56 x57 ∈ int) ⟶ ∀ x56 : ι → ι . (∀ x57 . x57 ∈ int ⟶ x56 x57 ∈ int) ⟶ ∀ x57 : ι → ι . (∀ x58 . x58 ∈ int ⟶ x57 x58 ∈ int) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x0 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x1 x58 x59 = add_SNo x58 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x2 x58 x59 = x59) ⟶ x3 = 2 ⟶ x4 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x5 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x0 (x5 (add_SNo x58 (minus_SNo 1)) x59 x60) (x6 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x6 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x1 (x5 (add_SNo x58 (minus_SNo 1)) x59 x60) (x6 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x7 x58 x59 = x5 (x2 x58 x59) x3 x4) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x8 x58 x59 = add_SNo (x7 x58 x59) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x9 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x10 x58 = x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x11 x58 x59 = If_i (SNoLe x58 0) x59 (x8 (x11 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x12 x58 x59 = x11 (x9 x58 x59) (x10 x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x13 x58 x59 = x12 x58 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x14 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x15 x58 = x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x16 x58 x59 = If_i (SNoLe x58 0) x59 (x13 (x16 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x17 x58 x59 = x16 (x14 x58 x59) (x15 x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x18 x58 x59 = x17 x58 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x19 x58 x59 = add_SNo 1 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x20 x58 = x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x21 x58 x59 = If_i (SNoLe x58 0) x59 (x18 (x21 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x22 x58 x59 = x21 (x19 x58 x59) (x20 x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x23 x58 x59 = x22 x58 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x24 x58 = x58) ⟶ x25 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x26 x58 x59 = If_i (SNoLe x58 0) x59 (x23 (x26 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x27 x58 = x26 (x24 x58) x25) ⟶ (∀ x58 . x58 ∈ int ⟶ x28 x58 = x27 x58) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x29 x58 x59 = add_SNo x58 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ x30 x58 = x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x31 x58 = x58) ⟶ x32 = add_SNo 2 2 ⟶ x33 = add_SNo 1 2 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x34 x58 x59 x60 = If_i (SNoLe x58 0) x59 (x29 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60) (x35 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ ∀ x60 . x60 ∈ int ⟶ x35 x58 x59 x60 = If_i (SNoLe x58 0) x60 (x30 (x34 (add_SNo x58 (minus_SNo 1)) x59 x60))) ⟶ (∀ x58 . x58 ∈ int ⟶ x36 x58 = x34 (x31 x58) x32 x33) ⟶ (∀ x58 . x58 ∈ int ⟶ x37 x58 = add_SNo (add_SNo (add_SNo (add_SNo (x36 x58) (minus_SNo 2)) (minus_SNo x58)) (minus_SNo x58)) (minus_SNo x58)) ⟶ x38 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x39 x58 x59 = add_SNo 2 x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x40 x58 x59 = If_i (SNoLe x58 0) x59 (x37 (x40 (add_SNo x58 (minus_SNo 1)) x59))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x41 x58 x59 = x40 x38 (x39 x58 x59)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x42 x58 x59 = add_SNo (x41 x58 x59) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x43 x58 = x58) ⟶ x44 = 0 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x45 x58 x59 = If_i (SNoLe x58 0) x59 (x42 (x45 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x46 x58 = x45 (x43 x58) x44) ⟶ (∀ x58 . x58 ∈ int ⟶ x47 x58 = x46 x58) ⟶ x48 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x49 x58 x59 = x59) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x50 x58 x59 = If_i (SNoLe x58 0) x59 (x47 (x50 (add_SNo x58 (minus_SNo 1)) x59))) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x51 x58 x59 = x50 x48 (x49 x58 x59)) ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x52 x58 x59 = add_SNo (x51 x58 x59) x58) ⟶ (∀ x58 . x58 ∈ int ⟶ x53 x58 = x58) ⟶ x54 = 1 ⟶ (∀ x58 . x58 ∈ int ⟶ ∀ x59 . x59 ∈ int ⟶ x55 x58 x59 = If_i (SNoLe x58 0) x59 (x52 (x55 (add_SNo x58 (minus_SNo 1)) x59) x58)) ⟶ (∀ x58 . x58 ∈ int ⟶ x56 x58 = x55 (x53 x58) x54) ⟶ (∀ x58 . x58 ∈ int ⟶ x57 x58 = add_SNo (x56 x58) (minus_SNo (mul_SNo x58 x58))) ⟶ ∀ x58 . x58 ∈ int ⟶ SNoLe 0 x58 ⟶ x28 x58 = x57 x58
Conjecture b6988..^A27942 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ x2 x3 x4 ∈ 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 ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ 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 : ι → ι → ι . (∀ 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 ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ 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 ⟶ ∀ 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 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ 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 ⟶ ∀ x34 . x34 ∈ int ⟶ x0 x33 x34 = add_SNo 2 (add_SNo x33 x34)) ⟶ (∀ x33 . x33 ∈ int ⟶ x1 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x2 x33 x34 = x34) ⟶ x3 = 1 ⟶ x4 = 0 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x5 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x0 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35) (x6 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x6 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x1 (x5 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x7 x33 x34 = x5 (x2 x33 x34) x3 x4) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = add_SNo (x7 x33 x34) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x9 x33 x34 = add_SNo x34 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x10 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x11 x33 x34 = If_i (SNoLe x33 0) x34 (x8 (x11 (add_SNo x33 (minus_SNo 1)) x34) x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x12 x33 x34 = x11 (x9 x33 x34) (x10 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x13 x33 x34 = x12 x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x14 x33 = x33) ⟶ x15 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x16 x33 x34 = If_i (SNoLe x33 0) x34 (x13 (x16 (add_SNo x33 (minus_SNo 1)) x34) x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x17 x33 = x16 (x14 x33) x15) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = add_SNo (x17 x33) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x19 x33 x34 = add_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x20 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x21 x33 = add_SNo x33 x33) ⟶ x22 = 2 ⟶ x23 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x24 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x19 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35) (x25 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x25 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x20 (x24 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x26 x33 = x24 (x21 x33) x22 x23) ⟶ (∀ x33 . x33 ∈ int ⟶ x27 x33 = add_SNo (add_SNo (add_SNo (x26 x33) (minus_SNo (mul_SNo (add_SNo x33 x33) x33))) (minus_SNo x33)) (minus_SNo x33)) ⟶ x28 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ x29 x33 = add_SNo 2 x33) ⟶ (∀ 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 (x29 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = add_SNo (x31 x33) x33) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x18 x33 = x32 x33
Conjecture 77e50..^A27871 : ∀ 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 ⟶ 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 . 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 ⟶ x20 x21 ∈ int) ⟶ ∀ x21 . x21 ∈ 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 = add_SNo (add_SNo x25 x25) x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = x26) ⟶ (∀ 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 ⟶ ∀ x26 . x26 ∈ int ⟶ x4 x25 x26 = x3 (x1 x25 x26) (x2 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x5 x25 x26 = add_SNo (x4 x25 x26) (minus_SNo x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x6 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 . x25 ∈ int ⟶ x9 x25 = x8 (x6 x25) x7) ⟶ (∀ x25 . x25 ∈ int ⟶ x10 x25 = x9 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x11 x25 x26 = mul_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x12 x25 x26 = add_SNo 1 (add_SNo (add_SNo x26 x26) x26)) ⟶ (∀ x25 . x25 ∈ int ⟶ x13 x25 = add_SNo x25 (minus_SNo 1)) ⟶ x14 = 1 ⟶ x15 = add_SNo 2 2 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x16 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x11 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x17 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x12 (x16 (add_SNo x25 (minus_SNo 1)) x26 x27) (x17 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x18 x25 = x16 (x13 x25) x14 x15) ⟶ (∀ x25 . x25 ∈ int ⟶ x19 x25 = add_SNo x25 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x25) ⟶ x21 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x22 x25 x26 = If_i (SNoLe x25 0) x26 (x19 (x22 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x22 (x20 x25) x21) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = mul_SNo (x18 x25) (x23 x25)) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture ae2ae..^A277748 : ∀ 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 ⟶ x6 x7 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ 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 ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ 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 ⟶ x0 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x1 x30 x31 = x31) ⟶ (∀ x30 . x30 ∈ int ⟶ x2 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x3 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x3 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x4 x30 x31 = x3 (x1 x30 x31) (x2 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x5 x30 x31 = x4 x30 x31) ⟶ (∀ x30 . x30 ∈ int ⟶ x6 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x7 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x8 x30 = x30) ⟶ x9 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x10 x30 x31 = If_i (SNoLe x30 0) x31 (x7 (x10 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x11 x30 = x10 (x8 x30) x9) ⟶ (∀ x30 . x30 ∈ int ⟶ x12 x30 = add_SNo (x11 x30) (minus_SNo (add_SNo 1 x30))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x13 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 (x6 x30) (x12 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x15 x30 = x14 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x16 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x17 x30 = x30) ⟶ x18 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x19 x30 x31 = If_i (SNoLe x30 0) x31 (x16 (x19 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x20 x30 = x19 (x17 x30) x18) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x21 x30 x31 = mul_SNo x30 x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x22 x30 x31 = add_SNo x31 x31) ⟶ (∀ x30 . x30 ∈ int ⟶ x23 x30 = x30) ⟶ x24 = 1 ⟶ x25 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x26 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x21 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x27 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x22 (x26 (add_SNo x30 (minus_SNo 1)) x31 x32) (x27 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ x28 x30 = x26 (x23 x30) x24 x25) ⟶ (∀ x30 . x30 ∈ int ⟶ x29 x30 = mul_SNo (add_SNo (add_SNo (x20 x30) (minus_SNo 1)) (minus_SNo x30)) (x28 x30)) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x15 x30 = x29 x30
Conjecture 21466..^A277491 : ∀ 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 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x0 x18 x19 = add_SNo (add_SNo x19 x19) x19) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x1 x18 x19 = add_SNo (add_SNo x18 x18) x19) ⟶ (∀ x18 . x18 ∈ int ⟶ x2 x18 = add_SNo x18 x18) ⟶ x3 = 1 ⟶ x4 = 2 ⟶ (∀ 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) (x6 (add_SNo x18 (minus_SNo 1)) x19 x20))) ⟶ (∀ x18 . x18 ∈ int ⟶ x7 x18 = x5 (x2 x18) x3 x4) ⟶ (∀ x18 . x18 ∈ int ⟶ x8 x18 = x7 x18) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x9 x18 x19 = mul_SNo 2 (add_SNo (mul_SNo x19 x19) (add_SNo x18 x18))) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x10 x18 x19 = add_SNo (add_SNo x19 x19) x19) ⟶ (∀ x18 . x18 ∈ int ⟶ x11 x18 = x18) ⟶ x12 = 1 ⟶ x13 = 2 ⟶ (∀ 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) (x15 (add_SNo x18 (minus_SNo 1)) x19 x20))) ⟶ (∀ x18 . x18 ∈ int ⟶ x16 x18 = x14 (x11 x18) x12 x13) ⟶ (∀ x18 . x18 ∈ int ⟶ x17 x18 = x16 x18) ⟶ ∀ x18 . x18 ∈ int ⟶ SNoLe 0 x18 ⟶ x8 x18 = x17 x18