Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: SNo x3.

set y4 to be ...

Claim L4: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (mul_SNo (add_SNo x0 x1) (add_SNo x2 x3))

Let x5 of type ι → ο be given.

Assume H4: x5 (add_SNo (mul_SNo x1 x3) (add_SNo (mul_SNo x1 y4) (add_SNo (mul_SNo x2 x3) (mul_SNo x2 y4)))).

Apply mul_SNo_distrL with add_SNo x1 x2, x3, y4, λ x6 . x5 leaving 4 subgoals.

Apply SNo_add_SNo with x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

set y6 to be ...

Claim L5: ∀ x7 : ι → ο . x7 y6 ⟶ x7 (add_SNo (mul_SNo (add_SNo x1 x2) x3) (mul_SNo (add_SNo x1 x2) y4))

Let x7 of type ι → ο be given.

Apply mul_SNo_distrR with x2, x3, y4, λ x8 x9 . (λ x10 . x7) (add_SNo x8 (mul_SNo (add_SNo x2 x3) x5)) (add_SNo x9 (mul_SNo ... ...)) leaving 3 subgoals.

...

set y7 to be λ x7 . y6

Apply L5 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.

Assume H6: y7 y6 y6.

The subproof is completed by applying H6.

set y8 to be add_SNo (add_SNo (mul_SNo x3 x5) (mul_SNo y4 x5)) (add_SNo (mul_SNo x3 y6) (mul_SNo y4 y6))

Claim L6: ∀ x9 : ι → ο . x9 y8 ⟶ x9 (add_SNo (add_SNo (mul_SNo x3 x5) (mul_SNo y4 x5)) (mul_SNo (add_SNo x3 y4) y6))

Let x9 of type ι → ο be given.

Apply mul_SNo_distrR with y4, x5, y7, λ x10 x11 . (λ x12 . x9) (add_SNo (add_SNo (mul_SNo y4 y6) (mul_SNo x5 y6)) x10) (add_SNo (add_SNo (mul_SNo y4 y6) (mul_SNo x5 y6)) x11) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

set y9 to be λ x9 . y8

Apply L6 with λ x10 . y9 x10 y8 ⟶ y9 y8 x10 leaving 2 subgoals.

Assume H7: y9 y8 y8.

The subproof is completed by applying H7.

Apply add_SNo_com_4_inner_mid with mul_SNo x5 y7, mul_SNo y6 y7, mul_SNo x5 y8, mul_SNo y6 y8, λ x10 x11 . x11 = add_SNo (mul_SNo x5 y7) (add_SNo (mul_SNo x5 y8) (add_SNo (mul_SNo y6 y7) (mul_SNo y6 y8))), λ x10 . y9 leaving 6 subgoals.

Apply SNo_mul_SNo with x5, y7 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

Apply SNo_mul_SNo with y6, y7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

Apply SNo_mul_SNo with x5, y8 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying L5.

Apply SNo_mul_SNo with y6, y8 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying L5.

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

Apply add_SNo_assoc with mul_SNo x5 y7, mul_SNo x5 y8, add_SNo (mul_SNo y6 y7) (mul_SNo y6 y8), λ x11 x12 . x10 x12 x11 leaving 3 subgoals.

Apply SNo_mul_SNo with x5, y7 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

Apply SNo_mul_SNo with x5, y8 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying L5.

Apply SNo_add_SNo with mul_SNo y6 y7, mul_SNo y6 y8 leaving 2 subgoals.

Apply SNo_mul_SNo with y6, y7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

Apply SNo_mul_SNo with y6, y8 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying L5.

The subproof is completed by applying L6.

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

Apply L4 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.

Assume H5: x5 y4 y4.

The subproof is completed by applying H5.

■

Proofgold Proof