Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLt 0 x0.
Assume H2: ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0.
Assume H3: ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).
Let x1 of type ι be given.
Assume H4: x1 ∈ omega.
Let x2 of type ο be given.
Assume H5: ∀ x3 . x3 ∈ SNoS_ omega ⟶ SNoLt 0 x3 ⟶ SNoLt x3 x0 ⟶ SNoLt x0 (add_SNo x3 (eps_ x1)) ⟶ x2.
Apply H3 with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H6: (λ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 (eps_ x1))))) x3.
Apply H6 with x2.
Assume H7: x3 ∈ SNoS_ omega.
Assume H8: and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1))).
Apply H8 with x2.
Assume H9: SNoLt x3 x0.
Assume H10: SNoLt x0 (add_SNo x3 (eps_ x1)).
Apply SNoS_E2 with omega, x3, x2 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H7.
Assume H11: SNoLev x3 ∈ omega.
Assume H12: ordinal (SNoLev x3).
Assume H13: SNo x3.
Assume H14: SNo_ (SNoLev x3) x3.
Apply SNoLtLe_or with 0, x3, x2 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H13.
Assume H15: SNoLt 0 x3.
Apply H5 with x3 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H15.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Assume H15: SNoLe x3 0.
Apply xm with ∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (eps_ x4), x2 leaving 2 subgoals.
Assume H16: ∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (eps_ x4).
Apply FalseE with x2.
Apply SNoLt_irref with x0.
Apply H2 with 0, λ x4 x5 . SNoLt x4 x0 leaving 3 subgoals.
Apply omega_SNoS_omega with 0.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Let x4 of type ι be given.
Assume H17: x4 ∈ omega.
Apply add_SNo_0L with minus_SNo x0, λ x5 x6 . SNoLt (abs_SNo x6) (eps_ x4) leaving 2 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying H0.
Apply abs_SNo_minus with x0, λ x5 x6 . SNoLt x6 (eps_ x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply pos_abs_SNo with x0, λ x5 x6 . SNoLt x6 (eps_ x4) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H16 with x4.
The subproof is completed by applying H17.
The subproof is completed by applying H1.
Assume H16: not (∀ x4 . x4 ∈ omega ⟶ SNoLt x0 (eps_ x4)).
Apply dneg with x2.
Assume H17: not x2.
Apply H16.
Let x4 of type ι be given.
Assume H18: x4 ∈ omega.
Apply SNoLtLe_or with x0, eps_ x4, SNoLt x0 (eps_ x4) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply SNo_eps_ with x4.
The subproof is completed by applying H18.
Assume H19: SNoLt x0 (eps_ x4).
The subproof is completed by applying H19.
Assume H19: SNoLe (eps_ x4) x0.
Claim L20: ...
...
Apply H17 with SNoLt x0 (eps_ x4).
Apply H5 with eps_ (ordsucc x4) leaving 4 subgoals.
Apply SNo_eps_SNoS_omega with ordsucc x4.
Apply omega_ordsucc with x4.
The subproof is completed by applying H18.
Apply SNo_eps_pos with ordsucc x4.
Apply omega_ordsucc with x4.
The subproof is completed by applying H18.
Apply SNoLtLe_tra with eps_ (ordsucc x4), eps_ x4, ... leaving 5 subgoals.
...
...
...
...
...
...
■