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 (minus_SNo x0).

Assume H2: x2 ∈ SNoS_ omega.

Assume H3: ∀ x4 . x4 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x4).

Assume H4: SNo x2.

Assume H5: SNo (add_SNo x2 (minus_SNo x0)).

Assume H6: ∀ x4 . x4 ∈ SNoS_ omega ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x4 (minus_SNo (ap x1 (ordsucc x3))))) (eps_ x5)) ⟶ x4 = ap x1 (ordsucc x3).

Assume H7: SNo (ap x1 (ordsucc x3)).

Assume H8: SNoLt (ap x1 (ordsucc x3)) x2.

Assume H9: SNoLt 0 (add_SNo x2 (minus_SNo (ap x1 (ordsucc x3)))).

Assume H10: SNoLt x0 (ap x1 (ordsucc x3)).

Assume H11: abs_SNo (add_SNo x2 (minus_SNo x0)) = add_SNo x2 (minus_SNo x0).

Assume H12: x2 = ap x1 (ordsucc x3).

Apply FalseE with SNoLt x2 (ap x1 x3).

Apply SNoLt_irref with x2.

Apply H12 with λ x4 x5 . SNoLt x5 x2.

The subproof is completed by applying H8.

■