Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

set y2 to be ...

Claim L2: ∀ x3 : ι → ο . x3 y2 ⟶ x3 (mul_SNo x0 x1)

Let x3 of type ι → ο be given.

Assume H2: x3 (mul_CSNo x1 y2).

Apply SNo_Re with x1, λ x4 x5 . mul_SNo x1 y2 = mul_SNo x5 (CSNo_Re y2), λ x4 . x3 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply SNo_Re with y2, λ x4 x5 . mul_SNo x1 y2 = mul_SNo x1 x5 leaving 2 subgoals.

The subproof is completed by applying H1.

set y4 to be mul_SNo x1 y2

Let x5 of type ι → ι → ο be given.

Assume H3: x5 y4 y4.

The subproof is completed by applying H3.

Apply SNo_pair_0 with mul_SNo (CSNo_Re x1) (CSNo_Re y2), λ x4 x5 . (λ x6 . x3) x5 x4.

set y4 to be ...

Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (SNo_pair (mul_SNo (CSNo_Re x1) (CSNo_Re y2)) 0)

Let x5 of type ι → ο be given.

Assume H3: x5 (SNo_pair (add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))) (add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Im x3)) (mul_SNo (CSNo_Im y2) (CSNo_Re x3)))).

Apply SNo_Im with y2, λ x6 x7 . mul_SNo (CSNo_Re y2) (CSNo_Re x3) = add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) (minus_SNo (mul_SNo x7 (CSNo_Im x3))), λ x6 x7 . (λ x8 . x5) (SNo_pair x6 0) (SNo_pair x7 0) leaving 3 subgoals.

The subproof is completed by applying H0.

Apply mul_SNo_zeroL with CSNo_Im x3, λ x6 x7 . mul_SNo (CSNo_Re y2) (CSNo_Re x3) = add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) (minus_SNo x7) leaving 2 subgoals.

Apply CSNo_ImR with x3.

Apply SNo_CSNo with x3.

The subproof is completed by applying H1.

Apply minus_SNo_0 with λ x6 x7 . mul_SNo (CSNo_Re y2) (CSNo_Re x3) = add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) x7.

Let x6 of type ι → ι → ο be given.

Apply add_SNo_0R with mul_SNo (CSNo_Re y2) (CSNo_Re x3), λ x7 x8 . x6 x8 x7.

Apply SNo_mul_SNo with CSNo_Re y2, CSNo_Re x3 leaving 2 subgoals.

Apply CSNo_ReR with y2.

Apply SNo_CSNo with y2.

The subproof is completed by applying H0.

Apply CSNo_ReR with x3.

Apply SNo_CSNo with x3.

The subproof is completed by applying H1.

Apply SNo_Im with y2, λ x6 x7 . 0 = add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Im x3)) (mul_SNo x7 (CSNo_Re x3)), λ x6 x7 . (λ x8 . x5) (SNo_pair (add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))) x6) (SNo_pair (add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x3)) (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))) x7) leaving 3 subgoals.

The subproof is completed by applying H0.

Apply SNo_Im with x3, λ x6 x7 . 0 = add_SNo (mul_SNo (CSNo_Re y2) x7) ... leaving 2 subgoals.

...

set y5 to be λ x5 . y4

Apply L3 with λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.

Assume H4: y5 y4 y4.

The subproof is completed by applying H4.

The subproof is completed by applying L3.

Let x3 of type ι → ι → ο be given.

Apply L2 with λ x4 . x3 x4 y2 ⟶ x3 y2 x4.

Assume H3: x3 y2 y2.

The subproof is completed by applying H3.

■

Proofgold Proof