Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

set y2 to be ...

set y3 to be ...

Claim L2: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2

Let x4 of type ι → ο be given.

Assume H2: x4 (mul_CSNo y2 y3).

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

The subproof is completed by applying H0.

Apply SNo_Re with y3, λ x5 x6 . mul_SNo y2 y3 = mul_SNo y2 x6 leaving 2 subgoals.

The subproof is completed by applying H1.

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

Assume H3: x5 (mul_SNo y2 y3) (mul_SNo y2 y3).

The subproof is completed by applying H3.

set y5 to be ...

Apply SNo_pair_0 with mul_SNo (CSNo_Re y2) (CSNo_Re y3), λ x6 x7 . y5 x7 x6.

Apply SNo_Re with y3, λ x6 x7 . SNo_pair (mul_SNo x7 (CSNo_Re x4)) 0 = SNo_pair (add_SNo (mul_SNo x7 (CSNo_Re x4)) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)))) (add_SNo (mul_SNo x7 (CSNo_Im x4)) (mul_SNo (CSNo_Im y3) (CSNo_Re x4))), λ x6 . y5 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply SNo_Re with x4, λ x6 x7 . SNo_pair (mul_SNo y3 x7) 0 = SNo_pair (add_SNo (mul_SNo y3 x7) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)))) (add_SNo (mul_SNo y3 (CSNo_Im x4)) (mul_SNo (CSNo_Im y3) x7)) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply SNo_Im with y3, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo (mul_SNo x7 (CSNo_Im x4)))) (add_SNo (mul_SNo y3 (CSNo_Im x4)) (mul_SNo x7 x4)) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply SNo_Im with x4, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo (mul_SNo 0 x7))) (add_SNo (mul_SNo y3 x7) (mul_SNo 0 x4)) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply mul_SNo_zeroR with 0, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo x7)) (add_SNo (mul_SNo y3 0) (mul_SNo 0 x4)) leaving 2 subgoals.

The subproof is completed by applying SNo_0.

Apply mul_SNo_zeroR with y3, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo 0)) (add_SNo x7 (mul_SNo 0 x4)) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply mul_SNo_com with 0, x4, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo 0)) (add_SNo 0 x7) leaving 3 subgoals.

The subproof is completed by applying SNo_0.

The subproof is completed by applying H1.

Apply mul_SNo_zeroR with x4, λ x6 x7 . SNo_pair (mul_SNo y3 x4) 0 = SNo_pair (add_SNo (mul_SNo y3 x4) (minus_SNo 0)) (add_SNo 0 ...) leaving 2 subgoals.

...

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

Apply L2 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H3: x4 y3 y3.

The subproof is completed by applying H3.

■

Proofgold Proof