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.

Let x4 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: ∀ x5 . x5 ∈ SNoS_ omega ⟶ (∀ x6 . x6 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x5 (minus_SNo x0))) (eps_ x6)) ⟶ x5 = x0.

Assume H3: ∀ x5 . x5 ∈ omega ⟶ SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5).

Assume H4: ∀ x5 . x5 ∈ omega ⟶ SNoLt (add_SNo x0 x1) (add_SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5) (eps_ x5)).

Assume H5: SNo x4.

Assume H6: SNoLt x4 x0.

Assume H7: x4 ∈ SNoS_ omega.

Assume H8: not (∃ x5 . and (x5 ∈ omega) (SNoLe (add_SNo x4 x1) (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5))).

Assume H9: SNoLt 0 (add_SNo x0 (minus_SNo x4)).

Assume H10: x4 = x0.

Apply SNoLt_irref with x4.

Apply H10 with λ x5 x6 . SNoLt x4 x6.

The subproof is completed by applying H6.

■