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: SNo (add_SNo x0 x1).

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

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

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

Assume H6: SNoLt x1 x4.

Assume H7: x4 ∈ SNoS_ omega.

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

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

Assume H10: x4 = x1.

Apply SNoLt_irref with x4.

Apply H10 with λ x5 x6 . SNoLt x6 x4.

The subproof is completed by applying H6.

■