Param int^int : ι
Param add_SNo^add_SNo : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Param minus_SNo^minus_SNo : ι → ι
Conjecture 80d00..^A16305 : ∀ 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 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ 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 ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 . x26 ∈ 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 ⟶ x0 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x1 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x2 x30 = add_SNo 1 (mul_SNo 2 (add_SNo x30 x30))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x3 x30 x31 = x31) ⟶ x4 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x5 x30 x31 = If_i (SNoLe x30 0) x31 (x2 (x5 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x6 x30 x31 = x5 (x3 x30 x31) x4) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x7 x30 x31 = add_SNo (add_SNo (add_SNo (x6 x30 x31) x30) x30) x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x8 x30 = x30) ⟶ x9 = 1 ⟶ (∀ 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 . x30 ∈ int ⟶ x11 x30 = x10 (x8 x30) x9) ⟶ (∀ x30 . x30 ∈ int ⟶ x12 x30 = x11 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x13 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 (x1 x30) (x12 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x15 x30 = x14 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x16 x30 x31 = add_SNo (mul_SNo 2 (add_SNo x30 x30)) x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x17 x30 x31 = add_SNo 1 (add_SNo (add_SNo x31 x31) x31)) ⟶ (∀ x30 . x30 ∈ int ⟶ x18 x30 = x30) ⟶ x19 = 1 ⟶ x20 = add_SNo 2 2 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ x23 x30 = x21 (x18 x30) x19 x20) ⟶ (∀ x30 . x30 ∈ int ⟶ x24 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x25 x30 = x30) ⟶ x26 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x28 x30 = x27 (x25 x30) x26) ⟶ (∀ x30 . x30 ∈ int ⟶ x29 x30 = mul_SNo (x23 x30) (x28 x30)) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x15 x30 = x29 x30
Conjecture 8ed32..^A16302 : ∀ 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 ⟶ 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 ⟶ ∀ 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 ⟶ ∀ 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 = mul_SNo (add_SNo 2 x44) x43) ⟶ x1 = 2 ⟶ (∀ x43 . x43 ∈ int ⟶ x2 x43 = x43) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x3 x43 x44 = If_i (SNoLe x43 0) x44 (x0 (x3 (add_SNo x43 (minus_SNo 1)) x44) x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ x4 x43 = x3 x1 (x2 x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x5 x43 x44 = add_SNo (x4 x43) x44) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x6 x43 x44 = add_SNo x44 x44) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x7 x43 x44 = x44) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x10 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x5 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x11 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x6 (x10 (add_SNo x43 (minus_SNo 1)) x44 x45) (x11 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x12 x43 x44 = x10 (x7 x43 x44) x8 x9) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x13 x43 x44 = add_SNo (add_SNo (x12 x43 x44) (mul_SNo 2 (add_SNo x43 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 ⟶ x19 x43 = add_SNo x43 x43) ⟶ (∀ x43 . x43 ∈ int ⟶ x20 x43 = x43) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x21 x43 x44 = add_SNo 1 (mul_SNo x43 x44)) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x22 x43 x44 = x44) ⟶ (∀ x43 . x43 ∈ int ⟶ x23 x43 = x43) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x26 x43 x44 x45 = If_i (SNoLe x43 0) x44 (x21 (x26 (add_SNo x43 (minus_SNo 1)) x44 x45) (x27 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x27 x43 x44 x45 = If_i (SNoLe x43 0) x45 (x22 (x26 (add_SNo x43 (minus_SNo 1)) x44 x45) (x27 (add_SNo x43 (minus_SNo 1)) x44 x45))) ⟶ (∀ x43 . x43 ∈ int ⟶ x28 x43 = x26 (x23 x43) x24 x25) ⟶ (∀ x43 . x43 ∈ int ⟶ x29 x43 = x28 x43) ⟶ (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x30 x43 x44 = If_i (SNoLe x43 0) x44 (x19 (x30 (add_SNo x43 (minus_SNo 1)) x44))) ⟶ (∀ x43 . x43 ∈ int ⟶ x31 x43 = x30 (x20 x43) (x29 x43)) ⟶ (∀ x43 . x43 ∈ int ⟶ x32 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) (mul_SNo 2 (add_SNo x43 x43))) x43) ⟶ (∀ 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 e704f..^A16299 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ∈ int ⟶ x3 x4 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ 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 ⟶ ∀ 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 ⟶ 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 ⟶ ∀ x28 . x28 ∈ int ⟶ x26 x27 x28 ∈ int) ⟶ ∀ x27 : ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 : ι → ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x31 x32 x33 x34 ∈ int) ⟶ ∀ x32 : ι → ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x32 x33 x34 x35 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 : ι → ι . (∀ x35 . x35 ∈ int ⟶ x34 x35 ∈ int) ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 : ι → ι → ι . (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x36 x37 x38 ∈ int) ⟶ ∀ x37 : ι → ι → ι . (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x37 x38 x39 ∈ int) ⟶ ∀ x38 : ι → ι → ι . (∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x38 x39 x40 ∈ int) ⟶ ∀ x39 : ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ x39 x40 x41 ∈ int) ⟶ ∀ x40 : ι → ι . (∀ x41 . x41 ∈ int ⟶ x40 x41 ∈ int) ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 : ι → ι → ι . (∀ x43 . x43 ∈ int ⟶ ∀ x44 . x44 ∈ int ⟶ x42 x43 x44 ∈ int) ⟶ ∀ x43 : ι → ι . (∀ x44 . x44 ∈ int ⟶ x43 x44 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ (∀ x45 . x45 ∈ int ⟶ x0 x45 = add_SNo (mul_SNo 2 (add_SNo x45 x45)) x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x1 x45 = x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x2 x45 = add_SNo x45 x45) ⟶ (∀ x45 . x45 ∈ int ⟶ x3 x45 = x45) ⟶ x4 = 2 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x5 x45 x46 = If_i (SNoLe x45 0) x46 (x2 (x5 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x6 x45 = x5 (x3 x45) x4) ⟶ (∀ x45 . x45 ∈ int ⟶ x7 x45 = add_SNo (x6 x45) (minus_SNo 1)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x8 x45 x46 = If_i (SNoLe x45 0) x46 (x0 (x8 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ x9 x45 = x8 (x1 x45) (x7 x45)) ⟶ (∀ x45 . x45 ∈ int ⟶ x10 x45 = x9 x45) ⟶ x11 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x12 x45 x46 = x46) ⟶ (∀ 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 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x14 x45 x46 = x13 x11 (x12 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x15 x45 x46 = add_SNo (add_SNo (x14 x45 x46) 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 . x45 ∈ int ⟶ x19 x45 = x18 (x16 x45) x17) ⟶ (∀ x45 . x45 ∈ int ⟶ x20 x45 = x19 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 ⟶ ∀ x46 . x46 ∈ int ⟶ x26 x45 x46 = mul_SNo x45 x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x27 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ x28 x45 = x45) ⟶ x29 = 1 ⟶ x30 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x31 x45 x46 x47 = If_i (SNoLe x45 0) x46 (x26 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x32 x45 x46 x47 = If_i (SNoLe x45 0) x47 (x27 (x31 (add_SNo x45 (minus_SNo 1)) x46 x47) (x32 (add_SNo x45 (minus_SNo 1)) x46 x47))) ⟶ (∀ x45 . x45 ∈ int ⟶ x33 x45 = x31 (x28 x45) x29 x30) ⟶ (∀ x45 . x45 ∈ int ⟶ x34 x45 = mul_SNo (add_SNo (x25 x45) (minus_SNo 1)) (x33 x45)) ⟶ x35 = 1 ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x36 x45 x46 = x46) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x37 x45 x46 = If_i (SNoLe x45 0) x46 (x34 (x37 (add_SNo x45 (minus_SNo 1)) x46))) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x38 x45 x46 = x37 x35 (x36 x45 x46)) ⟶ (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ x39 x45 x46 = add_SNo (add_SNo (x38 x45 x46) 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 ⟶ x20 x45 = x44 x45
Conjecture bd38e..^A16294 : ∀ 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 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ 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 ⟶ 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 ⟶ x27 x28 ∈ int) ⟶ ∀ x28 . x28 ∈ 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 ⟶ x0 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x1 x32 = x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x2 x32 = add_SNo 1 (mul_SNo 2 (add_SNo (add_SNo x32 x32) x32))) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x3 x32 x33 = x33) ⟶ x4 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x5 x32 x33 = If_i (SNoLe x32 0) x33 (x2 (x5 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x6 x32 x33 = x5 (x3 x32 x33) x4) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x7 x32 x33 = add_SNo (add_SNo (x6 x32 x33) x32) x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x8 x32 = x32) ⟶ x9 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x10 x32 x33 = If_i (SNoLe x32 0) x33 (x7 (x10 (add_SNo x32 (minus_SNo 1)) x33) x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ x11 x32 = x10 (x8 x32) x9) ⟶ (∀ x32 . x32 ∈ int ⟶ x12 x32 = x11 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x13 x32 x33 = If_i (SNoLe x32 0) x33 (x0 (x13 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x14 x32 = x13 (x1 x32) (x12 x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ x15 x32 = x14 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x16 x32 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x32 x32) x32)) (minus_SNo 1)) ⟶ (∀ x32 . x32 ∈ int ⟶ x17 x32 = x32) ⟶ x18 = 2 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x19 x32 x33 = If_i (SNoLe x32 0) x33 (x16 (x19 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x20 x32 = x19 (x17 x32) x18) ⟶ (∀ x32 . x32 ∈ int ⟶ x21 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x22 x32 = x32) ⟶ x23 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x24 x32 x33 = If_i (SNoLe x32 0) x33 (x21 (x24 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x25 x32 = x24 (x22 x32) x23) ⟶ (∀ x32 . x32 ∈ int ⟶ x26 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x27 x32 = x32) ⟶ x28 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x29 x32 x33 = If_i (SNoLe x32 0) x33 (x26 (x29 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x30 x32 = x29 (x27 x32) x28) ⟶ (∀ x32 . x32 ∈ int ⟶ x31 x32 = mul_SNo (add_SNo (x20 x32) (minus_SNo (x25 x32))) (x30 x32)) ⟶ ∀ x32 . x32 ∈ int ⟶ SNoLe 0 x32 ⟶ x15 x32 = x31 x32
Conjecture e16bf..^A16293 : ∀ 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 (mul_SNo 2 (add_SNo (add_SNo (mul_SNo 2 (add_SNo x18 x18)) (mul_SNo x19 x19)) x18)) (minus_SNo x19)) x18) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x1 x18 x19 = add_SNo x19 x19) ⟶ (∀ x18 . x18 ∈ int ⟶ x2 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 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo (mul_SNo x19 x19) x18) (mul_SNo 2 (add_SNo x18 x18)))) (minus_SNo x19)) x18) ⟶ (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x10 x18 x19 = add_SNo 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
Conjecture 9252c..^A16292 : ∀ 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 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ 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 ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 . x26 ∈ 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 ⟶ x0 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x1 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x2 x30 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x30 x30)) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x3 x30 x31 = x31) ⟶ x4 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x5 x30 x31 = If_i (SNoLe x30 0) x31 (x2 (x5 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x6 x30 x31 = x5 (x3 x30 x31) x4) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x7 x30 x31 = add_SNo (add_SNo (x6 x30 x31) x30) x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x8 x30 = x30) ⟶ x9 = 1 ⟶ (∀ 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 . x30 ∈ int ⟶ x11 x30 = x10 (x8 x30) x9) ⟶ (∀ x30 . x30 ∈ int ⟶ x12 x30 = x11 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x0 (x13 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 (x1 x30) (x12 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x15 x30 = x14 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x16 x30 x31 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (add_SNo x30 x30) x31)) (minus_SNo 1)) x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x17 x30 x31 = add_SNo x31 x31) ⟶ (∀ x30 . x30 ∈ int ⟶ x18 x30 = x30) ⟶ x19 = 1 ⟶ x20 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ x23 x30 = x21 (x18 x30) x19 x20) ⟶ (∀ x30 . x30 ∈ int ⟶ x24 x30 = add_SNo x30 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ x25 x30 = x30) ⟶ x26 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ x28 x30 = x27 (x25 x30) x26) ⟶ (∀ x30 . x30 ∈ int ⟶ x29 x30 = mul_SNo (x23 x30) (x28 x30)) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x15 x30 = x29 x30
Conjecture b437c..^A16281 : ∀ 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 ⟶ 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 ⟶ ∀ x29 . x29 ∈ int ⟶ x27 x28 x29 ∈ int) ⟶ ∀ x28 : ι → ι → ι . (∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x28 x29 x30 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 : ι → ι → ι → ι . (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x32 x33 x34 x35 ∈ int) ⟶ ∀ x33 : ι → ι → ι → ι . (∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x33 x34 x35 x36 ∈ int) ⟶ ∀ x34 : ι → ι . (∀ x35 . x35 ∈ int ⟶ x34 x35 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x0 x36 x37 = mul_SNo (add_SNo 2 x37) x36) ⟶ x1 = 2 ⟶ (∀ x36 . x36 ∈ int ⟶ x2 x36 = x36) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x3 x36 x37 = If_i (SNoLe x36 0) x37 (x0 (x3 (add_SNo x36 (minus_SNo 1)) x37) x36)) ⟶ (∀ x36 . x36 ∈ int ⟶ x4 x36 = x3 x1 (x2 x36)) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x5 x36 x37 = add_SNo (x4 x36) x37) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x6 x36 x37 = add_SNo x37 x37) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x7 x36 x37 = x37) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x10 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x5 (x10 (add_SNo x36 (minus_SNo 1)) x37 x38) (x11 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x11 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x6 (x10 (add_SNo x36 (minus_SNo 1)) x37 x38) (x11 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x12 x36 x37 = x10 (x7 x36 x37) x8 x9) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x13 x36 x37 = add_SNo (add_SNo (add_SNo (x12 x36 x37) x36) x36) x36) ⟶ (∀ x36 . x36 ∈ int ⟶ x14 x36 = x36) ⟶ x15 = 1 ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x16 x36 x37 = If_i (SNoLe x36 0) x37 (x13 (x16 (add_SNo x36 (minus_SNo 1)) x37) x36)) ⟶ (∀ x36 . x36 ∈ int ⟶ x17 x36 = x16 (x14 x36) x15) ⟶ (∀ x36 . x36 ∈ int ⟶ x18 x36 = x17 x36) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x19 x36 x37 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo (add_SNo x36 x36) x36)) (minus_SNo x37))) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x20 x36 x37 = add_SNo x37 x37) ⟶ (∀ x36 . x36 ∈ int ⟶ x21 x36 = x36) ⟶ x22 = 2 ⟶ x23 = 2 ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x24 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x19 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38) (x25 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x25 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x20 (x24 (add_SNo x36 (minus_SNo 1)) x37 x38) (x25 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ x26 x36 = x24 (x21 x36) x22 x23) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x27 x36 x37 = mul_SNo x36 x37) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x28 x36 x37 = x37) ⟶ (∀ x36 . x36 ∈ int ⟶ x29 x36 = x36) ⟶ x30 = 1 ⟶ x31 = add_SNo 1 2 ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x32 x36 x37 x38 = If_i (SNoLe x36 0) x37 (x27 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38) (x33 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x33 x36 x37 x38 = If_i (SNoLe x36 0) x38 (x28 (x32 (add_SNo x36 (minus_SNo 1)) x37 x38) (x33 (add_SNo x36 (minus_SNo 1)) x37 x38))) ⟶ (∀ x36 . x36 ∈ int ⟶ x34 x36 = x32 (x29 x36) x30 x31) ⟶ (∀ x36 . x36 ∈ int ⟶ x35 x36 = add_SNo (x26 x36) (minus_SNo (x34 x36))) ⟶ ∀ x36 . x36 ∈ int ⟶ SNoLe 0 x36 ⟶ x18 x36 = x35 x36
Conjecture 26b77..^A16268 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ 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 ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ 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 ⟶ ∀ x30 . x30 ∈ int ⟶ x28 x29 x30 ∈ int) ⟶ ∀ x29 : ι → ι → ι . (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x29 x30 x31 ∈ 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 . x36 ∈ int ⟶ x0 x35 x36 = mul_SNo (add_SNo 2 x36) x35) ⟶ x1 = 2 ⟶ (∀ x35 . x35 ∈ int ⟶ x2 x35 = x35) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x3 x35 x36 = If_i (SNoLe x35 0) x36 (x0 (x3 (add_SNo x35 (minus_SNo 1)) x36) x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x4 x35 = x3 x1 (x2 x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x5 x35 = add_SNo 1 (x4 x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x6 x35 x36 = x36) ⟶ x7 = 1 ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x8 x35 x36 = If_i (SNoLe x35 0) x36 (x5 (x8 (add_SNo x35 (minus_SNo 1)) x36))) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x9 x35 x36 = x8 (x6 x35 x36) x7) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x10 x35 x36 = mul_SNo (add_SNo 2 x36) x35) ⟶ x11 = 2 ⟶ (∀ x35 . x35 ∈ int ⟶ x12 x35 = x35) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x13 x35 x36 = If_i (SNoLe x35 0) x36 (x10 (x13 (add_SNo x35 (minus_SNo 1)) x36) x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x14 x35 = x13 x11 (x12 x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x15 x35 x36 = add_SNo (add_SNo (x9 x35 x36) (minus_SNo x35)) (x14 x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x16 x35 = x35) ⟶ x17 = 1 ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x18 x35 x36 = If_i (SNoLe x35 0) x36 (x15 (x18 (add_SNo x35 (minus_SNo 1)) x36) x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x19 x35 = x18 (x16 x35) x17) ⟶ (∀ x35 . x35 ∈ int ⟶ x20 x35 = x19 x35) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x21 x35 x36 = add_SNo 1 (mul_SNo x35 x36)) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x22 x35 x36 = x36) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x23 x35 x36 = x36) ⟶ x24 = 1 ⟶ x25 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2)) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x26 x35 x36 x37 = If_i (SNoLe x35 0) x36 (x21 (x26 (add_SNo x35 (minus_SNo 1)) x36 x37) (x27 (add_SNo x35 (minus_SNo 1)) x36 x37))) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ ∀ x37 . x37 ∈ int ⟶ x27 x35 x36 x37 = If_i (SNoLe x35 0) x37 (x22 (x26 (add_SNo x35 (minus_SNo 1)) x36 x37) (x27 (add_SNo x35 (minus_SNo 1)) x36 x37))) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x28 x35 x36 = x26 (x23 x35 x36) x24 x25) ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x29 x35 x36 = add_SNo (add_SNo (x28 x35 x36) (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x35 x35)) x35))) x35) ⟶ (∀ x35 . x35 ∈ int ⟶ x30 x35 = x35) ⟶ x31 = 1 ⟶ (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x32 x35 x36 = If_i (SNoLe x35 0) x36 (x29 (x32 (add_SNo x35 (minus_SNo 1)) x36) x35)) ⟶ (∀ x35 . x35 ∈ int ⟶ x33 x35 = x32 (x30 x35) x31) ⟶ (∀ x35 . x35 ∈ int ⟶ x34 x35 = x33 x35) ⟶ ∀ x35 . x35 ∈ int ⟶ SNoLe 0 x35 ⟶ x20 x35 = x34 x35
Conjecture aa994..^A16267 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x23 x24 x25 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x24 x25 x26 ∈ int) ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 . x26 ∈ 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 ⟶ x0 x30 = add_SNo 1 (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x30 x30)) x30))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x1 x30 x31 = x31) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x5 x30 x31 = mul_SNo (add_SNo 2 x31) x30) ⟶ x6 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ x7 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x9 x30 = x8 x6 (x7 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x10 x30 x31 = add_SNo (x4 x30 x31) (x9 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x11 x30 = x30) ⟶ x12 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 (x11 x30) x12) ⟶ (∀ x30 . x30 ∈ int ⟶ x15 x30 = x14 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x16 x30 x31 = add_SNo 1 (mul_SNo x30 x31)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x17 x30 x31 = x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x18 x30 x31 = x31) ⟶ x19 = 1 ⟶ x20 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x21 x30 x31 x32 = If_i (SNoLe x30 0) x31 (x16 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ ∀ x32 . x32 ∈ int ⟶ x22 x30 x31 x32 = If_i (SNoLe x30 0) x32 (x17 (x21 (add_SNo x30 (minus_SNo 1)) x31 x32) (x22 (add_SNo x30 (minus_SNo 1)) x31 x32))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x23 x30 x31 = x21 (x18 x30 x31) x19 x20) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x24 x30 x31 = add_SNo (x23 x30 x31) (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x30 x30) x30)))) ⟶ (∀ x30 . x30 ∈ int ⟶ x25 x30 = x30) ⟶ x26 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x27 x30 x31 = If_i (SNoLe x30 0) x31 (x24 (x27 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x28 x30 = x27 (x25 x30) x26) ⟶ (∀ x30 . x30 ∈ int ⟶ x29 x30 = x28 x30) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x15 x30 = x29 x30
Conjecture e15d0..^A162670 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x10 x11 x12 x13 ∈ int) ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ 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 ⟶ x0 x28 = add_SNo 1 (mul_SNo (add_SNo 2 x28) x28)) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x3 x28 x29 = If_i (SNoLe x28 0) x29 (x0 (x3 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x5 x28 x29 = add_SNo (mul_SNo x4 x29) x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x6 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x7 x28 = x28) ⟶ x8 = 1 ⟶ x9 = 0 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x10 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x5 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30) (x11 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x11 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x6 (x10 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ x12 x28 = x10 (x7 x28) x8 x9) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = x12 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x14 x28 = mul_SNo x28 x28) ⟶ x15 = 1 ⟶ x16 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x17 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x17 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ x18 = x17 x15 x16 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x19 x28 x29 = add_SNo (mul_SNo x18 x29) x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x20 x28 = x28) ⟶ (∀ x28 . x28 ∈ int ⟶ x21 x28 = add_SNo x28 (minus_SNo 1)) ⟶ x22 = 1 ⟶ x23 = 1 ⟶ (∀ 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))) ⟶ (∀ x28 . x28 ∈ int ⟶ x26 x28 = x24 (x21 x28) x22 x23) ⟶ (∀ x28 . x28 ∈ int ⟶ x27 x28 = x26 x28) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x13 x28 = x27 x28
Conjecture 6ec93..^A162666 : ∀ 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 ⟶ x7 x8 ∈ int) ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x10 x11 x12 x13 ∈ int) ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x20 x21 x22 x23 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x0 x23 x24 = mul_SNo (add_SNo 2 x24) x23) ⟶ x1 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x3 x23 x24 = If_i (SNoLe x23 0) x24 (x0 (x3 (add_SNo x23 (minus_SNo 1)) x24) x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x4 x23 = x3 x1 (x2 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x5 x23 x24 = add_SNo (x4 x23) (minus_SNo x24)) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x6 x23 x24 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x24 x24)) x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x7 x23 = x23) ⟶ x8 = 1 ⟶ x9 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x5 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x6 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x7 x23) x8 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo x23 x23))) x24) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x15 x23 x24 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo (add_SNo x24 x24) x24)) (minus_SNo x23))) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = x23) ⟶ x17 = 1 ⟶ x18 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x19 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x14 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x20 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x15 (x19 (add_SNo x23 (minus_SNo 1)) x24 x25) (x20 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x21 x23 = x19 (x16 x23) x17 x18) ⟶ (∀ x23 . x23 ∈ int ⟶ x22 x23 = x21 x23) ⟶ ∀ x23 . x23 ∈ int ⟶ SNoLe 0 x23 ⟶ x13 x23 = x22 x23
Conjecture 30f35..^A16263 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ (∀ x30 . x30 ∈ int ⟶ x0 x30 = add_SNo (add_SNo x30 x30) x30) ⟶ x1 = 2 ⟶ (∀ 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 ⟶ x4 x30 = x3 x1 (x2 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x5 x30 = add_SNo 1 (x4 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x6 x30 x31 = x31) ⟶ x7 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x9 x30 x31 = x8 (x6 x30 x31) x7) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x10 x30 x31 = mul_SNo (add_SNo 2 x31) x30) ⟶ x11 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ x12 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 x11 (x12 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x15 x30 x31 = add_SNo (x9 x30 x31) (x14 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x16 x30 = x30) ⟶ x17 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x18 x30 x31 = If_i (SNoLe x30 0) x31 (x15 (x18 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x19 x30 = x18 (x16 x30) x17) ⟶ (∀ x30 . x30 ∈ int ⟶ x20 x30 = x19 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x21 x30 x31 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x30 x30) x30))) x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x22 x30 x31 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo (add_SNo (add_SNo x31 x31) x31) x31)) x31)) ⟶ (∀ x30 . x30 ∈ int ⟶ x23 x30 = x30) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 (mul_SNo 2 (add_SNo 2 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 = x28 x30) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x20 x30 = x29 x30
Conjecture 81f02..^A16262 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι → ι . (∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x15 x16 x17 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x18 x19 x20 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x21 x22 x23 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι → ι . (∀ x27 . x27 ∈ int ⟶ ∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x26 x27 x28 x29 ∈ int) ⟶ ∀ x27 : ι → ι → ι → ι . (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x27 x28 x29 x30 ∈ int) ⟶ ∀ x28 : ι → ι . (∀ x29 . x29 ∈ int ⟶ x28 x29 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ (∀ x30 . x30 ∈ int ⟶ x0 x30 = add_SNo (add_SNo x30 x30) x30) ⟶ x1 = 2 ⟶ (∀ 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 ⟶ x4 x30 = x3 x1 (x2 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x5 x30 = add_SNo 1 (x4 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x6 x30 x31 = x31) ⟶ x7 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x8 x30 x31 = If_i (SNoLe x30 0) x31 (x5 (x8 (add_SNo x30 (minus_SNo 1)) x31))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x9 x30 x31 = x8 (x6 x30 x31) x7) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x10 x30 x31 = mul_SNo (add_SNo 2 x31) x30) ⟶ x11 = 2 ⟶ (∀ x30 . x30 ∈ int ⟶ x12 x30 = x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x13 x30 x31 = If_i (SNoLe x30 0) x31 (x10 (x13 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x14 x30 = x13 x11 (x12 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x15 x30 x31 = add_SNo (add_SNo (x9 x30 x31) (minus_SNo x30)) (x14 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x16 x30 = x30) ⟶ x17 = 1 ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x18 x30 x31 = If_i (SNoLe x30 0) x31 (x15 (x18 (add_SNo x30 (minus_SNo 1)) x31) x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x19 x30 = x18 (x16 x30) x17) ⟶ (∀ x30 . x30 ∈ int ⟶ x20 x30 = x19 x30) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x21 x30 x31 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x30 x30)) x30)) x30) x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x22 x30 x31 = add_SNo (add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo x31 x31))) x31) 1) ⟶ (∀ x30 . x30 ∈ int ⟶ x23 x30 = x30) ⟶ x24 = 1 ⟶ x25 = add_SNo (mul_SNo (add_SNo 2 2) 2) 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 = x28 x30) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x20 x30 = x29 x30
Conjecture 85db5..^A16260 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x25 x25)))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = x26) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x5 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x6 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x7 x25 = x25) ⟶ (∀ 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 (x7 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x10 x25 x26 = add_SNo (x4 x25 x26) (x9 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = If_i (SNoLe x25 0) x26 (x10 (x13 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = x13 (x11 x25) x12) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x14 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x16 x25 x26 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))) x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x17 x25 x26 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x26 x26)))) ⟶ (∀ x25 . x25 ∈ int ⟶ x18 x25 = x25) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x21 (x18 x25) x19 x20) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x15 x25 = x24 x25
Conjecture 2deba..^A16256 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x25 x25)))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = x26) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ x5 x25 = add_SNo (add_SNo x25 x25) x25) ⟶ x6 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x7 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x8 x25 x26 = If_i (SNoLe x25 0) x26 (x5 (x8 (add_SNo x25 (minus_SNo 1)) x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x9 x25 = x8 x6 (x7 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x10 x25 x26 = add_SNo (x4 x25 x26) (x9 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = If_i (SNoLe x25 0) x26 (x10 (x13 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = x13 (x11 x25) x12) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x14 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x16 x25 x26 = add_SNo (mul_SNo (add_SNo 1 2) (add_SNo (add_SNo x25 x25) x25)) x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x17 x25 x26 = add_SNo 1 (mul_SNo 2 (mul_SNo 2 (add_SNo x26 x26)))) ⟶ (∀ x25 . x25 ∈ int ⟶ x18 x25 = x25) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x21 (x18 x25) x19 x20) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x15 x25 = x24 x25
Conjecture b80fd..^A162523 : ∀ 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 : ι → ι → ι . (∀ 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 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 : ι → ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x0 x25 x26 = add_SNo x26 (minus_SNo x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = add_SNo 2 (add_SNo x26 (minus_SNo x25))) ⟶ (∀ x25 . x25 ∈ int ⟶ x2 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x3 x25 x26 = If_i (SNoLe x25 0) x26 (x0 (x3 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ 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) x26) ⟶ (∀ 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 = add_SNo (add_SNo (x9 x25) 2) x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x11 x25 x26 = add_SNo 0 (minus_SNo (add_SNo x25 x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x12 x25 x26 = add_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x13 x25 = add_SNo x25 (minus_SNo 1)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = If_i (SNoLe x25 0) 1 2) ⟶ x15 = 1 ⟶ (∀ 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 x25) x15) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x19 x25 x26 = add_SNo x25 x26) ⟶ (∀ x25 . x25 ∈ int ⟶ x20 x25 = x25) ⟶ (∀ x25 . x25 ∈ int ⟶ x21 x25 = x25) ⟶ (∀ 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 . x25 ∈ int ⟶ x23 x25 = x22 (x20 x25) (x21 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = add_SNo (add_SNo (x18 x25) (x23 x25)) 2) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x10 x25 = x24 x25
Conjecture 555e3..^A16237 : ∀ 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 . x4 ∈ int ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ 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 ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 . x33 ∈ int ⟶ x0 x33 = add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x1 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x2 x33 = add_SNo 1 (add_SNo x33 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = x34) ⟶ x4 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x5 x33 x34 = If_i (SNoLe x33 0) x34 (x2 (x5 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x6 x33 x34 = x5 (x3 x33 x34) x4) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x7 x33 x34 = x6 x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x8 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x9 x33 x34 = x8 (x1 x33 x34) (x7 x33 x34)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x10 x33 x34 = add_SNo (x9 x33 x34) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x11 x33 = x33) ⟶ x12 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x13 x33 x34 = If_i (SNoLe x33 0) x34 (x10 (x13 (add_SNo x33 (minus_SNo 1)) x34) x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x14 x33 = x13 (x11 x33) x12) ⟶ (∀ x33 . x33 ∈ int ⟶ x15 x33 = x14 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x16 x33 x34 = add_SNo 2 (mul_SNo x33 x34)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x17 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = x33) ⟶ x19 = 2 ⟶ x20 = add_SNo 2 (mul_SNo 2 (add_SNo 2 2)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x21 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x16 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x22 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x17 (x21 (add_SNo x33 (minus_SNo 1)) x34 x35) (x22 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x23 x33 = x21 (x18 x33) x19 x20) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x24 x33 x34 = add_SNo 1 (mul_SNo x33 x34)) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x25 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x26 x33 = x33) ⟶ x27 = 1 ⟶ x28 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x29 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x24 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x30 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x25 (x29 (add_SNo x33 (minus_SNo 1)) x34 x35) (x30 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x31 x33 = x29 (x26 x33) x27 x28) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = add_SNo (x23 x33) (minus_SNo (x31 x33))) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x15 x33 = x32 x33
Conjecture 703b8..^A16227 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = add_SNo 1 (mul_SNo 2 (add_SNo x25 x25))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = x26) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x5 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x6 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x7 x25 = x25) ⟶ (∀ 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 (x7 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x10 x25 x26 = add_SNo (x4 x25 x26) (x9 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = If_i (SNoLe x25 0) x26 (x10 (x13 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = x13 (x11 x25) x12) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x14 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x16 x25 x26 = add_SNo (mul_SNo 2 (mul_SNo 2 (add_SNo (add_SNo x25 x25) x25))) x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x17 x25 x26 = add_SNo 1 (mul_SNo 2 (add_SNo x26 x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x18 x25 = x25) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x21 (x18 x25) x19 x20) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x15 x25 = x24 x25
Conjecture 5b0e3..^A16226 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 : ι → ι . (∀ x8 . x8 ∈ int ⟶ x7 x8 ∈ int) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ x10 x11 x12 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 : ι → ι → ι → ι . (∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x21 x22 x23 x24 ∈ int) ⟶ ∀ x22 : ι → ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x22 x23 x24 x25 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ (∀ x25 . x25 ∈ int ⟶ x0 x25 = add_SNo 1 (mul_SNo 2 (add_SNo x25 x25))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x1 x25 x26 = x26) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x5 x25 x26 = mul_SNo (add_SNo 2 x26) x25) ⟶ x6 = 2 ⟶ (∀ x25 . x25 ∈ int ⟶ x7 x25 = x25) ⟶ (∀ 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 (x7 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x10 x25 x26 = add_SNo (add_SNo (x4 x25 x26) (minus_SNo x25)) (x9 x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x11 x25 = x25) ⟶ x12 = 1 ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x13 x25 x26 = If_i (SNoLe x25 0) x26 (x10 (x13 (add_SNo x25 (minus_SNo 1)) x26) x25)) ⟶ (∀ x25 . x25 ∈ int ⟶ x14 x25 = x13 (x11 x25) x12) ⟶ (∀ x25 . x25 ∈ int ⟶ x15 x25 = x14 x25) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x16 x25 x26 = add_SNo (add_SNo (mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x25 x25)) x25)) x25) x26) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x17 x25 x26 = add_SNo 1 (mul_SNo 2 (add_SNo x26 x26))) ⟶ (∀ x25 . x25 ∈ int ⟶ x18 x25 = x25) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x21 x25 x26 x27 = If_i (SNoLe x25 0) x26 (x16 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x22 x25 x26 x27 = If_i (SNoLe x25 0) x27 (x17 (x21 (add_SNo x25 (minus_SNo 1)) x26 x27) (x22 (add_SNo x25 (minus_SNo 1)) x26 x27))) ⟶ (∀ x25 . x25 ∈ int ⟶ x23 x25 = x21 (x18 x25) x19 x20) ⟶ (∀ x25 . x25 ∈ int ⟶ x24 x25 = x23 x25) ⟶ ∀ x25 . x25 ∈ int ⟶ SNoLe 0 x25 ⟶ x15 x25 = x24 x25
Conjecture 1ad85..^A16197 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι → ι . (∀ x11 . x11 ∈ int ⟶ ∀ 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 ⟶ 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 ⟶ ∀ 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 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x0 x38 x39 = mul_SNo (add_SNo 2 x39) x38) ⟶ x1 = 2 ⟶ (∀ x38 . x38 ∈ int ⟶ x2 x38 = x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x3 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x3 (add_SNo x38 (minus_SNo 1)) x39) x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x4 x38 = x3 x1 (x2 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x5 x38 = x4 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ x6 x38 = x38) ⟶ x7 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x8 x38 x39 = If_i (SNoLe x38 0) x39 (x5 (x8 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x9 x38 = x8 (x6 x38) x7) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x10 x38 x39 = mul_SNo (add_SNo 2 x39) x38) ⟶ x11 = 2 ⟶ (∀ x38 . x38 ∈ int ⟶ x12 x38 = x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x13 x38 x39 = If_i (SNoLe x38 0) x39 (x10 (x13 (add_SNo x38 (minus_SNo 1)) x39) x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x14 x38 = x13 x11 (x12 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x15 x38 = add_SNo (x14 x38) (minus_SNo x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x16 x38 = x38) ⟶ x17 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x18 x38 x39 = If_i (SNoLe x38 0) x39 (x15 (x18 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x19 x38 = x18 (x16 x38) x17) ⟶ (∀ x38 . x38 ∈ int ⟶ x20 x38 = add_SNo (x9 x38) (minus_SNo (x19 x38))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x21 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x22 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x23 x38 = x38) ⟶ x24 = 1 ⟶ x25 = mul_SNo 2 (add_SNo 2 (add_SNo 2 2)) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x26 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x21 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40) (x27 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x27 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x22 (x26 (add_SNo x38 (minus_SNo 1)) x39 x40) (x27 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x28 x38 = x26 (x23 x38) x24 x25) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x29 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x30 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x31 x38 = x38) ⟶ x32 = 1 ⟶ x33 = add_SNo 1 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x34 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x29 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x35 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x30 (x34 (add_SNo x38 (minus_SNo 1)) x39 x40) (x35 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x36 x38 = x34 (x31 x38) x32 x33) ⟶ (∀ x38 . x38 ∈ int ⟶ x37 x38 = add_SNo (x28 x38) (minus_SNo (x36 x38))) ⟶ ∀ x38 . x38 ∈ int ⟶ SNoLe 0 x38 ⟶ x20 x38 = x37 x38

Proofgold Address