Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι be given.

Assume H1: x1 ∈ omega.

Apply nat_inv with x0, add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0) leaving 3 subgoals.

Apply omega_nat_p with x0.

The subproof is completed by applying H0.

Assume H2: x0 = 0.

Apply nat_inv with x1, add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0) leaving 3 subgoals.

Apply omega_nat_p with x1.

The subproof is completed by applying H1.

Assume H3: x1 = 0.

Assume H4: add_nat x0 x1 = 0.

Apply andI with x0 = 0, x1 = 0 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Assume H3: ∃ x2 . and (nat_p x2) (x1 = ordsucc x2).

Apply H3 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).

Let x2 of type ι be given.

Assume H4: (λ x3 . and (nat_p x3) (x1 = ordsucc x3)) x2.

Apply H4 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).

Assume H5: nat_p x2.

Assume H6: x1 = ordsucc x2.

Apply H6 with λ x3 x4 . add_nat x0 x4 = 0 ⟶ and (x0 = 0) (x4 = 0).

Apply add_nat_SR with x0, x2, λ x3 x4 . x4 = 0 ⟶ and (x0 = 0) (ordsucc x2 = 0) leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H7: ordsucc (add_nat x0 x2) = 0.

Apply FalseE with and (x0 = 0) (ordsucc x2 = 0).

Apply neq_ordsucc_0 with add_nat x0 x2.

The subproof is completed by applying H7.

Assume H2: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).

Apply H2 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).

Let x2 of type ι be given.

Assume H3: (λ x3 . and (nat_p x3) (x0 = ordsucc x3)) x2.

Apply H3 with add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0).

Assume H4: nat_p x2.

Assume H5: x0 = ordsucc x2.

Apply H5 with λ x3 x4 . add_nat x4 x1 = 0 ⟶ and (x4 = 0) (x1 = 0).

Apply add_nat_SL with x2, x1, λ x3 x4 . x4 = 0 ⟶ and (ordsucc x2 = 0) (x1 = 0) leaving 3 subgoals.

The subproof is completed by applying H4.

Apply omega_nat_p with x1.

The subproof is completed by applying H1.

Assume H6: ordsucc (add_nat x2 x1) = 0.

Apply FalseE with and (ordsucc x2 = 0) (x1 = 0).

Apply neq_ordsucc_0 with add_nat x2 x1.

The subproof is completed by applying H6.

■

Proofgold Proof