Proofgold Asset

Param int^int : ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param SNoLe^SNoLe : ι → ι → ο
Param minus_SNo^minus_SNo : ι → ι
Conjecture df9be..^A139745 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ 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 ⟶ ∀ x34 . x34 ∈ int ⟶ x0 x33 x34 = mul_SNo (add_SNo 2 x34) x33) ⟶ x1 = 2 ⟶ (∀ x33 . x33 ∈ int ⟶ x2 x33 = x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34) x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x4 x33 = x3 x1 (x2 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x5 x33 = add_SNo (x4 x33) (minus_SNo x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x6 x33 = x33) ⟶ x7 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = If_i (SNoLe x33 0) x34 (x5 (x8 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x9 x33 = x8 (x6 x33) x7) ⟶ (∀ x33 . x33 ∈ int ⟶ x10 x33 = add_SNo (mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)) 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 ∈ int ⟶ x14 x33 = x13 (x11 x33) x12) ⟶ (∀ x33 . x33 ∈ int ⟶ x15 x33 = add_SNo (x9 x33) (minus_SNo (x14 x33))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x16 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x17 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = x33) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (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 = 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 (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 ce4d6..^A139740 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ 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 ⟶ ∀ x31 . x31 ∈ int ⟶ x0 x30 x31 = mul_SNo (add_SNo 2 x31) 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 . x30 ∈ int ⟶ x4 x30 = x3 x1 (x2 x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x5 x30 = add_SNo (x4 x30) (minus_SNo x30)) ⟶ (∀ x30 . x30 ∈ int ⟶ x6 x30 = x30) ⟶ 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 ⟶ x9 x30 = x8 (x6 x30) x7) ⟶ (∀ x30 . x30 ∈ int ⟶ x10 x30 = add_SNo x30 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 ∈ int ⟶ x14 x30 = x13 (x11 x30) x12) ⟶ (∀ x30 . x30 ∈ int ⟶ x15 x30 = add_SNo (x9 x30) (minus_SNo (x14 x30))) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x16 x30 x31 = mul_SNo x30 x31) ⟶ (∀ x30 . x30 ∈ int ⟶ ∀ x31 . x31 ∈ int ⟶ x17 x30 x31 = x31) ⟶ (∀ x30 . x30 ∈ int ⟶ x18 x30 = x30) ⟶ x19 = 1 ⟶ x20 = add_SNo 1 (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 ⟶ 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 = add_SNo (x23 x30) (minus_SNo (x28 x30))) ⟶ ∀ x30 . x30 ∈ int ⟶ SNoLe 0 x30 ⟶ x15 x30 = x29 x30
Conjecture c77d4..^A13897 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x36 x37 ∈ int) ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x39 x40 x41 x42 ∈ int) ⟶ ∀ x40 : ι → ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x40 x41 x42 x43 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ (∀ x46 . x46 ∈ int ⟶ x0 x46 = mul_SNo 2 (add_SNo 2 x46)) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x3 x46 x47 = If_i (SNoLe x46 0) x47 (x0 (x3 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x46 . x46 ∈ int ⟶ x5 x46 = mul_SNo x4 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x6 x46 = add_SNo (mul_SNo 2 (add_SNo 2 (add_SNo x46 x46))) x46) ⟶ x7 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x8 x46 x47 = If_i (SNoLe x46 0) x47 (x5 (x8 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x9 x46 = x8 (x6 x46) x7) ⟶ (∀ x46 . x46 ∈ int ⟶ x10 x46 = x9 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x11 x46 = mul_SNo x46 x46) ⟶ x12 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x13 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x14 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x15 x46 = x46) ⟶ x16 = 1 ⟶ x17 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x18 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x13 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x19 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x14 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x20 x46 = x18 (x15 x46) x16 x17) ⟶ (∀ x46 . x46 ∈ int ⟶ x21 x46 = x20 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x22 x46 x47 = If_i (SNoLe x46 0) x47 (x11 (x22 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x23 x46 = x22 x12 (x21 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x24 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x25 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x26 x46 = add_SNo 2 x46) ⟶ x27 = 1 ⟶ x28 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x29 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x24 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x30 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x25 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x31 x46 = x29 (x26 x46) x27 x28) ⟶ (∀ x46 . x46 ∈ int ⟶ x32 x46 = mul_SNo x46 x46) ⟶ x33 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x34 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x35 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x36 x46 = add_SNo 1 x46) ⟶ x37 = 1 ⟶ x38 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x39 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x34 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x40 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x35 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x41 x46 = x39 (x36 x46) x37 x38) ⟶ (∀ x46 . x46 ∈ int ⟶ x42 x46 = x41 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x43 x46 x47 = If_i (SNoLe x46 0) x47 (x32 (x43 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x44 x46 = x43 x33 (x42 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ x45 x46 = mul_SNo (mul_SNo (x23 x46) (x31 x46)) (x44 x46)) ⟶ ∀ x46 . x46 ∈ int ⟶ SNoLe 0 x46 ⟶ x10 x46 = x45 x46
Conjecture 68c4e..^A13896 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ 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 ⟶ ∀ 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 ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x23 x24 x25 x26 ∈ int) ⟶ ∀ x24 : ι → ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x24 x25 x26 x27 ∈ 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 ⟶ ∀ 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 : ι → ι → ι . (∀ 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 ⟶ x41 x42 ∈ int) ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ ∀ x44 : ι → ι → ι → ι . (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x44 x45 x46 x47 ∈ int) ⟶ ∀ x45 : ι → ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x45 x46 x47 x48 ∈ int) ⟶ ∀ x46 : ι → ι . (∀ x47 . x47 ∈ int ⟶ x46 x47 ∈ int) ⟶ ∀ x47 : ι → ι . (∀ x48 . x48 ∈ int ⟶ x47 x48 ∈ int) ⟶ ∀ x48 : ι → ι → ι . (∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x48 x49 x50 ∈ int) ⟶ ∀ x49 : ι → ι . (∀ x50 . x50 ∈ int ⟶ x49 x50 ∈ int) ⟶ ∀ x50 : ι → ι . (∀ x51 . x51 ∈ int ⟶ x50 x51 ∈ int) ⟶ (∀ x51 . x51 ∈ int ⟶ x0 x51 = mul_SNo 2 (add_SNo 2 x51)) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x3 x51 x52 = If_i (SNoLe x51 0) x52 (x0 (x3 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x51 . x51 ∈ int ⟶ x5 x51 = mul_SNo x4 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ x6 x51 = add_SNo 1 (add_SNo x51 x51)) ⟶ x7 = 2 ⟶ (∀ x51 . x51 ∈ int ⟶ x8 x51 = x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x9 x51 x52 = If_i (SNoLe x51 0) x52 (x6 (x9 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x10 x51 = x9 x7 (x8 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ x11 x51 = add_SNo (x10 x51) x51) ⟶ x12 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x13 x51 x52 = If_i (SNoLe x51 0) x52 (x5 (x13 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x14 x51 = x13 (x11 x51) x12) ⟶ (∀ x51 . x51 ∈ int ⟶ x15 x51 = x14 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ x16 x51 = mul_SNo x51 x51) ⟶ x17 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x18 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x19 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x20 x51 = x51) ⟶ x21 = 1 ⟶ x22 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x23 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x18 (x23 (add_SNo x51 (minus_SNo 1)) x52 x53) (x24 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x24 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x19 (x23 (add_SNo x51 (minus_SNo 1)) x52 x53) (x24 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x25 x51 = x23 (x20 x51) x21 x22) ⟶ (∀ x51 . x51 ∈ int ⟶ x26 x51 = x25 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x27 x51 x52 = If_i (SNoLe x51 0) x52 (x16 (x27 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x28 x51 = x27 x17 (x26 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x29 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x30 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x31 x51 = add_SNo 1 x51) ⟶ x32 = 1 ⟶ x33 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x34 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x29 (x34 (add_SNo x51 (minus_SNo 1)) x52 x53) (x35 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x35 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x30 (x34 (add_SNo x51 (minus_SNo 1)) x52 x53) (x35 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x36 x51 = x34 (x31 x51) x32 x33) ⟶ (∀ x51 . x51 ∈ int ⟶ x37 x51 = mul_SNo x51 x51) ⟶ x38 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x39 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x40 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x41 x51 = add_SNo 1 x51) ⟶ x42 = 1 ⟶ x43 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x44 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x39 (x44 (add_SNo x51 (minus_SNo 1)) x52 x53) (x45 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x45 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x40 (x44 (add_SNo x51 (minus_SNo 1)) x52 x53) (x45 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x46 x51 = x44 (x41 x51) x42 x43) ⟶ (∀ x51 . x51 ∈ int ⟶ x47 x51 = x46 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x48 x51 x52 = If_i (SNoLe x51 0) x52 (x37 (x48 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x49 x51 = x48 x38 (x47 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ x50 x51 = mul_SNo (mul_SNo (x28 x51) (x36 x51)) (x49 x51)) ⟶ ∀ x51 . x51 ∈ int ⟶ SNoLe 0 x51 ⟶ x15 x51 = x50 x51
Conjecture b6557..^A13895 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x36 x37 ∈ int) ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x39 x40 x41 x42 ∈ int) ⟶ ∀ x40 : ι → ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x40 x41 x42 x43 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ (∀ x46 . x46 ∈ int ⟶ x0 x46 = mul_SNo 2 (add_SNo 2 x46)) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x3 x46 x47 = If_i (SNoLe x46 0) x47 (x0 (x3 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x46 . x46 ∈ int ⟶ x5 x46 = mul_SNo x4 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x6 x46 = add_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x46 x46)) x46)) ⟶ x7 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x8 x46 x47 = If_i (SNoLe x46 0) x47 (x5 (x8 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x9 x46 = x8 (x6 x46) x7) ⟶ (∀ x46 . x46 ∈ int ⟶ x10 x46 = x9 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x11 x46 = mul_SNo x46 x46) ⟶ x12 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x13 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x14 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x15 x46 = x46) ⟶ x16 = 1 ⟶ x17 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x18 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x13 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x19 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x14 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x20 x46 = x18 (x15 x46) x16 x17) ⟶ (∀ x46 . x46 ∈ int ⟶ x21 x46 = x20 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x22 x46 x47 = If_i (SNoLe x46 0) x47 (x11 (x22 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x23 x46 = x22 x12 (x21 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x24 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x25 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x26 x46 = add_SNo 2 x46) ⟶ x27 = 1 ⟶ x28 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x29 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x24 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x30 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x25 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x31 x46 = x29 (x26 x46) x27 x28) ⟶ (∀ x46 . x46 ∈ int ⟶ x32 x46 = mul_SNo x46 x46) ⟶ x33 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x34 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x35 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x36 x46 = x46) ⟶ x37 = 1 ⟶ x38 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x39 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x34 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x40 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x35 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x41 x46 = x39 (x36 x46) x37 x38) ⟶ (∀ x46 . x46 ∈ int ⟶ x42 x46 = x41 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x43 x46 x47 = If_i (SNoLe x46 0) x47 (x32 (x43 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x44 x46 = x43 x33 (x42 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ x45 x46 = mul_SNo (mul_SNo (x23 x46) (x31 x46)) (x44 x46)) ⟶ ∀ x46 . x46 ∈ int ⟶ SNoLe 0 x46 ⟶ x10 x46 = x45 x46
Conjecture 4ddb0..^A13894 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x36 x37 ∈ int) ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x39 x40 x41 x42 ∈ int) ⟶ ∀ x40 : ι → ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x40 x41 x42 x43 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ (∀ x46 . x46 ∈ int ⟶ x0 x46 = mul_SNo 2 (add_SNo 2 x46)) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x3 x46 x47 = If_i (SNoLe x46 0) x47 (x0 (x3 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x46 . x46 ∈ int ⟶ x5 x46 = mul_SNo x4 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x6 x46 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x46 x46)) x46)) ⟶ x7 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x8 x46 x47 = If_i (SNoLe x46 0) x47 (x5 (x8 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x9 x46 = x8 (x6 x46) x7) ⟶ (∀ x46 . x46 ∈ int ⟶ x10 x46 = x9 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x11 x46 = mul_SNo x46 x46) ⟶ x12 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x13 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x14 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x15 x46 = x46) ⟶ x16 = 1 ⟶ x17 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x18 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x13 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x19 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x14 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x20 x46 = x18 (x15 x46) x16 x17) ⟶ (∀ x46 . x46 ∈ int ⟶ x21 x46 = x20 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x22 x46 x47 = If_i (SNoLe x46 0) x47 (x11 (x22 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x23 x46 = x22 x12 (x21 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x24 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x25 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x26 x46 = add_SNo 1 x46) ⟶ x27 = 1 ⟶ x28 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x29 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x24 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x30 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x25 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x31 x46 = x29 (x26 x46) x27 x28) ⟶ (∀ x46 . x46 ∈ int ⟶ x32 x46 = mul_SNo x46 x46) ⟶ x33 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x34 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x35 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x36 x46 = x46) ⟶ x37 = 1 ⟶ x38 = mul_SNo 2 (add_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x39 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x34 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x40 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x35 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x41 x46 = x39 (x36 x46) x37 x38) ⟶ (∀ x46 . x46 ∈ int ⟶ x42 x46 = x41 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x43 x46 x47 = If_i (SNoLe x46 0) x47 (x32 (x43 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x44 x46 = x43 x33 (x42 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ x45 x46 = mul_SNo (mul_SNo (x23 x46) (x31 x46)) (x44 x46)) ⟶ ∀ x46 . x46 ∈ int ⟶ SNoLe 0 x46 ⟶ x10 x46 = x45 x46
Conjecture 1f9f9..^A13873 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ (∀ x38 . x38 ∈ int ⟶ x0 x38 = mul_SNo x38 x38) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x3 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x3 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x38 . x38 ∈ int ⟶ x5 x38 = mul_SNo (add_SNo x4 (minus_SNo 2)) x38) ⟶ (∀ x38 . x38 ∈ int ⟶ x6 x38 = add_SNo (mul_SNo 2 (add_SNo 2 (add_SNo x38 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 ⟶ x10 x38 = x9 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ x11 x38 = mul_SNo (mul_SNo x38 x38) x38) ⟶ x12 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x13 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x14 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x15 x38 = x38) ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x18 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x13 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x19 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x14 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x20 x38 = x18 (x15 x38) x16 x17) ⟶ (∀ x38 . x38 ∈ int ⟶ x21 x38 = x20 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x22 x38 x39 = If_i (SNoLe x38 0) x39 (x11 (x22 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x23 x38 = x22 x12 (x21 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x24 x38 = mul_SNo x38 x38) ⟶ x25 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x26 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x27 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x28 x38 = add_SNo 2 x38) ⟶ x29 = 1 ⟶ x30 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x31 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x26 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x32 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x27 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x33 x38 = x31 (x28 x38) x29 x30) ⟶ (∀ x38 . x38 ∈ int ⟶ x34 x38 = x33 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x35 x38 x39 = If_i (SNoLe x38 0) x39 (x24 (x35 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x36 x38 = x35 x25 (x34 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x37 x38 = mul_SNo (x23 x38) (x36 x38)) ⟶ ∀ x38 . x38 ∈ int ⟶ SNoLe 0 x38 ⟶ x10 x38 = x37 x38
Conjecture 24e20..^A13872 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ 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 ⟶ ∀ 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 ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι → ι → ι . (∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ x23 x24 x25 x26 ∈ int) ⟶ ∀ x24 : ι → ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ x26 . x26 ∈ int ⟶ ∀ x27 . x27 ∈ int ⟶ x24 x25 x26 x27 ∈ 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 ⟶ ∀ 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 : ι → ι → ι . (∀ 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 ⟶ x41 x42 ∈ int) ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ ∀ x44 : ι → ι → ι → ι . (∀ x45 . x45 ∈ int ⟶ ∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x44 x45 x46 x47 ∈ int) ⟶ ∀ x45 : ι → ι → ι → ι . (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x45 x46 x47 x48 ∈ int) ⟶ ∀ x46 : ι → ι . (∀ x47 . x47 ∈ int ⟶ x46 x47 ∈ int) ⟶ ∀ x47 : ι → ι . (∀ x48 . x48 ∈ int ⟶ x47 x48 ∈ int) ⟶ ∀ x48 : ι → ι → ι . (∀ x49 . x49 ∈ int ⟶ ∀ x50 . x50 ∈ int ⟶ x48 x49 x50 ∈ int) ⟶ ∀ x49 : ι → ι . (∀ x50 . x50 ∈ int ⟶ x49 x50 ∈ int) ⟶ ∀ x50 : ι → ι . (∀ x51 . x51 ∈ int ⟶ x50 x51 ∈ int) ⟶ (∀ x51 . x51 ∈ int ⟶ x0 x51 = mul_SNo x51 x51) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x3 x51 x52 = If_i (SNoLe x51 0) x52 (x0 (x3 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x51 . x51 ∈ int ⟶ x5 x51 = mul_SNo (add_SNo x4 (minus_SNo 2)) x51) ⟶ (∀ x51 . x51 ∈ int ⟶ x6 x51 = add_SNo 1 (add_SNo x51 x51)) ⟶ x7 = 2 ⟶ (∀ x51 . x51 ∈ int ⟶ x8 x51 = x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x9 x51 x52 = If_i (SNoLe x51 0) x52 (x6 (x9 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x10 x51 = x9 x7 (x8 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ x11 x51 = add_SNo (x10 x51) x51) ⟶ x12 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x13 x51 x52 = If_i (SNoLe x51 0) x52 (x5 (x13 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x14 x51 = x13 (x11 x51) x12) ⟶ (∀ x51 . x51 ∈ int ⟶ x15 x51 = x14 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ x16 x51 = mul_SNo x51 x51) ⟶ x17 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x18 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x19 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x20 x51 = x51) ⟶ x21 = 1 ⟶ x22 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x23 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x18 (x23 (add_SNo x51 (minus_SNo 1)) x52 x53) (x24 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x24 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x19 (x23 (add_SNo x51 (minus_SNo 1)) x52 x53) (x24 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x25 x51 = x23 (x20 x51) x21 x22) ⟶ (∀ x51 . x51 ∈ int ⟶ x26 x51 = x25 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x27 x51 x52 = If_i (SNoLe x51 0) x52 (x16 (x27 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x28 x51 = x27 x17 (x26 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x29 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x30 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x31 x51 = add_SNo 1 x51) ⟶ x32 = 1 ⟶ x33 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x34 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x29 (x34 (add_SNo x51 (minus_SNo 1)) x52 x53) (x35 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x35 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x30 (x34 (add_SNo x51 (minus_SNo 1)) x52 x53) (x35 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x36 x51 = x34 (x31 x51) x32 x33) ⟶ (∀ x51 . x51 ∈ int ⟶ x37 x51 = mul_SNo x51 x51) ⟶ x38 = 1 ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x39 x51 x52 = mul_SNo x51 x52) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x40 x51 x52 = x52) ⟶ (∀ x51 . x51 ∈ int ⟶ x41 x51 = add_SNo 1 x51) ⟶ x42 = 1 ⟶ x43 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x44 x51 x52 x53 = If_i (SNoLe x51 0) x52 (x39 (x44 (add_SNo x51 (minus_SNo 1)) x52 x53) (x45 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ ∀ x53 . x53 ∈ int ⟶ x45 x51 x52 x53 = If_i (SNoLe x51 0) x53 (x40 (x44 (add_SNo x51 (minus_SNo 1)) x52 x53) (x45 (add_SNo x51 (minus_SNo 1)) x52 x53))) ⟶ (∀ x51 . x51 ∈ int ⟶ x46 x51 = x44 (x41 x51) x42 x43) ⟶ (∀ x51 . x51 ∈ int ⟶ x47 x51 = x46 x51) ⟶ (∀ x51 . x51 ∈ int ⟶ ∀ x52 . x52 ∈ int ⟶ x48 x51 x52 = If_i (SNoLe x51 0) x52 (x37 (x48 (add_SNo x51 (minus_SNo 1)) x52))) ⟶ (∀ x51 . x51 ∈ int ⟶ x49 x51 = x48 x38 (x47 x51)) ⟶ (∀ x51 . x51 ∈ int ⟶ x50 x51 = mul_SNo (mul_SNo (x28 x51) (x36 x51)) (x49 x51)) ⟶ ∀ x51 . x51 ∈ int ⟶ SNoLe 0 x51 ⟶ x15 x51 = x50 x51
Conjecture 3af29..^A13871 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x36 x37 ∈ int) ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x39 x40 x41 x42 ∈ int) ⟶ ∀ x40 : ι → ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x40 x41 x42 x43 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ (∀ x46 . x46 ∈ int ⟶ x0 x46 = mul_SNo x46 x46) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x3 x46 x47 = If_i (SNoLe x46 0) x47 (x0 (x3 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x46 . x46 ∈ int ⟶ x5 x46 = mul_SNo (add_SNo x4 (minus_SNo 2)) x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x6 x46 = add_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x46 x46)) x46)) ⟶ x7 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x8 x46 x47 = If_i (SNoLe x46 0) x47 (x5 (x8 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x9 x46 = x8 (x6 x46) x7) ⟶ (∀ x46 . x46 ∈ int ⟶ x10 x46 = x9 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x11 x46 = mul_SNo x46 x46) ⟶ x12 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x13 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x14 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x15 x46 = x46) ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x18 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x13 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x19 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x14 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x20 x46 = x18 (x15 x46) x16 x17) ⟶ (∀ x46 . x46 ∈ int ⟶ x21 x46 = x20 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x22 x46 x47 = If_i (SNoLe x46 0) x47 (x11 (x22 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x23 x46 = x22 x12 (x21 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x24 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x25 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x26 x46 = add_SNo 2 x46) ⟶ x27 = 1 ⟶ x28 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x29 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x24 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x30 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x25 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x31 x46 = x29 (x26 x46) x27 x28) ⟶ (∀ x46 . x46 ∈ int ⟶ x32 x46 = mul_SNo x46 x46) ⟶ x33 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x34 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x35 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x36 x46 = x46) ⟶ x37 = 1 ⟶ x38 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x39 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x34 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x40 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x35 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x41 x46 = x39 (x36 x46) x37 x38) ⟶ (∀ x46 . x46 ∈ int ⟶ x42 x46 = x41 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x43 x46 x47 = If_i (SNoLe x46 0) x47 (x32 (x43 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x44 x46 = x43 x33 (x42 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ x45 x46 = mul_SNo (mul_SNo (x23 x46) (x31 x46)) (x44 x46)) ⟶ ∀ x46 . x46 ∈ int ⟶ SNoLe 0 x46 ⟶ x10 x46 = x45 x46
Conjecture 965fa..^A13870 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι → ι . (∀ x25 . x25 ∈ int ⟶ ∀ 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 ⟶ ∀ 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 ⟶ x36 x37 ∈ int) ⟶ ∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ ∀ x39 : ι → ι → ι → ι . (∀ x40 . x40 ∈ int ⟶ ∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ x39 x40 x41 x42 ∈ int) ⟶ ∀ x40 : ι → ι → ι → ι . (∀ x41 . x41 ∈ int ⟶ ∀ x42 . x42 ∈ int ⟶ ∀ x43 . x43 ∈ int ⟶ x40 x41 x42 x43 ∈ int) ⟶ ∀ x41 : ι → ι . (∀ x42 . x42 ∈ int ⟶ x41 x42 ∈ int) ⟶ ∀ x42 : ι → ι . (∀ x43 . x43 ∈ int ⟶ x42 x43 ∈ int) ⟶ ∀ x43 : ι → ι → ι . (∀ x44 . x44 ∈ int ⟶ ∀ x45 . x45 ∈ int ⟶ x43 x44 x45 ∈ int) ⟶ ∀ x44 : ι → ι . (∀ x45 . x45 ∈ int ⟶ x44 x45 ∈ int) ⟶ ∀ x45 : ι → ι . (∀ x46 . x46 ∈ int ⟶ x45 x46 ∈ int) ⟶ (∀ x46 . x46 ∈ int ⟶ x0 x46 = mul_SNo x46 x46) ⟶ x1 = 2 ⟶ x2 = 2 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x3 x46 x47 = If_i (SNoLe x46 0) x47 (x0 (x3 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ x4 = x3 x1 x2 ⟶ (∀ x46 . x46 ∈ int ⟶ x5 x46 = mul_SNo (add_SNo x4 (minus_SNo 2)) x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x6 x46 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x46 x46)) x46)) ⟶ x7 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x8 x46 x47 = If_i (SNoLe x46 0) x47 (x5 (x8 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x9 x46 = x8 (x6 x46) x7) ⟶ (∀ x46 . x46 ∈ int ⟶ x10 x46 = x9 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ x11 x46 = mul_SNo x46 x46) ⟶ x12 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x13 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x14 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x15 x46 = x46) ⟶ x16 = 1 ⟶ x17 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x18 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x13 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x19 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x14 (x18 (add_SNo x46 (minus_SNo 1)) x47 x48) (x19 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x20 x46 = x18 (x15 x46) x16 x17) ⟶ (∀ x46 . x46 ∈ int ⟶ x21 x46 = x20 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x22 x46 x47 = If_i (SNoLe x46 0) x47 (x11 (x22 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x23 x46 = x22 x12 (x21 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x24 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x25 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x26 x46 = add_SNo 1 x46) ⟶ x27 = 1 ⟶ x28 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x29 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x24 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x30 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x25 (x29 (add_SNo x46 (minus_SNo 1)) x47 x48) (x30 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x31 x46 = x29 (x26 x46) x27 x28) ⟶ (∀ x46 . x46 ∈ int ⟶ x32 x46 = mul_SNo x46 x46) ⟶ x33 = 1 ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x34 x46 x47 = mul_SNo x46 x47) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x35 x46 x47 = x47) ⟶ (∀ x46 . x46 ∈ int ⟶ x36 x46 = x46) ⟶ x37 = 1 ⟶ x38 = add_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x39 x46 x47 x48 = If_i (SNoLe x46 0) x47 (x34 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ ∀ x48 . x48 ∈ int ⟶ x40 x46 x47 x48 = If_i (SNoLe x46 0) x48 (x35 (x39 (add_SNo x46 (minus_SNo 1)) x47 x48) (x40 (add_SNo x46 (minus_SNo 1)) x47 x48))) ⟶ (∀ x46 . x46 ∈ int ⟶ x41 x46 = x39 (x36 x46) x37 x38) ⟶ (∀ x46 . x46 ∈ int ⟶ x42 x46 = x41 x46) ⟶ (∀ x46 . x46 ∈ int ⟶ ∀ x47 . x47 ∈ int ⟶ x43 x46 x47 = If_i (SNoLe x46 0) x47 (x32 (x43 (add_SNo x46 (minus_SNo 1)) x47))) ⟶ (∀ x46 . x46 ∈ int ⟶ x44 x46 = x43 x33 (x42 x46)) ⟶ (∀ x46 . x46 ∈ int ⟶ x45 x46 = mul_SNo (mul_SNo (x23 x46) (x31 x46)) (x44 x46)) ⟶ ∀ x46 . x46 ∈ int ⟶ SNoLe 0 x46 ⟶ x10 x46 = x45 x46
Conjecture d1066..^A138590 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ int ⟶ x2 x3 ∈ int) ⟶ ∀ x3 . x3 ∈ int ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ 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 ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι → ι → ι . (∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 . x23 ∈ int ⟶ x20 x21 x22 x23 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι . (∀ x23 . x23 ∈ int ⟶ x22 x23 ∈ int) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x0 x23 x24 = add_SNo x23 x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x1 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x2 x23 = add_SNo (add_SNo x23 x23) x23) ⟶ x3 = 2 ⟶ (∀ x23 . x23 ∈ int ⟶ x4 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x5 x23 x24 = If_i (SNoLe x23 0) x24 (x2 (x5 (add_SNo x23 (minus_SNo 1)) x24))) ⟶ (∀ x23 . x23 ∈ int ⟶ x6 x23 = x5 x3 (x4 x23)) ⟶ (∀ x23 . x23 ∈ int ⟶ x7 x23 = x6 x23) ⟶ x8 = 0 ⟶ x9 = 1 ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x10 x23 x24 x25 = If_i (SNoLe x23 0) x24 (x0 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25) (x11 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 . x25 ∈ int ⟶ x11 x23 x24 x25 = If_i (SNoLe x23 0) x25 (x1 (x10 (add_SNo x23 (minus_SNo 1)) x24 x25))) ⟶ (∀ x23 . x23 ∈ int ⟶ x12 x23 = x10 (x7 x23) x8 x9) ⟶ (∀ x23 . x23 ∈ int ⟶ x13 x23 = x12 x23) ⟶ (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x14 x23 x24 = add_SNo (mul_SNo (add_SNo 2 2) x23) x24) ⟶ (∀ x23 . x23 ∈ int ⟶ x15 x23 = x23) ⟶ (∀ x23 . x23 ∈ int ⟶ x16 x23 = add_SNo (add_SNo x23 x23) x23) ⟶ x17 = 0 ⟶ 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))) ⟶ (∀ 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 c9cac..^A138525 : ∀ x0 : ι → ι → ι . (∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ x0 x1 x2 ∈ int) ⟶ ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ x1 x2 x3 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ x5 x6 x7 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ 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 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x16 x17 x18 x19 ∈ int) ⟶ ∀ x17 : ι → ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ x17 x18 x19 x20 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x0 x20 x21 = mul_SNo x20 x21) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x1 x20 x21 = add_SNo x21 x21) ⟶ x2 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x3 x20 x21 = If_i (SNoLe x20 0) x21 (x0 (x3 (add_SNo x20 (minus_SNo 1)) x21) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x4 x20 x21 = x3 (x1 x20 x21) x2) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x5 x20 x21 = add_SNo (x4 x20 x21) x20) ⟶ (∀ x20 . x20 ∈ int ⟶ x6 x20 = x20) ⟶ x7 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x8 x20 x21 = If_i (SNoLe x20 0) x21 (x5 (x8 (add_SNo x20 (minus_SNo 1)) x21) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x9 x20 = x8 (x6 x20) x7) ⟶ (∀ x20 . x20 ∈ int ⟶ x10 x20 = x9 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x11 x20 x21 = add_SNo 1 (mul_SNo (add_SNo (mul_SNo x21 x21) (minus_SNo x21)) x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x12 x20 x21 = add_SNo x21 (minus_SNo 2)) ⟶ (∀ x20 . x20 ∈ int ⟶ x13 x20 = add_SNo x20 (minus_SNo 1)) ⟶ x14 = 1 ⟶ (∀ x20 . x20 ∈ int ⟶ x15 x20 = add_SNo x20 x20) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x16 x20 x21 x22 = If_i (SNoLe x20 0) x21 (x11 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x17 x20 x21 x22 = If_i (SNoLe x20 0) x22 (x12 (x16 (add_SNo x20 (minus_SNo 1)) x21 x22) (x17 (add_SNo x20 (minus_SNo 1)) x21 x22))) ⟶ (∀ x20 . x20 ∈ int ⟶ x18 x20 = x16 (x13 x20) x14 (x15 x20)) ⟶ (∀ x20 . x20 ∈ int ⟶ x19 x20 = add_SNo (mul_SNo (x18 x20) (If_i (SNoLe x20 0) 0 2)) 1) ⟶ ∀ x20 . x20 ∈ int ⟶ SNoLe 0 x20 ⟶ x10 x20 = x19 x20
Conjecture 94268..^A13839 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ 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 ⟶ x0 x33 = mul_SNo 2 (add_SNo (add_SNo x33 x33) x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x1 x33 = add_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33)) ⟶ x2 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x4 x33 = x3 (x1 x33) x2) ⟶ (∀ x33 . x33 ∈ int ⟶ x5 x33 = x4 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x6 x33 = mul_SNo (mul_SNo x33 x33) x33) ⟶ x7 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x9 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x10 x33 = x33) ⟶ x11 = 1 ⟶ x12 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x13 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x8 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x14 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x9 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x15 x33 = x13 (x10 x33) x11 x12) ⟶ (∀ x33 . x33 ∈ int ⟶ x16 x33 = x15 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x17 x33 x34 = If_i (SNoLe x33 0) x34 (x6 (x17 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = x17 x7 (x16 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x19 x33 = mul_SNo x33 x33) ⟶ x20 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x21 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x22 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x23 x33 = add_SNo 1 x33) ⟶ x24 = 1 ⟶ x25 = add_SNo 2 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x26 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x21 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x27 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x22 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x28 x33 = x26 (x23 x33) x24 x25) ⟶ (∀ x33 . x33 ∈ int ⟶ x29 x33 = x28 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x30 x33 x34 = If_i (SNoLe x33 0) x34 (x19 (x30 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x31 x33 = x30 x20 (x29 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = mul_SNo (x18 x33) (x31 x33)) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x5 x33 = x32 x33
Conjecture f23d9..^A13838 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ x6 x7 x8 ∈ int) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ x7 x8 x9 ∈ int) ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 : ι → ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ x11 x12 x13 x14 ∈ int) ⟶ ∀ x12 : ι → ι → ι → ι . (∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x12 x13 x14 x15 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ 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 ⟶ ∀ x27 . x27 ∈ int ⟶ x25 x26 x27 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 : ι → ι . (∀ x28 . x28 ∈ int ⟶ x27 x28 ∈ int) ⟶ (∀ x28 . x28 ∈ int ⟶ x0 x28 = mul_SNo 2 (add_SNo (add_SNo x28 x28) x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x1 x28 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x28 x28)) x28)) ⟶ x2 = 1 ⟶ (∀ 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 ∈ int ⟶ x5 x28 = x4 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x6 x28 x29 = mul_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x7 x28 x29 = x29) ⟶ (∀ x28 . x28 ∈ int ⟶ x8 x28 = x28) ⟶ x9 = 2 ⟶ x10 = mul_SNo 2 (mul_SNo 2 (add_SNo 2 (add_SNo 2 2))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x11 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x6 (x11 (add_SNo x28 (minus_SNo 1)) x29 x30) (x12 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x12 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x7 (x11 (add_SNo x28 (minus_SNo 1)) x29 x30) (x12 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ x13 x28 = x11 (x8 x28) x9 x10) ⟶ (∀ x28 . x28 ∈ int ⟶ x14 x28 = mul_SNo x28 x28) ⟶ x15 = 1 ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x16 x28 x29 = mul_SNo x28 x29) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x17 x28 x29 = x29) ⟶ (∀ x28 . x28 ∈ int ⟶ x18 x28 = x28) ⟶ x19 = 1 ⟶ x20 = add_SNo 2 (mul_SNo 2 (mul_SNo 2 (add_SNo 2 2))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x21 x28 x29 x30 = If_i (SNoLe x28 0) x29 (x16 (x21 (add_SNo x28 (minus_SNo 1)) x29 x30) (x22 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x22 x28 x29 x30 = If_i (SNoLe x28 0) x30 (x17 (x21 (add_SNo x28 (minus_SNo 1)) x29 x30) (x22 (add_SNo x28 (minus_SNo 1)) x29 x30))) ⟶ (∀ x28 . x28 ∈ int ⟶ x23 x28 = x21 (x18 x28) x19 x20) ⟶ (∀ x28 . x28 ∈ int ⟶ x24 x28 = x23 x28) ⟶ (∀ x28 . x28 ∈ int ⟶ ∀ x29 . x29 ∈ int ⟶ x25 x28 x29 = If_i (SNoLe x28 0) x29 (x14 (x25 (add_SNo x28 (minus_SNo 1)) x29))) ⟶ (∀ x28 . x28 ∈ int ⟶ x26 x28 = x25 x15 (x24 x28)) ⟶ (∀ x28 . x28 ∈ int ⟶ x27 x28 = mul_SNo (mul_SNo (add_SNo 1 2) (x13 x28)) (x26 x28)) ⟶ ∀ x28 . x28 ∈ int ⟶ SNoLe 0 x28 ⟶ x5 x28 = x27 x28
Conjecture c4ac6..^A13837 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ 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 ⟶ x0 x33 = add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x1 x33 = add_SNo (mul_SNo 2 (add_SNo 2 (add_SNo x33 x33))) x33) ⟶ x2 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x4 x33 = x3 (x1 x33) x2) ⟶ (∀ x33 . x33 ∈ int ⟶ x5 x33 = x4 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x6 x33 = mul_SNo (mul_SNo x33 x33) x33) ⟶ x7 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x9 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x10 x33 = x33) ⟶ x11 = 1 ⟶ x12 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x13 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x8 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x14 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x9 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x15 x33 = x13 (x10 x33) x11 x12) ⟶ (∀ x33 . x33 ∈ int ⟶ x16 x33 = x15 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x17 x33 x34 = If_i (SNoLe x33 0) x34 (x6 (x17 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = x17 x7 (x16 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x19 x33 = mul_SNo x33 x33) ⟶ x20 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x21 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x22 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x23 x33 = add_SNo 2 x33) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x26 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x21 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x27 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x22 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x28 x33 = x26 (x23 x33) x24 x25) ⟶ (∀ x33 . x33 ∈ int ⟶ x29 x33 = x28 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x30 x33 x34 = If_i (SNoLe x33 0) x34 (x19 (x30 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x31 x33 = x30 x20 (x29 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = mul_SNo (x18 x33) (x31 x33)) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x5 x33 = x32 x33
Conjecture ef5dd..^A13836 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ∈ int ⟶ x3 x4 ∈ int) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ int ⟶ ∀ x6 . x6 ∈ int ⟶ x4 x5 x6 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ ∀ x18 : ι → ι → ι → ι . (∀ x19 . x19 ∈ int ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x18 x19 x20 x21 ∈ int) ⟶ ∀ x19 : ι → ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ ∀ x22 . x22 ∈ int ⟶ x19 x20 x21 x22 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 : ι → ι → ι . (∀ x23 . x23 ∈ int ⟶ ∀ x24 . x24 ∈ int ⟶ x22 x23 x24 ∈ int) ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 : ι → ι . (∀ x25 . x25 ∈ int ⟶ x24 x25 ∈ int) ⟶ ∀ x25 . x25 ∈ int ⟶ ∀ x26 : ι → ι → ι . (∀ 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 ⟶ ∀ x37 . x37 ∈ int ⟶ x35 x36 x37 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ ∀ x37 : ι → ι . (∀ x38 . x38 ∈ int ⟶ x37 x38 ∈ int) ⟶ (∀ x38 . x38 ∈ int ⟶ x0 x38 = add_SNo (mul_SNo 2 (add_SNo x38 x38)) x38) ⟶ (∀ x38 . x38 ∈ int ⟶ x1 x38 = add_SNo 1 (add_SNo x38 x38)) ⟶ x2 = 2 ⟶ (∀ x38 . x38 ∈ int ⟶ x3 x38 = x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x4 x38 x39 = If_i (SNoLe x38 0) x39 (x1 (x4 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x5 x38 = x4 x2 (x3 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x6 x38 = add_SNo (x5 x38) x38) ⟶ x7 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x8 x38 x39 = If_i (SNoLe x38 0) x39 (x0 (x8 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x9 x38 = x8 (x6 x38) x7) ⟶ (∀ x38 . x38 ∈ int ⟶ x10 x38 = x9 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ x11 x38 = mul_SNo (mul_SNo x38 x38) x38) ⟶ x12 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x13 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x14 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x15 x38 = add_SNo 1 x38) ⟶ x16 = 1 ⟶ x17 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x18 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x13 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x19 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x14 (x18 (add_SNo x38 (minus_SNo 1)) x39 x40) (x19 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x20 x38 = x18 (x15 x38) x16 x17) ⟶ (∀ x38 . x38 ∈ int ⟶ x21 x38 = x20 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x22 x38 x39 = If_i (SNoLe x38 0) x39 (x11 (x22 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x23 x38 = x22 x12 (x21 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x24 x38 = mul_SNo x38 x38) ⟶ x25 = 1 ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x26 x38 x39 = mul_SNo x38 x39) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x27 x38 x39 = x39) ⟶ (∀ x38 . x38 ∈ int ⟶ x28 x38 = x38) ⟶ x29 = 1 ⟶ x30 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x31 x38 x39 x40 = If_i (SNoLe x38 0) x39 (x26 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ ∀ x40 . x40 ∈ int ⟶ x32 x38 x39 x40 = If_i (SNoLe x38 0) x40 (x27 (x31 (add_SNo x38 (minus_SNo 1)) x39 x40) (x32 (add_SNo x38 (minus_SNo 1)) x39 x40))) ⟶ (∀ x38 . x38 ∈ int ⟶ x33 x38 = x31 (x28 x38) x29 x30) ⟶ (∀ x38 . x38 ∈ int ⟶ x34 x38 = x33 x38) ⟶ (∀ x38 . x38 ∈ int ⟶ ∀ x39 . x39 ∈ int ⟶ x35 x38 x39 = If_i (SNoLe x38 0) x39 (x24 (x35 (add_SNo x38 (minus_SNo 1)) x39))) ⟶ (∀ x38 . x38 ∈ int ⟶ x36 x38 = x35 x25 (x34 x38)) ⟶ (∀ x38 . x38 ∈ int ⟶ x37 x38 = mul_SNo (x23 x38) (x36 x38)) ⟶ ∀ x38 . x38 ∈ int ⟶ SNoLe 0 x38 ⟶ x10 x38 = x37 x38
Conjecture 0210b..^A13835 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ int ⟶ ∀ x10 . x10 ∈ int ⟶ x8 x9 x10 ∈ int) ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . x10 ∈ int ⟶ ∀ x11 . x11 ∈ int ⟶ x9 x10 x11 ∈ int) ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x13 x14 x15 x16 ∈ int) ⟶ ∀ x14 : ι → ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ ∀ x17 . x17 ∈ int ⟶ x14 x15 x16 x17 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ ∀ x17 : ι → ι → ι . (∀ x18 . x18 ∈ int ⟶ ∀ x19 . x19 ∈ int ⟶ x17 x18 x19 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι . (∀ x20 . x20 ∈ int ⟶ x19 x20 ∈ int) ⟶ ∀ x20 . x20 ∈ int ⟶ ∀ 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 ⟶ x0 x33 = add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x1 x33 = add_SNo 2 (add_SNo (mul_SNo 2 (add_SNo x33 x33)) x33)) ⟶ x2 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x3 x33 x34 = If_i (SNoLe x33 0) x34 (x0 (x3 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x4 x33 = x3 (x1 x33) x2) ⟶ (∀ x33 . x33 ∈ int ⟶ x5 x33 = x4 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ x6 x33 = mul_SNo (mul_SNo x33 x33) x33) ⟶ x7 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x8 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x9 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x10 x33 = x33) ⟶ x11 = 1 ⟶ x12 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x13 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x8 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x14 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x9 (x13 (add_SNo x33 (minus_SNo 1)) x34 x35) (x14 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x15 x33 = x13 (x10 x33) x11 x12) ⟶ (∀ x33 . x33 ∈ int ⟶ x16 x33 = x15 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x17 x33 x34 = If_i (SNoLe x33 0) x34 (x6 (x17 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x18 x33 = x17 x7 (x16 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x19 x33 = mul_SNo x33 x33) ⟶ x20 = 1 ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x21 x33 x34 = mul_SNo x33 x34) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x22 x33 x34 = x34) ⟶ (∀ x33 . x33 ∈ int ⟶ x23 x33 = add_SNo 1 x33) ⟶ x24 = 1 ⟶ x25 = add_SNo 1 (add_SNo 2 2) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x26 x33 x34 x35 = If_i (SNoLe x33 0) x34 (x21 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ ∀ x35 . x35 ∈ int ⟶ x27 x33 x34 x35 = If_i (SNoLe x33 0) x35 (x22 (x26 (add_SNo x33 (minus_SNo 1)) x34 x35) (x27 (add_SNo x33 (minus_SNo 1)) x34 x35))) ⟶ (∀ x33 . x33 ∈ int ⟶ x28 x33 = x26 (x23 x33) x24 x25) ⟶ (∀ x33 . x33 ∈ int ⟶ x29 x33 = x28 x33) ⟶ (∀ x33 . x33 ∈ int ⟶ ∀ x34 . x34 ∈ int ⟶ x30 x33 x34 = If_i (SNoLe x33 0) x34 (x19 (x30 (add_SNo x33 (minus_SNo 1)) x34))) ⟶ (∀ x33 . x33 ∈ int ⟶ x31 x33 = x30 x20 (x29 x33)) ⟶ (∀ x33 . x33 ∈ int ⟶ x32 x33 = mul_SNo (x18 x33) (x31 x33)) ⟶ ∀ x33 . x33 ∈ int ⟶ SNoLe 0 x33 ⟶ x5 x33 = x32 x33
Conjecture 2759b..^A13834 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 : ι → ι . (∀ x10 . x10 ∈ int ⟶ x9 x10 ∈ int) ⟶ ∀ x10 . x10 ∈ int ⟶ ∀ x11 : ι → ι → ι . (∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ x11 x12 x13 ∈ int) ⟶ ∀ x12 : ι → ι . (∀ x13 . x13 ∈ int ⟶ x12 x13 ∈ int) ⟶ ∀ x13 : ι → ι . (∀ x14 . x14 ∈ int ⟶ x13 x14 ∈ int) ⟶ ∀ x14 : ι → ι → ι . (∀ x15 . x15 ∈ int ⟶ ∀ x16 . x16 ∈ int ⟶ x14 x15 x16 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι . (∀ x17 . x17 ∈ int ⟶ x16 x17 ∈ int) ⟶ (∀ x17 . x17 ∈ int ⟶ x0 x17 = add_SNo (mul_SNo 2 (add_SNo x17 x17)) x17) ⟶ (∀ x17 . x17 ∈ int ⟶ x1 x17 = add_SNo 1 (add_SNo (mul_SNo 2 (add_SNo x17 x17)) x17)) ⟶ x2 = 1 ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x3 x17 x18 = If_i (SNoLe x17 0) x18 (x0 (x3 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x4 x17 = x3 (x1 x17) x2) ⟶ (∀ x17 . x17 ∈ int ⟶ x5 x17 = x4 x17) ⟶ (∀ x17 . x17 ∈ int ⟶ x6 x17 = mul_SNo (mul_SNo (mul_SNo (mul_SNo x17 x17) (add_SNo (mul_SNo 2 2) 1)) x17) (mul_SNo x17 x17)) ⟶ x7 = 1 ⟶ (∀ x17 . x17 ∈ int ⟶ x8 x17 = add_SNo (mul_SNo 2 (add_SNo x17 x17)) x17) ⟶ (∀ x17 . x17 ∈ int ⟶ x9 x17 = x17) ⟶ x10 = 1 ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x11 x17 x18 = If_i (SNoLe x17 0) x18 (x8 (x11 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x12 x17 = x11 (x9 x17) x10) ⟶ (∀ x17 . x17 ∈ int ⟶ x13 x17 = x12 x17) ⟶ (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x14 x17 x18 = If_i (SNoLe x17 0) x18 (x6 (x14 (add_SNo x17 (minus_SNo 1)) x18))) ⟶ (∀ x17 . x17 ∈ int ⟶ x15 x17 = x14 x7 (x13 x17)) ⟶ (∀ x17 . x17 ∈ int ⟶ x16 x17 = x15 x17) ⟶ ∀ x17 . x17 ∈ int ⟶ SNoLe 0 x17 ⟶ x5 x17 = x16 x17
Conjecture ab1e3..^A13833 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ 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 ⟶ x0 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x1 x32 = mul_SNo 2 (add_SNo (mul_SNo 2 (add_SNo 2 (add_SNo x32 x32))) x32)) ⟶ x2 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x3 x32 x33 = If_i (SNoLe x32 0) x33 (x0 (x3 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x4 x32 = x3 (x1 x32) x2) ⟶ (∀ x32 . x32 ∈ int ⟶ x5 x32 = x4 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x6 x32 = mul_SNo (mul_SNo x32 x32) x32) ⟶ x7 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ x8 x32 = mul_SNo x32 x32) ⟶ x9 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ x10 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x11 x32 = x32) ⟶ x12 = 1 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x13 x32 x33 = If_i (SNoLe x32 0) x33 (x10 (x13 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x14 x32 = x13 (x11 x32) x12) ⟶ (∀ x32 . x32 ∈ int ⟶ x15 x32 = x14 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x16 x32 x33 = If_i (SNoLe x32 0) x33 (x8 (x16 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x17 x32 = x16 x9 (x15 x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ x18 x32 = x17 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x19 x32 x33 = If_i (SNoLe x32 0) x33 (x6 (x19 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x20 x32 = x19 x7 (x18 x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ x21 x32 = mul_SNo x32 x32) ⟶ x22 = 2 ⟶ (∀ x32 . x32 ∈ int ⟶ x23 x32 = add_SNo x32 x32) ⟶ (∀ x32 . x32 ∈ int ⟶ x24 x32 = x32) ⟶ x25 = 2 ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x26 x32 x33 = If_i (SNoLe x32 0) x33 (x23 (x26 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x27 x32 = x26 (x24 x32) x25) ⟶ (∀ x32 . x32 ∈ int ⟶ x28 x32 = mul_SNo 2 (x27 x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x29 x32 x33 = If_i (SNoLe x32 0) x33 (x21 (x29 (add_SNo x32 (minus_SNo 1)) x33))) ⟶ (∀ x32 . x32 ∈ int ⟶ x30 x32 = x29 x22 (x28 x32)) ⟶ (∀ x32 . x32 ∈ int ⟶ x31 x32 = mul_SNo (x20 x32) (x30 x32)) ⟶ ∀ x32 . x32 ∈ int ⟶ SNoLe 0 x32 ⟶ x5 x32 = x31 x32
Conjecture d732b..^A13832 : ∀ x0 : ι → ι . (∀ x1 . x1 ∈ int ⟶ x0 x1 ∈ int) ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ int ⟶ x1 x2 ∈ int) ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x3 x4 x5 ∈ int) ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ int ⟶ x4 x5 ∈ int) ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ int ⟶ x5 x6 ∈ int) ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ int ⟶ x6 x7 ∈ int) ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ int ⟶ x8 x9 ∈ int) ⟶ ∀ x9 . x9 ∈ int ⟶ ∀ x10 : ι → ι . (∀ x11 . x11 ∈ int ⟶ x10 x11 ∈ int) ⟶ ∀ x11 : ι → ι . (∀ x12 . x12 ∈ int ⟶ x11 x12 ∈ int) ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 : ι → ι → ι . (∀ x14 . x14 ∈ int ⟶ ∀ x15 . x15 ∈ int ⟶ x13 x14 x15 ∈ int) ⟶ ∀ x14 : ι → ι . (∀ x15 . x15 ∈ int ⟶ x14 x15 ∈ int) ⟶ ∀ x15 : ι → ι . (∀ x16 . x16 ∈ int ⟶ x15 x16 ∈ int) ⟶ ∀ x16 : ι → ι → ι . (∀ x17 . x17 ∈ int ⟶ ∀ x18 . x18 ∈ int ⟶ x16 x17 x18 ∈ int) ⟶ ∀ x17 : ι → ι . (∀ x18 . x18 ∈ int ⟶ x17 x18 ∈ int) ⟶ ∀ x18 : ι → ι . (∀ x19 . x19 ∈ int ⟶ x18 x19 ∈ int) ⟶ ∀ x19 : ι → ι → ι . (∀ x20 . x20 ∈ int ⟶ ∀ x21 . x21 ∈ int ⟶ x19 x20 x21 ∈ int) ⟶ ∀ x20 : ι → ι . (∀ x21 . x21 ∈ int ⟶ x20 x21 ∈ int) ⟶ ∀ x21 : ι → ι . (∀ x22 . x22 ∈ int ⟶ x21 x22 ∈ int) ⟶ ∀ x22 . x22 ∈ int ⟶ ∀ x23 : ι → ι . (∀ x24 . x24 ∈ int ⟶ x23 x24 ∈ int) ⟶ ∀ x24 . x24 ∈ int ⟶ ∀ x25 : ι → ι . (∀ x26 . x26 ∈ int ⟶ x25 x26 ∈ int) ⟶ ∀ x26 : ι → ι . (∀ x27 . x27 ∈ int ⟶ x26 x27 ∈ int) ⟶ ∀ x27 . x27 ∈ int ⟶ ∀ x28 : ι → ι → ι . (∀ x29 . x29 ∈ int ⟶ ∀ x30 . x30 ∈ int ⟶ x28 x29 x30 ∈ int) ⟶ ∀ x29 : ι → ι . (∀ x30 . x30 ∈ int ⟶ x29 x30 ∈ int) ⟶ ∀ x30 : ι → ι . (∀ x31 . x31 ∈ int ⟶ x30 x31 ∈ int) ⟶ ∀ x31 : ι → ι → ι . (∀ x32 . x32 ∈ int ⟶ ∀ x33 . x33 ∈ int ⟶ x31 x32 x33 ∈ int) ⟶ ∀ x32 : ι → ι . (∀ x33 . x33 ∈ int ⟶ x32 x33 ∈ int) ⟶ ∀ x33 : ι → ι . (∀ x34 . x34 ∈ int ⟶ x33 x34 ∈ int) ⟶ ∀ x34 : ι → ι → ι . (∀ x35 . x35 ∈ int ⟶ ∀ x36 . x36 ∈ int ⟶ x34 x35 x36 ∈ int) ⟶ ∀ x35 : ι → ι . (∀ x36 . x36 ∈ int ⟶ x35 x36 ∈ int) ⟶ ∀ x36 : ι → ι . (∀ x37 . x37 ∈ int ⟶ x36 x37 ∈ int) ⟶ (∀ x37 . x37 ∈ int ⟶ x0 x37 = add_SNo x37 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ x1 x37 = mul_SNo (add_SNo 1 (add_SNo 2 2)) (add_SNo 1 (add_SNo x37 x37))) ⟶ x2 = 2 ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x3 x37 x38 = If_i (SNoLe x37 0) x38 (x0 (x3 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x4 x37 = x3 (x1 x37) x2) ⟶ (∀ x37 . x37 ∈ int ⟶ x5 x37 = x4 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ x6 x37 = mul_SNo (mul_SNo x37 x37) x37) ⟶ x7 = 1 ⟶ (∀ x37 . x37 ∈ int ⟶ x8 x37 = mul_SNo x37 x37) ⟶ x9 = 1 ⟶ (∀ x37 . x37 ∈ int ⟶ x10 x37 = add_SNo x37 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ x11 x37 = x37) ⟶ x12 = 1 ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x13 x37 x38 = If_i (SNoLe x37 0) x38 (x10 (x13 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x14 x37 = x13 (x11 x37) x12) ⟶ (∀ x37 . x37 ∈ int ⟶ x15 x37 = x14 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x16 x37 x38 = If_i (SNoLe x37 0) x38 (x8 (x16 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x17 x37 = x16 x9 (x15 x37)) ⟶ (∀ x37 . x37 ∈ int ⟶ x18 x37 = x17 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x19 x37 x38 = If_i (SNoLe x37 0) x38 (x6 (x19 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x20 x37 = x19 x7 (x18 x37)) ⟶ (∀ x37 . x37 ∈ int ⟶ x21 x37 = mul_SNo x37 x37) ⟶ x22 = 1 ⟶ (∀ x37 . x37 ∈ int ⟶ x23 x37 = mul_SNo (mul_SNo x37 2) x37) ⟶ x24 = 1 ⟶ (∀ x37 . x37 ∈ int ⟶ x25 x37 = add_SNo x37 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ x26 x37 = x37) ⟶ x27 = 2 ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x28 x37 x38 = If_i (SNoLe x37 0) x38 (x25 (x28 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x29 x37 = x28 (x26 x37) x27) ⟶ (∀ x37 . x37 ∈ int ⟶ x30 x37 = x29 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x31 x37 x38 = If_i (SNoLe x37 0) x38 (x23 (x31 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x32 x37 = x31 x24 (x30 x37)) ⟶ (∀ x37 . x37 ∈ int ⟶ x33 x37 = x32 x37) ⟶ (∀ x37 . x37 ∈ int ⟶ ∀ x38 . x38 ∈ int ⟶ x34 x37 x38 = If_i (SNoLe x37 0) x38 (x21 (x34 (add_SNo x37 (minus_SNo 1)) x38))) ⟶ (∀ x37 . x37 ∈ int ⟶ x35 x37 = x34 x22 (x33 x37)) ⟶ (∀ x37 . x37 ∈ int ⟶ x36 x37 = mul_SNo (x20 x37) (x35 x37)) ⟶ ∀ x37 . x37 ∈ int ⟶ SNoLe 0 x37 ⟶ x5 x37 = x36 x37