Search for blocks/addresses/...

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 x0))) (eps_ x6)) ⟶ x5 = x0.
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: SNo 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 x4 x1))).
Assume H9: SNoLt 0 (add_SNo x4 (minus_SNo x0)).
Assume H10: x4 = x0.
Apply SNoLt_irref with x4.
Apply H10 with λ x5 x6 . SNoLt x6 x4.
Apply add_SNo_0L with x0, λ x5 x6 . SNoLt x5 x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_SNo_minus_Lt2 with x4, x0, 0 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H9.
■