Apply SNoLev_ind3 with λ x0 x1 x2 . mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2).

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo x2.

Assume H3: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ mul_SNo (add_SNo x3 x1) x2 = add_SNo (mul_SNo x3 x2) (mul_SNo x1 x2).

Assume H4: ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo (add_SNo x0 x3) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x3 x2).

Assume H5: ∀ x3 . x3 ∈ SNoS_ (SNoLev x2) ⟶ mul_SNo (add_SNo x0 x1) x3 = add_SNo (mul_SNo x0 x3) (mul_SNo x1 x3).

Assume H6: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo (add_SNo x3 x4) x2 = add_SNo (mul_SNo x3 x2) (mul_SNo x4 x2).

Assume H7: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x2) ⟶ mul_SNo (add_SNo x3 x1) x4 = add_SNo (mul_SNo x3 x4) (mul_SNo x1 x4).

Assume H8: ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x2) ⟶ mul_SNo (add_SNo x0 x3) x4 = add_SNo (mul_SNo x0 x4) (mul_SNo x3 x4).

Assume H9: ∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ ∀ x5 . x5 ∈ SNoS_ (SNoLev x2) ⟶ mul_SNo (add_SNo x3 x4) x5 = add_SNo (mul_SNo x3 x5) (mul_SNo x4 x5).

Apply mul_SNo_eq_3 with add_SNo x0 x1, x2, mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2) leaving 3 subgoals.

Apply SNo_add_SNo with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H10: SNoCutP x3 x4.

Assume H11: ∀ x5 . ... ⟶ ∀ x6 : ο . (∀ x7 . ... ⟶ ∀ x8 . ... ⟶ x5 = add_SNo (mul_SNo x7 x2) (add_SNo (mul_SNo (add_SNo x0 x1) x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ (∀ x7 . x7 ∈ SNoR (add_SNo x0 x1) ⟶ ∀ x8 . x8 ∈ SNoR x2 ⟶ x5 = add_SNo (mul_SNo x7 x2) (add_SNo (mul_SNo (add_SNo x0 x1) x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ x6.

...

■

Proofgold Proof