Proofgold Proof

pf

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.

Apply SNo_foil with x0, minus_SNo x1, x2, minus_SNo x3, λ x4 x5 . x5 = add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) leaving 5 subgoals.

The subproof is completed by applying H0.

Apply SNo_minus_SNo with x1.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply SNo_minus_SNo with x3.

The subproof is completed by applying H3.

Apply mul_SNo_minus_minus with x1, x3, λ x4 x5 . add_SNo (mul_SNo x0 x2) (add_SNo (mul_SNo x0 (minus_SNo x3)) (add_SNo (mul_SNo (minus_SNo x1) x2) x5)) = add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

Apply mul_SNo_minus_distrL with x1, x2, λ x4 x5 . add_SNo (mul_SNo x0 x2) (add_SNo (mul_SNo x0 (minus_SNo x3)) (add_SNo x5 (mul_SNo x1 x3))) = add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply mul_SNo_minus_distrR with x0, x3, λ x4 x5 . add_SNo (mul_SNo x0 x2) (add_SNo x5 (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) = add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

set y4 to be add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3)))

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

Assume H4: x5 y4 y4.

The subproof is completed by applying H4.

■