| ∀ x0 x1 x2 : ι → ι → ι → ι . ∀ x3 x4 x5 : ι → ι → ι → ο . (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo x6 (mul_SNo 2 x8)) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x1 x6 x7 x8 = x8) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ x2 x6 x7 x8 = add_SNo x7 (minus_SNo (add_SNo x6 x8))) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo (mul_SNo 2 x7) (minus_SNo x6)) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x1 x6 x7 x8 = x7) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x2 x6 x7 x8 = add_SNo x6 (add_SNo x8 (minus_SNo x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x0 x6 x7 x8 = add_SNo x6 (minus_SNo (mul_SNo 2 x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x1 x6 x7 x8 = add_SNo x6 (add_SNo x8 (minus_SNo x7))) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x2 x6 x7 x8 = x7) ⟶ (∀ x6 x7 x8 . add_SNo x6 x8 ∈ x7 ⟶ x3 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x3 x6 x7 x8 ⟶ add_SNo x6 x8 ∈ x7) ⟶ (∀ x6 x7 x8 . x7 ∈ add_SNo x6 x8 ⟶ x6 ∈ mul_SNo 2 x7 ⟶ x4 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x7 ∈ add_SNo x6 x8) ⟶ (∀ x6 x7 x8 . x4 x6 x7 x8 ⟶ x6 ∈ mul_SNo 2 x7) ⟶ (∀ x6 x7 x8 . x7 ∈ add_SNo x6 x8 ⟶ mul_SNo 2 x7 ∈ x6 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ x7 ∈ add_SNo x6 x8) ⟶ (∀ x6 x7 x8 . x5 x6 x7 x8 ⟶ mul_SNo 2 x7 ∈ x6) ⟶ ∀ x6 . x6 ∈ omega ⟶ ∀ x7 . equip x7 x6 ⟶ (∀ x8 . x8 ∈ x7 ⟶ lam 3 (λ x10 . If_i (x10 = 0) (ap x8 0) (If_i (x10 = 1) (ap x8 1) (ap x8 2))) = x8) ⟶ (∀ x8 x9 x10 . lam 3 (λ x11 . If_i (x11 = 0) x8 (If_i (x11 = 1) x9 x10)) ∈ x7 ⟶ ∀ x11 : ο . (x8 ∈ omega ⟶ x9 ∈ omega ⟶ x10 ∈ omega ⟶ SNoLt 0 x8 ⟶ SNoLt 0 x9 ⟶ SNoLt 0 x10 ⟶ (add_SNo x8 x10 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = mul_SNo 2 x9 ⟶ ∀ x12 : ο . x12) ⟶ lam 3 (λ x12 . If_i (x12 = 0) x8 (If_i (x12 = 1) x10 x9)) ∈ x7 ⟶ x11) ⟶ x11) ⟶ (∀ x8 x9 x10 x11 . x11 ∈ omega ⟶ ∀ x12 . x12 ∈ omega ⟶ ∀ x13 . x13 ∈ omega ⟶ lam 3 (λ x14 . If_i (x14 = 0) x8 (If_i (x14 = 1) x9 x10)) ∈ x7 ⟶ add_SNo (mul_SNo x11 x11) (mul_SNo 4 (mul_SNo x12 x13)) = add_SNo (mul_SNo x8 x8) (mul_SNo 4 (mul_SNo x9 x10)) ⟶ lam 3 (λ x14 . If_i (x14 = 0) x11 (If_i (x14 = 1) x12 x13)) ∈ x7) ⟶ ∀ x8 x9 x10 . lam 3 (λ x11 . If_i (x11 = 0) x8 (If_i (x11 = 1) x9 x10)) ∈ x7 ⟶ x0 x8 x9 x10 = x8 ⟶ x1 x8 x9 x10 = x9 ⟶ x2 x8 x9 x10 = x10 ⟶ (∀ x11 x12 x13 . lam 3 (λ x14 . If_i (x14 = 0) x11 (If_i (x14 = 1) x12 x13)) ∈ x7 ⟶ x0 x11 x12 x13 = x11 ⟶ x1 x11 x12 x13 = x12 ⟶ x2 x11 x12 x13 = x13 ⟶ and (and (x11 = x8) (x12 = x9)) (x13 = x10)) ⟶ ∀ x11 : ο . (∀ x12 . (∀ x13 : ο . (∀ x14 . lam 3 (λ x15 . If_i (x15 = 0) x12 (If_i (x15 = 1) x14 x14)) ∈ x7 ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11 |
|